src/Pure/PIDE/protocol.ML
22 months ago ago treat sessions as entities with defining position;
22 months ago ago formal treatment of documentation names;
23 months ago ago added document antiquotation @{session name};
2017-09-28 ago session-qualified theory names are mandatory;
2017-08-08 ago maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
2017-08-07 ago more synchronized Execution.snapshot;
2017-04-21 ago eliminated default_qualifier: just a constant;
2017-04-13 ago clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";
2017-04-12 ago global session_base for PIDE interaction;
2017-03-18 ago clarified signature;
2016-09-05 ago clarified modules;
2016-07-10 ago tuned signature: more uniform Keyword.spec;
2016-03-12 ago clarified session build options: already provided by ML_Process;
2016-03-08 ago separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";
2016-03-03 ago clarified modules;
2016-02-29 ago clarified ML heap operations;
2015-10-10 ago more explicit HTML.symbols;
2015-10-09 ago output HTML text according to Isabelle/Scala Symbol.Interpretation;
2015-06-29 ago improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
2015-04-15 ago GUI controls for ML_statistics, for more digestible protocol dump;
2015-04-06 ago more position information and PIDE markup for command keywords;
2015-03-16 ago avoid duplicate header errors, more precise positions;
2015-03-16 ago tuned protocol -- resolve command positions in ML;
2015-03-12 ago clarified markup for embedded files, early before execution;
2015-03-10 ago more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
2015-01-28 ago more robust protocol command: purge removed execs asynchronously, to remain reactive despite problems to cancel "Command.run_process" in a situation of overrunning non-terminating tasks (see also 59f1591a11cb);
2015-01-15 ago refrain from default task_context for all protocol commands, e.g. relevant for "build_theories" to admit Session.shutdown;
2015-01-14 ago clarified build_theories: proper protocol handler;
2015-01-14 ago clarified build_theories;
2015-01-13 ago some support for PIDE batch session;
2014-12-03 ago node-specific keywords, with session base syntax as default;
2014-12-03 ago clarified define_command: send tokens more directly, without requiring keywords in ML;
2014-11-07 ago plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
2014-08-05 ago protocol command for heap management, e.g. in Isabelle/jEdit/Scala console: PIDE.session.protocol_command("ML_System.share_common_data");
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;