src/Pure/Isar/toplevel.ML
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;
2008-04-10 ago made purely value-oriented, moved global state to structure Isar (cf. isar.ML);
2008-03-29 ago added generic_theory transaction;
2008-03-15 ago tuned;
2008-03-11 ago raw_loop: more graceful crash recovery;
2008-03-11 ago added exception CONTEXT, indicating context of another exception;
2008-02-16 ago exn_message: added TimeLimit.TimeOut;
2008-01-24 ago removed unused properties;
2008-01-06 ago removed obsolete prompt markup;
2008-01-03 ago replaced thread_properties by simplified version in position.ML;
2008-01-03 ago toplevel print_exn: proper setmp_thread_properties;
2008-01-03 ago maintain thread transition properties;
2008-01-02 ago type transition: added properties field;
2007-12-08 ago Isar loop: recover after toplevel crashes;
2007-12-06 ago replaced Markup.enclose by Markup.markup, which operates on plain strings instead of raw output;
2007-12-04 ago Toplevel.loop: explicit argument for secure loop, no warning on quit;
2007-11-18 ago init_empty: check before change (avoids non-linear update);
2007-11-05 ago simplified LocalTheory.reinit;
2007-11-02 ago clarified theory target interface
2007-10-28 ago safe_exit: controlled_execution;
2007-10-09 ago TheoryTarget.init_cmd;
2007-10-09 ago generic Syntax.pretty/string_of operations;
2007-10-01 ago print_state_context: local theory context, not proof context;
2007-09-30 ago local_theory transactions: more careful treatment of context position;
2007-09-18 ago simplified PrintMode interfaces;
2007-08-28 ago Added local_theory_to_proof'
2007-08-16 ago global state transformation: non-critical, but also non-thread-safe;
2007-07-29 ago NAMED_CRITICAL;
2007-07-29 ago added TOPLEVEL_ERROR (simplified version from output.ML);
2007-07-24 ago *** empty log message ***
2007-07-24 ago moved exception capture/release to structure Exn;
2007-07-23 ago marked some CRITICAL sections;
2007-07-22 ago init_empty: invoke operation *after* safe_exit;
2007-07-10 ago Markup.enclose;
2007-07-10 ago Markup.output;
2007-07-09 ago prompt: plain string, not output;
2007-07-08 ago simplified/more robust print_state;
2007-07-07 ago toplevel prompt/print_state: proper markup, removed hooks;
2007-07-07 ago tuned;
2007-06-19 ago oops -- fixed profiling;