src/Pure/PIDE/document.ML
2012-04-10 wenzelm 2012-04-10 tuned future priorities: print 0, goal ~1, execute ~2;
2012-04-09 wenzelm 2012-04-09 more explicit last exec result;
2012-04-09 wenzelm 2012-04-09 dynamic propagation of node "updated" status, which is required to propagate edits and re-assigments and allow direct memo_result; discontinued odd "touched" field -- check given edits directly;
2012-04-09 wenzelm 2012-04-09 tuned;
2012-04-09 wenzelm 2012-04-09 simplified Future.cancel/cancel_group (again) -- running threads only; more robust update/cancel_execution: full join_tasks of group before exec state assignment; tuned signature;
2012-04-07 wenzelm 2012-04-07 added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);
2012-04-07 wenzelm 2012-04-07 explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions; tuned;
2012-04-06 wenzelm 2012-04-06 discontinued obsolete last_execs (cf. cd3ab7625519);
2012-04-06 wenzelm 2012-04-06 stop node execution at first unassigned exec;
2012-04-06 wenzelm 2012-04-06 discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;
2012-04-05 wenzelm 2012-04-05 more scalable execute/update: avoid redundant traversal of invisible/finished nodes; tuned;
2012-04-05 wenzelm 2012-04-05 less ambitious memo_eval, since memo_result is still not robust here;
2012-04-05 wenzelm 2012-04-05 less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;
2012-04-05 wenzelm 2012-04-05 more explicit memo_eval vs. memo_result, to enforce bottom-up execution; edit of perspective touches node superficially, to ensure revisit after update;
2012-04-05 wenzelm 2012-04-05 Command.memo including physical interrupts (unlike Lazy.lazy); re-assign unstable exec, i.e. reset interrupted transaction; node result as direct exec -- avoid potential interrupt instability of Lazy.map;
2012-04-05 wenzelm 2012-04-05 tuned;
2012-04-04 wenzelm 2012-04-04 tuned -- NB: get_theory still needs to apply Lazy.force due to interrupt instabilities;
2012-04-04 wenzelm 2012-04-04 separate module for prover command execution;
2012-04-04 wenzelm 2012-04-04 tuned;
2012-03-20 wenzelm 2012-03-20 minimalistic support for remote URLs: no master dir here;
2012-03-16 wenzelm 2012-03-16 define keywords early when processing the theory header, before running the body commands;
2012-03-15 wenzelm 2012-03-15 declare command keywords via theory header, including strict checking outside Pure;
2012-03-15 wenzelm 2012-03-15 declare keywords as side-effect of header edit; parse_command span is now lazy instead of future, to happen synchronously after header edit in new_exec (before execution);
2012-03-15 wenzelm 2012-03-15 some support for outer syntax keyword declarations within theory header; more uniform Thy_Header.header as argument for begin_theory etc.;
2012-03-13 wenzelm 2012-03-13 clarified command state -- markup within proper_range, excluding trailing whitespace;
2012-03-12 wenzelm 2012-03-12 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 wenzelm 2012-03-01 clarified document nodes (full import graph) vs. node_status (non-preloaded theories); tuned;
2011-11-29 wenzelm 2011-11-29 clarified Time vs. Timing;
2011-11-28 wenzelm 2011-11-28 separate module for concrete Isabelle markup;
2011-09-18 wenzelm 2011-09-18 explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;
2011-09-07 wenzelm 2011-09-07 no print_state for final proof commands, which return to theory state;
2011-09-03 wenzelm 2011-09-03 discontinued predefined empty command (obsolete!?);
2011-09-03 wenzelm 2011-09-03 discontinued global execs: store exec value directly within entries; simplified entries: no extra copy of command_id;
2011-09-03 wenzelm 2011-09-03 Document.remove_versions on ML side;
2011-09-02 wenzelm 2011-09-02 less agressive parsing of commands (priority ~1); join commands just before actual assignment;
2011-09-02 wenzelm 2011-09-02 more precise iterate_entries_after if start refers to last entry; do not assign exec states after bad theory init; reject illegal theory header after end of theory;
2011-09-02 wenzelm 2011-09-02 clarified define_command: store name as structural information;
2011-09-01 wenzelm 2011-09-01 amended last_common, if that happens to the very last entry (important to load HOL/Auth, for example); clarified touch_node: reset result explicitly;
2011-09-01 wenzelm 2011-09-01 more careful treatment of interrupts, to retain them within forked/joined boundary of command transactions;
2011-08-31 wenzelm 2011-08-31 explicit running_color; stronger colors for overview, more transparent colors for status within text;
2011-08-31 wenzelm 2011-08-31 tuned join_commands: avoid traversing cumulative table;
2011-08-27 wenzelm 2011-08-27 more precise treatment of nodes that are fully required for partially visible ones;
2011-08-26 wenzelm 2011-08-26 tuned signature -- iterate subsumes both fold and get_first;
2011-08-26 wenzelm 2011-08-26 further clarification of Document.updated, based on last_common and after_entry; tuned;
2011-08-26 wenzelm 2011-08-26 tuned signature;
2011-08-26 wenzelm 2011-08-26 improved Document.edit: more accurate update_start and no_execs; tuned;
2011-08-26 wenzelm 2011-08-26 refined document state assignment: observe perspective, more explicit assignment message; misc tuning and clarification;
2011-08-25 wenzelm 2011-08-25 tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;
2011-08-25 wenzelm 2011-08-25 propagate information about last command with exec state assignment through document model;
2011-08-24 wenzelm 2011-08-24 misc tuning and simplification;
2011-08-24 wenzelm 2011-08-24 tuned pri: prefer purging of canceled execution;
2011-08-24 wenzelm 2011-08-24 tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;
2011-08-24 wenzelm 2011-08-24 misc tuning and simplification;
2011-08-24 wenzelm 2011-08-24 ignore irrelevant timings;
2011-08-24 wenzelm 2011-08-24 print state only for visible command, to avoid wasting resources for the larger part of the text;
2011-08-24 wenzelm 2011-08-24 update_perspective without actual edits, bypassing the full state assignment protocol; edit_nodes/Perspective: do not touch_descendants here; propagate editor scroll events via update_perspective; misc tuning;
2011-08-23 wenzelm 2011-08-23 tuned;
2011-08-23 wenzelm 2011-08-23 some support for toplevel printing wrt. editor perspective (still inactive);
2011-08-23 wenzelm 2011-08-23 propagate editor perspective through document model;
2011-08-22 wenzelm 2011-08-22 some support for editor perspective;