always consolidate: allow errors in presentation;

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

tuned -- short-circuit result;

proper function invocation with all arguments;

fork parallel prints early in execution: avoid degradation of priority due to main eval task;

record active execution task and depend on it -- avoid new executions bumping into old ones;

clarified priority;

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

more node status information;

clarified "consolidation" vs. "presentation";

support for dynamic document output while editing;

tuned: prefer list operations over Source.source;
approximative parsing of theory header;

clarified implicit Pure.thy;

PIDE markup for session ROOT files;

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

tuned spelling;

tuned;

more informative task_statistics;

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

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

more IDE support for Isabelle/Pure bootstrap;

support ROOT0.ML as well -- independently of ROOT.ML;

treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";

prefer infix operations;

clarified modules;
tuned signature;

thread context for exceptions from forks, e.g. relevant when printing errors;
tuned signature;

clarified context;

set breakpoint state on ML side, relying on stable situation within the PIDE editing queue;

clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;

more position information and PIDE markup for command keywords;

misc tuning and simplification;

more precises positions;
more permissive imports;

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

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

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

tuned;

clarified markup for embedded files, early before execution;

more explicit errors;

clarified execution graph traversal: stable imports are required to proceed, e.g. relevant to avoid crash of init_theory after discontinued execution;

eliminated Document.execution frontier (again, see 627fb639a2d9): just run into older execution, potentially stalling worker thread, but without global delay due to long-running tasks (notably sledgehammer);
clarified Command.run_process etc.: join running eval, bypass running print;
eliminated Command.memo in favour of regular Lazy.lazy;
more Lazy.lazy status information;

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

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

tuned signature;

even more exception traces for Document.update, which goes through additional execution wrappers;

always traverse required nodes, e.g. relevant for inlined errors of imported theory header;

prefer externally provided keywords -- Command.read_thy may degenerate to bootstrap_thy in case of errors;
tuned message;

plain value Keywords.keywords, which might be used outside theory for bootstrap purposes;
plain value Outer_Syntax within theory: parsing requires current theory context;
clarified name of Keyword.is_literal according to its semantics;
eliminated pointless type Keyword.T;
simplified @{command_spec};
clarified bootstrap keywords and syntax: take it as basis instead of side-branch;

more explicit Keyword.keywords;

simplified keyword kinds;
more explicit bootstrap syntax;

explicit type Keyword.keywords;
tuned signature;

tuned signature according to Scala version -- prefer explicit argument;

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

tuned comments;

make SML/NJ happy;

less authentic SHA1.digest: trust Scala side on blobs and avoid re-calculation via Foreign Language Interface, which might be a cause of problems;

avoid redundant data structure;

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

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

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;

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

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

tuned comment;

tuned signature;

store blobs / inlined files as separate text lines: smaller values are more healthy for the Poly/ML RTS and allow implicit sharing;
integrity check of SHA1 digests produced in Scala vs. ML;
tuned signature;

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

more total master_directory -- NB: this is used outside command transactions (see also 92961f196d9e);

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

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

proper theory name vs. node name;

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

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

support print functions with explicit arguments, as provided by overlays;

maintain overlays within node perspective;
tuned signature;

simplified / clarified execution priority: auto prints << 0, proofs < 0, eval = 0, print_state = 1;

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

recovered delay for Document.start_execution (see also 627fb639a2d9), which potentially improves throughput when many consecutive edits arrive;

more timing;

more timing;
tuned -- Execution.is_running always holds due to immediate start;

de-assign execs that were not registered as running yet -- observe change of perspective more thoroughly;

traverse node on change of "required" state;

keep memo_exec execution running, which is important to cancel goal forks eventually;
run as nested worker task to keep main group valid, even after cancelation of removed subgroups;
do not memoize interrupt, but absorb it silently in main execution;
Goal.purge_futures: rough sanity check of group status;

maintain explicit execution frontier: avoid conflict with former task via static dependency;
start execution immediate after assignment, to keep frontier simple;

clarified conditions for node traversal;

tuned;

discontinued notion of "stable" result -- running execution is never canceled;

document update at high priority -- important;

option editor_execution_priority;

more careful termination of removed execs, leaving running execs undisturbed;

clarified execution: maintain running execs only, check "stable" separately via memo (again);
tuned signatures;

tuned signature;
tuned comments;

clarified module name;

--HG--
rename : src/Pure/PIDE/exec.ML => src/Pure/PIDE/execution.ML

more explicit type Exec.context;
eliminated obsolete execution group -- NB: cancelation happens individually for registered execs;

strictly monotonic Document.update: avoid disruptive cancel_execution, merely discontinue_execution and cancel/terminate old execs individually;

more abstract types;
tuned signature;

tuned;

global management of command execution fragments;
tuned;

fully synchronized guard of running execution;
tuned;

re-assign prints of unchanged eval only -- avoid crash of new_exec;

tuned -- refrain from odd optimization;

tuned;

tuned start_execution: avoid sleep on worker thread;

clarified Command.print: update old prints here;

produce print_execs assignment earlier during last_common phase (referring to current command_id, not prev);

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

tuned signature;
tuned comments;

tuned signature;
tuned;

clarified type Command.eval;

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;

more Command.memo operations;
more explicit types Command.eval vs. Command.print vs. Document.exec;
clarified print function parameters;

made SML/NJ happy;

more print function parameters;
check command_visible statically in assignment, instead of dynamically in execution;

tuned;

discontinued odd workaround for some old Poly/ML, which is still supported but of little practical relevance;

tuned;

allow multiple print functions;

tuned signature;

tuned signature;

tuned;

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

discontinued obsolete 'uses' within theory header;

simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
eliminated separate Outer_Syntax.read_element;

more sensible order of theory nodes (correspondance to Scala version), e.g. relevant to theory progress;

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

more official Future.terminate;
tuned signature;

eliminated potentially confusing terminology of Scala "layer";

--HG--
extra : rebase_source : 41ab848ec8aa777e906b6bbae5026666f025f458

maintain stable state of node entries from last round -- bypass slightly different Thm.join_theory_proofs;

central management of forked goals wrt. transaction id;
clarified stable_exec_id: consider ragular failure as stable;
more robust counting of forked proofs, with global reset after cancellation due to document editing;

refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
stretched meaning of Goal.parallel_proofs to enable future_terminal_proofs in interactive document model, despite its lack for regular forking of proofs;

some support for registering forked proofs within Proof.state, using its bottom context;
tuned signature;

tuned signature;

theory def/ref position reports, which enable hyperlinks etc.;
more official header command parsing;

check side-comments of command spans (normally filtered out in Outer_Syntax.toplevel_source);

vacuous execution after first malformed command;

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;

even more permissive approximation of master_dir, which is only required to access external resources ('uses' etc.);

simplified Document.Node.Header -- internalized errors;

improved interleaving of start_execution vs. cancel_execution of the next update;

always revisit nodes independently of "required" flag, which may change during editing -- avoid "bloodbath effect" when changing perspective while loading;

tuned;

builtin timing for main operations;

tuned;

just one dedicated execution per document version -- NB: non-monotonicity of cancel always requires fresh update;
explicit terminate_execution;
tuned source structure;

tuned future priorities: print 0, goal ~1, execute ~2;

more explicit last exec result;

dynamic propagation of node "updated" status, which is required to propagate edits and re-assigments and allow direct memo_result;
discontinued odd "touched" field -- check given edits directly;

tuned;

simplified Future.cancel/cancel_group (again) -- running threads only;
more robust update/cancel_execution: full join_tasks of group before exec state assignment;
tuned signature;

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

explicit checks stable_finished_theory/stable_command allow parallel asynchronous command transactions;
tuned;

discontinued obsolete last_execs (cf. cd3ab7625519);

stop node execution at first unassigned exec;

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

more scalable execute/update: avoid redundant traversal of invisible/finished nodes;
tuned;

less ambitious memo_eval, since memo_result is still not robust here;

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

more explicit memo_eval vs. memo_result, to enforce bottom-up execution;
edit of perspective touches node superficially, to ensure revisit after update;

Command.memo including physical interrupts (unlike Lazy.lazy);
re-assign unstable exec, i.e. reset interrupted transaction;
node result as direct exec -- avoid potential interrupt instability of Lazy.map;

tuned;

tuned -- NB: get_theory still needs to apply Lazy.force due to interrupt instabilities;

separate module for prover command execution;

tuned;

minimalistic support for remote URLs: no master dir here;

define keywords early when processing the theory header, before running the body commands;

declare command keywords via theory header, including strict checking outside Pure;

declare keywords as side-effect of header edit;
parse_command span is now lazy instead of future, to happen synchronously after header edit in new_exec (before execution);

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;

refined define_command vs. run_command: static tokenization vs. dynamic parsing, to increase the chance that the proper transaction is run after redefining commands (NB: requires slightly more space and time for document state);

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

clarified Time vs. Timing;

--HG--
rename : src/Pure/General/timing.scala => src/Pure/General/time.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

explicit master_dir as part of header -- still required (for Cygwin) since Scala layer does not pass file content yet;

no print_state for final proof commands, which return to theory state;

discontinued predefined empty command (obsolete!?);

discontinued global execs: store exec value directly within entries;
simplified entries: no extra copy of command_id;

Document.remove_versions on ML side;

less agressive parsing of commands (priority ~1);
join commands just before actual assignment;

more precise iterate_entries_after if start refers to last entry;
do not assign exec states after bad theory init;
reject illegal theory header after end of theory;

clarified define_command: store name as structural information;

amended last_common, if that happens to the very last entry (important to load HOL/Auth, for example);
clarified touch_node: reset result explicitly;

more careful treatment of interrupts, to retain them within forked/joined boundary of command transactions;

explicit running_color;
stronger colors for overview, more transparent colors for status within text;

tuned join_commands: avoid traversing cumulative table;

more precise treatment of nodes that are fully required for partially visible ones;

tuned signature -- iterate subsumes both fold and get_first;

further clarification of Document.updated, based on last_common and after_entry;
tuned;

tuned signature;

improved Document.edit: more accurate update_start and no_execs;
tuned;

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

tuned signature -- emphasize traditional read/eval/print terminology, which is still relevant here;

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

misc tuning and simplification;

tuned pri: prefer purging of canceled execution;

tuned Document.node: maintain "touched" flag to indicate changes in entries etc.;

misc tuning and simplification;

ignore irrelevant timings;

print state only for visible command, to avoid wasting resources for the larger part of the text;

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;

some support for toplevel printing wrt. editor perspective (still inactive);

propagate editor perspective through document model;

some support for editor perspective;

refined Graph implementation: more abstract/scalable Graph.Keys instead of plain lists -- order of adjacency is now standardized wrt. Key.ord;

added Future.joins convenience;
clarified Future.map: based on Future.cond_forks;

tuned;

tuned signature (again);
tuned;

tuned signature -- treat structure Task_Queue as private to implementation;

refined Future.cancel: explicit future allows to join actual cancellation;
Document.cancel_execution: join nested future groups as well;

more precise treatment of exception nesting and serial numbers;

more careful treatment of exception serial numbers, with propagation to message channel;

more systematic handling of parallel exceptions;
distinguish exception concatanation EXCEPTIONS from parallel Par_Exn;

workaround for Cygwin, to make it work in the important special case without extra files;

more robust treatment of node dependencies in incremental edits;

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

touch descendants of edited nodes;
more precise handling of Graph exceptions;

parellel scheduling of node edits and execution;

tuned error message;

retrieve imports from document state, with fall-back on theory loader for preloaded theories;
misc tuning;

explicit check of finished evaluation;

refined Document.edit: less stateful update via Graph.schedule;
clarified node result -- more direct get_theory;
clarified Document.joint_commands;

simplified exec: eliminated unused status flag;

simplified Toplevel.init_theory: discontinued special master argument;

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;

future_job: explicit indication of interrupts;

tuned signature -- corresponding to Scala version;

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

moved global state to structure Document (again);

get theory from last executation state;
tuned error messages;

clarified cancel_execution/await_cancellation;

tuned;

more permissive run_command: identity execution for empty toplevel, e.g. after malformed theory header;

structure Timing: covers former start_timing/end_timing and Output.timeit etc;
explicit Timing.message function;
eliminated Output.timing flag, cf. Toplevel.timing;
tuned;

tuned signature;
tuned vacous forks;

support named tasks, for improved tracing;

more direct Future.bulk, which potentially reduces overhead for Par_List;
tuned signature;

cancel document execution before editing, to improve reactivity on systems with few cores;

singleton (sequential) execution, to avoid race conditions in theory loader state (e.g. when multiple independent theories import the same theory);

workaround for odd x86_64 problem in Poly/ML 5.4.0 (actually SVN 1151?), which causes unexpected nontermination of Isabelle/Scala document editing;

full theory path enables loading parents via master directory and keeps files strictly separate;

clarified interact/print state: proof commands are treated as in TTY mode to get full response;

always print state of proof commands (notably "qed" etc.);

await_cancellation in the main thread, independently of the execution futures, which might get interrupted or be absent after node deletetion;

more precise treatment of deleted nodes;

added general Synchronized.counter convenience;

continue after failed commands;

explicit "timing" status for toplevel transactions;

tuned;

Document.async_state: some attempts to make this more robust wrt. cancelation of the main transaction -- avoid confusing feedback about pending forks;

refined Runtime.toplevel_error/Document.run_command: let interrupts pass unhindered;

more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;

moved Toplevel.run_command to Pure/PIDE/document.ML;
eliminated aliases of exception Toplevel.TERMINATE and Toplevel.EXCURSION_FAIL;
tuned signatures;

tuned;

tune;

added functor Linear_Set, based on former adhoc structures in document.ML;
Linear_Set.delete_after (ML): actually delete table entries;
Scala Linear_Set: clarified exceptions, according to ML version;
simplified Document.node using Linear_Set;
ML Document.edit: refer to start via NONE instead of no_id, according to Scala version;

document commands: maintain transition as future (wrt. potentially slow Outer_Syntax.prepare_command), refrain from second Toplevel.put_id;

renamed create_id to new_id;

more explicit / functional ML version of document model;
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;

tuned;

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

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

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;