src/Pure/PIDE/document.ML
2011-08-15 wenzelm 2011-08-15 simplified exec: eliminated unused status flag;
2011-08-13 wenzelm 2011-08-13 simplified Toplevel.init_theory: discontinued special master argument;
2011-08-13 wenzelm 2011-08-13 provide node header via Scala layer; clarified node edit Clear: retain header information; run_command: node info via document model, error handling within transaction; node names without ".thy" suffix, to coincide with traditional theory loader treatment;
2011-08-13 wenzelm 2011-08-13 clarified node header -- exclude master_dir;
2011-08-13 wenzelm 2011-08-13 maintain node header; misc tuning and clarification;
2011-08-12 wenzelm 2011-08-12 clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
2011-08-11 wenzelm 2011-08-11 uniform treatment of header edits as document edits;
2011-08-11 wenzelm 2011-08-11 explicit datatypes for document node edits;
2011-08-10 wenzelm 2011-08-10 future_job: explicit indication of interrupts;
2011-07-11 wenzelm 2011-07-11 tuned signature -- corresponding to Scala version;
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 Document.id (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;