Skip to content
[Jenkins]Jenkins
log in
Success

Changes

Summary

  1. more robust timing info: do not rely on order of markup;
  2. clarified signature;
  3. field "kind" is always present, with default "writeln";
Changeset 67933:604da273e18d by wenzelm:
more robust timing info: do not rely on order of markup;
The file was modified src/Pure/PIDE/rendering.scala (diff)
Changeset 67932:04352338f7f3 by wenzelm:
clarified signature;
The file was modified src/Pure/General/timing.ML (diff)
The file was modified src/Pure/Isar/proof.ML (diff)
The file was modified src/Pure/Isar/toplevel.ML (diff)
Changeset 67931:f7917c15b566 by wenzelm:
field "kind" is always present, with default "writeln";
The file was modified src/Doc/System/Server.thy (diff)
The file was modified src/Pure/Tools/server.scala (diff)
The file was modified src/Pure/Tools/server_commands.scala (diff)