load_thy: more precise treatment of improper cmd or proof (notably 'oops');

schedule_tasks: single theory is loaded concurrently as well (cf. concurrent Toplevel.excursion);

added unit_source: commands with proof;

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;

load_thy: Toplevel.excursion based on units of command/proof pairs;

more command categories; tuned;

renamed Future.fork_irrelevant to Future.fork_background; tuned;

export explicit joint_futures, removed Theory.at_end hook; renamed Future.fork_irrelevant to Future.fork_background;

tuned

turned process_thy into present_thy, which merely does presentation (wrt. persistent intermediate states);

Toplevel.commit_exit: position;

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

simplified process_file, eliminated Toplevel.excursion; load_thy: separation of Toplevel.command_excursion and ThyOutput.present_thy (intermediate state persist until commit_exit);

clarified codegen interfaces

tuned

reorganized examples

fixed slips

re-canibalised manual

slightly different command line for makedist_mercurial

put_thms: ContextPosition.set_visible false;

added type pp, which helps installing polymorphic pretty printers;

added str_of;

install_pp Future.T (polyml only);

report_token/parse_token: back to context-less version;

back to plain Position.report for regular references;

back to plain Position.report for regular references; ContextPosition.report_visible for decls; report_token/parse_token: back to context-less version;

promise global proofs;

renamed report to report_visible; tuned comments;

code example: back to individual ML commands, which are now thread-safe;

ContextPosition.report; parse_token/report_token: explicit context;