src/Pure/PIDE/document.ML
2013-07-31 wenzelm 2013-07-31 allow explicit indication of required node: full eval, no prints;
2013-07-30 wenzelm 2013-07-30 recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
2013-07-30 wenzelm 2013-07-30 more timing;
2013-07-30 wenzelm 2013-07-30 more timing; tuned -- Execution.is_running always holds due to immediate start;
2013-07-30 wenzelm 2013-07-30 de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
2013-07-29 wenzelm 2013-07-29 traverse node on change of "required" state;
2013-07-29 wenzelm 2013-07-29 keep memo_exec execution running, which is important to cancel goal forks eventually; run as nested worker task to keep main group valid, even after cancelation of removed subgroups; do not memoize interrupt, but absorb it silently in main execution; Goal.purge_futures: rough sanity check of group status;
2013-07-29 wenzelm 2013-07-29 maintain explicit execution frontier: avoid conflict with former task via static dependency; start execution immediate after assignment, to keep frontier simple;
2013-07-29 wenzelm 2013-07-29 clarified conditions for node traversal;
2013-07-29 wenzelm 2013-07-29 tuned;
2013-07-29 wenzelm 2013-07-29 discontinued notion of "stable" result -- running execution is never canceled;
2013-07-20 wenzelm 2013-07-20 document update at high priority -- important;
2013-07-20 wenzelm 2013-07-20 option editor_execution_priority;
2013-07-15 wenzelm 2013-07-15 more careful termination of removed execs, leaving running execs undisturbed;
2013-07-12 wenzelm 2013-07-12 clarified execution: maintain running execs only, check "stable" separately via memo (again); tuned signatures;
2013-07-12 wenzelm 2013-07-12 tuned signature; tuned comments;
2013-07-12 wenzelm 2013-07-12 clarified module name;
2013-07-11 wenzelm 2013-07-11 more explicit type Exec.context; eliminated obsolete execution group -- NB: cancelation happens individually for registered execs;
2013-07-11 wenzelm 2013-07-11 strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
2013-07-11 wenzelm 2013-07-11 more abstract types; tuned signature;
2013-07-11 wenzelm 2013-07-11 tuned;
2013-07-11 wenzelm 2013-07-11 global management of command execution fragments; tuned;
2013-07-11 wenzelm 2013-07-11 fully synchronized guard of running execution; tuned;
2013-07-11 wenzelm 2013-07-11 re-assign prints of unchanged eval only -- avoid crash of new_exec;
2013-07-11 wenzelm 2013-07-11 tuned -- refrain from odd optimization;
2013-07-11 wenzelm 2013-07-11 tuned;
2013-07-10 wenzelm 2013-07-10 tuned start_execution: avoid sleep on worker thread;
2013-07-10 wenzelm 2013-07-10 clarified Command.print: update old prints here;
2013-07-09 wenzelm 2013-07-09 produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
2013-07-09 wenzelm 2013-07-09 more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
2013-07-05 wenzelm 2013-07-05 tuned signature; tuned comments;
2013-07-05 wenzelm 2013-07-05 tuned signature; tuned;
2013-07-05 wenzelm 2013-07-05 clarified type Command.eval;
2013-07-05 wenzelm 2013-07-05 tuned signature;
2013-07-05 wenzelm 2013-07-05 explicit module Document_ID as source of globally unique identifiers across ML/Scala;
2013-07-04 wenzelm 2013-07-04 separate exec_id assignment for Command.print states, without affecting result of eval; tuned signature; tuned;
2013-07-04 wenzelm 2013-07-04 more Command.memo operations; more explicit types Command.eval vs. Command.print vs. Document.exec; clarified print function parameters;
2013-07-04 wenzelm 2013-07-04 made SML/NJ happy;
2013-07-03 wenzelm 2013-07-03 more print function parameters; check command_visible statically in assignment, instead of dynamically in execution;
2013-07-03 wenzelm 2013-07-03 tuned;
2013-07-03 wenzelm 2013-07-03 discontinued odd workaround for some old Poly/ML, which is still supported but of little practical relevance;
2013-07-03 wenzelm 2013-07-03 tuned;
2013-07-03 wenzelm 2013-07-03 allow multiple print functions;
2013-07-03 wenzelm 2013-07-03 tuned signature;
2013-07-03 wenzelm 2013-07-03 tuned signature;
2013-07-03 wenzelm 2013-07-03 tuned;
2013-02-27 wenzelm 2013-02-27 discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;
2013-02-27 wenzelm 2013-02-27 discontinued obsolete 'uses' within theory header;
2013-02-24 wenzelm 2013-02-24 simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored; eliminated separate Outer_Syntax.read_element;
2013-01-13 wenzelm 2013-01-13 more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;
2012-11-25 wenzelm 2012-11-25 Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
2012-10-18 wenzelm 2012-10-18 more official Future.terminate; tuned signature;
2012-09-05 wenzelm 2012-09-05 eliminated potentially confusing terminology of Scala "layer";
2012-09-02 wenzelm 2012-09-02 maintain stable state of node entries from last round -- bypass slightly different Thm.join_theory_proofs;
2012-09-01 wenzelm 2012-09-01 central management of forked goals wrt. transaction id; clarified stable_exec_id: consider ragular failure as stable; more robust counting of forked proofs, with global reset after cancellation due to document editing;
2012-08-30 wenzelm 2012-08-30 refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390); stretched meaning of Goal.parallel_proofs to enable future_terminal_proofs in interactive document model, despite its lack for regular forking of proofs;
2012-08-30 wenzelm 2012-08-30 some support for registering forked proofs within Proof.state, using its bottom context; tuned signature;
2012-08-30 wenzelm 2012-08-30 tuned signature;
2012-08-26 wenzelm 2012-08-26 theory def/ref position reports, which enable hyperlinks etc.; more official header command parsing;
2012-08-24 wenzelm 2012-08-24 check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);