Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. some export of foundational theory content;
  2. support for general theory presentation;
  3. guard result exports via export_pattern -- avoid bombing client via huge blobs;
  4. tuned;
  5. clarified output: avoid costly operations on huge blobs;
  6. unused;
  7. more scalable -- avoid huge lines within stdout;
  8. slightly more ambitious parallelism (again);
  9. more scalable API;
  10. proper heading;
  11. removed unused Java FX modules (it will be unbundled from JDK eventually);
Changeset 68154:42d63ea39161 by wenzelm:
some export of foundational theory content;
The file was addedsrc/Pure/Thy/export_theory.ML
The file was modified etc/options (diff)
The file was modified src/Pure/ROOT.ML (diff)
Changeset 68153:e469d529e6da by wenzelm:
support for general theory presentation;
The file was modified src/Pure/Thy/thy_info.ML (diff)
Changeset 68152:619de043389f by wenzelm:
guard result exports via export_pattern -- avoid bombing client via huge blobs;
The file was modified src/Doc/System/Server.thy (diff)
The file was modified src/Doc/System/Sessions.thy (diff)
The file was modified src/Pure/Tools/server_commands.scala (diff)
Changeset 68151:3c321783bae3 by wenzelm:
tuned;
The file was modified src/Pure/Thy/export.scala (diff)
Changeset 68150:f0f34cbed539 by wenzelm:
clarified output: avoid costly operations on huge blobs;
The file was modified src/Pure/General/bytes.scala (diff)
Changeset 68149:9a4a6adb95b5 by wenzelm:
unused;
The file was modified src/Pure/General/bytes.scala (diff)
The file was modified src/Pure/library.ML (diff)
Changeset 68148:fb661e4c4717 by wenzelm:
more scalable -- avoid huge lines within stdout;
The file was modified src/Pure/PIDE/markup.scala (diff)
The file was modified src/Pure/Tools/build.ML (diff)
The file was modified src/Pure/Tools/build.scala (diff)
Changeset 68147:a8f40dd73c61 by wenzelm:
slightly more ambitious parallelism (again);
The file was modified src/Pure/Concurrent/future.ML (diff)
Changeset 68146:d23af2dbb4e7 by wenzelm:
more scalable API;
The file was modified src/Pure/Thy/export.ML (diff)
Changeset 68145:edacd2a050be by wenzelm:
proper heading;
The file was modified src/Doc/System/Server.thy (diff)
Changeset 68144:7b995cd6d5d4 by wenzelm:
removed unused Java FX modules (it will be unbundled from JDK eventually);
The file was modified src/Pure/ROOT.scala (diff)
The file was modified src/Pure/build-jars (diff)
The file was removedsrc/Pure/GUI/html5_panel.scala
The file was removedsrc/Pure/GUI/jfx_gui.scala