| Fri, 19 Aug 2011 18:01:23 +0200 |
tuned;
|
file | diff | annotate |
| Fri, 19 Aug 2011 17:39:37 +0200 |
tuned signature (again);
|
file | diff | annotate |
| Fri, 19 Aug 2011 16:13:26 +0200 |
tuned signature -- treat structure Task_Queue as private to implementation;
|
file | diff | annotate |
| Fri, 19 Aug 2011 15:56:26 +0200 |
refined Future.cancel: explicit future allows to join actual cancellation;
|
file | diff | annotate |
| Thu, 18 Aug 2011 18:07:40 +0200 |
more precise treatment of exception nesting and serial numbers;
|
file | diff | annotate |
| Thu, 18 Aug 2011 17:53:32 +0200 |
more careful treatment of exception serial numbers, with propagation to message channel;
|
file | diff | annotate |
| Wed, 17 Aug 2011 22:14:22 +0200 |
more systematic handling of parallel exceptions;
|
file | diff | annotate |
| Tue, 16 Aug 2011 23:17:26 +0200 |
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 |
more robust treatment of node dependencies in incremental edits;
|
file | diff | annotate |
| Tue, 16 Aug 2011 21:13:52 +0200 |
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 |
touch descendants of edited nodes;
|
file | diff | annotate |
| Mon, 15 Aug 2011 21:05:30 +0200 |
parellel scheduling of node edits and execution;
|
file | diff | annotate |
| Mon, 15 Aug 2011 20:38:16 +0200 |
tuned error message;
|
file | diff | annotate |
| Mon, 15 Aug 2011 20:19:41 +0200 |
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 |
explicit check of finished evaluation;
|
file | diff | annotate |
| Mon, 15 Aug 2011 16:38:42 +0200 |
refined Document.edit: less stateful update via Graph.schedule;
|
file | diff | annotate |
| Mon, 15 Aug 2011 14:54:36 +0200 |
simplified exec: eliminated unused status flag;
|
file | diff | annotate |
| Sat, 13 Aug 2011 20:41:29 +0200 |
simplified Toplevel.init_theory: discontinued special master argument;
|
file | diff | annotate |
| Sat, 13 Aug 2011 20:20:36 +0200 |
provide node header via Scala layer;
|
file | diff | annotate |
| Sat, 13 Aug 2011 15:59:26 +0200 |
clarified node header -- exclude master_dir;
|
file | diff | annotate |
| Sat, 13 Aug 2011 13:42:35 +0200 |
maintain node header;
|
file | diff | annotate |
| Fri, 12 Aug 2011 15:28:30 +0200 |
clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
|
file | diff | annotate |
| Thu, 11 Aug 2011 20:32:44 +0200 |
uniform treatment of header edits as document edits;
|
file | diff | annotate |
| Thu, 11 Aug 2011 18:01:28 +0200 |
explicit datatypes for document node edits;
|
file | diff | annotate |
| Wed, 10 Aug 2011 16:05:14 +0200 |
future_job: explicit indication of interrupts;
|
file | diff | annotate |
| Mon, 11 Jul 2011 22:55:47 +0200 |
tuned signature -- corresponding to Scala version;
|
file | diff | annotate |
| Sun, 10 Jul 2011 00:21:19 +0200 |
propagate header changes to prover process;
|
file | diff | annotate |
| Fri, 08 Jul 2011 22:00:53 +0200 |
moved global state to structure Document (again);
|
file | diff | annotate |
| Tue, 05 Jul 2011 20:36:49 +0200 |
get theory from last executation state;
|
file | diff | annotate |
| Tue, 05 Jul 2011 11:45:48 +0200 |
clarified cancel_execution/await_cancellation;
|
file | diff | annotate |
| Sat, 02 Jul 2011 20:22:02 +0200 |
tuned;
|
file | diff | annotate |
| Mon, 11 Apr 2011 17:23:20 +0200 |
more permissive run_command: identity execution for empty toplevel, e.g. after malformed theory header;
|
file | diff | annotate |
| Sun, 20 Mar 2011 21:28:11 +0100 |
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
|
file | diff | annotate |
| Mon, 31 Jan 2011 23:02:53 +0100 |
tuned signature;
|
file | diff | annotate |
| Mon, 31 Jan 2011 22:57:01 +0100 |
support named tasks, for improved tracing;
|
file | diff | annotate |
| Mon, 31 Jan 2011 21:54:49 +0100 |
more direct Future.bulk, which potentially reduces overhead for Par_List;
|
file | diff | annotate |
| Thu, 27 Jan 2011 12:24:00 +0100 |
cancel document execution before editing, to improve reactivity on systems with few cores;
|
file | diff | annotate |
| Tue, 25 Jan 2011 21:26:25 +0100 |
singleton (sequential) execution, to avoid race conditions in theory loader state (e.g. when multiple independent theories import the same theory);
|
file | diff | annotate |
| Tue, 25 Jan 2011 20:06:32 +0100 |
workaround for odd x86_64 problem in Poly/ML 5.4.0 (actually SVN 1151?), which causes unexpected nontermination of Isabelle/Scala document editing;
|
file | diff | annotate |
| Thu, 13 Jan 2011 17:39:35 +0100 |
full theory path enables loading parents via master directory and keeps files strictly separate;
|
file | diff | annotate |
| Sun, 14 Nov 2010 14:05:08 +0100 |
clarified interact/print state: proof commands are treated as in TTY mode to get full response;
|
file | diff | annotate |
| Sat, 13 Nov 2010 21:46:24 +0100 |
always print state of proof commands (notably "qed" etc.);
|
file | diff | annotate |
| Sat, 13 Nov 2010 11:41:02 +0100 |
await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;
|
file | diff | annotate |
| Thu, 11 Nov 2010 19:58:07 +0100 |
more precise treatment of deleted nodes;
|
file | diff | annotate |
| Tue, 09 Nov 2010 21:44:19 +0100 |
added general Synchronized.counter convenience;
|
file | diff | annotate |
| Sat, 06 Nov 2010 20:59:59 +0100 |
continue after failed commands;
|
file | diff | annotate |
| Sat, 06 Nov 2010 16:31:35 +0100 |
explicit "timing" status for toplevel transactions;
|
file | diff | annotate |
| Sat, 06 Nov 2010 16:03:49 +0100 |
tuned;
|
file | diff | annotate |
| Wed, 15 Sep 2010 16:06:52 +0200 |
Document.async_state: some attempts to make this more robust wrt. cancelation of the main transaction -- avoid confusing feedback about pending forks;
|
file | diff | annotate |
| Thu, 09 Sep 2010 18:21:06 +0200 |
refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
|
file | diff | annotate |
| Thu, 09 Sep 2010 17:20:27 +0200 |
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
|
file | diff | annotate |
| Tue, 31 Aug 2010 23:46:49 +0200 |
moved Toplevel.run_command to Pure/PIDE/document.ML;
|
file | diff | annotate |
| Mon, 30 Aug 2010 14:56:27 +0200 |
tuned;
|
file | diff | annotate |
| Tue, 17 Aug 2010 15:54:04 +0200 |
tune;
|
file | diff | annotate |
| Tue, 17 Aug 2010 15:10:49 +0200 |
added functor Linear_Set, based on former adhoc structures in document.ML;
|
file | diff | annotate |
| Sun, 15 Aug 2010 20:13:07 +0200 |
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
|
file | diff | annotate |
| Sun, 15 Aug 2010 19:30:11 +0200 |
renamed create_id to new_id;
|
file | diff | annotate |
| Sun, 15 Aug 2010 18:41:23 +0200 |
more explicit / functional ML version of document model;
|
file | diff | annotate |
| Sat, 14 Aug 2010 22:45:23 +0200 |
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
|
file | diff | annotate |
| Sat, 14 Aug 2010 11:52:24 +0200 |
tuned;
|
file | diff | annotate |