| Fri, 02 Aug 2013 16:00:14 +0200 |
wenzelm |
support print functions with explicit arguments, as provided by overlays;
|
file |
diff |
annotate
|
| Fri, 02 Aug 2013 14:26:09 +0200 |
wenzelm |
maintain overlays within node perspective;
|
file |
diff |
annotate
|
| Wed, 31 Jul 2013 12:46:53 +0200 |
wenzelm |
simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;
|
file |
diff |
annotate
|
| Wed, 31 Jul 2013 12:14:13 +0200 |
wenzelm |
allow explicit indication of required node: full eval, no prints;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 16:22:07 +0200 |
wenzelm |
more timing;
|
file |
diff |
annotate
|
| Tue, 30 Jul 2013 16:01:19 +0200 |
wenzelm |
more timing;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 19:55:38 +0200 |
wenzelm |
traverse node on change of "required" state;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 18:59:58 +0200 |
wenzelm |
keep memo_exec execution running, which is important to cancel goal forks eventually;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 16:52:04 +0200 |
wenzelm |
maintain explicit execution frontier: avoid conflict with former task via static dependency;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 15:59:47 +0200 |
wenzelm |
clarified conditions for node traversal;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 15:20:02 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 29 Jul 2013 13:24:15 +0200 |
wenzelm |
discontinued notion of "stable" result -- running execution is never canceled;
|
file |
diff |
annotate
|
| Sat, 20 Jul 2013 16:29:06 +0200 |
wenzelm |
document update at high priority -- important;
|
file |
diff |
annotate
|
| Sat, 20 Jul 2013 16:27:55 +0200 |
wenzelm |
option editor_execution_priority;
|
file |
diff |
annotate
|
| Mon, 15 Jul 2013 10:25:35 +0200 |
wenzelm |
more careful termination of removed execs, leaving running execs undisturbed;
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 12:04:16 +0200 |
wenzelm |
clarified execution: maintain running execs only, check "stable" separately via memo (again);
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 11:28:03 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 12 Jul 2013 11:07:02 +0200 |
wenzelm |
clarified module name;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 23:24:40 +0200 |
wenzelm |
more explicit type Exec.context;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 16:26:14 +0200 |
wenzelm |
more abstract types;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 16:01:48 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 14:42:11 +0200 |
wenzelm |
global management of command execution fragments;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 12:28:24 +0200 |
wenzelm |
fully synchronized guard of running execution;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 11:37:06 +0200 |
wenzelm |
re-assign prints of unchanged eval only -- avoid crash of new_exec;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 11:09:23 +0200 |
wenzelm |
tuned -- refrain from odd optimization;
|
file |
diff |
annotate
|
| Thu, 11 Jul 2013 10:43:53 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 10 Jul 2013 12:33:28 +0200 |
wenzelm |
tuned start_execution: avoid sleep on worker thread;
|
file |
diff |
annotate
|
| Wed, 10 Jul 2013 11:26:55 +0200 |
wenzelm |
clarified Command.print: update old prints here;
|
file |
diff |
annotate
|
| 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
|