2010-07-24 ago tuned;
2010-07-24 ago moved basic thy file name operations from Thy_Load to Thy_Header;
2010-07-24 ago moved management of auxiliary theory source files to Thy_Load -- as theory data instead of accidental loader state;
2010-07-22 ago tuned signature;
2010-07-22 ago eliminated some unreferenced identifiers;
2010-07-22 ago tuned;
2010-07-21 ago clarified/exported Future.worker_subgroup, which is already the default for Future.fork;
2010-07-20 ago avoid duplicate printing of 'theory' state (cf. 173974e07dea);
2010-07-20 ago toplevel pp for Proof.state and Toplevel.state;
2010-07-20 ago Topelevel.run_command: interactive mode for initial 'theory' ensures that Thy_Info.begin_theory loads parent theories;
2010-07-20 ago 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;
2010-07-05 ago async_state: report within proper transaction context;
2010-07-04 ago general -- also for Toplevel.async_state;
2010-07-03 ago run_command: actually observe "print" flag;
2010-07-03 ago Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-31 ago Toplevel.run_command: reraise Interrupt, to terminate the Isar_Document.execution and not store a failed attempt;
2010-05-15 ago refer directly to structure Keyword and Parse;
2010-04-26 ago 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;
2010-04-23 ago added keyword category "schematic goal", which prevents any attempt to fork the proof;
2010-02-18 ago removed unused Theory_Target.begin;
2009-11-17 ago init_theory: Runtime.controlled_execution for proper exception trace etc.;
2009-11-17 ago implicit name space grouping for theory/local_theory transactions;
2009-11-13 ago modernized structure Local_Theory;
2009-11-10 ago Toplevel.thread provides Isar-style exception output;
2009-11-10 ago modernized structure Theory_Target;
2009-11-08 ago adapted Generic_Data, Proof_Data;
2009-11-02 ago modernized structure Proof_Node;
2009-10-27 ago non-critical atomic accesses;
2009-09-30 ago eliminated dead code;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-07-20 ago Proof.future_proof: declare all assumptions as well;
2009-07-19 ago more abstract Future.is_worker;
2009-06-06 ago moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
2009-06-04 ago exn_message/raised: ML_Compiler.exception_position;
2009-03-30 ago added Toplevel.previous_node_of;
2009-03-21 ago restricted interrupts for tasks running as future worker thread -- attempt to prevent interrupt race conditions;
2009-03-18 ago reduced verbosity;
2009-03-11 ago debugging: special handling of EXCURSION_FAIL;
2009-03-10 ago controlled_execution/debugging: special handling of UNDEF to prevent it to appear in exception_trace;
2009-03-09 ago simplified presentation_context_of;
2009-03-08 ago simplified presentation: built into transaction, pass state directly;
2009-01-16 ago run_command: check theory name for init;
2009-01-15 ago added run_command (from isar_document.ML);
2009-01-11 ago added Goal.future_enabled abstraction -- now also checks that this is already
2009-01-10 ago added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
2009-01-10 ago excursion: commit_exit internally -- checkpoints are fully persistent now;
2009-01-07 ago Proof.global_future_proof;
2009-01-07 ago added local_theory';
2009-01-04 ago future proofs: back to Future.fork_pri ~1 for improved parallelism;
2008-12-16 ago future proofs: Future.fork_pri 1 minimizes queue length and pending promises
2008-12-16 ago Future.fork_pri;
2008-12-11 ago removed spurious exception_trace;
2008-12-11 ago export context_node;
2008-12-06 ago excursion: improve parallelism by not joining proofs here (depends on persistent checkpoints);
2008-12-04 ago excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
2008-10-21 ago added Future.enabled check;
2008-10-09 ago Multithreading.enabled;
2008-10-02 ago program wrapper: controlled_execution ensures proper thread attributes (global default is unsafe due to InterruptAsynch;
2008-10-02 ago simplified Exn.EXCEPTIONS;