discontinued pointless dump_checkpoint and share_common_data -- superseded by base logic image in Isabelle/MMT;

clarified signature: prefer operations without position;

support for share_common_data after define_command and before actual update: this affects string particles of command tokens;

tuned;

less wasteful consolidation, based on PIDE front-end state and recent changes;

Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
tuned;

even more robust syntax (amending 122df1fde073);

clarified node_syntax (amending ae38b8c0fdd9): default to overall_syntax, e.g. relevant for command spans wrt. bad header;

more accurate node_syntax: avoid overall_syntax for PIDE edits;

tuned signature;

more informative loaded_theories: dependencies and syntax;

tuned signature;

tuned signature;

tuned signature;

improved performance of remove, e.g. relevant for Theories_Dockable.purge;

tuned signature;

obsolete;

misc tuning and clarification;

tuned;

tuned signature -- prover-independence is presently theoretical;

support 'abbrevs' within theory header;
simplified 'keywords': no abbreviations here;

proper comparison of blobs_info (amending illtyped equality from 86a76300137e) -- avoid redundant update of unchanged commands;

clarified span position;

tuned;

tuned;

hybrid use of command blobs: inlined errors and auxiliary files;
static check of theory imports;

tuned;

clarified positions of theory imports;

simplified Command.resolve_files in ML, using blobs_index from Scala;
clarified modules;

clarified command content;

proper update of perspective after implicit edit due to reparse (e.g. ~~/src/HOL/Nat.thy);

tuned;

node-specific keywords, with session base syntax as default;

node-specific syntax, with base_syntax as default;
clarified Document_Model.init: convergence of editor events towards buffer-specific token marker;

misc tuning, based on warnings by IntelliJ IDEA;

tuned;

tuned signature;

separate module Command_Span: mostly syntactic representation;
potentially prover-specific Output_Syntax.parse_spans;

tuned signature;

tuned output, in accordance to transaction name in ML;

more explicit type Span in Scala, according to ML version;

clarified modules;

more direct access to persistent blobs (see also 8953d4cc060a), avoiding fragile digest lookup from later version (which might have removed unused blobs already);

more frugal edits;

simplified Text.Chunk -- eliminated ooddities;
afford strict symbol_index, which is usually empty anyway;

clarified Version.syntax -- avoid guessing initial situation;

more abstract Prover.Syntax, as proposed by Carst Tankink;

tuned signature -- more explicit iterator terminology;

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;

tuned signature -- more static typing;

store blob content within document node: aux. files that were once open are made persistent;
proper structural equality for Command.File and Symbol.Index;

propagate deps_changed, to resolve missing files without requiring jEdit events (e.g. buffer load/save);
tuned signature;

tuned signature;

tuned signature;

clarifed module name;

--HG--
rename : src/Pure/Thy/thy_load.ML => src/Pure/PIDE/resources.ML
rename : src/Pure/Thy/thy_load.scala => src/Pure/PIDE/resources.scala
rename : src/Tools/jEdit/src/jedit_thy_load.scala => src/Tools/jEdit/src/jedit_resources.scala

reparse only for actually changed blobs;
tuned signature;

more formal Document.Blobs;
removed junk;

tuned;

maintain blob edits within history, which is important for Snapshot.convert/revert;

common Command.Chunk for command source and auxiliary files (static Symbol.Index without actual String content);
more informative type Blob, to allow markup reports;

propagate update of outer syntax keywords: global propertiesChanged, buffer TokenMarker.markTokens, text area repainting;

clarified approximative syntax of thy_load commands: first name after command keyword, after cleaning wrt. tags and cmts;

clarified node edits sent to prover -- Clear/Blob only required for text edits within editor;

more explicit indication of missing files;

clarified Document.Blobs environment vs. actual edits of auxiliary files;
more robust handling of vacuous edits;

maintain blobs within document state: digest + text in ML, digest-only in Scala;
resolve files for command span, based on defined blobs;
tuned;

always reparse nodes with thy_load commands, to update inlined files;

proper Thy_Load.append of auxiliary file names;
inlined errors;

clarified boundary cases of Document.Node.Name;

inline blobs into command, via SHA1 digest;
broadcast all blobs within edit, without storing the result;

maintain document model for all files, with document view for theory only, and special blob for non-theory files;

explicit indication of thy_load commands;

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;

maintain commands together with index -- avoid redundant reconstruction of full_index;

commands with overlay remain visible, to avoid loosing printed output;

maintain overlays within node perspective;
tuned signature;

tuned signature;

allow explicit indication of required node: full eval, no prints;

tuned signature -- eliminated pointless type synonym;

explicit module Document_ID as source of globally unique identifiers across ML/Scala;

export some generally useful operations;

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;

Thy_Syntax.consolidate_spans is subject to editor_reparse_limit, for improved experience of unbalanced comments etc.;

some support for inital command markup;
tuned signature;

more direct cumulation of (sparse) keywords;
discontinued slightly odd patching of Pure keywords;
tuned signature;

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;

clarified undefined, unparsed, unfinished command spans;
common reparse_spans, diff_commands;
some support for consolidate_spans after change of perspective;

refined recover_spans: take visible range into account, reparse and trim results -- to improve editing experience wrt. unbalanced quotations etc.;
tuned signature;

tuned signature;

more direct Linear_Set.reverse, swapping orientation of the graph;
tuned;

more structural parsing for minor modes;
tuned signatures;

simplified Document.Node.Header -- internalized errors;

tuned signature;

reparse descendants after update of imports, e.g. required for 'primrec' (line 17 of "src/HOL/Power.thy");

discontinued Document.update_perspective side-entry (cf. 546adfa8a6fc) -- NB: re-assignment is always necessary due to non-monotonic cancel_execution;

clarified command span classification: strict Command.is_command, permissive Command.name;

more abstract heading level;

more explicit header_edits before main text_edits;
handle reparses caused by syntax update;

basic support for outer syntax keywords in theory header;

maintain Version.syntax within document state;
clarified Outer_Syntax.empty vs. Outer_Syntax.init, which pulls in Isabelle_System symbol completions;

clarified command span: include trailing whitespace/comments and thus reduce number of ignored spans with associated transactions and states (factor 2);
simplified signatures;

proper update_header;

clarified module Thy_Load;
more precise graph based on Document.Node.Deps with actual Node.Name dependencies;

more abstract class Document.Version;
tuned (NB: Version.nodes is total);

more abstract class Document.Node;

sharing of token source with span source;

more abstract Document.Node.Name;
tuned signature;

maintain name of *the* enclosing node as part of command -- avoid full document traversal;

slightly more abstract Command.Perspective;

slightly more abstract Text.Perspective;

clarified Document.Node.clear -- retain header (cf. ML version);

update_perspective without actual edits, bypassing the full state assignment protocol;
edit_nodes/Perspective: do not touch_descendants here;
propagate editor scroll events via update_perspective;
misc tuning;

tuned signature;

propagate editor perspective through document model;

provide node header via Scala layer;
clarified node edit Clear: retain header information;
run_command: node info via document model, error handling within transaction;
node names without ".thy" suffix, to coincide with traditional theory loader treatment;

clarified node header -- exclude master_dir;

maintain node header;
misc tuning and clarification;

clarified document model header: master_dir (native wrt. editor, potentially URL) and node_name (full canonical path);

uniform treatment of header edits as document edits;

explicit datatypes for document node edits;

propagate header changes to prover process;
simplified Document case classes;
Document.State.assignments: indexed by Version_ID;

some support for blobs (arbitrary text files) within document nodes;

explicit Document.Node.Header, with master_dir and thy_name;
imitate ML path operations more closely;

Document.no_id/new_id as in ML (new_id *could* be session-specific but it isn't right now);

explicit class Counter;

tuned signature;

tuned signature;

unified type Document.Edit;

replaced Document.Node_Text_Edit by Document.Text_Edit, with treatment of deleted nodes;
Document_Model.pending_edits: more robust treatment of init, including buffer reload event (jEdit 4.3.2 produces malformed remove/insert that lacks the last character);
tuned;

proper treatment of equal heading level;

some support for nested source structure, based on section headings;

text_edits/recover_spans: reparse at least until line boundary -- increases chance of recovery for bad ML text, for example;

tuned signatures;

moved Text_Edit to Text.Edit;
tuned;

--HG--
rename : src/Pure/PIDE/text_edit.scala => src/Pure/PIDE/text.scala

renamed create_id to new_id;

renamed class Document to Document.Version etc.;
renamed Change.prev to Change.previous, and Change.document to Change.current;
tuned;

moved Document.text_edits to Thy_Syntax;

tuned;

parse_spans: somewhat faster low-level implementation;

renamed class Outer_Lex to Token and Token_Kind to Token.Kind;

--HG--
rename : src/Pure/Isar/outer_lex.scala => src/Pure/Isar/token.scala

renamed Outer_Parse to Parse (in Scala);

--HG--
rename : src/Pure/Isar/outer_parse.scala => src/Pure/Isar/parse.scala

Outer_Lex.is_ignored;

plain object;

separate module Thy_Syntax for command span parsing;