tuned signature;

more scalable output;

clarified signature: persistent results;

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

clarified signature: prefer Document.Snapshot;

clarified: consolidated result is last command;

more node status information;

tuned signature;

tuned signature;

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

retain isolated blob nodes (amending deb2fcbda16e): avoid failure of Session.handle_change with "Missing blob", when opening theory with load command later;

clarified signature -- avoid confusion with Resources.is_hidden;

more robust: self-export only;

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

purge history more thoroughly (see also 3156faac30a7);

clarified theory node name;
purge_theories: return purged, retained;
tuned documentation;

more position information;

update XML cache for slightly modified messages;

tuned signature;

tuned signature;

implicit thy_load context for bibtex files;

store full blob source for the sake of markup_to_XML;

PIDE markup for non-theory nodes;

tuned signature;

clarified signature;

tuned output;

removed inaccessible blobs from Document.Nodes;

purge hidden nodes more thoroughly: is_hidden may become true only later;

tuned signature;

more robust: allow Windows file names;

tuned signature;

tuned signature;

tuned signature;

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

proper bootstrap_name (amending b42743f5b595);

tuned signature;

clarified signature;

tuned signature;

clarified signature;

HTML preview based on PIDE markup;

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

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

more operations;

tuned signature;

tuned signature;

tuned signature;

simplified direct theory name (again, see also 570ba266f5b5, 2a7f9e79cb28);

tuned;

tuned signature;

tuned signature;

more abstract module Document;

clarified current_command: index refers to node content, negative index means first command;

discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;

tuned;

tuned;

support "purge" operation on document model;

tuned signature;

uniform Document.Model.node_edits (without void edits);

obsolete;

tuned;

tuned;

misc tuning and clarification;

tuned;

tuned;

clarified modules;

clarified signature: explicit Length to avoid implicit mistakes;

tuned;

tuned signature -- prover-independence is presently theoretical;

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

reactivated other_id reports (see also db929027e701, 8eda56033203);

tuned signature;

clarified modules;

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

clarified undefined_blobs: already loaded theories are suppressed;
enabled jedit_auto_resolve (again): e.g. relevant for debugging when following links through source files;

more robust access to stable tip version: take all pending edits into account, don't assume model for current buffer;

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

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

clarified positions of theory imports;

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

tuned;

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;

postpone changes in intermediate state between remove_versions/removed_versions, which is important for handle_change to refer to defined items on prover side;

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;

more explicit treatment of cleared nodes (removal is implicit);

clarified display;

clarified display;

avoid redundant data structure;

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

tuned;

tuned signature;

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

tuned signature;

tuned signature;

tuned signature;

clarified treatment of markup ranges wrt. revert/convert: inflate_singularity allows to retrieve information like language_context more reliably during editing;

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;

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);

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

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

afford larger full_index, to save a few milliseconds during rendering (notably text_overview);

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;

more direct command states -- merge_results is hardly ever needed;

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;

tuned signature;

tuned -- avoid code duplication;

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

tuned signature;

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

tuned signature -- expose less intermediate information;

clarified valid_id: always standardize towards static command.id;

tuned rendering -- avoid flashing background of aux. files that are disconnected from the document model;

tuned signature -- more explicit Document.Elements;

tuned data structure;

tuned;

more formal Document.Blobs;
removed junk;

tuned output;

tuned output;

tuned messages;

tuned signature -- avoid redundancy and confusion of flags;

tuned signature;

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

cumulate/select wrt. precise elements guard;
tuned signature;

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

more accurate eq_content;

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;

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

actually expose errors of cumulative theory dependencies;
more informative error messages;

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

refer to thy_load command of auxiliary file;

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;

clarified boundary cases of Document.Node.Name;

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

tuned;

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;

more strict find_command -- avoid invalid hyperlink_command;

prefer PIDE editor operations;
apply_query: insist in non-outdated snapshot via editor.current_command;
tuned signature;

central management of Document.Overlays, independent of Document_Model;

tuned -- use Multi_Map;

tuned signature;

proper low-level comparison -- heed warning by Scala compiler;

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

more elementary list structures for markup tree traversal;

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

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

maintain overlays within node perspective;
tuned signature;

more tight interface for markup cumulate/select: avoid duplicate application, allow to defer decision about definedness;

tuned signature;

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

tuned;

more formal type assign_update: avoid duplicate results and redundant update of global State.execs;

tuned signature -- NB: Command.read is actually part of Command.eval;

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;

tuned;

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

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

discontinued obsolete 'uses' within theory header;

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;

tuned signature -- avoid intrusion of module Path in generic PIDE concepts;

removed unused module Blob;

tuned signature;

accumulate under exec_id as well;

some support for inital command markup;
tuned signature;

more efficient painting based on cached result;

prefer jEdit file name representation (potentially via VFS);
tuned;

even more defensive path expansion (see also 8d381fdef898);

simplified Document.Node.Header -- internalized errors;

tuned signature;

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

discontinued obsolete last_execs (cf. cd3ab7625519);

misc tuning to accomodate scala-2.10.0-M2;

more recent recent_syntax, e.g. relevant for document rendering during startup;

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;

explicit Outer_Syntax.Decl;

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

removed obsolete proper_command_at (cf. 03a2dc9e0624);

clarified document nodes (full import graph) vs. node_status (non-preloaded theories);
tuned;

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

more explicit development graph;

prefer final ADTs -- prevent ooddities;

more abstract class Document.State;

more abstract class Document.State.Assignment;

tuned signature;

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

more abstract class Document.Node;

more abstract class Document.History;

more abstract class Document.Change;

tuned;

tuned signature;

improved select_markup: include filtering of defined results;

clarified Isabelle_Rendering vs. physical painting;
discontinued slightly odd object-oriented Markup_Tree.Cumulate/Select;

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

prefer sorting from Scala library;

index markup elements for more efficient cumulate/select operations;

tuned signature;
express select in terms of cumulate;

tuned signature;

added markup_cumulate operator;

class Counter as abstract datatype;

graph traversal in topological order;
Session.snapshot() with sensible defaults;

Document.Node.Name convenience;

more elaborate Node_Renderer, which paints node_name.theory only;

Document.removed_versions on Scala side;

some support to prune_history;
clarified signature: recent_stable is supposed to be always defined;

more redable Document.Node.toString;

tuned signature;

more abstract Document.Node.Name;
tuned signature;

crude display of node status;
tuned signature;

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

tuned signature;

dynamic exec state lookup for implicit position information (e.g. 'definition' without binding);

some support for hyperlinks between different buffers;
tuned signature;

de-assigned commands also count as changed;

tuned Session.edit_node: update_perspective based on last_exec_offset;

refined document state assignment: observe perspective, more explicit assignment message;
misc tuning and clarification;

maintain last_execs assignment on Scala side;
prefer tables over IDs instead of objects;

propagate information about last command with exec state assignment through document model;

tuned signature;

slightly more abstract Command.Perspective;

misc tuning and simplification;

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

clarified norm_header/header_edit -- disallow update of loaded theories;

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;

propagate editor perspective through document model;

some support for editor perspective;

discontinued redundant Edit_Command_ID;

use full .thy file name as node name, which makes MiscUtilities.resolveSymlinks/File.getCanonicalPath more predictable;
more robust treatment of node dependencies;
misc tuning;

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;

tuned signature;

clarified node header -- exclude master_dir;

normalized theory dependencies wrt. file_store;

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

simplified class Thy_Header;

uniform treatment of header edits as document edits;

explicit datatypes for document node edits;

more uniform Properties in ML and Scala;

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);

select_markup: no filtering here -- results may be distorted anyway;

more explicit error message;
convert/revert range;
tuned;

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;

tuned signature;

Snapshot.convert/revert: explicit error report to isolate sporadic crash;

concentrate Isabelle specific physical rendering markup selection in isabelle_markup.scala;

simplified Markup_Tree.select: Stream instead of Iterator (again), explicit Option instead of default;
tuned Snapshot.convert/revert;

Document.State.Assignment: eliminated promise in favour of plain values -- signalling is done via event bus in Session;

Node.full_index: allow command spans larger than block_size;

Document state assignment indicates command change;

simplified/clarified Document_View.text_area_extension;
tuned Document.Node.block_size, trading some space for better time;

Document.Node: significant speedup of command_range etc. via lazy full_index;

Command.results: ordered by serial number;

use Future.get_finished where this is the intended meaning -- prefer immediate crash over deadlock due to promises that are never fulfilled;
clarified session signalling;

added Document.Snapshot.select_markup, which includes command iteration, range conversion etc.;
Markup_Tree.select: plain Iterator;
misc tuning and simplification;

include Document.History in Document.State -- just one universal session state maintained by main actor;
Session.command_change_buffer: thread actor ensures asynchronous dispatch;
misc tuning;

tuned signatures;

some derived operations on Text.Range;

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

moved Text_Edit to Text.Edit;
tuned;

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

moved History/Snapshot to document.scala;

more explicit / functional ML version of document model;
tuned;

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

more basic Markup.parse_int/print_int (using signed_string_of_int) (ML);
added convenient Markup.Int/Long objects (Scala);
simplified "assign" message format -- explicit version id;
misc tuning and simplification;

moved Document.text_edits to Thy_Syntax;

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;

simplified/clarified Change: transition prev --edits--> result, based on futures;
Session.history: plain List instead of somewhat indirect Change.ancestors;
tuned;

moved snapshot to Session (cf. 96b22dfeb56a);

Change: eliminated id, which is merely the resulting document id and is only required in joined state anyway;
Document.edit_text: create new document id here;

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

specific command state;

consider command state as part of Snapshot, not Document;

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);

concentrate structural document notions in document.scala;
tuned;

avoid null in Scala;
tuned comments;

explicit Change.Snapshot and Document.Node;
misc tuning and clarification;
Document_View: explicitly highlight outdated command status;

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;

Session: predefined real time parameters;
Document_View: delayed caret handling, for improved reactivity;
selected_command: proper_command_at ignores ignored commands;

more efficient document model/view -- avoid repeated iteration over commands from start, prefer bulk operations;
misc tuning;

explicit markup for forked goals, as indicated by Goal.fork;
accumulate pending forks within command state and hilight accordingly;
Isabelle_Process: enforce future_terminal_proof, which gives some impression of non-linear/parallel checking;

@tailrec annotation;

renamed "rev" to "reverse" following usual Scala conventions;

parse_spans: cover full range including adjacent well-formed commands -- intermediate ignored and malformed commands are reparsed as well;

removed timing;

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

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

removed junk;

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