src/Pure/PIDE/document.ML
2014-11-06 ago more explicit Keyword.keywords;
2014-11-06 ago simplified keyword kinds;
2014-11-05 ago explicit type Keyword.keywords;
2014-08-12 ago tuned signature according to Scala version -- prefer explicit argument;
2014-08-12 ago separate module Command_Span: mostly syntactic representation;
2014-08-09 ago tuned comments;
2014-07-24 ago make SML/NJ happy;
2014-07-24 ago 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 ago avoid redundant data structure;
2014-07-23 ago more explicit discrimination of empty nodes -- suppress from Theories panel;
2014-04-30 ago some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;
2014-04-07 ago simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
2014-04-07 ago separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;
2014-03-18 ago clarifed module name;
2014-02-28 ago tuned comment;
2014-02-28 ago tuned signature;
2014-02-27 ago store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
2013-11-22 ago clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
2013-11-22 ago more total master_directory -- NB: this is used outside command transactions (see also 92961f196d9e);
2013-11-20 ago load files that are not provided by PIDE blobs;
2013-11-19 ago maintain blobs within document state: digest + text in ML, digest-only in Scala;
2013-11-19 ago proper theory name vs. node name;
2013-11-18 ago maintain document model for all files, with document view for theory only, and special blob for non-theory files;
2013-08-05 ago tuned signature -- more uniform treatment of overlays as command mapping;
2013-08-02 ago support print functions with explicit arguments, as provided by overlays;
2013-08-02 ago maintain overlays within node perspective;
2013-07-31 ago simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;
2013-07-31 ago allow explicit indication of required node: full eval, no prints;
2013-07-30 ago recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;
2013-07-30 ago more timing;
2013-07-30 ago more timing;
2013-07-30 ago de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;
2013-07-29 ago traverse node on change of "required" state;
2013-07-29 ago keep memo_exec execution running, which is important to cancel goal forks eventually;
2013-07-29 ago maintain explicit execution frontier: avoid conflict with former task via static dependency;
2013-07-29 ago clarified conditions for node traversal;
2013-07-29 ago tuned;
2013-07-29 ago discontinued notion of "stable" result -- running execution is never canceled;
2013-07-20 ago document update at high priority -- important;
2013-07-20 ago option editor_execution_priority;
2013-07-15 ago more careful termination of removed execs, leaving running execs undisturbed;
2013-07-12 ago clarified execution: maintain running execs only, check "stable" separately via memo (again);
2013-07-12 ago tuned signature;
2013-07-12 ago clarified module name;
2013-07-11 ago more explicit type Exec.context;
2013-07-11 ago strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;
2013-07-11 ago more abstract types;
2013-07-11 ago tuned;
2013-07-11 ago global management of command execution fragments;
2013-07-11 ago fully synchronized guard of running execution;
2013-07-11 ago re-assign prints of unchanged eval only -- avoid crash of new_exec;
2013-07-11 ago tuned -- refrain from odd optimization;
2013-07-11 ago tuned;
2013-07-10 ago tuned start_execution: avoid sleep on worker thread;
2013-07-10 ago clarified Command.print: update old prints here;
2013-07-09 ago produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);
2013-07-09 ago more formal type assign_update: avoid duplicate results and redundant update of global State.execs;
2013-07-05 ago tuned signature;
2013-07-05 ago tuned signature;
2013-07-05 ago clarified type Command.eval;