src/Pure/Isar/toplevel.ML
2009-11-10 wenzelm 2009-11-10 Toplevel.thread provides Isar-style exception output;
2009-11-10 wenzelm 2009-11-10 modernized structure Theory_Target;
2009-11-08 wenzelm 2009-11-08 adapted Generic_Data, Proof_Data; tuned;
2009-11-02 wenzelm 2009-11-02 modernized structure Proof_Node;
2009-10-27 wenzelm 2009-10-27 non-critical atomic accesses;
2009-09-30 wenzelm 2009-09-30 eliminated dead code; eliminated redundant parameters;
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-07-20 wenzelm 2009-07-20 Proof.future_proof: declare all assumptions as well; Proof.future_proof: removed spurious exception_trace (which might cause crash-by-interrupt); replaced Future.fork_local by Future.fork_pri (again, until group exceptions are propagated properly);
2009-07-19 wenzelm 2009-07-19 more abstract Future.is_worker; Future.fork_local: inherit from worker (if available);
2009-06-06 wenzelm 2009-06-06 moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
2009-06-04 wenzelm 2009-06-04 exn_message/raised: ML_Compiler.exception_position;
2009-03-30 wenzelm 2009-03-30 added Toplevel.previous_node_of; keep type Toplevel.node private (formerly required in document antiquotations, which now operate on plain Toplevel.state);
2009-03-21 wenzelm 2009-03-21 restricted interrupts for tasks running as future worker thread -- attempt to prevent interrupt race conditions;
2009-03-18 wenzelm 2009-03-18 reduced verbosity;
2009-03-11 wenzelm 2009-03-11 debugging: special handling of EXCURSION_FAIL;
2009-03-10 wenzelm 2009-03-10 controlled_execution/debugging: special handling of UNDEF to prevent it to appear in exception_trace;
2009-03-09 wenzelm 2009-03-09 simplified presentation_context_of;
2009-03-08 wenzelm 2009-03-08 simplified presentation: built into transaction, pass state directly;
2009-01-16 wenzelm 2009-01-16 run_command: check theory name for init;
2009-01-15 wenzelm 2009-01-15 added run_command (from isar_document.ML); tuned;
2009-01-11 wenzelm 2009-01-11 added Goal.future_enabled abstraction -- now also checks that this is already a future task, which excludes interactive commands of the old toplevel;
2009-01-10 wenzelm 2009-01-10 added parallel_proofs flag (default true, cf. usedir option -Q), which can be disabled in low-memory situations;
2009-01-10 wenzelm 2009-01-10 excursion: commit_exit internally -- checkpoints are fully persistent now; excursion: do not force intermediate result states yet -- great performance improvement;
2009-01-07 wenzelm 2009-01-07 Proof.global_future_proof;
2009-01-07 wenzelm 2009-01-07 added local_theory';
2009-01-04 wenzelm 2009-01-04 future proofs: back to Future.fork_pri ~1 for improved parallelism;
2008-12-16 wenzelm 2008-12-16 future proofs: Future.fork_pri 1 minimizes queue length and pending promises -- slight improvement of throughput, at the cost of a bit of parallelism;
2008-12-16 wenzelm 2008-12-16 Future.fork_pri;
2008-12-11 wenzelm 2008-12-11 removed spurious exception_trace;
2008-12-11 wenzelm 2008-12-11 export context_node;
2008-12-06 wenzelm 2008-12-06 excursion: improve parallelism by not joining proofs here (depends on persistent checkpoints);
2008-12-04 wenzelm 2008-12-04 excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
2008-10-21 wenzelm 2008-10-21 added Future.enabled check;
2008-10-09 wenzelm 2008-10-09 Multithreading.enabled;
2008-10-02 wenzelm 2008-10-02 program wrapper: controlled_execution ensures proper thread attributes (global default is unsafe due to InterruptAsynch;
2008-10-02 wenzelm 2008-10-02 simplified Exn.EXCEPTIONS;
2008-10-01 wenzelm 2008-10-01 excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context; tuned;
2008-10-01 wenzelm 2008-10-01 datatype transition: internal trans field is maintained in reverse order; tuned;
2008-10-01 wenzelm 2008-10-01 renamed promise to future, tuned related interfaces;
2008-10-01 wenzelm 2008-10-01 more robust treatment of Interrupt (cf. exn.ML);
2008-09-30 wenzelm 2008-09-30 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;
2008-09-30 wenzelm 2008-09-30 export setmp_thread_position; commit_exit: position; added plain command execution; simplified command_excursion, eliminated old (present_)excursion;
2008-09-29 wenzelm 2008-09-29 LocalTheory.exit_global;
2008-09-03 wenzelm 2008-09-03 added pos_of;
2008-09-03 wenzelm 2008-09-03 simplified Toplevel.add_hook: cover successful transactions only;
2008-09-02 wenzelm 2008-09-02 added add_hook interface for post-transition hooks;
2008-08-13 wenzelm 2008-08-13 simplified present_local_theory/proof;
2008-08-12 wenzelm 2008-08-12 added ignored, malformed transitions;
2008-07-15 wenzelm 2008-07-15 support for command status;
2008-07-15 wenzelm 2008-07-15 tuned;
2008-07-15 wenzelm 2008-07-15 simplified commit_exit: operate on previous node of final state, include warning here; misc tuning;
2008-07-14 wenzelm 2008-07-14 export EXCURSION_FAIL;
2008-07-14 wenzelm 2008-07-14 eliminated internal command history -- superceeded by global Isar state (cf. isar.ML); added commit_exit; removed obsolete exception RESTART; init_theory: removed obsolete kill argument; removed obsolete undo_limit, undo_exit, kill, history; misc tuning;
2008-07-14 wenzelm 2008-07-14 replaced obsolete ProofHistory by ProofNode (backtracking only);
2008-07-08 wenzelm 2008-07-08 export str_of;
2008-07-02 wenzelm 2008-07-02 init_theory: pass name explicitly; empty transition: empty name;
2008-07-01 wenzelm 2008-07-01 added name_of; added get_id/put_id; tuned;
2008-05-24 wenzelm 2008-05-24 present_excursion: setmp_thread_position during presentation;
2008-04-10 wenzelm 2008-04-10 transaction/init: ensure stable theory (non-draft);
2008-04-10 wenzelm 2008-04-10 eliminated unused name_of, source, source_of, print', print3, three_buffersN; tuned;