src/Pure/PIDE/protocol.ML
4 months ago wenzelm 2019-05-19 more thorough assignment, e.g. when "purge" removes commands that were not assigned;
7 months ago wenzelm 2019-02-28 more scalable on 32-bit Poly/ML;
7 months ago wenzelm 2019-02-27 more compact representation: approx. factor 2;
7 months ago wenzelm 2019-02-27 more scalable on 32-bit Poly/ML;
16 months ago wenzelm 2018-06-05 less wasteful consolidation, based on PIDE front-end state and recent changes;
16 months ago wenzelm 2018-05-31 Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread; tuned;
20 months ago wenzelm 2018-01-23 treat sessions as entities with defining position; tuned signature;
21 months ago wenzelm 2018-01-19 formal treatment of documentation names;
22 months ago wenzelm 2017-12-16 added document antiquotation @{session name}; renamed protocol function "Prover.session_base" to "Prover.init_session_base" according to the ML/Scala operation;
2017-09-28 wenzelm 2017-09-28 session-qualified theory names are mandatory;
2017-08-08 wenzelm 2017-08-08 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
2017-08-07 wenzelm 2017-08-07 more synchronized Execution.snapshot;
2017-04-21 wenzelm 2017-04-21 eliminated default_qualifier: just a constant;
2017-04-13 wenzelm 2017-04-13 clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";
2017-04-12 wenzelm 2017-04-12 global session_base for PIDE interaction;
2017-03-18 wenzelm 2017-03-18 clarified signature;
2016-09-05 wenzelm 2016-09-05 clarified modules;
2016-07-10 wenzelm 2016-07-10 tuned signature: more uniform Keyword.spec;
2016-03-12 wenzelm 2016-03-12 clarified session build options: already provided by ML_Process; tuned signature;
2016-03-08 wenzelm 2016-03-08 separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";
2016-03-03 wenzelm 2016-03-03 clarified modules; tuned signature;
2016-02-29 wenzelm 2016-02-29 clarified ML heap operations;
2015-10-10 wenzelm 2015-10-10 more explicit HTML.symbols; tuned signature;
2015-10-09 wenzelm 2015-10-09 output HTML text according to Isabelle/Scala Symbol.Interpretation;
2015-06-29 wenzelm 2015-06-29 improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
2015-04-15 wenzelm 2015-04-15 GUI controls for ML_statistics, for more digestible protocol dump;
2015-04-06 wenzelm 2015-04-06 more position information and PIDE markup for command keywords;
2015-03-16 wenzelm 2015-03-16 avoid duplicate header errors, more precise positions; tuned signature;
2015-03-16 wenzelm 2015-03-16 tuned protocol -- resolve command positions in ML;
2015-03-12 wenzelm 2015-03-12 clarified markup for embedded files, early before execution;
2015-03-10 wenzelm 2015-03-10 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
2015-01-28 wenzelm 2015-01-28 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 wenzelm 2015-01-15 refrain from default task_context for all protocol commands, e.g. relevant for "build_theories" to admit Session.shutdown;
2015-01-14 wenzelm 2015-01-14 clarified build_theories: proper protocol handler;
2015-01-14 wenzelm 2015-01-14 clarified build_theories;
2015-01-13 wenzelm 2015-01-13 some support for PIDE batch session; clarified Thy_Info.use_thys_options and corresponding protocol command;
2014-12-03 wenzelm 2014-12-03 node-specific keywords, with session base syntax as default;
2014-12-03 wenzelm 2014-12-03 clarified define_command: send tokens more directly, without requiring keywords in ML;
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-08-05 wenzelm 2014-08-05 protocol command for heap management, e.g. in Isabelle/jEdit/Scala console: PIDE.session.protocol_command("ML_System.share_common_data");
2014-04-17 wenzelm 2014-04-17 added protocol command "use_theories", with core functionality of batch build;
2014-04-07 wenzelm 2014-04-07 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name; more liberal hyperlink to files, allow hyperlinks within editor files independently of the (POSIX) file-system;
2014-04-07 wenzelm 2014-04-07 separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
2014-04-03 wenzelm 2014-04-03 more general prover operations;
2014-03-31 wenzelm 2014-03-31 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 wenzelm 2013-12-11 support for polml-5.5.2; support Thread.numPhysicalProcessors of polyml-5.5.2 (according to SVN 1890); clarified max_threads: store plain value internally, reproduce result only on startup, and thus avoid potential system overhead;
2013-11-22 wenzelm 2013-11-22 clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
2013-11-20 wenzelm 2013-11-20 load files that are not provided by PIDE blobs; uniform resolve_files via Command.read;
2013-11-19 wenzelm 2013-11-19 maintain blobs within document state: digest + text in ML, digest-only in Scala; resolve files for command span, based on defined blobs; tuned;
2013-08-25 wenzelm 2013-08-25 maintain goal forks as part of global execution; tuned;
2013-08-09 wenzelm 2013-08-09 cancel_query via direct access to the exec_id of the running query process;
2013-08-05 wenzelm 2013-08-05 tuned signature -- more uniform treatment of overlays as command mapping;
2013-08-02 wenzelm 2013-08-02 maintain overlays within node perspective; tuned signature;
2013-07-31 wenzelm 2013-07-31 allow explicit indication of required node: full eval, no prints;
2013-07-30 wenzelm 2013-07-30 tuned signature; removed notoriously outdated comments;
2013-07-29 wenzelm 2013-07-29 keep memo_exec execution running, which is important to cancel goal forks eventually; run as nested worker task to keep main group valid, even after cancelation of removed subgroups; do not memoize interrupt, but absorb it silently in main execution; Goal.purge_futures: rough sanity check of group status;
2013-07-29 wenzelm 2013-07-29 maintain explicit execution frontier: avoid conflict with former task via static dependency; start execution immediate after assignment, to keep frontier simple;
2013-07-29 wenzelm 2013-07-29 actually purge removed goal futures -- avoid memory leak;
2013-07-29 wenzelm 2013-07-29 obsolete;
2013-07-15 wenzelm 2013-07-15 more careful termination of removed execs, leaving running execs undisturbed;