src/Pure/PIDE/document.ML
Thu, 06 Nov 2014 11:44:41 +0100 wenzelm simplified keyword kinds;
Wed, 05 Nov 2014 20:20:57 +0100 wenzelm explicit type Keyword.keywords;
Tue, 12 Aug 2014 20:18:27 +0200 wenzelm tuned signature according to Scala version -- prefer explicit argument;
Tue, 12 Aug 2014 00:08:32 +0200 wenzelm separate module Command_Span: mostly syntactic representation;
Sat, 09 Aug 2014 11:43:58 +0200 wenzelm tuned comments;
Thu, 24 Jul 2014 13:48:00 +0200 wenzelm make SML/NJ happy;
Thu, 24 Jul 2014 10:38:46 +0200 wenzelm less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;
Wed, 23 Jul 2014 14:50:20 +0200 wenzelm avoid redundant data structure;
Wed, 23 Jul 2014 13:01:30 +0200 wenzelm more explicit discrimination of empty nodes -- suppress from Theories panel;
Wed, 30 Apr 2014 22:34:11 +0200 wenzelm some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
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;
Tue, 18 Mar 2014 17:39:03 +0100 wenzelm clarifed module name;
Fri, 28 Feb 2014 11:48:14 +0100 wenzelm tuned comment;
Fri, 28 Feb 2014 11:46:54 +0100 wenzelm tuned signature;
Thu, 27 Feb 2014 17:29:58 +0100 wenzelm store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
Fri, 22 Nov 2013 21:13:44 +0100 wenzelm clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
Fri, 22 Nov 2013 20:28:49 +0100 wenzelm more total master_directory -- NB: this is used outside command transactions (see also 92961f196d9e);
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;
Tue, 19 Nov 2013 13:13:51 +0100 wenzelm proper theory name vs. node name;
Mon, 18 Nov 2013 17:16:56 +0100 wenzelm maintain document model for all files, with document view for theory only, and special blob for non-theory files;
Mon, 05 Aug 2013 15:29:10 +0200 wenzelm tuned signature -- more uniform treatment of overlays as command mapping;
Fri, 02 Aug 2013 16:00:14 +0200 wenzelm support print functions with explicit arguments, as provided by overlays;
Fri, 02 Aug 2013 14:26:09 +0200 wenzelm maintain overlays within node perspective;
Wed, 31 Jul 2013 12:46:53 +0200 wenzelm simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;
Wed, 31 Jul 2013 12:14:13 +0200 wenzelm allow explicit indication of required node: full eval, no prints;
Tue, 30 Jul 2013 18:19:16 +0200 wenzelm recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
Tue, 30 Jul 2013 16:22:07 +0200 wenzelm more timing;
Tue, 30 Jul 2013 16:01:19 +0200 wenzelm more timing;
Tue, 30 Jul 2013 11:38:43 +0200 wenzelm de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
Mon, 29 Jul 2013 19:55:38 +0200 wenzelm traverse node on change of "required" state;
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 15:59:47 +0200 wenzelm clarified conditions for node traversal;
Mon, 29 Jul 2013 15:20:02 +0200 wenzelm tuned;
Mon, 29 Jul 2013 13:24:15 +0200 wenzelm discontinued notion of "stable" result -- running execution is never canceled;
Sat, 20 Jul 2013 16:29:06 +0200 wenzelm document update at high priority -- important;
Sat, 20 Jul 2013 16:27:55 +0200 wenzelm option editor_execution_priority;
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:26:14 +0200 wenzelm more abstract types;
Thu, 11 Jul 2013 16:01:48 +0200 wenzelm tuned;
Thu, 11 Jul 2013 14:42:11 +0200 wenzelm global management of command execution fragments;
Thu, 11 Jul 2013 12:28:24 +0200 wenzelm fully synchronized guard of running execution;
Thu, 11 Jul 2013 11:37:06 +0200 wenzelm re-assign prints of unchanged eval only -- avoid crash of new_exec;
Thu, 11 Jul 2013 11:09:23 +0200 wenzelm tuned -- refrain from odd optimization;
Thu, 11 Jul 2013 10:43:53 +0200 wenzelm tuned;
Wed, 10 Jul 2013 12:33:28 +0200 wenzelm tuned start_execution: avoid sleep on worker thread;
Wed, 10 Jul 2013 11:26:55 +0200 wenzelm clarified Command.print: update old prints here;
Tue, 09 Jul 2013 23:49:19 +0200 wenzelm produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
Tue, 09 Jul 2013 17:58:38 +0200 wenzelm more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
Fri, 05 Jul 2013 22:58:24 +0200 wenzelm tuned signature;
Fri, 05 Jul 2013 18:37:44 +0200 wenzelm tuned signature;
Fri, 05 Jul 2013 17:09:28 +0200 wenzelm clarified type Command.eval;
Fri, 05 Jul 2013 16:22:28 +0200 wenzelm tuned signature;
less more (0) -100 -60 tip