| 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
|
| Wed, 04 Apr 2012 14:00:47 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 20 Mar 2012 18:01:34 +0100 |
wenzelm |
minimalistic support for remote URLs: no master dir here;
|
file |
diff |
annotate
|
| Fri, 16 Mar 2012 13:05:30 +0100 |
wenzelm |
define keywords early when processing the theory header, before running the body commands;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 22:08:53 +0100 |
wenzelm |
declare command keywords via theory header, including strict checking outside Pure;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 17:40:26 +0100 |
wenzelm |
declare keywords as side-effect of header edit;
|
file |
diff |
annotate
|
| Thu, 15 Mar 2012 00:10:45 +0100 |
wenzelm |
some support for outer syntax keyword declarations within theory header;
|
file |
diff |
annotate
|
| Tue, 13 Mar 2012 21:17:37 +0100 |
wenzelm |
clarified command state -- markup within proper_range, excluding trailing whitespace;
|
file |
diff |
annotate
|
| Mon, 12 Mar 2012 17:27:52 +0100 |
wenzelm |
refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);
|
file |
diff |
annotate
|
| Thu, 01 Mar 2012 11:28:33 +0100 |
wenzelm |
clarified document nodes (full import graph) vs. node_status (non-preloaded theories);
|
file |
diff |
annotate
|
| Tue, 29 Nov 2011 21:50:00 +0100 |
wenzelm |
clarified Time vs. Timing;
|
file |
diff |
annotate
|
| Mon, 28 Nov 2011 22:05:32 +0100 |
wenzelm |
separate module for concrete Isabelle markup;
|
file |
diff |
annotate
|
| Sun, 18 Sep 2011 19:49:35 +0200 |
wenzelm |
explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
|
file |
diff |
annotate
|
| Wed, 07 Sep 2011 21:31:50 +0200 |
wenzelm |
no print_state for final proof commands, which return to theory state;
|
file |
diff |
annotate
|
| Sat, 03 Sep 2011 19:47:31 +0200 |
wenzelm |
discontinued predefined empty command (obsolete!?);
|
file |
diff |
annotate
|
| Sat, 03 Sep 2011 19:39:16 +0200 |
wenzelm |
discontinued global execs: store exec value directly within entries;
|
file |
diff |
annotate
|
| Sat, 03 Sep 2011 18:08:09 +0200 |
wenzelm |
Document.remove_versions on ML side;
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 21:06:05 +0200 |
wenzelm |
less agressive parsing of commands (priority ~1);
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 15:21:40 +0200 |
wenzelm |
more precise iterate_entries_after if start refers to last entry;
|
file |
diff |
annotate
|
| Fri, 02 Sep 2011 11:52:13 +0200 |
wenzelm |
clarified define_command: store name as structural information;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2011 23:08:42 +0200 |
wenzelm |
amended last_common, if that happens to the very last entry (important to load HOL/Auth, for example);
|
file |
diff |
annotate
|
| Thu, 01 Sep 2011 11:33:44 +0200 |
wenzelm |
more careful treatment of interrupts, to retain them within forked/joined boundary of command transactions;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2011 20:32:24 +0200 |
wenzelm |
explicit running_color;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2011 19:52:13 +0200 |
wenzelm |
tuned join_commands: avoid traversing cumulative table;
|
file |
diff |
annotate
|
| Sat, 27 Aug 2011 13:26:06 +0200 |
wenzelm |
more precise treatment of nodes that are fully required for partially visible ones;
|
file |
diff |
annotate
|
| Fri, 26 Aug 2011 21:27:58 +0200 |
wenzelm |
tuned signature -- iterate subsumes both fold and get_first;
|
file |
diff |
annotate
|
| Fri, 26 Aug 2011 21:18:42 +0200 |
wenzelm |
further clarification of Document.updated, based on last_common and after_entry;
|
file |
diff |
annotate
|
| Fri, 26 Aug 2011 16:06:58 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 26 Aug 2011 15:56:30 +0200 |
wenzelm |
improved Document.edit: more accurate update_start and no_execs;
|
file |
diff |
annotate
|
| Fri, 26 Aug 2011 15:09:54 +0200 |
wenzelm |
refined document state assignment: observe perspective, more explicit assignment message;
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 19:12:58 +0200 |
wenzelm |
tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
|
file |
diff |
annotate
|
| Thu, 25 Aug 2011 16:44:06 +0200 |
wenzelm |
propagate information about last command with exec state assignment through document model;
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 17:25:45 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 17:16:48 +0200 |
wenzelm |
tuned pri: prefer purging of canceled execution;
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 17:14:31 +0200 |
wenzelm |
tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 15:55:43 +0200 |
wenzelm |
misc tuning and simplification;
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 15:30:43 +0200 |
wenzelm |
ignore irrelevant timings;
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 13:40:10 +0200 |
wenzelm |
print state only for visible command, to avoid wasting resources for the larger part of the text;
|
file |
diff |
annotate
|
| Wed, 24 Aug 2011 13:03:39 +0200 |
wenzelm |
update_perspective without actual edits, bypassing the full state assignment protocol;
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 21:19:24 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 15:48:41 +0200 |
wenzelm |
some support for toplevel printing wrt. editor perspective (still inactive);
|
file |
diff |
annotate
|
| Tue, 23 Aug 2011 12:20:12 +0200 |
wenzelm |
propagate editor perspective through document model;
|
file |
diff |
annotate
|
| Mon, 22 Aug 2011 21:42:02 +0200 |
wenzelm |
some support for editor perspective;
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 23:35:30 +0200 |
wenzelm |
refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
|
file |
diff |
annotate
|
| Sat, 20 Aug 2011 15:52:29 +0200 |
wenzelm |
added Future.joins convenience;
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 18:01:23 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 17:39:37 +0200 |
wenzelm |
tuned signature (again);
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 16:13:26 +0200 |
wenzelm |
tuned signature -- treat structure Task_Queue as private to implementation;
|
file |
diff |
annotate
|
| Fri, 19 Aug 2011 15:56:26 +0200 |
wenzelm |
refined Future.cancel: explicit future allows to join actual cancellation;
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 18:07:40 +0200 |
wenzelm |
more precise treatment of exception nesting and serial numbers;
|
file |
diff |
annotate
|
| Thu, 18 Aug 2011 17:53:32 +0200 |
wenzelm |
more careful treatment of exception serial numbers, with propagation to message channel;
|
file |
diff |
annotate
|
| Wed, 17 Aug 2011 22:14:22 +0200 |
wenzelm |
more systematic handling of parallel exceptions;
|
file |
diff |
annotate
|