| 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
|
| Tue, 16 Aug 2011 23:17:26 +0200 |
wenzelm |
workaround for Cygwin, to make it work in the important special case without extra files;
|
file |
diff |
annotate
|
| Tue, 16 Aug 2011 21:50:53 +0200 |
wenzelm |
more robust treatment of node dependencies in incremental edits;
|
file |
diff |
annotate
|
| Tue, 16 Aug 2011 21:13:52 +0200 |
wenzelm |
use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
|
file |
diff |
annotate
|
| Mon, 15 Aug 2011 21:54:32 +0200 |
wenzelm |
touch descendants of edited nodes;
|
file |
diff |
annotate
|
| Mon, 15 Aug 2011 21:05:30 +0200 |
wenzelm |
parellel scheduling of node edits and execution;
|
file |
diff |
annotate
|
| Mon, 15 Aug 2011 20:38:16 +0200 |
wenzelm |
tuned error message;
|
file |
diff |
annotate
|
| Mon, 15 Aug 2011 20:19:41 +0200 |
wenzelm |
retrieve imports from document state, with fall-back on theory loader for preloaded theories;
|
file |
diff |
annotate
|
| Mon, 15 Aug 2011 19:27:55 +0200 |
wenzelm |
explicit check of finished evaluation;
|
file |
diff |
annotate
|