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;

more node status information;

tuned signature;

clarified exported messages, e.g. suppress "information", "tracing";
export "legacy_feature" as "warning", in accordance to console default output;

tuned;

support for "use_theories";

treat sessions as entities with defining position;
tuned signature;

formal treatment of documentation names;

added document antiquotation @{session name};
renamed protocol function "Prover.session_base" to "Prover.init_session_base" according to the ML/Scala operation;

provide theory timing information, similar to command timing but always considered relevant;

more informative loaded_theories: dependencies and syntax;

session-qualified theory names are mandatory;

proper standard_path to revert platform_path in JEdit_Sessions.session_base;

more explicit failure;

explicit indication of consolidated nodes;

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

eliminated default_qualifier: just a constant;

clarified loaded_theories: map to qualified theory name;
proper theory_name for PIDE editors;

global session_base for PIDE interaction;

more qualifier treatment, but in the end it is still ignored;

tuned signature;

more explicit types;

clarified YXML vs. symbol encoding: operate on whole message;
tuned signature;

more realistic PIDE build session;

tuned;

clarified modules;

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

tuned signature: more uniform Keyword.spec;

more explicit HTML.symbols;
tuned signature;

output HTML text according to Isabelle/Scala Symbol.Interpretation;

clarified modules, like ML version;

tuned signature;
more rendering;

more thorough Encode.string;

misc tuning and simplification;

tuned protocol -- resolve command positions in ML;

clarified modules;

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

clarified positions of theory imports;

clarified markup for embedded files, early before execution;

more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML;

clarified build_theories;

some support for PIDE batch session;
clarified Thy_Info.use_thys_options and corresponding protocol command;

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

explicit message channels for "state", "information";
separate state_message_color;

clarified define_command: send tokens more directly, without requiring keywords in ML;

default command position is only valid for default text chunk (amending dcb758188aa6);

generic process wrapping in Prover;
clarified module arrangement;

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

proper priority for error over warning also for node_status (see 9c5220e05e04);

some support for session-qualified theories: allow to refer to resources via qualified name instead of odd file-system path;

tuned signature;

tuned signature;

added protocol command "use_theories", with core functionality of batch build;

more explicit message discrimination;

more direct interpretation of "warned" status, like "failed" and independently of "finished", e.g. relevant for Rendering.overview_color of aux. files where main command status is unavailable (amending 0546e036d1c0);

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 explicit Command.Chunk types, less ooddities;
tuned;

simplified blob again (amending 1e77ed11f2f7): only store file node name, i.e. the raw editor file name;
more liberal hyperlink to files, allow hyperlinks within editor files independently of the (POSIX) file-system;

support for URL as file name, similar to treatment in jEdit.java;

separate file_node vs. file_path, e.g. relevant on Windows for hyperlink to the latter;

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

more general prover operations;

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;

tuned for-comprehensions -- less structure mapping;

some rephrasing to ensure that this becomes cheap "foreach" and not expensive "map" (cf. 0fc032898b05);

unused;

more frugal command_status, which is often used in a tight loop;

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

back to cumulative treatment of command status, which is important for total accounting (amending 8201790fdeb9);

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;

tuned signature -- more explicit Document.Elements;

more formal Document.Blobs;
removed junk;

tuned signature;

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

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;

report (but ignore) markup within auxiliary files;

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

load files that are not provided by PIDE blobs;
uniform resolve_files via Command.read;

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;

clarified boundary cases of Document.Node.Name;

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

cancel_query via direct access to the exec_id of the running query process;

tuned signature -- more uniform treatment of overlays as command mapping;

maintain overlays within node perspective;
tuned signature;

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

obsolete;

more rendering for information messages;

tuned signature;

tuned protocol terminology;
tuned signature;

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;

explicit management of Session.Protocol_Handlers, with protocol state and functions;
more self-contained ML/Scala module Invoke_Scala;

tuned signature;

clarified module dependencies: avoid Properties and Document introding minimal "PIDE";

dockable window for timing information;

discontinued obsolete header "files" -- these are loaded explicitly after exploring dependencies;

discontinued obsolete 'uses' within theory header;

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;

support dialog via document content;

generalized notion of active area, where sendback is just one application;
some support for graphview via active area;

--HG--
rename : src/Pure/PIDE/sendback.ML => src/Pure/PIDE/active.ML
rename : src/Tools/jEdit/src/sendback.scala => src/Tools/jEdit/src/active.scala

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

tuned whitespace;

alternative completion for outer syntax keywords;

support for wrapped XML elements, which allows to preserve full markup tree information in to_XML/from_XML conversion;

eliminated dead code;

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

more explicit message markup and rendering;

clarified command status (again);

further refinement of command status, to accomodate forked proofs;

refined status of forked goals;

added keyword kind "thy_load" (with optional list of file extensions);

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;

simplified Document.Node.Header -- internalized errors;

tuned signature -- slightly more abstract text representation of prover process;

more robust Sendback handling: JVM/jEdit paranoia for case matching, treat Pretty body not just XML.Text, replace proper_range only (without trailing whitespace);

added static command status markup, to emphasize accepted but unassigned/unparsed commands (notably in overview panel);

discontinued obsolete last_execs (cf. cd3ab7625519);

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

less aggressive discontinue_execution before document update, to avoid unstable execs that need to be re-assigned;

some support for outer syntax keyword declarations within theory header;
more uniform Thy_Header.header as argument for begin_theory etc.;

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

clarified special eol treatment and moved to gfx_range -- enables error messages at end of input, e.g. "prop PROP";

retain original "uses" (again) -- still required for Thy_Load.use_file etc. in ML (notably for maintaining required/provided);
tuned;

Symbol.encode header edits;

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

include warning messages in node status;

more precise rendering of overview_color/gutter_message/squiggly_underline based on cumulation of command status and warning/error messages;

tuned comments;

clarified partial restrict operation;

command status color via regular markup;

prefer raw_message for protocol implementation;

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