Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. NEWS;
  2. proper function invocation with all arguments;
  3. fork parallel prints early in execution: avoid degradation of priority due to main eval task;
  4. clarified signature: prefer Document.Snapshot;
Changeset 68368:b00b40dc41af by wenzelm:
NEWS;
The file was modified NEWS (diff)
Changeset 68367:2549d7d4718a by wenzelm:
proper function invocation with all arguments;
The file was modified src/Pure/PIDE/document.ML (diff)
Changeset 68366:cd387c55e085 by wenzelm:
fork parallel prints early in execution: avoid degradation of priority due to main eval task;
The file was modified src/Pure/PIDE/command.ML (diff)
The file was modified src/Pure/PIDE/document.ML (diff)
Changeset 68365:f9379279f98c by wenzelm:
clarified signature: prefer Document.Snapshot;
The file was modified src/Pure/PIDE/document.scala (diff)
The file was modified src/Pure/Thy/thy_resources.scala (diff)
The file was modified src/Pure/Tools/dump.scala (diff)
The file was modified src/Pure/Tools/server_commands.scala (diff)