src/Pure/Isar/toplevel.ML
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;
2006-01-06 wenzelm 2006-01-06 transactions now always see quasi-functional intermediate checkpoint; removed obsolete theory_theory_to_proof; added
2006-01-05 wenzelm 2006-01-05 hide type datatype node; added theory_node, proof_node, is_theory, is_proof, proof_position_of, checkpoint, copy; no_body_context: no history; transaction: test save = true;
2006-01-04 wenzelm 2006-01-04 added theory_to_theory_to_proof, which may change theory before entering the proof; added forget_proof (from isar_thy.ML);
2006-01-04 wenzelm 2006-01-04 tuned;
2005-10-18 wenzelm 2005-10-18 simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
2005-09-20 wenzelm 2005-09-20 get_interrupt: special handling of IO.io now in ML-Systems/smlnj-basis-compat.ML;
2005-09-20 paulson 2005-09-20 uniform handling of interrupts
2005-09-17 wenzelm 2005-09-17 theory_to_proof: check theory of initial proof state, which must not be changed;
2005-09-16 paulson 2005-09-16 catching exception Io
2005-09-13 wenzelm 2005-09-13 added three_buffersN, print3; tuned theory_to_proof: plain Proof.state instead of history; added EXCEPTION; removed DATA_FAIL, TRANSLATION_FAIL;
2005-09-12 wenzelm 2005-09-12 added interact flag to control mode of excursions;
2005-09-11 wenzelm 2005-09-11 excursion: interactive if debug;
2005-09-05 wenzelm 2005-09-05 added assert, command;
2005-08-31 wenzelm 2005-08-31 added no_body_context;
2005-08-18 wenzelm 2005-08-18 proof_to_theory_context: interaction flag;
2005-08-16 wenzelm 2005-08-16 state: body context; added theory_context, proof_to_theory_context; added is_proof, level; turned excursion_result into present_excursion;
2005-07-13 wenzelm 2005-07-13 added print_state_hook; renamed proof'' to actual_proof; tuned;
2005-07-06 wenzelm 2005-07-06 debug: exception_trace; tuned;
2005-07-04 wenzelm 2005-07-04 tuned;
2005-07-01 wenzelm 2005-07-01 added profile flag;
2005-06-29 wenzelm 2005-06-29 added print': print depending on print_mode;
2005-06-20 wenzelm 2005-06-20 tuned;
2005-06-17 wenzelm 2005-06-17 Context.DATA_FAIL; accomodate identification of type Sign.sg and theory;
2005-06-02 wenzelm 2005-06-02 tuned msgs; exn_message: added Fail; timing: info channel;
2005-05-23 wenzelm 2005-05-23 node_trans: revert to original transaction code (pre 1.54);
2005-05-17 wenzelm 2005-05-17 tuned;
2005-04-07 wenzelm 2005-04-07 improved exn_message;
2005-03-26 paulson 2005-03-26 new display of theory stamps
2005-03-10 ballarin 2005-03-10 Registrations of global locale interpretations: improved, better naming.
2005-03-09 ballarin 2005-03-09 First version of global registration command.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-23 berghofe 2005-02-23 Modified node_trans to avoid duplication of signature stamps when undoing.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-02-10 ballarin 2005-02-10 Toplevel.debug for debugging in Isar.
2005-01-11 berghofe 2005-01-11 excursion_result now also passes previous state to presentation functions. This is useful for hiding proof scripts.