src/Pure/PIDE/document.ML
2013-07-29 ago discontinued notion of "stable" result -- running execution is never canceled;
2013-07-20 ago document update at high priority -- important;
2013-07-20 ago option editor_execution_priority;
2013-07-15 ago more careful termination of removed execs, leaving running execs undisturbed;
2013-07-12 ago clarified execution: maintain running execs only, check "stable" separately via memo (again);
2013-07-12 ago tuned signature;
2013-07-12 ago clarified module name;
2013-07-11 ago more explicit type Exec.context;
2013-07-11 ago strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
2013-07-11 ago more abstract types;
2013-07-11 ago tuned;
2013-07-11 ago global management of command execution fragments;
2013-07-11 ago fully synchronized guard of running execution;
2013-07-11 ago re-assign prints of unchanged eval only -- avoid crash of new_exec;
2013-07-11 ago tuned -- refrain from odd optimization;
2013-07-11 ago tuned;
2013-07-10 ago tuned start_execution: avoid sleep on worker thread;
2013-07-10 ago clarified Command.print: update old prints here;
2013-07-09 ago produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
2013-07-09 ago more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
2013-07-05 ago tuned signature;
2013-07-05 ago tuned signature;
2013-07-05 ago clarified type Command.eval;
2013-07-05 ago tuned signature;
2013-07-05 ago explicit module Document_ID as source of globally unique identifiers across ML/Scala;
2013-07-04 ago separate exec_id assignment for Command.print states, without affecting result of eval;
2013-07-04 ago more Command.memo operations;
2013-07-04 ago made SML/NJ happy;
2013-07-03 ago more print function parameters;
2013-07-03 ago tuned;
2013-07-03 ago discontinued odd workaround for some old Poly/ML, which is still supported but of little practical relevance;
2013-07-03 ago tuned;
2013-07-03 ago allow multiple print functions;
2013-07-03 ago tuned signature;
2013-07-03 ago tuned signature;
2013-07-03 ago tuned;
2013-02-27 ago discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
2013-02-27 ago discontinued obsolete 'uses' within theory header;
2013-02-24 ago simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
2013-01-13 ago more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
2012-11-25 ago Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-18 ago more official Future.terminate;
2012-09-05 ago eliminated potentially confusing terminology of Scala "layer";
2012-09-02 ago maintain stable state of node entries from last round -- bypass slightly different Thm.join_theory_proofs;
2012-09-01 ago central management of forked goals wrt. transaction id;
2012-08-30 ago refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
2012-08-30 ago some support for registering forked proofs within Proof.state, using its bottom context;
2012-08-30 ago tuned signature;
2012-08-26 ago theory def/ref position reports, which enable hyperlinks etc.;
2012-08-24 ago check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);
2012-08-11 ago vacuous execution after first malformed command;
2012-08-10 ago apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.;
2012-07-27 ago even more permissive approximation of master_dir, which is only required to access external resources ('uses' etc.);
2012-08-07 ago simplified Document.Node.Header -- internalized errors;
2012-04-20 ago improved interleaving of start_execution vs. cancel_execution of the next update;
2012-04-20 ago always revisit nodes independently of "required" flag, which may change during editing -- avoid "bloodbath effect" when changing perspective while loading;
2012-04-20 ago tuned;
2012-04-20 ago builtin timing for main operations;
2012-04-11 ago tuned;
2012-04-11 ago just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;