src/Pure/PIDE/document.ML
13 months ago wenzelm 2018-05-14 support for dynamic document output while editing;
17 months ago wenzelm 2018-01-24 tuned: prefer list operations over Source.source; approximative parsing of theory header;
17 months ago wenzelm 2018-01-08 clarified implicit Pure.thy;
18 months ago wenzelm 2017-12-16 PIDE markup for session ROOT files;
22 months ago wenzelm 2017-08-08 maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
22 months ago wenzelm 2017-08-07 tuned spelling;
22 months ago wenzelm 2017-08-07 tuned;
2017-06-22 wenzelm 2017-06-22 more informative task_statistics;
2017-04-08 wenzelm 2017-04-08 more qualifier treatment, but in the end it is still ignored;
2017-04-03 wenzelm 2017-04-03 simplified direct theory name (again, see also 570ba266f5b5, 2a7f9e79cb28);
2016-04-19 wenzelm 2016-04-19 more IDE support for Isabelle/Pure bootstrap;
2016-04-09 wenzelm 2016-04-09 support ROOT0.ML as well -- independently of ROOT.ML;
2016-04-06 wenzelm 2016-04-06 treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
2016-04-02 wenzelm 2016-04-02 prefer infix operations;
2016-03-03 wenzelm 2016-03-03 clarified modules; tuned signature;
2015-09-01 wenzelm 2015-09-01 thread context for exceptions from forks, e.g. relevant when printing errors; tuned signature;
2015-08-15 wenzelm 2015-08-15 clarified context;
2015-08-10 wenzelm 2015-08-10 set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;
2015-04-24 wenzelm 2015-04-24 always traverse required nodes, e.g. relevant for inlined errors of imported theory header;
2015-04-12 wenzelm 2015-04-12 clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;
2015-04-06 wenzelm 2015-04-06 more position information and PIDE markup for command keywords;
2015-03-17 wenzelm 2015-03-17 misc tuning and simplification;
2015-03-16 wenzelm 2015-03-16 more precises positions; more permissive imports;
2015-03-16 wenzelm 2015-03-16 avoid duplicate header errors, more precise positions; tuned signature;
2015-03-15 wenzelm 2015-03-15 hybrid use of command blobs: inlined errors and auxiliary files; static check of theory imports;
2015-03-13 wenzelm 2015-03-13 simplified Command.resolve_files in ML, using blobs_index from Scala; clarified modules;
2015-03-13 wenzelm 2015-03-13 tuned;
2015-03-12 wenzelm 2015-03-12 clarified markup for embedded files, early before execution;
2015-01-11 wenzelm 2015-01-11 more explicit errors;
2014-12-29 wenzelm 2014-12-29 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 wenzelm 2014-12-28 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); clarified Command.run_process etc.: join running eval, bypass running print; eliminated Command.memo in favour of regular Lazy.lazy; more Lazy.lazy status information;
2014-12-03 wenzelm 2014-12-03 node-specific keywords, with session base syntax as default;
2014-12-03 wenzelm 2014-12-03 clarified define_command: send tokens more directly, without requiring keywords in ML;
2014-12-03 wenzelm 2014-12-03 tuned signature;
2014-11-26 wenzelm 2014-11-26 even more exception traces for Document.update, which goes through additional execution wrappers;
2014-11-07 wenzelm 2014-11-07 prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors; tuned message;
2014-11-07 wenzelm 2014-11-07 plain value Keywords.keywords, which might be used outside theory for bootstrap purposes; plain value Outer_Syntax within theory: parsing requires current theory context; clarified name of Keyword.is_literal according to its semantics; eliminated pointless type Keyword.T; simplified @{command_spec}; clarified bootstrap keywords and syntax: take it as basis instead of side-branch;
2014-11-06 wenzelm 2014-11-06 more explicit Keyword.keywords;
2014-11-06 wenzelm 2014-11-06 simplified keyword kinds; more explicit bootstrap syntax;
2014-11-05 wenzelm 2014-11-05 explicit type Keyword.keywords; tuned signature;
2014-08-12 wenzelm 2014-08-12 tuned signature according to Scala version -- prefer explicit argument;
2014-08-12 wenzelm 2014-08-12 separate module Command_Span: mostly syntactic representation; potentially prover-specific Output_Syntax.parse_spans;
2014-08-09 wenzelm 2014-08-09 tuned comments;
2014-07-24 wenzelm 2014-07-24 make SML/NJ happy;
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;