| 2011-07-10 |
wenzelm |
2011-07-10 |
propagate header changes to prover process;
simplified Document case classes;
Document.State.assignments: indexed by Version_ID;
|
file | diff | annotate |
| 2011-07-08 |
wenzelm |
2011-07-08 |
moved global state to structure Document (again);
|
file | diff | annotate |
| 2011-07-05 |
wenzelm |
2011-07-05 |
get theory from last executation state;
tuned error messages;
|
file | diff | annotate |
| 2011-07-05 |
wenzelm |
2011-07-05 |
clarified cancel_execution/await_cancellation;
|
file | diff | annotate |
| 2011-07-02 |
wenzelm |
2011-07-02 |
tuned;
|
file | diff | annotate |
| 2011-04-11 |
wenzelm |
2011-04-11 |
more permissive run_command: identity execution for empty toplevel, e.g. after malformed theory header;
|
file | diff | annotate |
| 2011-03-20 |
wenzelm |
2011-03-20 |
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
explicit Timing.message function;
eliminated Output.timing flag, cf. Toplevel.timing;
tuned;
|
file | diff | annotate |
| 2011-01-31 |
wenzelm |
2011-01-31 |
tuned signature;
tuned vacous forks;
|
file | diff | annotate |
| 2011-01-31 |
wenzelm |
2011-01-31 |
support named tasks, for improved tracing;
|
file | diff | annotate |
| 2011-01-31 |
wenzelm |
2011-01-31 |
more direct Future.bulk, which potentially reduces overhead for Par_List;
tuned signature;
|
file | diff | annotate |
| 2011-01-27 |
wenzelm |
2011-01-27 |
cancel document execution before editing, to improve reactivity on systems with few cores;
|
file | diff | annotate |
| 2011-01-25 |
wenzelm |
2011-01-25 |
singleton (sequential) execution, to avoid race conditions in theory loader state (e.g. when multiple independent theories import the same theory);
|
file | diff | annotate |
| 2011-01-25 |
wenzelm |
2011-01-25 |
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 |
| 2011-01-13 |
wenzelm |
2011-01-13 |
full theory path enables loading parents via master directory and keeps files strictly separate;
|
file | diff | annotate |
| 2010-11-14 |
wenzelm |
2010-11-14 |
clarified interact/print state: proof commands are treated as in TTY mode to get full response;
|
file | diff | annotate |
| 2010-11-13 |
wenzelm |
2010-11-13 |
always print state of proof commands (notably "qed" etc.);
|
file | diff | annotate |
| 2010-11-13 |
wenzelm |
2010-11-13 |
await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;
|
file | diff | annotate |
| 2010-11-11 |
wenzelm |
2010-11-11 |
more precise treatment of deleted nodes;
|
file | diff | annotate |
| 2010-11-09 |
wenzelm |
2010-11-09 |
added general Synchronized.counter convenience;
|
file | diff | annotate |
| 2010-11-06 |
wenzelm |
2010-11-06 |
continue after failed commands;
|
file | diff | annotate |
| 2010-11-06 |
wenzelm |
2010-11-06 |
explicit "timing" status for toplevel transactions;
|
file | diff | annotate |
| 2010-11-06 |
wenzelm |
2010-11-06 |
tuned;
|
file | diff | annotate |
| 2010-09-15 |
wenzelm |
2010-09-15 |
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 |
| 2010-09-09 |
wenzelm |
2010-09-09 |
refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
|
file | diff | annotate |
| 2010-09-09 |
wenzelm |
2010-09-09 |
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
|
file | diff | annotate |
| 2010-08-31 |
wenzelm |
2010-08-31 |
moved Toplevel.run_command to Pure/PIDE/document.ML;
eliminated aliases of exception Toplevel.TERMINATE and Toplevel.EXCURSION_FAIL;
tuned signatures;
|
file | diff | annotate |
| 2010-08-30 |
wenzelm |
2010-08-30 |
tuned;
|
file | diff | annotate |
| 2010-08-17 |
wenzelm |
2010-08-17 |
tune;
|
file | diff | annotate |
| 2010-08-17 |
wenzelm |
2010-08-17 |
added functor Linear_Set, based on former adhoc structures in document.ML;
Linear_Set.delete_after (ML): actually delete table entries;
Scala Linear_Set: clarified exceptions, according to ML version;
simplified Document.node using Linear_Set;
ML Document.edit: refer to start via NONE instead of no_id, according to Scala version;
|
file | diff | annotate |
| 2010-08-15 |
wenzelm |
2010-08-15 |
document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;
|
file | diff | annotate |
| 2010-08-15 |
wenzelm |
2010-08-15 |
renamed create_id to new_id;
|
file | diff | annotate |
| 2010-08-15 |
wenzelm |
2010-08-15 |
more explicit / functional ML version of document model;
tuned;
|
file | diff | annotate |
| 2010-08-14 |
wenzelm |
2010-08-14 |
more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
added convenient Markup.Int/Long objects (Scala);
simplified "assign" message format -- explicit version id;
misc tuning and simplification;
|
file | diff | annotate |
| 2010-08-14 |
wenzelm |
2010-08-14 |
tuned;
|
file | diff | annotate |
| 2010-08-12 |
wenzelm |
2010-08-12 |
clarified "state" (accumulated data) vs. "exec" (execution that produces data);
generic type Document.id (ML) / Document.ID;
|
file | diff | annotate |
| 2010-08-11 |
wenzelm |
2010-08-11 |
represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);
|
file | diff | annotate |
| 2010-08-05 |
wenzelm |
2010-08-05 |
simplified/refined document model: collection of named nodes, without proper dependencies yet;
moved basic type definitions for ids and edits from Isar_Document to Document;
removed begin_document/end_document for now -- nodes emerge via edits;
edits refer to named nodes explicitly;
|
file | diff | annotate |