src/Pure/PIDE/protocol.ML
Mon, 04 Nov 2019 20:24:52 +0100 wenzelm proper message (amending 94442fce40a5);
Sat, 02 Nov 2019 12:02:27 +0100 wenzelm more scalable protocol_message: use XML.body directly (Output.output hook is not required);
Mon, 16 Sep 2019 16:00:10 +0200 wenzelm find theories via session directories only -- ignore known_theories;
Thu, 12 Sep 2019 13:33:09 +0200 wenzelm find theory files via session structure: much faster Prover IDE startup;
Fri, 06 Sep 2019 19:44:54 +0200 wenzelm prefer commands_accepted: fewer protocol messages;
Fri, 06 Sep 2019 18:59:24 +0200 wenzelm prefer define_commands_bulk: fewer protocol messages;
Fri, 06 Sep 2019 17:10:23 +0200 wenzelm clarified signature;
Sun, 19 May 2019 18:10:45 +0200 wenzelm more thorough assignment, e.g. when "purge" removes commands that were not assigned;
Thu, 28 Feb 2019 21:37:24 +0100 wenzelm more scalable on 32-bit Poly/ML;
Wed, 27 Feb 2019 21:30:16 +0100 wenzelm more compact representation: approx. factor 2;
Wed, 27 Feb 2019 17:33:39 +0100 wenzelm more scalable on 32-bit Poly/ML;
Tue, 05 Jun 2018 16:12:26 +0200 wenzelm less wasteful consolidation, based on PIDE front-end state and recent changes;
Thu, 31 May 2018 22:27:13 +0200 wenzelm Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
Tue, 23 Jan 2018 19:25:39 +0100 wenzelm treat sessions as entities with defining position;
Fri, 19 Jan 2018 14:55:46 +0100 wenzelm formal treatment of documentation names;
Sat, 16 Dec 2017 21:53:07 +0100 wenzelm added document antiquotation @{session name};
Thu, 28 Sep 2017 15:11:32 +0200 wenzelm session-qualified theory names are mandatory;
Tue, 08 Aug 2017 22:13:05 +0200 wenzelm maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
Mon, 07 Aug 2017 15:13:21 +0200 wenzelm more synchronized Execution.snapshot;
Fri, 21 Apr 2017 14:09:03 +0200 wenzelm eliminated default_qualifier: just a constant;
Thu, 13 Apr 2017 12:39:36 +0200 wenzelm clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";
Wed, 12 Apr 2017 21:13:43 +0200 wenzelm global session_base for PIDE interaction;
Sat, 18 Mar 2017 12:24:56 +0100 wenzelm clarified signature;
Mon, 05 Sep 2016 23:11:00 +0200 wenzelm clarified modules;
Sun, 10 Jul 2016 11:18:35 +0200 wenzelm tuned signature: more uniform Keyword.spec;
Sat, 12 Mar 2016 20:17:37 +0100 wenzelm clarified session build options: already provided by ML_Process;
Tue, 08 Mar 2016 20:24:41 +0100 wenzelm separate Isabelle_Process.init_options after Options.load_defaults, notably for "isabelle console";
Thu, 03 Mar 2016 15:23:02 +0100 wenzelm clarified modules;
Mon, 29 Feb 2016 15:23:13 +0100 wenzelm clarified ML heap operations;
Sat, 10 Oct 2015 16:21:34 +0200 wenzelm more explicit HTML.symbols;
Fri, 09 Oct 2015 19:25:13 +0200 wenzelm output HTML text according to Isabelle/Scala Symbol.Interpretation;
Mon, 29 Jun 2015 20:55:46 +0200 wenzelm improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
Wed, 15 Apr 2015 13:55:01 +0200 wenzelm GUI controls for ML_statistics, for more digestible protocol dump;
Mon, 06 Apr 2015 16:00:19 +0200 wenzelm more position information and PIDE markup for command keywords;
Mon, 16 Mar 2015 13:32:31 +0100 wenzelm avoid duplicate header errors, more precise positions;
Mon, 16 Mar 2015 11:30:54 +0100 wenzelm tuned protocol -- resolve command positions in ML;
Thu, 12 Mar 2015 22:00:51 +0100 wenzelm clarified markup for embedded files, early before execution;
Tue, 10 Mar 2015 20:12:30 +0100 wenzelm more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;
Wed, 28 Jan 2015 22:19:22 +0100 wenzelm 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);
Thu, 15 Jan 2015 14:01:26 +0100 wenzelm refrain from default task_context for all protocol commands, e.g. relevant for "build_theories" to admit Session.shutdown;
Wed, 14 Jan 2015 16:27:19 +0100 wenzelm clarified build_theories: proper protocol handler;
Wed, 14 Jan 2015 14:28:52 +0100 wenzelm clarified build_theories;
Tue, 13 Jan 2015 21:46:09 +0100 wenzelm some support for PIDE batch session;
Wed, 03 Dec 2014 22:34:28 +0100 wenzelm node-specific keywords, with session base syntax as default;
Wed, 03 Dec 2014 20:45:20 +0100 wenzelm clarified define_command: send tokens more directly, without requiring keywords in ML;
Fri, 07 Nov 2014 16:36:55 +0100 wenzelm plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
Tue, 05 Aug 2014 23:52:56 +0200 wenzelm protocol command for heap management, e.g. in Isabelle/jEdit/Scala console: PIDE.session.protocol_command("ML_System.share_common_data");
Thu, 17 Apr 2014 13:21:36 +0200 wenzelm added protocol command "use_theories", with core functionality of batch build;
Mon, 07 Apr 2014 23:02:29 +0200 wenzelm simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
Mon, 07 Apr 2014 13:06:34 +0200 wenzelm separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
Thu, 03 Apr 2014 14:54:17 +0200 wenzelm more general prover operations;
Mon, 31 Mar 2014 10:28:08 +0200 wenzelm 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;
Wed, 11 Dec 2013 18:02:22 +0100 wenzelm support for polml-5.5.2;
Fri, 22 Nov 2013 21:13:44 +0100 wenzelm clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
Wed, 20 Nov 2013 11:55:52 +0100 wenzelm load files that are not provided by PIDE blobs;
Tue, 19 Nov 2013 19:33:27 +0100 wenzelm maintain blobs within document state: digest + text in ML, digest-only in Scala;
Sun, 25 Aug 2013 20:32:26 +0200 wenzelm maintain goal forks as part of global execution;
Fri, 09 Aug 2013 11:18:36 +0200 wenzelm cancel_query via direct access to the exec_id of the running query process;
Mon, 05 Aug 2013 15:29:10 +0200 wenzelm tuned signature -- more uniform treatment of overlays as command mapping;
Fri, 02 Aug 2013 14:26:09 +0200 wenzelm maintain overlays within node perspective;
less more (0) -100 -60 tip