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);
|
file |
diff |
annotate
|
Tue, 09 Jul 2013 17:58:38 +0200 |
wenzelm |
more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
|
file |
diff |
annotate
|
Fri, 05 Jul 2013 22:58:24 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 05 Jul 2013 18:37:44 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 05 Jul 2013 17:09:28 +0200 |
wenzelm |
clarified type Command.eval;
|
file |
diff |
annotate
|
Fri, 05 Jul 2013 16:22:28 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 05 Jul 2013 15:38:03 +0200 |
wenzelm |
explicit module Document_ID as source of globally unique identifiers across ML/Scala;
|
file |
diff |
annotate
|
Thu, 04 Jul 2013 23:51:47 +0200 |
wenzelm |
separate exec_id assignment for Command.print states, without affecting result of eval;
|
file |
diff |
annotate
|
Thu, 04 Jul 2013 16:04:53 +0200 |
wenzelm |
more Command.memo operations;
|
file |
diff |
annotate
|
Thu, 04 Jul 2013 11:55:45 +0200 |
wenzelm |
made SML/NJ happy;
|
file |
diff |
annotate
|
Wed, 03 Jul 2013 22:30:33 +0200 |
wenzelm |
more print function parameters;
|
file |
diff |
annotate
|
Wed, 03 Jul 2013 21:55:15 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Wed, 03 Jul 2013 21:32:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 03 Jul 2013 17:50:47 +0200 |
wenzelm |
allow multiple print functions;
|
file |
diff |
annotate
|
Wed, 03 Jul 2013 16:58:35 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 03 Jul 2013 16:19:57 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 03 Jul 2013 15:19:36 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 27 Feb 2013 16:27:44 +0100 |
wenzelm |
discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
|
file |
diff |
annotate
|
Wed, 27 Feb 2013 12:45:19 +0100 |
wenzelm |
discontinued obsolete 'uses' within theory header;
|
file |
diff |
annotate
|
Sun, 24 Feb 2013 17:29:55 +0100 |
wenzelm |
simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Sun, 25 Nov 2012 19:49:24 +0100 |
wenzelm |
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
|
file |
diff |
annotate
|
Thu, 18 Oct 2012 12:00:27 +0200 |
wenzelm |
more official Future.terminate;
|
file |
diff |
annotate
|
Wed, 05 Sep 2012 20:54:40 +0200 |
wenzelm |
eliminated potentially confusing terminology of Scala "layer";
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Sat, 01 Sep 2012 19:27:28 +0200 |
wenzelm |
central management of forked goals wrt. transaction id;
|
file |
diff |
annotate
|
Thu, 30 Aug 2012 21:23:04 +0200 |
wenzelm |
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
|
file |
diff |
annotate
|
Thu, 30 Aug 2012 19:18:49 +0200 |
wenzelm |
some support for registering forked proofs within Proof.state, using its bottom context;
|
file |
diff |
annotate
|
Thu, 30 Aug 2012 16:39:50 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sun, 26 Aug 2012 21:46:50 +0200 |
wenzelm |
theory def/ref position reports, which enable hyperlinks etc.;
|
file |
diff |
annotate
|
Fri, 24 Aug 2012 12:35:39 +0200 |
wenzelm |
check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
|
file |
diff |
annotate
|
Sat, 11 Aug 2012 19:34:36 +0200 |
wenzelm |
vacuous execution after first malformed command;
|
file |
diff |
annotate
|
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.;
|
file |
diff |
annotate
|
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.);
|
file |
diff |
annotate
|
Tue, 07 Aug 2012 15:01:48 +0200 |
wenzelm |
simplified Document.Node.Header -- internalized errors;
|
file |
diff |
annotate
|
Fri, 20 Apr 2012 23:16:46 +0200 |
wenzelm |
improved interleaving of start_execution vs. cancel_execution of the next update;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Fri, 20 Apr 2012 22:51:06 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 20 Apr 2012 20:21:22 +0200 |
wenzelm |
builtin timing for main operations;
|
file |
diff |
annotate
|
Wed, 11 Apr 2012 14:20:51 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
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;
|
file |
diff |
annotate
|
Tue, 10 Apr 2012 20:42:17 +0200 |
wenzelm |
tuned future priorities: print 0, goal ~1, execute ~2;
|
file |
diff |
annotate
|
Mon, 09 Apr 2012 20:42:05 +0200 |
wenzelm |
more explicit last exec result;
|
file |
diff |
annotate
|
Mon, 09 Apr 2012 19:50:04 +0200 |
wenzelm |
dynamic propagation of node "updated" status, which is required to propagate edits and re-assigments and allow direct memo_result;
|
file |
diff |
annotate
|
Mon, 09 Apr 2012 17:38:39 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Mon, 09 Apr 2012 17:22:23 +0200 |
wenzelm |
simplified Future.cancel/cancel_group (again) -- running threads only;
|
file |
diff |
annotate
|
Sat, 07 Apr 2012 19:28:44 +0200 |
wenzelm |
added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
|
file |
diff |
annotate
|
Sat, 07 Apr 2012 16:41:59 +0200 |
wenzelm |
explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
|
file |
diff |
annotate
|
Fri, 06 Apr 2012 23:34:38 +0200 |
wenzelm |
discontinued obsolete last_execs (cf. cd3ab7625519);
|
file |
diff |
annotate
|
Fri, 06 Apr 2012 12:02:24 +0200 |
wenzelm |
stop node execution at first unassigned exec;
|
file |
diff |
annotate
|
Fri, 06 Apr 2012 11:49:08 +0200 |
wenzelm |
discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;
|
file |
diff |
annotate
|
Thu, 05 Apr 2012 22:33:52 +0200 |
wenzelm |
more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
|
file |
diff |
annotate
|
Thu, 05 Apr 2012 14:34:54 +0200 |
wenzelm |
less ambitious memo_eval, since memo_result is still not robust here;
|
file |
diff |
annotate
|
Thu, 05 Apr 2012 14:14:51 +0200 |
wenzelm |
less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
|
file |
diff |
annotate
|
Thu, 05 Apr 2012 13:01:54 +0200 |
wenzelm |
more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
|
file |
diff |
annotate
|
Thu, 05 Apr 2012 11:58:46 +0200 |
wenzelm |
Command.memo including physical interrupts (unlike Lazy.lazy);
|
file |
diff |
annotate
|
Thu, 05 Apr 2012 10:45:53 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 04 Apr 2012 21:03:30 +0200 |
wenzelm |
tuned -- NB: get_theory still needs to apply Lazy.force due to interrupt instabilities;
|
file |
diff |
annotate
|
Wed, 04 Apr 2012 14:19:47 +0200 |
wenzelm |
separate module for prover command execution;
|
file |
diff |
annotate
|