src/Pure/PIDE/protocol.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;
Wed, 31 Jul 2013 12:14:13 +0200 wenzelm allow explicit indication of required node: full eval, no prints;
Tue, 30 Jul 2013 11:54:57 +0200 wenzelm tuned signature;
Mon, 29 Jul 2013 18:59:58 +0200 wenzelm keep memo_exec execution running, which is important to cancel goal forks eventually;
Mon, 29 Jul 2013 16:52:04 +0200 wenzelm maintain explicit execution frontier: avoid conflict with former task via static dependency;
Mon, 29 Jul 2013 14:18:57 +0200 wenzelm actually purge removed goal futures -- avoid memory leak;
Mon, 29 Jul 2013 13:00:36 +0200 wenzelm obsolete;
Mon, 15 Jul 2013 10:25:35 +0200 wenzelm more careful termination of removed execs, leaving running execs undisturbed;
Fri, 12 Jul 2013 12:04:16 +0200 wenzelm clarified execution: maintain running execs only, check "stable" separately via memo (again);
Fri, 12 Jul 2013 11:28:03 +0200 wenzelm tuned signature;
Fri, 12 Jul 2013 11:07:02 +0200 wenzelm clarified module name;
Thu, 11 Jul 2013 23:24:40 +0200 wenzelm more explicit type Exec.context;
Thu, 11 Jul 2013 18:41:05 +0200 wenzelm strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
Thu, 11 Jul 2013 16:35:37 +0200 wenzelm tuned -- cleanup before publishing assignment;
Thu, 11 Jul 2013 14:42:11 +0200 wenzelm global management of command execution fragments;
Wed, 10 Jul 2013 23:30:10 +0200 wenzelm added "echo" command for demonstration purposes;
Wed, 10 Jul 2013 21:13:32 +0200 wenzelm make SML/NJ happy;
Wed, 10 Jul 2013 12:33:28 +0200 wenzelm tuned start_execution: avoid sleep on worker thread;
Tue, 09 Jul 2013 13:17:22 +0200 wenzelm tuned protocol terminology;
Fri, 05 Jul 2013 15:38:03 +0200 wenzelm explicit module Document_ID as source of globally unique identifiers across ML/Scala;
Thu, 04 Jul 2013 23:51:47 +0200 wenzelm separate exec_id assignment for Command.print states, without affecting result of eval;
Wed, 22 May 2013 14:10:45 +0200 wenzelm explicit management of Session.Protocol_Handlers, with protocol state and functions;
Wed, 27 Feb 2013 16:27:44 +0100 wenzelm discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
Wed, 27 Feb 2013 12:45:19 +0100 wenzelm discontinued obsolete 'uses' within theory header;
Thu, 13 Dec 2012 19:53:55 +0100 wenzelm smarter handling of tracing messages: prover process pauses and enters user dialog;
Thu, 13 Dec 2012 13:52:18 +0100 wenzelm identify dialogs via official serial and maintain as result message;
Wed, 12 Dec 2012 21:50:42 +0100 wenzelm support dialog via document content;
Sun, 25 Nov 2012 19:49:24 +0100 wenzelm Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
Thu, 18 Oct 2012 19:58:30 +0200 wenzelm more basic Goal.reset_futures as snapshot of implicit state;
Fri, 28 Sep 2012 16:51:58 +0200 wenzelm smarter handling of tracing messages;
Thu, 20 Sep 2012 19:23:05 +0200 wenzelm more management of Invoke_Scala tasks;
Sat, 01 Sep 2012 19:27:28 +0200 wenzelm central management of forked goals wrt. transaction id;
Sun, 26 Aug 2012 21:46:50 +0200 wenzelm theory def/ref position reports, which enable hyperlinks etc.;
Mon, 20 Aug 2012 14:09:09 +0200 wenzelm added keyword kind "thy_load" (with optional list of file extensions);
Fri, 10 Aug 2012 15:14:45 +0200 wenzelm apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.;
Tue, 07 Aug 2012 15:01:48 +0200 wenzelm simplified Document.Node.Header -- internalized errors;
Wed, 11 Apr 2012 11:44:21 +0200 wenzelm just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
Mon, 09 Apr 2012 17:22:23 +0200 wenzelm simplified Future.cancel/cancel_group (again) -- running threads only;
Fri, 06 Apr 2012 23:34:38 +0200 wenzelm discontinued obsolete last_execs (cf. cd3ab7625519);
less more (0) -60 tip