# HG changeset patch # User wenzelm # Date 1120489699 -7200 # Node ID 154a84e1a4f78a0e4d89ff607e772d8806e1e023 # Parent d54dfd724b3552a930b42a2a12442597aae16286 tuned; diff -r d54dfd724b35 -r 154a84e1a4f7 src/Pure/Isar/toplevel.ML --- a/src/Pure/Isar/toplevel.ML Mon Jul 04 17:07:15 2005 +0200 +++ b/src/Pure/Isar/toplevel.ML Mon Jul 04 17:08:19 2005 +0200 @@ -27,9 +27,13 @@ val context_of: state -> Proof.context val proof_of: state -> Proof.state val enter_forward_proof: state -> Proof.state - type transition + val quiet: bool ref + val debug: bool ref + val timing: bool ref + val profiling: int ref exception TERMINATE exception RESTART + type transition val undo_limit: bool -> int option val empty: transition val name_of: transition -> string @@ -65,9 +69,6 @@ val unknown_theory: transition -> transition val unknown_proof: transition -> transition val unknown_context: transition -> transition - val quiet: bool ref - val debug: bool ref - val profiling: int ref val exn_message: exn -> string val apply: bool -> transition -> state -> (state * (exn * string) option) option val excursion_result: ((transition * (state -> state -> 'a -> 'a)) list * 'a) -> 'a @@ -180,6 +181,11 @@ (** toplevel transitions **) +val quiet = ref false; +val debug = ref false; +val timing = Output.timing; +val profiling = ref 0; + exception TERMINATE; exception RESTART; exception EXCURSION_FAIL of exn * string; @@ -420,11 +426,6 @@ (** toplevel transactions **) -val quiet = ref false; -val debug = ref false; -val profiling = ref 0; - - (* print exceptions *) local @@ -495,12 +496,15 @@ fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state = let - val _ = - if int orelse not int_only then () - else warning (command_msg "Interactive-only " tr); + val _ = conditional (not int andalso int_only) (fn () => + warning (command_msg "Interactive-only " tr)); + + fun do_timing f x = (info (command_msg "" tr); timeap f x); + fun do_profiling f x = profile (! profiling) f x; + val (result, opt_exn) = - (if ! Output.timing andalso not no_timing then (info (command_msg "" tr); timeap) else I) - (profile (! profiling) (apply_trans int trans)) state; + (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I) + ((if ! profiling > 0 then do_profiling else I) (apply_trans int trans)) state; val _ = conditional (int andalso not (! quiet) andalso exists (fn m => m mem_string print) ("" :: ! print_mode)) (fn () => print_state false result); diff -r d54dfd724b35 -r 154a84e1a4f7 src/Pure/drule.ML --- a/src/Pure/drule.ML Mon Jul 04 17:07:15 2005 +0200 +++ b/src/Pure/drule.ML Mon Jul 04 17:08:19 2005 +0200 @@ -155,24 +155,23 @@ struct -(** some cterm->cterm operations: much faster than calling cterm_of! **) +(** some cterm->cterm operations: faster than calling cterm_of! **) -(** SAME NAMES as in structure Logic: use compound identifiers! **) +(* FIXME exception CTERM (!?) *) -(*dest_implies for cterms. Note T=prop below*) fun dest_implies ct = - case term_of ct of - (Const("==>", _) $ _ $ _) => - let val (ct1,ct2) = Thm.dest_comb ct - in (#2 (Thm.dest_comb ct1), ct2) end - | _ => raise TERM ("dest_implies", [term_of ct]) ; + (case Thm.term_of ct of + (Const ("==>", _) $ _ $ _) => + let val (ct1, ct2) = Thm.dest_comb ct + in (#2 (Thm.dest_comb ct1), ct2) end + | _ => raise TERM ("dest_implies", [term_of ct])); fun dest_equals ct = - case term_of ct of - (Const("==", _) $ _ $ _) => - let val (ct1,ct2) = Thm.dest_comb ct - in (#2 (Thm.dest_comb ct1), ct2) end - | _ => raise TERM ("dest_equals", [term_of ct]) ; + (case Thm.term_of ct of + (Const ("==", _) $ _ $ _) => + let val (ct1, ct2) = Thm.dest_comb ct + in (#2 (Thm.dest_comb ct1), ct2) end + | _ => raise TERM ("dest_equals", [term_of ct])); (* A1==>...An==>B goes to [A1,...,An], where B is not an implication *) @@ -729,7 +728,7 @@ let val p as (ct1, ct2) = Thm.dest_comb ct in (case pairself term_of p of (Const ("all", _), Abs (s, _, _)) => - let val (v, ct') = Thm.dest_abs (SOME "@") ct2; + let val (v, ct') = Thm.dest_abs (SOME (gensym "all_")) ct2; in Thm.combination (Thm.reflexive ct1) (Thm.abstract_rule s v (forall_conv cv ct')) end