src/Pure/Isar/toplevel.ML
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;
2008-04-10 wenzelm 2008-04-10 made purely value-oriented, moved global state to structure Isar (cf. isar.ML); export toplevel, error_msg (formerly print_exn), transition (formerly apply); moved type isar to structure OuterSyntax; moved crashes to structure Isar;
2008-03-29 wenzelm 2008-03-29 added generic_theory transaction;
2008-03-15 wenzelm 2008-03-15 tuned;
2008-03-11 wenzelm 2008-03-11 raw_loop: more graceful crash recovery;
2008-03-11 wenzelm 2008-03-11 added exception CONTEXT, indicating context of another exception; exn_message: explicit context, *not* ML_Context.get_context; toplevel_error/apply: explicit exn_context; explicit Markup.location for exn_info (cf. at_command); fixed spelling; tuned;
2008-02-16 wenzelm 2008-02-16 exn_message: added TimeLimit.TimeOut; replaced ignore/raise_interrupt by more flexible (un)interruptible combinators;
2008-01-24 wenzelm 2008-01-24 removed unused properties; replaced ContextPosition by Position.thread_data;
2008-01-06 wenzelm 2008-01-06 removed obsolete prompt markup;
2008-01-03 wenzelm 2008-01-03 replaced thread_properties by simplified version in position.ML;
2008-01-03 wenzelm 2008-01-03 toplevel print_exn: proper setmp_thread_properties;
2008-01-03 wenzelm 2008-01-03 maintain thread transition properties;
2008-01-02 wenzelm 2008-01-02 type transition: added properties field;
2007-12-08 wenzelm 2007-12-08 Isar loop: recover after toplevel crashes;
2007-12-06 wenzelm 2007-12-06 replaced Markup.enclose by Markup.markup, which operates on plain strings instead of raw output;
2007-12-04 wenzelm 2007-12-04 Toplevel.loop: explicit argument for secure loop, no warning on quit;
2007-11-18 wenzelm 2007-11-18 init_empty: check before change (avoids non-linear update);
2007-11-05 wenzelm 2007-11-05 simplified LocalTheory.reinit; tuned;
2007-11-02 haftmann 2007-11-02 clarified theory target interface