2011-07-10 wenzelm 2011-07-10 propagate header changes to prover process; simplified Document case classes; Document.State.assignments: indexed by Version_ID;
2011-07-08 wenzelm 2011-07-08 moved global state to structure Document (again);
2011-07-05 wenzelm 2011-07-05 get theory from last executation state; tuned error messages;
2011-07-05 wenzelm 2011-07-05 clarified cancel_execution/await_cancellation;
2011-07-02 wenzelm 2011-07-02 tuned;
2011-04-11 wenzelm 2011-04-11 more permissive run_command: identity execution for empty toplevel, e.g. after malformed theory header;
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;
2011-01-31 wenzelm 2011-01-31 tuned signature; tuned vacous forks;
2011-01-31 wenzelm 2011-01-31 support named tasks, for improved tracing;
2011-01-31 wenzelm 2011-01-31 more direct Future.bulk, which potentially reduces overhead for Par_List; tuned signature;
2011-01-27 wenzelm 2011-01-27 cancel document execution before editing, to improve reactivity on systems with few cores;
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);
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;
2011-01-13 wenzelm 2011-01-13 full theory path enables loading parents via master directory and keeps files strictly separate;
2010-11-14 wenzelm 2010-11-14 clarified interact/print state: proof commands are treated as in TTY mode to get full response;
2010-11-13 wenzelm 2010-11-13 always print state of proof commands (notably "qed" etc.);
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;
2010-11-11 wenzelm 2010-11-11 more precise treatment of deleted nodes;
2010-11-09 wenzelm 2010-11-09 added general Synchronized.counter convenience;
2010-11-06 wenzelm 2010-11-06 continue after failed commands;
2010-11-06 wenzelm 2010-11-06 explicit "timing" status for toplevel transactions;
2010-11-06 wenzelm 2010-11-06 tuned;
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;
2010-09-09 wenzelm 2010-09-09 refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;
2010-09-09 wenzelm 2010-09-09 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
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;
2010-08-30 wenzelm 2010-08-30 tuned;
2010-08-17 wenzelm 2010-08-17 tune;
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;
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;
2010-08-15 wenzelm 2010-08-15 renamed create_id to new_id;
2010-08-15 wenzelm 2010-08-15 more explicit / functional ML version of document model; tuned;
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;
2010-08-14 wenzelm 2010-08-14 tuned;
2010-08-12 wenzelm 2010-08-12 clarified "state" (accumulated data) vs. "exec" (execution that produces data); generic type (ML) / Document.ID;
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);
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;