2011-09-03 wenzelm 2011-09-03 Document.removed_versions on Scala side;
2011-09-03 wenzelm 2011-09-03 Document.remove_versions on ML side;
2011-09-02 wenzelm 2011-09-02 raw message function "assign_execs" avoids full overhead of decoding and caching message body;
2011-09-02 wenzelm 2011-09-02 less agressive parsing of commands (priority ~1); join commands just before actual assignment;
2011-09-02 wenzelm 2011-09-02 clarified define_command: store name as structural information;
2011-08-31 wenzelm 2011-08-31 explicit cancel_execution before queueing new edits -- potential performance improvement for machines with few cores;
2011-08-31 wenzelm 2011-08-31 tuned join_commands: avoid traversing cumulative table;
2011-08-26 wenzelm 2011-08-26 tuned signature;
2011-08-26 wenzelm 2011-08-26 refined document state assignment: observe perspective, more explicit assignment message; misc tuning and clarification;
2011-08-25 wenzelm 2011-08-25 propagate information about last command with exec state assignment through document model;
2011-08-24 wenzelm 2011-08-24 update_perspective without actual edits, bypassing the full state assignment protocol; edit_nodes/Perspective: do not touch_descendants here; propagate editor scroll events via update_perspective; misc tuning;
2011-08-22 wenzelm 2011-08-22 some support for editor perspective;
2011-08-19 wenzelm 2011-08-19 tuned signature (again); tuned;
2011-08-19 wenzelm 2011-08-19 refined Future.cancel: explicit future allows to join actual cancellation; Document.cancel_execution: join nested future groups as well;
2011-08-15 wenzelm 2011-08-15 refined Document.edit: less stateful update via Graph.schedule; clarified node result -- more direct get_theory; clarified Document.joint_commands;
2011-08-13 wenzelm 2011-08-13 provide node header via Scala layer; clarified node edit Clear: retain header information; run_command: node info via document model, error handling within transaction; node names without ".thy" suffix, to coincide with traditional theory loader treatment;
2011-08-13 wenzelm 2011-08-13 clarified node header -- exclude master_dir;
2011-08-11 wenzelm 2011-08-11 uniform treatment of header edits as document edits;
2011-08-11 wenzelm 2011-08-11 explicit datatypes for document node edits;
2011-07-12 wenzelm 2011-07-12 tuned XML modules;
2011-07-11 wenzelm 2011-07-11 JVM method invocation service via Scala layer;
2011-07-10 wenzelm 2011-07-10 inner syntax supports inlined YXML according to Term_XML (particularly useful for producing text under program control); tuned signature;
2011-07-10 wenzelm 2011-07-10 simplified XML_Data;
2011-07-10 wenzelm 2011-07-10 propagate header changes to prover process; simplified Document case classes; Document.State.assignments: indexed by Version_ID;
2011-07-08 wenzelm 2011-07-08 moved global state to structure Document (again);
2011-07-05 wenzelm 2011-07-05 get theory from last executation state; tuned error messages;
2011-07-05 wenzelm 2011-07-05 clarified cancel_execution/await_cancellation;
2011-07-05 wenzelm 2011-07-05 tuned signature; tuned;
2011-01-27 wenzelm 2011-01-27 cancel document execution before editing, to improve reactivity on systems with few cores;
2010-08-20 wenzelm 2010-08-20 concentrate protocol message formats in Isar_Document;
2010-08-19 wenzelm 2010-08-19 moved Isar_Document to Pure/PIDE;