# HG changeset patch # User wenzelm # Date 1305210193 -7200 # Node ID 0bbb5686709179a174b57aacf248054363a4f546 # Parent 45eb6829dde2db4a506e04d2b1588e65348b2217 proper configuration options Proof_Context.debug and Proof_Context.verbose; discontinued alias Proof.verbose = Proof_Context.verbose; diff -r 45eb6829dde2 -r 0bbb56867091 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Thu May 12 16:00:48 2011 +0200 +++ b/src/Pure/Isar/proof.ML Thu May 12 16:23:13 2011 +0200 @@ -31,7 +31,6 @@ val assert_no_chain: state -> state val enter_forward: state -> state val goal_message: (unit -> Pretty.T) -> state -> state - val verbose: bool Unsynchronized.ref val pretty_state: int -> state -> Pretty.T list val pretty_goals: bool -> state -> Pretty.T list val refine: Method.text -> state -> state Seq.seq @@ -324,8 +323,6 @@ (** pretty_state **) -val verbose = Proof_Context.verbose; - fun pretty_facts _ _ NONE = [] | pretty_facts s ctxt (SOME ths) = [Pretty.big_list (s ^ "this:") (map (Display.pretty_thm ctxt) ths), Pretty.str ""]; @@ -333,6 +330,7 @@ fun pretty_state nr state = let val {context = ctxt, facts, mode, goal = _} = current state; + val verbose = Config.get ctxt Proof_Context.verbose; fun levels_up 0 = "" | levels_up 1 = "1 level up" @@ -357,15 +355,15 @@ | prt_goal NONE = []; val prt_ctxt = - if ! verbose orelse mode = Forward then Proof_Context.pretty_context ctxt + if verbose orelse mode = Forward then Proof_Context.pretty_context ctxt else if mode = Backward then Proof_Context.pretty_ctxt ctxt else []; in [Pretty.str ("proof (" ^ mode_name mode ^ "): step " ^ string_of_int nr ^ - (if ! verbose then ", depth " ^ string_of_int (level state div 2 - 1) else "")), + (if verbose then ", depth " ^ string_of_int (level state div 2 - 1) else "")), Pretty.str ""] @ (if null prt_ctxt then [] else prt_ctxt @ [Pretty.str ""]) @ - (if ! verbose orelse mode = Forward then + (if verbose orelse mode = Forward then pretty_facts "" ctxt facts @ prt_goal (try find_goal state) else if mode = Chain then pretty_facts "picking " ctxt facts else prt_goal (try find_goal state)) diff -r 45eb6829dde2 -r 0bbb56867091 src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu May 12 16:00:48 2011 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu May 12 16:23:13 2011 +0200 @@ -151,8 +151,8 @@ val print_binds: Proof.context -> unit val print_lthms: Proof.context -> unit val print_cases: Proof.context -> unit - val debug: bool Unsynchronized.ref - val verbose: bool Unsynchronized.ref + val debug: bool Config.T + val verbose: bool Config.T val pretty_ctxt: Proof.context -> Pretty.T list val pretty_context: Proof.context -> Pretty.T list end; @@ -1235,11 +1235,11 @@ (* core context *) -val debug = Unsynchronized.ref false; -val verbose = Unsynchronized.ref false; +val debug = Config.bool (Config.declare "Proof_Context.debug" (K (Config.Bool false))); +val verbose = Config.bool (Config.declare "Proof_Context.verbose" (K (Config.Bool false))); fun pretty_ctxt ctxt = - if not (! debug) then [] + if not (Config.get ctxt debug) then [] else let val prt_term = Syntax.pretty_term ctxt; @@ -1275,8 +1275,8 @@ fun pretty_context ctxt = let - val is_verbose = ! verbose; - fun verb f x = if is_verbose then f (x ()) else []; + val verbose = Config.get ctxt verbose; + fun verb f x = if verbose then f (x ()) else []; val prt_term = Syntax.pretty_term ctxt; val prt_typ = Syntax.pretty_typ ctxt; diff -r 45eb6829dde2 -r 0bbb56867091 src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Thu May 12 16:00:48 2011 +0200 +++ b/src/Pure/Isar/proof_display.ML Thu May 12 16:23:13 2011 +0200 @@ -27,7 +27,7 @@ (* toplevel pretty printing *) fun pp_context ctxt = - (if ! Proof_Context.debug then + (if Config.get ctxt Proof_Context.debug then Pretty.quote (Pretty.big_list "proof context:" (Proof_Context.pretty_context ctxt)) else Pretty.str "");