clarified default tag;

clarified future scheduling parameters, with support for parallel_limit;

clarified signature;

clarified apply_transaction: always continue without presentation context;

more tight presentation context: avoid storing full Toplevel.state;

tuned;

tuned;

clarified signature;

clarified presentation_state with provide presentation_context;

theory Pure is default presentation context;

more operations;

uniform use of original theory;

clarified document preparation vs. skip_proofs;

keep original bottom-up order of proof forks, which potentially reduces thread congestion due to Proofterm.consolidate;

clarified build errors;
tuned signature;

clarified priority: zero can mean unknown/long or irrelevant/short time;

absent timing information means zero, according to 0070053570c4, f235646b1b73;

tuned;

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

clarified modules;
tuned signature;

prefer infix operations;

careful export of type-dependent functions, without losing their special status;

clarified modules;
tuned signature;

clarified modules;
tuned signature;

tuned;

discontinued built-in profiling: avoid danger of conflicting invocations (multithreading etc.);

separate panel for proof state output;

default ML context for all command transactions, e.g. relevant for debugging and toplevel pretty-printing;

more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;

tuned signature;

tuned output;

discontinued pointless warnings: commands are only defined inside a theory context;

explicit error for Toplevel.proof_of;
eliminated obsolete Toplevel.unknown_proof;
more total Toplevel.proof_position_of;

tuned messages;

clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);

support for 'restricted' modifier: only qualified accesses outside the local scope;

support private scope for individual local theory commands;
tuned signature;

discontinued special treatment of malformed commands (reverting e46cd0d26481), i.e. errors in outer syntax failure are treated like errors in inner syntax, name space lookup etc.;

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

tuned;

more informative failure of protocol commands, with exception trace;
eliminated obsolete Runtime.TERMINATE (left-over from former 'exit' command);

tuned;

allow diagnostic proof commands with skip_proofs;

tuned signature;

uniform treatment of all document markup commands: 'text' and 'txt' merely differ in LaTeX style;
discontinued obsolete 'txt_raw' (superseded by 'text_raw');
eliminated obsolete Outer_Syntax.markup (superseded by keyword kinds);
'text' and 'txt' no longer appear in Sidekick tree due to change of keyword kind;
changed tagging of diagnostic commands within proof;

more explicit Keyword.keywords;

eliminated unused int_only flag (see also c12484a27367);
just proper commands;

discontinued pointless option: timing is always on (overall theory only);

eliminated odd flags and hook;

'oops' requires proper goal statement -- exclude 'notepad' to avoid disrupting begin/end structure;

tuned;

centralized (ad-hoc) switching of targets in named_target.ML

avoid odd Named_Target.reinit altogether

clarified terminology: toplevel is interwined with named targets in particular, not with local theories in general

smarter recovery from toplevel type error;

print results as "state", to avoid intrusion into the source text;
print new local theory (again);

discontinued Toplevel.print flag -- print uniformly according to Keyword.is_printed;

tuned;

clarified print_state, which goes back to TTY loop before Proof General, and before separate print_context;

more print operations;
preserve declaration order;

some shortcuts for chunks, which sometimes avoid bulky string output;

clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;

discontinued Toplevel.debug in favour of system option "exception_trace";

prefer more robust Synchronized.var;

more explicit Sign.change_check -- detect structural mistakes where they emerge, not at later theory merges;
clarified sublocale_global: proper Local_Theory.exit (see also 8fe7414f00b1);

slightly more rubust (and opportunistic) exit for old-fashioned theory_to_proof, which is used by global 'sublocale' with Named_Target.init but without proper exit;

tuned whitespace;

more uniform status -- accommodate spurious Exn.Interrupt from user code, allow ML_Compiler.exn_messages_id to crash;
tuned signature;

tuned signature;

improved printing of exception trace in Poly/ML 5.5.1;

some explicit indication of Proof General legacy;

maintain goal forks as part of global execution;
tuned;

discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
simplified Goal.future_enabled;

type theory is purely value-oriented;

immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 -> 100000, JinjaThreads: 65000 -> 300000) -- minimal measurable impact on inference kernel performance;

tuned message;

tuned signature;
tuned comments;

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

clarified Proofterm.proofs vs. Goal.skip_proofs;

mark local theory as brittle also after interpretation inside locales;
more correct bookkeeping on brittleness: must store directly beside lthy data, with implicit default true for levels > 1;
check brittleness only during context switch using (in ...) syntax, not for arbitrary exit of local theory

brittleness stamping for local theories

just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;

clarified protocol_message undefinedness;

discontinued Toplevel.no_timing complication -- also recovers timing of diagnostic commands, e.g. 'find_theorems';
print timing as tracing, to keep it out of the way in Proof General;
no timing of control commands, especially relevant for Proof General;

more explicit Goal.fork_params -- avoid implicit arguments via thread data;
actually fork terminal proofs in interactive mode (amending 8707df0b0255);

more centralized command timing;
clarified old-style timing message;

extra checkpoint to avoid stale theory in skip_proof context, e.g. in 'instance' proof;

explicit Toplevel.is_skipped_proof;
tuned;

more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);

clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
clarified unknown timing vs. zero timing;
tuned;

refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
refined parallel_proofs = 3: fork terminal proofs, as poor man's parallelization in interactive mode;

uniform treatment of global/local proofs;
tuned;

tuned;

clarified Toplevel.element_result wrt. Toplevel.is_ignored;

more Thy_Syntax.element operations;

simplified Proof.future_proof;

tuned signature;

fork diagnostic commands (theory loader and PIDE interaction);
explicit id for load_thy, for more robust Goal.fork accounting and commit for each theory -- NB: use_thys nodes become subject to Position.is_reported like PIDE document transactions;
clarified Toplevel.command_exception vs. Toplevel.command_errors;

tuned 2464ba6e6fc9 -- NB: approximative_id is NONE for PIDE document transactions;

tuned;

discontinued pointless command category "thy_schematic_goal" -- this is checked dynamically;

clarified Toplevel.element_result: scheduling policies happen here;
tuned;

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

make SML/NJ happy;

eliminated hard tabs;

highest priority for proofs with unknown / very short timing -- recover original scheduling with parallel_proofs_reuse_timing = false;

more tight representation of command timing;
tuned signatures;
tuned;

proper check of Proof.is_relevant (again, cf. c3e99efacb67 and df8fc0567a3d);

improved scheduling of forked proofs, based on elapsed time estimate (from last run via session log file);

suppress timing message in full PIDE protocol -- this is for batch build;

support for prescient timing information within command transactions;

emit command_timing properties into build log;
tuned;

tuned signature;

more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
explicit target for context within global theory with after_close = exit to manage the 2 levels involved here;
reject "(in target)" for nested contexts more reliably -- difficult to handle due to lack of nested reinit;

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

more informative errors for 'proof' and 'apply' steps;
more Seq.result operations;

discontinued complicated/unreliable notion of recent proofs within context;

more precise register_proofs for local goals;
tuned signature;

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;

tuned signature;

renamed Position.str_of to Position.here;

vacuous execution after first malformed command;

recovered comination of Toplevel.skip_proofs and Goal.parallel_proofs from 9679bab23f93 (NB: skip_proofs leads to failure of Toplevel.proof_of);

tuned error -- reduce potential for confusion in a higher-level context, e.g. partial checking of theory sub-graph;

clarified proof_result: finish proof formally via head tr, not end_tr;

misc tuning and simplification;

static relevance of proof via syntax keywords;

misc tuning and simplification;

more explicit Toplevel.open_target/close_target;
replaced 'context_includes' by 'context' 'includes';
tuned command descriptions;

defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;

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

pass positions for named targets, for formal links in the document model;

maintain recent future proofs at transaction boundaries;

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

tuned error message;

clarified Toplevel.end_theory;

simplified Toplevel.init_theory: discontinued special name argument;

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;

get theory from last executation state;
tuned error messages;

explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
reduced Theory.end_theory to plain projection, outside transaction context (see also ddc3b72f9a42);

tuned signature;
tuned;

modernized structure Proof_Context;

present theory content as future, depending on intermediate proof state futures -- potential to reduce memory requirements and improve parallelization;

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

parallelization of nested Isar proofs is subject to Goal.parallel_proofs_threshold;

tuned signature;
tuned vacous forks;

support named tasks, for improved tracing;

Toplevel.init_theory: maintain optional master directory, to allow bypassing global Thy_Load.master_path;

formal notepad without any result;

renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;

discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);

avoid extra wrapping for interrupts;

removed dead code;

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;

Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.;
simplified Toplevel.error_msg;

tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);

added some proof state markup, notably number of subgoals (e.g. for indentation);
tuned;

named target is optional; explicit Name_Target.reinit

Named_Target.init: empty string represents theory target

Named_Target.theory_init

removed obsolete Toplevel.enter_proof_body;

avoid arcane Local_Theory.reinit entirely

renamed Theory_Target to the more appropriate Named_Target

--HG--
rename : src/Pure/Isar/theory_target.ML => src/Pure/Isar/named_target.ML

explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);

simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
explicit Thy_Info.toplevel_begin_theory, which does not maintain theory loader database;
Outer_Syntax.load_thy: modify Toplevel.init for theory loading, and avoid slightly odd implicit batch mode of 'theory' command;
added Thy_Load.begin_theory for clarity;
structure ProofGeneral.ThyLoad.add_path appears to be old ThyLoad.add_path to Proof General, but actually operates on new Thy_Load.master_path instead -- for more precise imitation of theory loader;
moved some basic commands from isar_cmd.ML to isar_syn.ML;
misc tuning and simplification;

simplified handling of theory begin/end wrt. toplevel and theory loader;

tuned;

moved basic thy file name operations from Thy_Load to Thy_Header;

moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
theory loader: reduced warnings -- thy database can be bypassed in certain situations;
Proof/Local_Theory.propagate_ml_env;
ML use function: propagate ML environment as well;
pervasive type generic_theory;

tuned signature;

eliminated some unreferenced identifiers;

tuned;

clarified/exported Future.worker_subgroup, which is already the default for Future.fork;

avoid duplicate printing of 'theory' state (cf. 173974e07dea);

toplevel pp for Proof.state and Toplevel.state;

Topelevel.run_command: interactive mode for initial 'theory' ensures that Thy_Info.begin_theory loads parent theories;

eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
tuned some error messages;

async_state: report within proper transaction context;

general Future.report -- also for Toplevel.async_state;

run_command: actually observe "print" flag;

Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);

modernized some structure names, keeping a few legacy aliases;

Toplevel.run_command: reraise Interrupt, to terminate the Isar_Document.execution and not store a failed attempt;

refer directly to structure Keyword and Parse;
eliminated old-style structure aliases K and P;

proofs that are discontinued via 'oops' are treated as relevant --- for improved robustness of the final join of all proofs, which is hooked to results that are missing here;

added keyword category "schematic goal", which prevents any attempt to fork the proof;

removed unused Theory_Target.begin;
Theory_Target.init: removed Locale.intern, which was accidentally introduced in 40b3630b0deb;
renamed Theory_Target.context to Theory_Target.context_cmd to emphasize that this involves Locale.intern;
tuned;

init_theory: Runtime.controlled_execution for proper exception trace etc.;

implicit name space grouping for theory/local_theory transactions;

modernized structure Local_Theory;

Toplevel.thread provides Isar-style exception output;

modernized structure Theory_Target;

adapted Generic_Data, Proof_Data;
tuned;

modernized structure Proof_Node;

non-critical atomic accesses;

eliminated dead code;
eliminated redundant parameters;

explicit indication of Unsynchronized.ref;

Proof.future_proof: declare all assumptions as well;
Proof.future_proof: removed spurious exception_trace (which might cause crash-by-interrupt);
replaced Future.fork_local by Future.fork_pri (again, until group exceptions are propagated properly);

more abstract Future.is_worker;
Future.fork_local: inherit from worker (if available);

moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);

exn_message/raised: ML_Compiler.exception_position;

added Toplevel.previous_node_of;
keep type Toplevel.node private (formerly required in document antiquotations, which now operate on plain Toplevel.state);

restricted interrupts for tasks running as future worker thread -- attempt to prevent interrupt race conditions;

reduced verbosity;

debugging: special handling of EXCURSION_FAIL;

controlled_execution/debugging: special handling of UNDEF to prevent it to appear in exception_trace;

simplified presentation_context_of;

simplified presentation: built into transaction, pass state directly;

run_command: check theory name for init;

added run_command (from isar_document.ML);
tuned;

added Goal.future_enabled abstraction -- now also checks that this is already
a future task, which excludes interactive commands of the old toplevel;

added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;

excursion: commit_exit internally -- checkpoints are fully persistent now;
excursion: do not force intermediate result states yet -- great performance improvement;

Proof.global_future_proof;

added local_theory';

future proofs: back to Future.fork_pri ~1 for improved parallelism;

future proofs: Future.fork_pri 1 minimizes queue length and pending promises
-- slight improvement of throughput, at the cost of a bit of parallelism;

Future.fork_pri;

removed spurious exception_trace;

export context_node;

excursion: improve parallelism by not joining proofs here (depends on persistent checkpoints);

excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;

added Future.enabled check;

Multithreading.enabled;

program wrapper: controlled_execution ensures proper thread attributes (global default is unsafe due to InterruptAsynch;

simplified Exn.EXCEPTIONS;

excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
tuned;

datatype transition: internal trans field is maintained in reverse order;
tuned;

renamed promise to future, tuned related interfaces;

more robust treatment of Interrupt (cf. exn.ML);

begin_proof: avoid race condition wrt. skip_proofs flag;
replaced command_excursion by excursion, which is based on units of command/proof pairs;
excursion: basic support for proof promises;

export setmp_thread_position;
commit_exit: position;
added plain command execution;
simplified command_excursion, eliminated old (present_)excursion;

LocalTheory.exit_global;

added pos_of;

simplified Toplevel.add_hook: cover successful transactions only;

added add_hook interface for post-transition hooks;

simplified present_local_theory/proof;

added ignored, malformed transitions;

support for command status;

tuned;

simplified commit_exit: operate on previous node of final state, include warning here;
misc tuning;

export EXCURSION_FAIL;

eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
added commit_exit;
removed obsolete exception RESTART;
init_theory: removed obsolete kill argument;
removed obsolete undo_limit, undo_exit, kill, history;
misc tuning;

replaced obsolete ProofHistory by ProofNode (backtracking only);

export str_of;

init_theory: pass name explicitly;
empty transition: empty name;

added name_of;
added get_id/put_id;
tuned;

present_excursion: setmp_thread_position during presentation;

transaction/init: ensure stable theory (non-draft);

eliminated unused name_of, source, source_of, print', print3, three_buffersN;
tuned;

made purely value-oriented, moved global state to structure Isar (cf. isar.ML);
export toplevel, error_msg (formerly print_exn), transition (formerly apply);
moved type isar to structure OuterSyntax;
moved crashes to structure Isar;

added generic_theory transaction;

tuned;

raw_loop: more graceful crash recovery;

added exception CONTEXT, indicating context of another exception;
exn_message: explicit context, *not* ML_Context.get_context;
toplevel_error/apply: explicit exn_context;
explicit Markup.location for exn_info (cf. at_command);
fixed spelling;
tuned;

exn_message: added TimeLimit.TimeOut;
replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;

removed unused properties;
replaced ContextPosition by Position.thread_data;

removed obsolete prompt markup;

replaced thread_properties by simplified version in position.ML;

toplevel print_exn: proper setmp_thread_properties;

maintain thread transition properties;

type transition: added properties field;

Isar loop: recover after toplevel crashes;

replaced Markup.enclose by Markup.markup, which operates on plain strings instead of raw output;

Toplevel.loop: explicit argument for secure loop, no warning on quit;

init_empty: check before change (avoids non-linear update);

simplified LocalTheory.reinit;
tuned;

clarified theory target interface

safe_exit: controlled_execution;

TheoryTarget.init_cmd;

generic Syntax.pretty/string_of operations;

print_state_context: local theory context, not proof context;
context_position: cover Theory case as well (requires additional checkpoint);

local_theory transactions: more careful treatment of context position;

simplified PrintMode interfaces;

Added local_theory_to_proof'

global state transformation: non-critical, but also non-thread-safe;

NAMED_CRITICAL;

added TOPLEVEL_ERROR (simplified version from output.ML);

*** empty log message ***

moved exception capture/release to structure Exn;

marked some CRITICAL sections;
eliminated transform_failure (to avoid critical section for main transactions);
removed unused exceptions MetaSimplifier.SIMPROC_FAIL, Attrib.ATTRIB_FAIL, Method.METHOD_FAIL, Antiquote.ANTIQUOTE_FAIL;

init_empty: invoke operation *after* safe_exit;

Markup.enclose;

Markup.output;
removed no_state markup -- produce empty state;

prompt: plain string, not output;

simplified/more robust print_state;
more robust prompt markup;

toplevel prompt/print_state: proper markup, removed hooks;
tuned;

tuned;

oops -- fixed profiling;

profiling: observe no_timing;

transaction: context_position (non-destructive only);

removed unused info channel;

Toplevel.debug: coincide with Output.debugging;

moved ML context stuff to from Context to ML_Context;

added generic_theory_of;
adapted ML context operations;

fixed exit: proper type check of state;
tuned signature;

removed Toplevel.print_exn hook -- existing error_msg_fn does the job;

eliminated Option.app

Expose command failure recovery code for top level.

removed conditional combinator;

refined notion of empty toplevel, admits undo of 'end';
added undo_exit, init_empty, init_state;
removed unused toplevel, reset;
tuned;

removed obsolete assert;

prefer Proof.context over Context.generic;

level: do not account for local theory blocks (relevant for document preparation);

simplified local theory wrappers;

LocalTheory.restore;

removed obsolete print_state_hook;

removed checkpoint interface;
moved back to copy/checkpoint instead of checkpoint/checkpoint
(NB 1: checkpoint is idempotent, i.e. impure data is being shared, which is inappropriate;
NB 2: copying a checkpoint always produces a related theory);
present_proof: proper treatment of history;
tuned;

renamed enter_forward_proof to enter_proof_body;
renamed exit_local_theory to end_local_theory;
added local_theory_to_proof;
tuned;

exit_local_theory: pass interactive flag;
begin_local_theory: generic init;

added type global_theory -- theory or local_theory;
added begin/exit_local_theory;
removed theory_context;
renamed body_context_node to presentation_context;
removed copy (checkpoint twice instead -- avoids unrelated theories);

loop: disallow exit in secure mode;

TheoryTarget;

member (op =);

global goals/qeds: after_qed operates on Proof.context (potentially local_theory);

keep/transaction: unified execution model (with debugging etc.);
tuned;

skip_proofs: do not skip proofs of schematic goals (warning);

avoid unqualified exception;

handle exception SYS_ERROR;

checkpoint/copy_node: reset body context;

added cases_node;
replaced body_context_of by body_context_node, removed no_body_context;
copy: ProofContext.transfer;
added present_local_theory, present_proof;
removed internal command interface;

added local_theory, with optional locale xname;

swapped theory_context;

keep: disable Output.toplevel_errors;
program: Output.ML_errors;

sane ERROR vs. TOPLEVEL_ERROR handling;
added program;

removed obsolete sign_of;

added context_of -- generic context;

transactions now always see quasi-functional intermediate checkpoint;
removed obsolete theory_theory_to_proof;
added

hide type datatype node;
added theory_node, proof_node, is_theory, is_proof, proof_position_of, checkpoint, copy;
no_body_context: no history;
transaction: test save = true;

added theory_to_theory_to_proof, which may change theory before entering the proof;
added forget_proof (from isar_thy.ML);

tuned;

simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;

get_interrupt: special handling of IO.io now in ML-Systems/smlnj-basis-compat.ML;

uniform handling of interrupts

theory_to_proof: check theory of initial proof state, which must not be changed;

catching exception Io

added three_buffersN, print3;
tuned theory_to_proof: plain Proof.state instead of history;
added EXCEPTION;
removed DATA_FAIL, TRANSLATION_FAIL;

added interact flag to control mode of excursions;

excursion: interactive if debug;

added assert, command;

added no_body_context;

proof_to_theory_context: interaction flag;

state: body context;
added theory_context, proof_to_theory_context;
added is_proof, level;
turned excursion_result into present_excursion;

added print_state_hook;
renamed proof'' to actual_proof;
tuned;

debug: exception_trace;
tuned;

tuned;

added profile flag;

added print': print depending on print_mode;

tuned;

Context.DATA_FAIL;
accomodate identification of type Sign.sg and theory;

tuned msgs;
exn_message: added Fail;
timing: info channel;

node_trans: revert to original transaction code (pre 1.54);

tuned;

improved exn_message;

new display of theory stamps

Registrations of global locale interpretations: improved, better naming.

First version of global registration command.

Move towards standard functions.

Modified node_trans to avoid duplication of signature stamps
when undoing.

Deleted Library.option type.

Toplevel.debug for debugging in Isar.

excursion_result now also passes previous state to presentation functions.
This is useful for hiding proof scripts.

Some changes to allow skipping of proof scripts.

added >>> : transition list -> unit;

Merged in license change from Isabelle2004

added name_of, source_of, source;

Output.timing;

A patch by david aspinall

exception SIMPROC_FAIL: solid error reporting of simprocs;

use ignore_interrupt, raise_interrupt;

ANTIQUOTE_FAIL;

tuned print_state interfaces;

added proof_to_theory';

simplified Proof.init_state:

Proof.init_state thy None;

Display.current_goals_markers;

tuned msg;

added unknown_theory/proof/context;

added enter_forward_proof;

excursion_result: transform_error;

tuned msg;

excursion_result;

Toplevel.no_timing;

global timing flag;

print_state: flag for proof only;

GPLed;

tuned msg;

tuned output;

eliminated toplevel stack;

added is_toplevel;

added keep', theory';

avoid interrupts of read loop;

added context_of;

print_context;

tuned print_state;
quiet flag;

init / init_theory: pass int flag;

Toplevel.excursion_error;

removed BREAK, ROLLBACK;

tuned Interrupt msgs;

fixed interrupts (eliminated races);

tuned;
added prompt_state_fn hook;
added kill operation;
provide toplevel node history, nests with proof history;
toplevel prompt includes nest level;
more robust recovery from stale signatures;

cleaned comments;
node_cases renamed to node_case;
more robust rollback of transactions via backup;

improved msg;

comment;

excursion: ERROR_MESSAGE;
exn_message: ERROR;

added exception RESTART;

print_state hook, obeys Goals.current_goals_markers by default;

break: exhibit state stack;

exn_message FAIL;

export exn_message;

BREAK: include state;
report Attrib.ATTRIB_FAIL, Method.METHOD_FAIL;

The Isabelle/Isar toplevel.