src/Pure/Thy/thy_syntax.scala
2017-03-01 wenzelm 2017-03-01 improved performance of remove, e.g. relevant for Theories_Dockable.purge;
2017-01-09 wenzelm 2017-01-09 tuned signature;
2017-01-07 wenzelm 2017-01-07 obsolete;
2017-01-05 wenzelm 2017-01-05 misc tuning and clarification;
2016-09-14 wenzelm 2016-09-14 tuned;
2016-08-02 wenzelm 2016-08-02 tuned signature -- prover-independence is presently theoretical;
2016-08-02 wenzelm 2016-08-02 support 'abbrevs' within theory header; simplified 'keywords': no abbreviations here;
2015-05-03 wenzelm 2015-05-03 misc tuning, based on warnings by IntelliJ IDEA;
2015-04-24 wenzelm 2015-04-24 tuned;
2015-03-24 wenzelm 2015-03-24 proper comparison of blobs_info (amending illtyped equality from 86a76300137e) -- avoid redundant update of unchanged commands;
2015-03-15 wenzelm 2015-03-15 clarified span position;
2015-03-15 wenzelm 2015-03-15 tuned;
2015-03-15 wenzelm 2015-03-15 tuned;
2015-03-15 wenzelm 2015-03-15 hybrid use of command blobs: inlined errors and auxiliary files; static check of theory imports;
2015-03-15 wenzelm 2015-03-15 tuned;
2015-03-14 wenzelm 2015-03-14 clarified positions 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-12 wenzelm 2015-03-12 clarified command content;
2015-01-15 wenzelm 2015-01-15 proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);
2015-01-08 wenzelm 2015-01-08 tuned;
2014-12-03 wenzelm 2014-12-03 node-specific keywords, with session base syntax as default;
2014-12-02 wenzelm 2014-12-02 node-specific syntax, with base_syntax as default; clarified Document_Model.init: convergence of editor events towards buffer-specific token marker;
2014-08-12 wenzelm 2014-08-12 tuned signature;
2014-08-12 wenzelm 2014-08-12 separate module Command_Span: mostly syntactic representation; potentially prover-specific Output_Syntax.parse_spans;
2014-08-11 wenzelm 2014-08-11 tuned signature;
2014-08-11 wenzelm 2014-08-11 tuned output, in accordance to transaction name in ML;
2014-08-11 wenzelm 2014-08-11 more explicit type Span in Scala, according to ML version;
2014-08-11 wenzelm 2014-08-11 clarified modules;
2014-08-02 wenzelm 2014-08-02 more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);
2014-07-23 wenzelm 2014-07-23 more frugal edits;
2014-04-08 wenzelm 2014-04-08 simplified Text.Chunk -- eliminated ooddities; afford strict symbol_index, which is usually empty anyway;
2014-04-03 wenzelm 2014-04-03 clarified Version.syntax -- avoid guessing initial situation;
2014-04-03 wenzelm 2014-04-03 more abstract Prover.Syntax, as proposed by Carst Tankink;
2014-04-02 wenzelm 2014-04-02 tuned signature -- more explicit iterator terminology;
2014-04-02 wenzelm 2014-04-02 more explicit iterator terminology, in accordance to Scala 2.8 library; clarified Graph.keys_iterator vs. Graph.keys, with subtle change of semantics; tuned output;
2014-03-31 wenzelm 2014-03-31 tuned signature -- more static typing;
2014-03-31 wenzelm 2014-03-31 store blob content within document node: aux. files that were once open are made persistent; proper structural equality for Command.File and Symbol.Index;
2014-03-29 wenzelm 2014-03-29 propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save); tuned signature;
2014-03-29 wenzelm 2014-03-29 tuned signature;
2014-03-29 wenzelm 2014-03-29 tuned signature;
2014-03-18 wenzelm 2014-03-18 clarifed module name;
2014-02-27 wenzelm 2014-02-27 reparse only for actually changed blobs; tuned signature;
2014-02-27 wenzelm 2014-02-27 more formal Document.Blobs; removed junk;
2014-02-27 wenzelm 2014-02-27 tuned;
2014-02-12 wenzelm 2014-02-12 maintain blob edits within history, which is important for Snapshot.convert/revert;
2014-02-11 wenzelm 2014-02-11 common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content); more informative type Blob, to allow markup reports;
2014-01-25 wenzelm 2014-01-25 propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;
2014-01-22 wenzelm 2014-01-22 clarified approximative syntax of thy_load commands: first name after command keyword, after cleaning wrt. tags and cmts;
2013-11-22 wenzelm 2013-11-22 clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;
2013-11-19 wenzelm 2013-11-19 more explicit indication of missing files;
2013-11-19 wenzelm 2013-11-19 clarified Document.Blobs environment vs. actual edits of auxiliary files; more robust handling of vacuous edits;
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 always reparse nodes with thy_load commands, to update inlined files;
2013-11-19 wenzelm 2013-11-19 proper Thy_Load.append of auxiliary file names; inlined errors;
2013-11-19 wenzelm 2013-11-19 clarified boundary cases of Document.Node.Name;
2013-11-18 wenzelm 2013-11-18 inline blobs into command, via SHA1 digest; broadcast all blobs within edit, without storing the result;
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-11-17 wenzelm 2013-11-17 explicit indication of thy_load commands;
2013-09-24 wenzelm 2013-09-24 clarified command spans (again, see also 03a2dc9e0624): restrict to proper range to allow Isabelle.command_edit adding material monotonically without destroying the command (e.g. relevant for sendback from sledgehammer); simplified command padding: always newline, despite lack of indentation;
2013-08-07 wenzelm 2013-08-07 maintain commands together with index -- avoid redundant reconstruction of full_index;