src/Pure/PIDE/document.ML
2 months ago ago clarified signature;
2 months ago ago clarified Toplevel.state: more explicit types;
2 months ago ago physical vs. logical events, the latter takes GC time into account;
8 months ago ago clarified message;
8 months ago ago tuned;
10 months ago ago always consolidate: allow errors in presentation;
11 months ago ago less wasteful consolidation, based on PIDE front-end state and recent changes;
11 months ago ago tuned -- short-circuit result;
11 months ago ago proper function invocation with all arguments;
11 months ago ago fork parallel prints early in execution: avoid degradation of priority due to main eval task;
11 months ago ago record active execution task and depend on it -- avoid new executions bumping into old ones;
11 months ago ago clarified priority;
11 months ago ago Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
11 months ago ago more node status information;
12 months ago ago clarified "consolidation" vs. "presentation";
12 months ago ago support for dynamic document output while editing;
15 months ago ago tuned: prefer list operations over Source.source;
16 months ago ago clarified implicit Pure.thy;
17 months ago ago PIDE markup for session ROOT files;
21 months ago ago maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
21 months ago ago tuned spelling;
21 months ago ago tuned;
23 months ago ago more informative task_statistics;
2017-04-08 ago more qualifier treatment, but in the end it is still ignored;
2017-04-03 ago simplified direct theory name (again, see also 570ba266f5b5, 2a7f9e79cb28);
2016-04-19 ago more IDE support for Isabelle/Pure bootstrap;
2016-04-09 ago support ROOT0.ML as well -- independently of ROOT.ML;
2016-04-06 ago treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
2016-04-02 ago prefer infix operations;
2016-03-03 ago clarified modules;
2015-09-01 ago thread context for exceptions from forks, e.g. relevant when printing errors;
2015-08-15 ago clarified context;
2015-08-10 ago set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
2015-04-24 ago always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
2015-04-12 ago clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;
2015-04-06 ago more position information and PIDE markup for command keywords;
2015-03-17 ago misc tuning and simplification;
2015-03-16 ago more precises positions;
2015-03-16 ago avoid duplicate header errors, more precise positions;
2015-03-15 ago hybrid use of command blobs: inlined errors and auxiliary files;
2015-03-13 ago simplified Command.resolve_files in ML, using blobs_index from Scala;
2015-03-13 ago tuned;
2015-03-12 ago clarified markup for embedded files, early before execution;
2015-01-11 ago more explicit errors;
2014-12-29 ago clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;
2014-12-28 ago eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
2014-12-03 ago node-specific keywords, with session base syntax as default;
2014-12-03 ago clarified define_command: send tokens more directly, without requiring keywords in ML;
2014-12-03 ago tuned signature;
2014-11-26 ago even more exception traces for Document.update, which goes through additional execution wrappers;
2014-11-07 ago prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
2014-11-07 ago plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
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;