src/Pure/Thy/thy_syntax.scala
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;
2012-08-09 wenzelm 2012-08-09 more direct Linear_Set.reverse, swapping orientation of the graph; tuned;
2012-08-07 wenzelm 2012-08-07 more structural parsing for minor modes; tuned signatures;
2012-08-07 wenzelm 2012-08-07 simplified Document.Node.Header -- internalized errors;
2012-08-07 wenzelm 2012-08-07 tuned signature;
2012-05-24 wenzelm 2012-05-24 reparse descendants after update of imports, e.g. required for 'primrec' (line 17 of "src/HOL/Power.thy");
2012-04-06 wenzelm 2012-04-06 discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;
2012-03-19 wenzelm 2012-03-19 clarified command span classification: strict Command.is_command, permissive Command.name;
2012-03-16 wenzelm 2012-03-16 more abstract heading level;
2012-03-15 wenzelm 2012-03-15 more explicit header_edits before main text_edits; handle reparses caused by syntax update;
2012-03-15 wenzelm 2012-03-15 basic support for outer syntax keywords in theory header;
2012-03-15 wenzelm 2012-03-15 maintain Version.syntax within document state; clarified Outer_Syntax.empty vs. Outer_Syntax.init, which pulls in Isabelle_System symbol completions;
2012-03-04 wenzelm 2012-03-04 clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2); simplified signatures;
2012-03-01 wenzelm 2012-03-01 proper update_header;
2012-02-29 wenzelm 2012-02-29 clarified module Thy_Load; more precise graph based on Document.Node.Deps with actual Node.Name dependencies;
2012-02-26 wenzelm 2012-02-26 more abstract class Document.Version; tuned (NB: Version.nodes is total);