src/Pure/Isar/toplevel.ML
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.
2004-10-11 berghofe 2004-10-11 Some changes to allow skipping of proof scripts.
2004-06-21 wenzelm 2004-06-21 added >>> : transition list -> unit;
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-12 wenzelm 2004-06-12 added name_of, source_of, source;
2004-05-29 wenzelm 2004-05-29 Output.timing;
2003-07-07 nipkow 2003-07-07 A patch by david aspinall
2002-08-08 wenzelm 2002-08-08 exception SIMPROC_FAIL: solid error reporting of simprocs;
2002-02-28 wenzelm 2002-02-28 use ignore_interrupt, raise_interrupt;
2002-02-12 wenzelm 2002-02-12 ANTIQUOTE_FAIL;
2001-12-08 wenzelm 2001-12-08 tuned print_state interfaces;
2001-11-28 wenzelm 2001-11-28 added proof_to_theory';
2001-11-04 wenzelm 2001-11-04 simplified Proof.init_state:
2001-10-31 wenzelm 2001-10-31 Proof.init_state thy None;
2001-10-22 wenzelm 2001-10-22 Display.current_goals_markers;