src/Pure/PIDE/protocol.ML
2014-04-17 ago added protocol command "use_theories", with core functionality of batch build;
2014-04-07 ago simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
2014-04-07 ago separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
2014-04-03 ago more general prover operations;
2014-03-31 ago support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
2013-12-11 ago support for polml-5.5.2;
2013-11-22 ago clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
2013-11-20 ago load files that are not provided by PIDE blobs;
2013-11-19 ago maintain blobs within document state: digest + text in ML, digest-only in Scala;
2013-08-25 ago maintain goal forks as part of global execution;
2013-08-09 ago cancel_query via direct access to the exec_id of the running query process;
2013-08-05 ago tuned signature -- more uniform treatment of overlays as command mapping;
2013-08-02 ago maintain overlays within node perspective;
2013-07-31 ago allow explicit indication of required node: full eval, no prints;
2013-07-30 ago tuned signature;
2013-07-29 ago keep memo_exec execution running, which is important to cancel goal forks eventually;
2013-07-29 ago maintain explicit execution frontier: avoid conflict with former task via static dependency;
2013-07-29 ago actually purge removed goal futures -- avoid memory leak;
2013-07-29 ago obsolete;
2013-07-15 ago more careful termination of removed execs, leaving running execs undisturbed;
2013-07-12 ago clarified execution: maintain running execs only, check "stable" separately via memo (again);
2013-07-12 ago tuned signature;
2013-07-12 ago clarified module name;
2013-07-11 ago more explicit type Exec.context;
2013-07-11 ago strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
2013-07-11 ago tuned -- cleanup before publishing assignment;
2013-07-11 ago global management of command execution fragments;
2013-07-10 ago added "echo" command for demonstration purposes;
2013-07-10 ago make SML/NJ happy;
2013-07-10 ago tuned start_execution: avoid sleep on worker thread;
2013-07-09 ago tuned protocol terminology;
2013-07-05 ago explicit module Document_ID as source of globally unique identifiers across ML/Scala;
2013-07-04 ago separate exec_id assignment for Command.print states, without affecting result of eval;
2013-05-22 ago explicit management of Session.Protocol_Handlers, with protocol state and functions;
2013-02-27 ago discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
2013-02-27 ago discontinued obsolete 'uses' within theory header;
2012-12-13 ago smarter handling of tracing messages: prover process pauses and enters user dialog;
2012-12-13 ago identify dialogs via official serial and maintain as result message;
2012-12-12 ago support dialog via document content;
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-18 ago more basic Goal.reset_futures as snapshot of implicit state;
2012-09-28 ago smarter handling of tracing messages;
2012-09-20 ago more management of Invoke_Scala tasks;
2012-09-01 ago central management of forked goals wrt. transaction id;
2012-08-26 ago theory def/ref position reports, which enable hyperlinks etc.;
2012-08-20 ago added keyword kind "thy_load" (with optional list of file extensions);
2012-08-10 ago apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.;
2012-08-07 ago simplified Document.Node.Header -- internalized errors;
2012-04-11 ago just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
2012-04-09 ago simplified Future.cancel/cancel_group (again) -- running threads only;
2012-04-06 ago discontinued obsolete last_execs (cf. cd3ab7625519);
2012-04-06 ago discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;
2012-04-05 ago less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
2012-03-15 ago some support for outer syntax keyword declarations within theory header;
2012-03-03 ago clarified terminology of raw protocol messages;
2012-01-05 ago tuned signature -- emphasize special nature of protocol commands;
2011-12-01 ago clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;