src/Pure/PIDE/document.ML
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;
2012-04-10 ago tuned future priorities: print 0, goal ~1, execute ~2;
2012-04-09 ago more explicit last exec result;
2012-04-09 ago dynamic propagation of node "updated" status, which is required to propagate edits and re-assigments and allow direct memo_result;
2012-04-09 ago tuned;
2012-04-09 ago simplified Future.cancel/cancel_group (again) -- running threads only;
2012-04-07 ago added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
2012-04-07 ago explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
2012-04-06 ago discontinued obsolete last_execs (cf. cd3ab7625519);
2012-04-06 ago stop node execution at first unassigned exec;
2012-04-06 ago discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;
2012-04-05 ago more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
2012-04-05 ago less ambitious memo_eval, since memo_result is still not robust here;
2012-04-05 ago less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
2012-04-05 ago more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
2012-04-05 ago Command.memo including physical interrupts (unlike Lazy.lazy);
2012-04-05 ago tuned;
2012-04-04 ago tuned -- NB: get_theory still needs to apply Lazy.force due to interrupt instabilities;
2012-04-04 ago separate module for prover command execution;
2012-04-04 ago tuned;
2012-03-20 ago minimalistic support for remote URLs: no master dir here;
2012-03-16 ago define keywords early when processing the theory header, before running the body commands;
2012-03-15 ago declare command keywords via theory header, including strict checking outside Pure;
2012-03-15 ago declare keywords as side-effect of header edit;
2012-03-15 ago some support for outer syntax keyword declarations within theory header;
2012-03-13 ago clarified command state -- markup within proper_range, excluding trailing whitespace;
2012-03-12 ago refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);
2012-03-01 ago clarified document nodes (full import graph) vs. node_status (non-preloaded theories);
2011-11-29 ago clarified Time vs. Timing;
2011-11-28 ago separate module for concrete Isabelle markup;
2011-09-18 ago explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
2011-09-07 ago no print_state for final proof commands, which return to theory state;
2011-09-03 ago discontinued predefined empty command (obsolete!?);
2011-09-03 ago discontinued global execs: store exec value directly within entries;
2011-09-03 ago Document.remove_versions on ML side;
2011-09-02 ago less agressive parsing of commands (priority ~1);
2011-09-02 ago more precise iterate_entries_after if start refers to last entry;
2011-09-02 ago clarified define_command: store name as structural information;
2011-09-01 ago amended last_common, if that happens to the very last entry (important to load HOL/Auth, for example);
2011-09-01 ago more careful treatment of interrupts, to retain them within forked/joined boundary of command transactions;
2011-08-31 ago explicit running_color;