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

tuned signature; tuned comments;

clarified module name;

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

tuned signature; unified exceptions for this module;

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

tuned -- cleanup before publishing assignment;

more abstract types; tuned signature;

tuned;

disallow concurrent execution attempt explicitly -- it should never happen due to management of singleton execution; tuned error messages: prefer plain "error" as in document.ML;

more precise fact declarations -- fewer warnings;

global management of command execution fragments; tuned;

fully synchronized guard of running execution; tuned;

merged

added exercises

optimize isar-proofs by trying different proof methods

made SML/NJ happy

tuned

tuned;

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

tuned -- refrain from odd optimization;

tuned;

added "echo" command for demonstration purposes;

more abstract message channel;

explicit shutdown of message output thread;

tuned signature;

no need for raw stdin;

fall back on synchronous message output for single-threaded SML/NJ;

make SML/NJ happy;

retain main thread for protocol loop -- no access to raw ML toplevel;

removed historic dimacs2hol (see also read_dimacs_cnf_file in src/HOL/Tools/sat_solver.ML);

less intrusive token_range rendering, which is relevant for inner parse errors;

made SML/NJ happy

merged

tuned start_execution: avoid sleep on worker thread;

print "persistent" flag allows to adjust tradeoff of ML run-time vs. JVM heap-space;

allow to remove print functions; tuned signature;

clarified Command.print: update old prints here;

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

tuned;

tuned proofs;

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

tuned message;

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

tuned protocol terminology; tuned signature;

tuned;

allow whitespace in file names;

tuned;