src/Pure/Isar/toplevel.ML
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;
2008-10-01 ago excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
2008-10-01 ago datatype transition: internal trans field is maintained in reverse order;
2008-10-01 ago renamed promise to future, tuned related interfaces;
2008-10-01 ago more robust treatment of Interrupt (cf. exn.ML);
2008-09-30 ago begin_proof: avoid race condition wrt. skip_proofs flag;
2008-09-30 ago export setmp_thread_position;
2008-09-29 ago LocalTheory.exit_global;
2008-09-03 ago added pos_of;
2008-09-03 ago simplified Toplevel.add_hook: cover successful transactions only;
2008-09-02 ago added add_hook interface for post-transition hooks;
2008-08-13 ago simplified present_local_theory/proof;
2008-08-12 ago added ignored, malformed transitions;
2008-07-15 ago support for command status;
2008-07-15 ago tuned;
2008-07-15 ago simplified commit_exit: operate on previous node of final state, include warning here;
2008-07-14 ago export EXCURSION_FAIL;
2008-07-14 ago eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
2008-07-14 ago replaced obsolete ProofHistory by ProofNode (backtracking only);
2008-07-08 ago export str_of;
2008-07-02 ago init_theory: pass name explicitly;
2008-07-01 ago added name_of;
2008-05-24 ago present_excursion: setmp_thread_position during presentation;
2008-04-10 ago transaction/init: ensure stable theory (non-draft);
2008-04-10 ago eliminated unused name_of, source, source_of, print', print3, three_buffersN;