src/Pure/PIDE/document.ML
2011-08-25 ago propagate information about last command with exec state assignment through document model;
2011-08-24 ago misc tuning and simplification;
2011-08-24 ago tuned pri: prefer purging of canceled execution;
2011-08-24 ago tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
2011-08-24 ago misc tuning and simplification;
2011-08-24 ago ignore irrelevant timings;
2011-08-24 ago print state only for visible command, to avoid wasting resources for the larger part of the text;
2011-08-24 ago update_perspective without actual edits, bypassing the full state assignment protocol;
2011-08-23 ago tuned;
2011-08-23 ago some support for toplevel printing wrt. editor perspective (still inactive);
2011-08-23 ago propagate editor perspective through document model;
2011-08-22 ago some support for editor perspective;
2011-08-20 ago refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
2011-08-20 ago added Future.joins convenience;
2011-08-19 ago tuned;
2011-08-19 ago tuned signature (again);
2011-08-19 ago tuned signature -- treat structure Task_Queue as private to implementation;
2011-08-19 ago refined Future.cancel: explicit future allows to join actual cancellation;
2011-08-18 ago more precise treatment of exception nesting and serial numbers;
2011-08-18 ago more careful treatment of exception serial numbers, with propagation to message channel;
2011-08-17 ago more systematic handling of parallel exceptions;
2011-08-16 ago workaround for Cygwin, to make it work in the important special case without extra files;
2011-08-16 ago more robust treatment of node dependencies in incremental edits;
2011-08-16 ago use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
2011-08-15 ago touch descendants of edited nodes;
2011-08-15 ago parellel scheduling of node edits and execution;
2011-08-15 ago tuned error message;
2011-08-15 ago retrieve imports from document state, with fall-back on theory loader for preloaded theories;
2011-08-15 ago explicit check of finished evaluation;
2011-08-15 ago refined Document.edit: less stateful update via Graph.schedule;
2011-08-15 ago simplified exec: eliminated unused status flag;
2011-08-13 ago simplified Toplevel.init_theory: discontinued special master argument;
2011-08-13 ago provide node header via Scala layer;
2011-08-13 ago clarified node header -- exclude master_dir;
2011-08-13 ago maintain node header;
2011-08-12 ago clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);
2011-08-11 ago uniform treatment of header edits as document edits;
2011-08-11 ago explicit datatypes for document node edits;
2011-08-10 ago future_job: explicit indication of interrupts;
2011-07-11 ago tuned signature -- corresponding to Scala version;
2011-07-10 ago propagate header changes to prover process;
2011-07-08 ago moved global state to structure Document (again);
2011-07-05 ago get theory from last executation state;
2011-07-05 ago clarified cancel_execution/await_cancellation;
2011-07-02 ago tuned;
2011-04-11 ago more permissive run_command: identity execution for empty toplevel, e.g. after malformed theory header;
2011-03-20 ago structure Timing: covers former start_timing/end_timing and Output.timeit etc;
2011-01-31 ago tuned signature;
2011-01-31 ago support named tasks, for improved tracing;
2011-01-31 ago more direct Future.bulk, which potentially reduces overhead for Par_List;
2011-01-27 ago cancel document execution before editing, to improve reactivity on systems with few cores;
2011-01-25 ago singleton (sequential) execution, to avoid race conditions in theory loader state (e.g. when multiple independent theories import the same theory);
2011-01-25 ago 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 ago full theory path enables loading parents via master directory and keeps files strictly separate;
2010-11-14 ago clarified interact/print state: proof commands are treated as in TTY mode to get full response;
2010-11-13 ago always print state of proof commands (notably "qed" etc.);
2010-11-13 ago await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;
2010-11-11 ago more precise treatment of deleted nodes;
2010-11-09 ago added general Synchronized.counter convenience;
2010-11-06 ago continue after failed commands;