src/Pure/PIDE/document.ML
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;
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;
Thu, 04 Jul 2013 16:04:53 +0200 wenzelm more Command.memo operations;
Thu, 04 Jul 2013 11:55:45 +0200 wenzelm made SML/NJ happy;
Wed, 03 Jul 2013 22:30:33 +0200 wenzelm more print function parameters;
Wed, 03 Jul 2013 21:55:15 +0200 wenzelm tuned;
Wed, 03 Jul 2013 21:38:10 +0200 wenzelm discontinued odd workaround for some old Poly/ML, which is still supported but of little practical relevance;
Wed, 03 Jul 2013 21:32:58 +0200 wenzelm tuned;
Wed, 03 Jul 2013 17:50:47 +0200 wenzelm allow multiple print functions;
Wed, 03 Jul 2013 16:58:35 +0200 wenzelm tuned signature;
Wed, 03 Jul 2013 16:19:57 +0200 wenzelm tuned signature;
Wed, 03 Jul 2013 15:19:36 +0200 wenzelm tuned;
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;
Sun, 24 Feb 2013 17:29:55 +0100 wenzelm simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
Sun, 13 Jan 2013 19:45:32 +0100 wenzelm more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
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 12:00:27 +0200 wenzelm more official Future.terminate;
Wed, 05 Sep 2012 20:54:40 +0200 wenzelm eliminated potentially confusing terminology of Scala "layer";
Sun, 02 Sep 2012 14:02:05 +0200 wenzelm maintain stable state of node entries from last round -- bypass slightly different Thm.join_theory_proofs;
Sat, 01 Sep 2012 19:27:28 +0200 wenzelm central management of forked goals wrt. transaction id;
Thu, 30 Aug 2012 21:23:04 +0200 wenzelm refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
Thu, 30 Aug 2012 19:18:49 +0200 wenzelm some support for registering forked proofs within Proof.state, using its bottom context;
Thu, 30 Aug 2012 16:39:50 +0200 wenzelm tuned signature;
Sun, 26 Aug 2012 21:46:50 +0200 wenzelm theory def/ref position reports, which enable hyperlinks etc.;
Fri, 24 Aug 2012 12:35:39 +0200 wenzelm check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
Sat, 11 Aug 2012 19:34:36 +0200 wenzelm vacuous execution after first malformed command;
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.;
Fri, 27 Jul 2012 20:54:01 +0200 wenzelm even more permissive approximation of master_dir, which is only required to access external resources ('uses' etc.);
Tue, 07 Aug 2012 15:01:48 +0200 wenzelm simplified Document.Node.Header -- internalized errors;
Fri, 20 Apr 2012 23:16:46 +0200 wenzelm improved interleaving of start_execution vs. cancel_execution of the next update;
Fri, 20 Apr 2012 22:48:48 +0200 wenzelm always revisit nodes independently of "required" flag, which may change during editing -- avoid "bloodbath effect" when changing perspective while loading;
Fri, 20 Apr 2012 22:51:06 +0200 wenzelm tuned;
Fri, 20 Apr 2012 20:21:22 +0200 wenzelm builtin timing for main operations;
Wed, 11 Apr 2012 14:20:51 +0200 wenzelm tuned;
less more (0) -100 -60 tip