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;
2007-06-19 ago profiling: observe no_timing;
2007-06-13 ago transaction: context_position (non-destructive only);
2007-04-04 ago removed unused info channel;
2007-01-20 ago Toplevel.debug: coincide with Output.debugging;
2007-01-19 ago moved ML context stuff to from Context to ML_Context;
2007-01-19 ago added generic_theory_of;
2007-01-10 ago fixed exit: proper type check of state;
2007-01-05 ago removed Toplevel.print_exn hook -- existing error_msg_fn does the job;
2007-01-04 ago eliminated
2007-01-03 ago Expose command failure recovery code for top level.
2006-12-30 ago removed conditional combinator;
2006-12-30 ago refined notion of empty toplevel, admits undo of 'end';
2006-12-15 ago removed obsolete assert;