Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more operations;
  2. merged
  3. return exports as result for Isabelle server;
  4. more checks;
  5. tuned;
  6. more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure; tuned;
  7. clarified signature; avoid pointless compression;
  8. store exports within PIDE command state; Markup.Export.unapply: proper NAME;
Changeset 68108:2277fe496d78 by wenzelm:
more operations;
The file was modified src/Pure/General/bytes.scala (diff)
Changeset 68107:3687109009c4 by wenzelm:
merged
Changeset 68106:a514e29db980 by wenzelm:
return exports as result for Isabelle server;
The file was modified src/Doc/System/Server.thy (diff)
The file was modified src/Pure/General/bytes.scala (diff)
The file was modified src/Pure/Thy/thy_resources.scala (diff)
The file was modified src/Pure/Tools/server_commands.scala (diff)
Changeset 68105:577072a0ceed by wenzelm:
more checks;
The file was modified src/Pure/Thy/export.ML (diff)
Changeset 68104:3795f67716e6 by wenzelm:
tuned;
The file was modified src/Pure/Thy/export.scala (diff)
Changeset 68103:c5764b8b2a87 by wenzelm:
more robust (synchronous) management of Export.Entry: Future.fork happens inside the data structure;<br>tuned;
The file was modified src/Pure/PIDE/session.scala (diff)
The file was modified src/Pure/Thy/export.scala (diff)
Changeset 68102:813b5d0904c6 by wenzelm:
clarified signature;<br>avoid pointless compression;
The file was modified src/Pure/Thy/export.ML (diff)
The file was modified src/Pure/Thy/export.scala (diff)
Changeset 68101:0699a0bacc50 by wenzelm:
store exports within PIDE command state;<br>Markup.Export.unapply: proper NAME;
The file was modified src/Pure/PIDE/command.scala (diff)
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Pure/PIDE/markup.ML (diff)
The file was modified src/Pure/PIDE/markup.scala (diff)
The file was modified src/Pure/PIDE/session.scala (diff)
The file was modified src/Pure/Thy/export.ML (diff)
The file was modified src/Pure/Thy/export.scala (diff)