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);
2012-08-11 wenzelm 2012-08-11 vacuous execution after first malformed command;
2012-08-10 wenzelm 2012-08-10 apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.; expand Clear edit before sending to prover; at most one full reparse of each node;
2012-07-27 wenzelm 2012-07-27 even more permissive approximation of master_dir, which is only required to access external resources ('uses' etc.);
2012-08-07 wenzelm 2012-08-07 simplified Document.Node.Header -- internalized errors;
2012-04-20 wenzelm 2012-04-20 improved interleaving of start_execution vs. cancel_execution of the next update;
2012-04-20 wenzelm 2012-04-20 always revisit nodes independently of "required" flag, which may change during editing -- avoid "bloodbath effect" when changing perspective while loading;
2012-04-20 wenzelm 2012-04-20 tuned;
2012-04-20 wenzelm 2012-04-20 builtin timing for main operations;
2012-04-11 wenzelm 2012-04-11 tuned;
2012-04-11 wenzelm 2012-04-11 just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update; explicit terminate_execution; tuned source structure;
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;
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;