src/Pure/Isar/toplevel.ML
2007-11-02 haftmann 2007-11-02 clarified theory target interface
2007-10-28 wenzelm 2007-10-28 safe_exit: controlled_execution;
2007-10-09 wenzelm 2007-10-09 TheoryTarget.init_cmd;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-10-01 wenzelm 2007-10-01 print_state_context: local theory context, not proof context; context_position: cover Theory case as well (requires additional checkpoint);
2007-09-30 wenzelm 2007-09-30 local_theory transactions: more careful treatment of context position;
2007-09-18 wenzelm 2007-09-18 simplified PrintMode interfaces;
2007-08-28 berghofe 2007-08-28 Added local_theory_to_proof'
2007-08-16 wenzelm 2007-08-16 global state transformation: non-critical, but also non-thread-safe;
2007-07-29 wenzelm 2007-07-29 NAMED_CRITICAL;
2007-07-29 wenzelm 2007-07-29 added TOPLEVEL_ERROR (simplified version from output.ML);
2007-07-24 wenzelm 2007-07-24 *** empty log message ***
2007-07-24 wenzelm 2007-07-24 moved exception capture/release to structure Exn;
2007-07-23 wenzelm 2007-07-23 marked some CRITICAL sections; eliminated transform_failure (to avoid critical section for main transactions); removed unused exceptions MetaSimplifier.SIMPROC_FAIL, Attrib.ATTRIB_FAIL, Method.METHOD_FAIL, Antiquote.ANTIQUOTE_FAIL;
2007-07-22 wenzelm 2007-07-22 init_empty: invoke operation *after* safe_exit;
2007-07-10 wenzelm 2007-07-10 Markup.enclose;
2007-07-10 wenzelm 2007-07-10 Markup.output; removed no_state markup -- produce empty state;
2007-07-09 wenzelm 2007-07-09 prompt: plain string, not output;
2007-07-08 wenzelm 2007-07-08 simplified/more robust print_state; more robust prompt markup;
2007-07-07 wenzelm 2007-07-07 toplevel prompt/print_state: proper markup, removed hooks; tuned;
2007-07-07 wenzelm 2007-07-07 tuned;
2007-06-19 wenzelm 2007-06-19 oops -- fixed profiling;
2007-06-19 wenzelm 2007-06-19 profiling: observe no_timing;
2007-06-13 wenzelm 2007-06-13 transaction: context_position (non-destructive only);
2007-04-04 wenzelm 2007-04-04 removed unused info channel;
2007-01-20 wenzelm 2007-01-20 Toplevel.debug: coincide with Output.debugging;
2007-01-19 wenzelm 2007-01-19 moved ML context stuff to from Context to ML_Context;
2007-01-19 wenzelm 2007-01-19 added generic_theory_of; adapted ML context operations;
2007-01-10 wenzelm 2007-01-10 fixed exit: proper type check of state; tuned signature;
2007-01-05 wenzelm 2007-01-05 removed Toplevel.print_exn hook -- existing error_msg_fn does the job;
2007-01-04 haftmann 2007-01-04 eliminated Option.app
2007-01-03 aspinall 2007-01-03 Expose command failure recovery code for top level.
2006-12-30 wenzelm 2006-12-30 removed conditional combinator;
2006-12-30 wenzelm 2006-12-30 refined notion of empty toplevel, admits undo of 'end'; added undo_exit, init_empty, init_state; removed unused toplevel, reset; tuned;
2006-12-15 wenzelm 2006-12-15 removed obsolete assert;
2006-11-23 wenzelm 2006-11-23 prefer Proof.context over Context.generic;
2006-11-11 wenzelm 2006-11-11 level: do not account for local theory blocks (relevant for document preparation);
2006-11-10 wenzelm 2006-11-10 simplified local theory wrappers;
2006-11-09 wenzelm 2006-11-09 LocalTheory.restore;
2006-11-07 wenzelm 2006-11-07 removed obsolete print_state_hook;
2006-11-04 wenzelm 2006-11-04 removed checkpoint interface; moved back to copy/checkpoint instead of checkpoint/checkpoint (NB 1: checkpoint is idempotent, i.e. impure data is being shared, which is inappropriate; NB 2: copying a checkpoint always produces a related theory); present_proof: proper treatment of history; tuned;
2006-10-12 wenzelm 2006-10-12 renamed enter_forward_proof to enter_proof_body; renamed exit_local_theory to end_local_theory; added local_theory_to_proof; tuned;
2006-10-11 wenzelm 2006-10-11 exit_local_theory: pass interactive flag; begin_local_theory: generic init;
2006-10-11 wenzelm 2006-10-11 added type global_theory -- theory or local_theory; added begin/exit_local_theory; removed theory_context; renamed body_context_node to presentation_context; removed copy (checkpoint twice instead -- avoids unrelated theories);
2006-10-09 wenzelm 2006-10-09 loop: disallow exit in secure mode;
2006-10-07 wenzelm 2006-10-07 TheoryTarget;
2006-09-21 wenzelm 2006-09-21 member (op =);
2006-08-09 wenzelm 2006-08-09 global goals/qeds: after_qed operates on Proof.context (potentially local_theory);
2006-07-14 wenzelm 2006-07-14 keep/transaction: unified execution model (with debugging etc.); tuned;
2006-07-04 wenzelm 2006-07-04 skip_proofs: do not skip proofs of schematic goals (warning);
2006-06-11 wenzelm 2006-06-11 avoid unqualified exception;
2006-05-02 wenzelm 2006-05-02 handle exception SYS_ERROR;
2006-02-17 wenzelm 2006-02-17 checkpoint/copy_node: reset body context;
2006-02-15 wenzelm 2006-02-15 added cases_node; replaced body_context_of by body_context_node, removed no_body_context; copy: ProofContext.transfer; added present_local_theory, present_proof; removed internal command interface;
2006-02-06 wenzelm 2006-02-06 added local_theory, with optional locale xname;
2006-01-27 wenzelm 2006-01-27 swapped theory_context;
2006-01-19 wenzelm 2006-01-19 keep: disable Output.toplevel_errors; program: Output.ML_errors;
2006-01-14 wenzelm 2006-01-14 sane ERROR vs. TOPLEVEL_ERROR handling; added program;
2006-01-13 wenzelm 2006-01-13 removed obsolete sign_of;
2006-01-10 wenzelm 2006-01-10 added context_of -- generic context;