tuned;

more frugal merge of markup trees: restrict to expected range before checking trivial cases, e.g. relevant for sporadic warnings (eval_exec) within big ML reports (print_exec);

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

tuned;

redirect ML_Compiler reports more directly: only the (big) parse tree report is deferred via Execution.print (NB: this does not work for asynchronous "diag" commands); more explicit ML_Compiler.flags;

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

more frugal merge of markup trees: non-overlapping tree counts as empty;

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;

support to redirect report on asynchronous / non-strict print function (NB: not scalable due to bulky merge of markup trees);

less markup by default -- this is stored persistently in Isabelle/Scala; removed dead code;

clarified valid_id: always standardize towards static command.id;

prefer Context_Position where a context is available; prefer explicit Context_Position.is_visible -- avoid redundant message composition; tuned signature;

unused;

more uniform Execution.fork vs. Execution.print; asynchronous Execution.fork_prints, entrusted to Execution.fork management (NB: Command.print_finished is only relevant for persistent print functions);

added Execution.print: accumulate print operations for some command execution, which are applied later and print time; misc tuning;

tuned proofs

Some useful lemmas

tuned comments;

tuned load order;

superseded by (provide_)parse_files;

tuned;

merged

more warnings for recent versions of Poly/ML (see also fe1f6a1707f7);

eliminated dead code;

proper configuration option "ML_print_depth"; proper ML_exception_trace for HOL-TPTP;

removed junk;

clarified options ML_source_trace and ML_exception_trace (NB: the latter needs to be a system option, since the context is sometimes not available, e.g. for 'theory' command);

separate tokenization and language context for SML: no symbols, no antiquotes;

separate "sml" mode, suppress old "ml" mode altogether;

some SML examples;

added command 'SML_file' for Standard ML without Isabelle/ML add-ons;

updated to scala-2.10.4;

cleanup auxiliary proofs for Brouwer fixpoint theorem (removes ~2400 lines)

prove theorems with fixed variables (export afterwards)

generalized theorems about derivatives of limits of sequences of funtions

removed unused 'ax_specification', to give 'specification' a chance to become localized; tuned whitespace;

merged;

merged

proper Sign.full_name to get internal name (like Sign.add_consts);

formal check of user input, avoiding direct references of interal names;

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

tuned proofs

made tactic more robust

inline helper function

rearranging some deriv theorems

modernized approximation, avoiding bad name binding;

more sensible treatment of quasi-local variables (NB: Variable.add_fixes is only for term variables, while Variable.declare takes care of types within given terms);

merged

more antiquotations;

more antiquotations;

more antiquotations; clarified file location;

more antiquotations;

more antiquotations;