clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;

tuned signature;

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

clarified: consolidated result is last command;

more node status information;

clarified signature: Known.theories retains Document.Node.Entry (with header);

more robust: self-export only;

store exports within PIDE command state;
Markup.Export.unapply: proper NAME;

tuned;

update XML cache for slightly modified messages;

more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);

discontinued old form of marginal comments;

clarified signature;

completion supports theory header imports;
tuned;

maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);

tuned signature;

tuned signature;

provide session qualifier via resources;

tuned signature;

support to encode/decode command state;
support to merge full contents of command state;

more uniform node_header (non-strict);
removed dead code;

tuned signature;

tuned signature;

suppress empty results;

more uniform path syntax, as in ML (see 5a7c919a4ada);

tuned signature -- prover-independence is presently theoretical;

eliminated "xname" and variants;

clarified syntax;

symbolic syntax "\<comment> text";

straight-forward refresh, without special preconditions;
eliminated somewhat expensive eq_content;

resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;

more general notion of command span: command keyword not necessarily at start;
support for special 'private' prefix for local_theory commands;
clarified parse_spans, with related operations for document Thy_Output and editor Token_Markup;

misc tuning and simplification;

avoid duplicate header errors, more precise positions;
tuned signature;

clarified modules;

more markup, which helps to create missing imports;

proper command id for inlined errors, which is important for Command.State.accumulate;

clarified span position;

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

tuned;

value-oriented user error, for well-defined Thy_Syntax.chop_common;

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

clarified command content;

explicit message channel for "legacy", which is nonetheless a variant of "warning";

tuned signature;

misc tuning, based on warnings by IntelliJ IDEA;

tuned;

clarified Position.Identified: do not require range from prover, default to command position;

maintain Command_Range position as in ML;

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;

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

more explicit discrimination of empty nodes -- suppress from Theories panel;

more systematic Isabelle output, like in classic Isabelle/ML (without markup);

tuned signature;

tuned signature;

ignore other_id reports for now (see 8eda56033203): massive amounts of redirections to 'class' etc. makes it difficult to edit main HOL;
silently ignore excessive reports -- no ambition to detect that situation accurately;

tuned;

expose more bad cases;

tuned signature;

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

accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);

avoid data redundancy;

tuned signature -- moved Command.Chunk to Text.Chunk;

more uniform Command.Chunk operations;

more explicit Command.Chunk types, less ooddities;
tuned;

more direct warning within persistent Protocol.Status;
consider Markup.ERROR (e.g. from Output.error_message without exception) as failure;
tuned;

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;

persistent protocol_status, to improve performance of node_status a little;

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

more frugal merge of markup trees: filter wrt. subsequent query;

more careful treatment of multiple command states (eval + prints): merge content that is actually required;
more standard Markup_Tree merge, including trivial cases;

clarified valid_id: always standardize towards static command.id;

tuned signature -- emphasize symbol positions (prover) vs. decoded text offsets (editor);

incorporate chunk range that is 1 off end-of-input, for improved error positions (NB: command spans are tight, without trailing whitespace);
tuned signature;

reparse only for actually changed blobs;
tuned signature;

tuned output;

tuned signature;

more general / abstract Command.Markups, with separate index for status elements;
slightly faster Rendering.overview_color;

tuned signature -- avoid obscure default arguments;

clarified markup cumulation order (see also 25306d92f4ad and 0009a6ebc83b), e.g. relevant for completion_context;

tuned imports;

more uniform/robust restriction of reported positions, e.g. relevant for "bad" markup due to unclosed comment in ML file;

more accurate eq_content;

clarified message_positions: cover alt_id as well;
tuned;

maintain multiple command chunks and markup trees: for main chunk and loaded files;
document view for all text areas, including auxiliary files;

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

tuned signature;

report (but ignore) markup within auxiliary files;

ranges of thy_load commands count as visible within perspective;
convert ranges wrt. snapshot -- relevant for outdated situation;

more explicit indication of missing files;

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

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

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

explicit indication of thy_load commands;

retain original messages properties, e.g. for retrieval via Command.Results;

maintain overlays within node perspective;
tuned signature;

full merge of Command.State, which enables Command.prints to augment markup as well (assuming that these dynamic overlays are relatively few);

tuned signature;
tuned comments;

tuned signature -- eliminated pointless type synonym;

tuned signature;

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

separate exec_id assignment for Command.print states, without affecting result of eval;
tuned signature;
tuned;

tuned;

tuned signature;

tuned signature;

retain original tooltip range, to avoid repeated window popup when the mouse is moved over the same content;

structural equality for Command.Results;
more general Command.State.eq_content;

clarified notion of Command.proper_range (according to Token.is_proper), especially relevant for Active.try_replace_command, to avoid loosing subsequent comments accidentally;
reverted f3588e59aeaa accordingly;

tuned;

tuned implementation according to Library.insert/merge in ML;

more formal class Command.Results;

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;

identify dialogs via official serial and maintain as result message;
clarified Protocol.is_inlined: suppress result/tracing/state messages uniformly;
cumulate_markup/select_markup depending on command state;
explicit Rendering.output_messages;
tuned source structure;

rendering of selected dialog_result as active_result_color, depending on dynamic command status in output panel, but not static popups etc.;

Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;

more abstract Sendback operations, with explicit id/exec_id properties;
purge result messages (again), cf. db58490a68ac, 7b61a539721e;

always retain message positions, in order to allow Isabelle_Rendering.sendback retrieve the exec_id, even in tooltip or detached window;

tuned signature;

operations to turn markup into XML;
tuned;

accumulate under exec_id as well;

more restrictive pattern, to avoid malformed positions intruding the command range (cf. d7a1973b063c);

more realistic sendback: pick exec_id from message position and text from buffer;

tuned signature;

earlier treatment of embedded report/no_report messages (see also 4110cc1b8f9f);

more explicit message markup and rendering;

some actual rich text markup via XML.content_markup;
tuned signature;

some support for inital command markup;
tuned signature;

refined output panel: more value-oriented approach to update and caret focus;

more markup for failed goal forks, reusing "bad";

more precise counting of line/column;

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

tuned signature;

more structural parsing for minor modes;
tuned signatures;

tuned signature;

include trailing comments in proper_command range;

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

clarified command state -- markup within proper_range, excluding trailing whitespace;

added Command.proper_range (still unused);

prefer final ADTs -- prevent ooddities;

tuned;

accumulate status as regular markup for command range;
tuned signature;

clarified modules (again) -- NB: both Document and Protocol are specific to this particular prover;

--HG--
rename : src/Pure/PIDE/isabelle_document.ML => src/Pure/PIDE/protocol.ML
rename : src/Pure/PIDE/isabelle_document.scala => src/Pure/PIDE/protocol.scala

clarified modules;

--HG--
rename : src/Pure/PIDE/isar_document.ML => src/Pure/PIDE/isabelle_document.ML
rename : src/Pure/PIDE/isar_document.scala => src/Pure/PIDE/isabelle_document.scala

separate module for concrete Isabelle markup;

--HG--
rename : src/Pure/General/markup.ML => src/Pure/General/isabelle_markup.ML
rename : src/Pure/General/markup.scala => src/Pure/General/isabelle_markup.scala

sharing of token source with span source;

prefer statically typed Text.Markup;

Document.Node.Name convenience;

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;

propagate editor perspective through document model;

some support for editor perspective;

tuned signature;

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

explicit import java.lang.System to prevent odd scope problems;

avoid spam;

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

Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;

allow embedded reports in regular prover messages, to avoid side-effects for errors for example;

Command.State.accumulate: check actual source range;

Isar_Document.reported_positions: slightly more robust treatment of positions outside the command range, notably parsing beyond EOF;

Command.State: add reported positions to markup tree, according main message position or Markup.binding/entity/report occurrences in body;
Position.Id_Range convenience;

Command.newlines: account for physical newlines;

Command.results: ordered by serial number;

tuned;

organized markup properties via apply/unapply patterns;

more precise Command.State accumulation;

tuned root markup;

tuned;

simplified Command.status again, reverting most of e5eed57913d0 (note that more complex information can be represented with full markup reports);

tuned signature;

renamed Markup_Tree.Node to Text.Info;
Markup_Tree.select: body may depend on full Text.Info, including range;
tuned;

Isabelle_Hyperlinks: select relevant information directly from Markup_Tree, without intermediate RefInfo;

Document_View.text_area_extension: select relevant information directly from Markup_Tree, without intermediate TypeInfo;

Command.State: accumulate markup reports uniformly;
Document_Model.token_marker: select relevant information directly from Markup_Tree, without intermediate HighlightInfo;
tuned;

parameterized type Markup_Tree.Node;
Markup_Tree.select: allow arbitrary interpretations, not just filtering;
renamed Text.Range.intersect to Text.Range.restrict -- emphasize that it is not directly related to contains/overlaps;

Command.status: full XML.Tree, i.e. Markup with potential "arguments";

more efficient Markup_Tree, based on branches sorted by quasi-order;
renamed markup_node.scala to markup_tree.scala and classes/objects accordingly;
Position.Range: produce actual Text.Range;
Symbol.Index.decode: convert 1-based Isabelle offsets here;
added static Command.range;
simplified Command.markup;
Document_Model.token_marker: flatten markup at most once;
tuned;

--HG--
rename : src/Pure/PIDE/markup_node.scala => src/Pure/PIDE/markup_tree.scala

decode Isabelle symbol positions in one spot;

simplified command status: interpret stacked markup on demand;

some derived operations on Text.Range;

specific types Text.Offset and Text.Range;
minor tuning;

Snapshot.state: fall back on Command.empty_state -- looked-up command might be unavailable due to editing divergence;

tuned;

explicit Document.State value, instead of individual state variables in Session, Command, Document;
Session.snapshot: pure value based on Document.State;
Document.edit_texts: no treatment of state assignment here;

more basic notion of unparsed input;

clarified "state" (accumulated data) vs. "exec" (execution that produces data);
generic type Document.id (ML) / Document.ID;

misc tuning and simplification;

specific command state;

specific Session.Commands_Changed;

represent document ids by (long) int, to benefit from the somewhat faster Inttab in ML (LinearSet in Scala is invariably indexed by native object ids);

avoid null in Scala;
tuned comments;

simplified/refined document model: collection of named nodes, without proper dependencies yet;
moved basic type definitions for ids and edits from Isar_Document to Document;
removed begin_document/end_document for now -- nodes emerge via edits;
edits refer to named nodes explicitly;

tuned Command.toString -- preserving uniqueness allows the Scala toplevel to print Linear_Set[Command] results without crashing;

more detailed token markup, including command kind as sub_kind;
type-safe access to Command.HighlightInfo;

tuned messages;

accumulate only local results -- no proper history support yet;

Command.toString: include id for debugging;
Command.consume: explicit forward, avoid dependency on Session and side-effect on event bus;
State.+ without side-effect on event bus;
Session.commands_changed: delayed command changes (outside of Swing thread), also subsumes former Session.results;
Document_View: tuned commands_changed handling and caret listening;
Document_View.selected_command: proper function, not event handler state;
Output_Dockable: directly act upon commands_changed, not caret events (via former Session.results);

explicit Command.Status.UNDEFINED -- avoid fragile/cumbersome treatment of Option[State];

some rearrangement of Scala sources;

--HG--
rename : src/Pure/Thy/change.scala => src/Pure/PIDE/change.scala
rename : src/Pure/Thy/command.scala => src/Pure/PIDE/command.scala
rename : src/Pure/Thy/document.scala => src/Pure/PIDE/document.scala
rename : src/Pure/General/event_bus.scala => src/Pure/PIDE/event_bus.scala
rename : src/Pure/Thy/markup_node.scala => src/Pure/PIDE/markup_node.scala
rename : src/Pure/Thy/state.scala => src/Pure/PIDE/state.scala
rename : src/Pure/Thy/text_edit.scala => src/Pure/PIDE/text_edit.scala
rename : src/Pure/General/download.scala => src/Pure/System/download.scala
rename : src/Pure/General/swing_thread.scala => src/Pure/System/swing_thread.scala