Summary
- more robust timing info: do not rely on order of markup;
- clarified signature;
- field "kind" is always present, with default "writeln";
The file was modified | src/Pure/PIDE/rendering.scala (diff) |
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) |
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) |