src/Pure/PIDE/document.ML
2014-07-24 wenzelm 2014-07-24 less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;
2014-07-23 wenzelm 2014-07-23 avoid redundant data structure;
2014-07-23 wenzelm 2014-07-23 more explicit discrimination of empty nodes -- suppress from Theories panel;
2014-04-30 wenzelm 2014-04-30 some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
2014-04-07 wenzelm 2014-04-07 simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name; more liberal hyperlink to files, allow hyperlinks within editor files independently of the (POSIX) file-system;
2014-04-07 wenzelm 2014-04-07 separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
2014-03-18 wenzelm 2014-03-18 clarifed module name;
2014-02-28 wenzelm 2014-02-28 tuned comment;
2014-02-28 wenzelm 2014-02-28 tuned signature;
2014-02-27 wenzelm 2014-02-27 store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing; integrity check of SHA1 digests produced in Scala vs. ML; tuned signature;
2013-11-22 wenzelm 2013-11-22 clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
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 Command.read;
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;