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;