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;
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;
2011-08-20 wenzelm 2011-08-20 refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;
2011-08-20 wenzelm 2011-08-20 added Future.joins convenience; clarified based on Future.cond_forks;
2011-08-19 wenzelm 2011-08-19 tuned;
2011-08-19 wenzelm 2011-08-19 tuned signature (again); tuned;
2011-08-19 wenzelm 2011-08-19 tuned signature -- treat structure Task_Queue as private to implementation;
2011-08-19 wenzelm 2011-08-19 refined Future.cancel: explicit future allows to join actual cancellation; Document.cancel_execution: join nested future groups as well;
2011-08-18 wenzelm 2011-08-18 more precise treatment of exception nesting and serial numbers;
2011-08-18 wenzelm 2011-08-18 more careful treatment of exception serial numbers, with propagation to message channel;
2011-08-17 wenzelm 2011-08-17 more systematic handling of parallel exceptions; distinguish exception concatanation EXCEPTIONS from parallel Par_Exn;
2011-08-16 wenzelm 2011-08-16 workaround for Cygwin, to make it work in the important special case without extra files;
2011-08-16 wenzelm 2011-08-16 more robust treatment of node dependencies in incremental edits;
2011-08-16 wenzelm 2011-08-16 use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable; more robust treatment of node dependencies; misc tuning;