src/Pure/Thy/thy_syntax.scala
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;
2013-08-07 wenzelm 2013-08-07 tuned signature;
2013-08-05 wenzelm 2013-08-05 commands with overlay remain visible, to avoid loosing printed output;
2013-08-02 wenzelm 2013-08-02 maintain overlays within node perspective; tuned signature;
2013-07-31 wenzelm 2013-07-31 allow explicit indication of required node: full eval, no prints;
2013-07-05 wenzelm 2013-07-05 tuned signature -- eliminated pointless type synonym;
2013-07-05 wenzelm 2013-07-05 explicit module Document_ID as source of globally unique identifiers across ML/Scala;
2013-01-06 wenzelm 2013-01-06 export some generally useful operations;
2012-12-13 wenzelm 2012-12-13 more careful handling of Dialog_Result, with active area and color feedback; more formal type Command.Results; propagate command results to output, which is required to resolve update of dialog state; clarified Markup.message: retain uninterpreted messages;
2012-09-22 wenzelm 2012-09-22 Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;
2012-09-18 wenzelm 2012-09-18 some support for inital command markup; tuned signature;
2012-08-21 wenzelm 2012-08-21 more direct cumulation of (sparse) keywords; discontinued slightly odd patching of Pure keywords; tuned signature;
2012-08-10 wenzelm 2012-08-10 apply all text edits to each node, before determining the resulting doc_edits -- allow several iterations to consolidate spans etc.; expand Clear edit before sending to prover; at most one full reparse of each node;
2012-08-10 wenzelm 2012-08-10 clarified undefined, unparsed, unfinished command spans; common reparse_spans, diff_commands; some support for consolidate_spans after change of perspective;
2012-08-09 wenzelm 2012-08-09 refined recover_spans: take visible range into account, reparse and trim results -- to improve editing experience wrt. unbalanced quotations etc.; tuned signature;
2012-08-09 wenzelm 2012-08-09 tuned signature;