src/Pure/Isar/toplevel.ML
2010-05-15 wenzelm 2010-05-15 refer directly to structure Keyword and Parse; eliminated old-style structure aliases K and P;
2010-04-26 wenzelm 2010-04-26 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 wenzelm 2010-04-23 added keyword category "schematic goal", which prevents any attempt to fork the proof;
2010-02-18 wenzelm 2010-02-18 removed unused Theory_Target.begin; Theory_Target.init: removed Locale.intern, which was accidentally introduced in 40b3630b0deb; renamed Theory_Target.context to Theory_Target.context_cmd to emphasize that this involves Locale.intern; tuned;
2009-11-17 wenzelm 2009-11-17 init_theory: Runtime.controlled_execution for proper exception trace etc.;
2009-11-17 wenzelm 2009-11-17 implicit name space grouping for theory/local_theory transactions;
2009-11-13 wenzelm 2009-11-13 modernized structure Local_Theory;
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;