src/Pure/Isar/toplevel.ML
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 Option.app
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;
2006-11-23 ago prefer Proof.context over Context.generic;
2006-11-11 ago level: do not account for local theory blocks (relevant for document preparation);
2006-11-10 ago simplified local theory wrappers;
2006-11-09 ago LocalTheory.restore;
2006-11-07 ago removed obsolete print_state_hook;
2006-11-04 ago removed checkpoint interface;
2006-10-12 ago renamed enter_forward_proof to enter_proof_body;
2006-10-11 ago exit_local_theory: pass interactive flag;
2006-10-11 ago added type global_theory -- theory or local_theory;
2006-10-09 ago loop: disallow exit in secure mode;