2011-08-31 ago tuned join_commands: avoid traversing cumulative table;
2011-08-26 ago tuned signature;
2011-08-26 ago refined document state assignment: observe perspective, more explicit assignment message;
2011-08-25 ago propagate information about last command with exec state assignment through document model;
2011-08-24 ago update_perspective without actual edits, bypassing the full state assignment protocol;
2011-08-22 ago some support for editor perspective;
2011-08-19 ago tuned signature (again);
2011-08-19 ago refined Future.cancel: explicit future allows to join actual cancellation;
2011-08-15 ago refined Document.edit: less stateful update via Graph.schedule;
2011-08-13 ago provide node header via Scala layer;
2011-08-13 ago clarified node header -- exclude master_dir;
2011-08-11 ago uniform treatment of header edits as document edits;
2011-08-11 ago explicit datatypes for document node edits;
2011-07-12 ago tuned XML modules;
2011-07-11 ago JVM method invocation service via Scala layer;
2011-07-10 ago inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control);
2011-07-10 ago simplified XML_Data;
2011-07-10 ago propagate header changes to prover process;
2011-07-08 ago moved global state to structure Document (again);
2011-07-05 ago get theory from last executation state;
2011-07-05 ago clarified cancel_execution/await_cancellation;
2011-07-05 ago tuned signature;
2011-01-27 ago cancel document execution before editing, to improve reactivity on systems with few cores;
2010-08-20 ago concentrate protocol message formats in Isar_Document;
2010-08-19 ago moved Isar_Document to Pure/PIDE;