2013-11-22 wenzelm 2013-11-22 more total master_directory -- NB: this is used outside command transactions (see also 92961f196d9e);
2013-11-20 wenzelm 2013-11-20 load files that are not provided by PIDE blobs; uniform resolve_files via;
2013-11-19 wenzelm 2013-11-19 maintain blobs within document state: digest + text in ML, digest-only in Scala; resolve files for command span, based on defined blobs; tuned;
2013-11-19 wenzelm 2013-11-19 proper theory name vs. node name;
2013-11-18 wenzelm 2013-11-18 maintain document model for all files, with document view for theory only, and special blob for non-theory files;
2013-08-05 wenzelm 2013-08-05 tuned signature -- more uniform treatment of overlays as command mapping;
2013-08-02 wenzelm 2013-08-02 support print functions with explicit arguments, as provided by overlays;
2013-08-02 wenzelm 2013-08-02 maintain overlays within node perspective; tuned signature;
2013-07-31 wenzelm 2013-07-31 simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;
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;