# HG changeset patch # User wenzelm # Date 1283541233 -7200 # Node ID f45d332a90e306e11d9bc2cdcc1d943fb1f3db5f # Parent 9bac2f4cfd6e5b6ba65a64e015cd5ea925c16d82 pretty_goals: turned some global references and function arguments into configuration options (goals_limit = 10, goals_total = true, show_main_goal = false) depending on the context; diff -r 9bac2f4cfd6e -r f45d332a90e3 NEWS --- a/NEWS Fri Sep 03 20:39:38 2010 +0200 +++ b/NEWS Fri Sep 03 21:13:53 2010 +0200 @@ -28,18 +28,21 @@ unsynchronized references. There are both ML Config.T entities and Isar declaration attributes to access these. - ML: Isar: - - Thy_Output.display thy_output_display - Thy_Output.quotes thy_output_quotes - Thy_Output.indent thy_output_indent - Thy_Output.source thy_output_source - Thy_Output.break thy_output_break - - show_question_marks show_question_marks - show_consts show_consts - -Note that the corresponding "..._default" references in ML may be only + ML (Config.T) Isar (attribute) + + Thy_Output.display thy_output_display + Thy_Output.quotes thy_output_quotes + Thy_Output.indent thy_output_indent + Thy_Output.source thy_output_source + Thy_Output.break thy_output_break + + show_question_marks show_question_marks + show_consts show_consts + + Goal_Display.goals_limit goals_limit + Goal_Display.show_main_goal show_main_goal + +Note that corresponding "..._default" references in ML may be only changed globally at the ROOT session setup, but *not* within a theory. diff -r 9bac2f4cfd6e -r f45d332a90e3 src/HOL/Prolog/prolog.ML --- a/src/HOL/Prolog/prolog.ML Fri Sep 03 20:39:38 2010 +0200 +++ b/src/HOL/Prolog/prolog.ML Fri Sep 03 21:13:53 2010 +0200 @@ -2,7 +2,7 @@ Author: David von Oheimb (based on a lecture on Lambda Prolog by Nadathur) *) -Proof.show_main_goal := true; +Goal_Display.show_main_goal_default := true; structure Prolog = struct diff -r 9bac2f4cfd6e -r f45d332a90e3 src/HOL/Tools/Function/lexicographic_order.ML --- a/src/HOL/Tools/Function/lexicographic_order.ML Fri Sep 03 20:39:38 2010 +0200 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Fri Sep 03 21:13:53 2010 +0200 @@ -135,7 +135,8 @@ (** Error reporting **) fun pr_goals ctxt st = - Goal_Display.pretty_goals ctxt {total = true, main = false, maxgoals = Thm.nprems_of st} st + Goal_Display.pretty_goals + (Config.put Goal_Display.goals_limit (Thm.nprems_of st) ctxt) st |> Pretty.chunks |> Pretty.string_of diff -r 9bac2f4cfd6e -r f45d332a90e3 src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Sep 03 20:39:38 2010 +0200 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Sep 03 21:13:53 2010 +0200 @@ -97,7 +97,7 @@ if (nprems_of st <= i) then Seq.single st else raise Fail ("assert_tac: Numbers of subgoals mismatch at goal state :" ^ "\n" ^ Pretty.string_of (Pretty.chunks - (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st))); + (Goal_Display.pretty_goals_without_context st))); (** fundamentals **) diff -r 9bac2f4cfd6e -r f45d332a90e3 src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Fri Sep 03 20:39:38 2010 +0200 +++ b/src/Pure/Isar/attrib.ML Fri Sep 03 21:13:53 2010 +0200 @@ -393,6 +393,8 @@ val _ = Context.>> (Context.map_theory (register_config Syntax.show_question_marks_value #> + register_config Goal_Display.goals_limit_value #> + register_config Goal_Display.show_main_goal_value #> register_config Goal_Display.show_consts_value #> register_config Unify.trace_bound_value #> register_config Unify.search_bound_value #> diff -r 9bac2f4cfd6e -r f45d332a90e3 src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Fri Sep 03 20:39:38 2010 +0200 +++ b/src/Pure/Isar/isar_cmd.ML Fri Sep 03 21:13:53 2010 +0200 @@ -272,8 +272,10 @@ | set_limit r (SOME n) = r := n; fun pr (modes, (lim1, lim2)) = Toplevel.keep (fn state => - (set_limit goals_limit lim1; set_limit ProofContext.prems_limit lim2; Toplevel.quiet := false; - Print_Mode.with_modes modes (Toplevel.print_state true) state)); + (set_limit Goal_Display.goals_limit_default lim1; + set_limit ProofContext.prems_limit lim2; + Toplevel.quiet := false; + Print_Mode.with_modes modes (Toplevel.print_state true) state)); val disable_pr = Toplevel.imperative (fn () => Toplevel.quiet := true); val enable_pr = Toplevel.imperative (fn () => Toplevel.quiet := false); diff -r 9bac2f4cfd6e -r f45d332a90e3 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Fri Sep 03 20:39:38 2010 +0200 +++ b/src/Pure/Isar/proof.ML Fri Sep 03 21:13:53 2010 +0200 @@ -30,7 +30,6 @@ val assert_no_chain: state -> state val enter_forward: state -> state val goal_message: (unit -> Pretty.T) -> state -> state - val show_main_goal: bool Unsynchronized.ref val verbose: bool Unsynchronized.ref val pretty_state: int -> state -> Pretty.T list val pretty_goals: bool -> state -> Pretty.T list @@ -322,7 +321,6 @@ (** pretty_state **) -val show_main_goal = Unsynchronized.ref false; val verbose = ProofContext.verbose; fun pretty_facts _ _ NONE = [] @@ -351,8 +349,7 @@ (if mode <> Backward orelse null using then NONE else SOME using) @ [Pretty.str ("goal" ^ description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @ - Goal_Display.pretty_goals ctxt - {total = true, main = ! show_main_goal, maxgoals = ! Display.goals_limit} goal @ + Goal_Display.pretty_goals ctxt goal @ (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages)) | prt_goal NONE = []; @@ -372,10 +369,12 @@ end; fun pretty_goals main state = - let val (ctxt, (_, goal)) = get_goal state in - Goal_Display.pretty_goals ctxt - {total = false, main = main, maxgoals = ! Display.goals_limit} goal - end; + let + val (ctxt, (_, goal)) = get_goal state; + val ctxt' = ctxt + |> Config.put Goal_Display.show_main_goal main + |> Config.put Goal_Display.goals_total false; + in Goal_Display.pretty_goals ctxt' goal end; @@ -478,8 +477,7 @@ val ngoals = Thm.nprems_of goal; val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks - (Goal_Display.pretty_goals ctxt - {total = true, main = ! show_main_goal, maxgoals = ! Display.goals_limit} goal @ + (Goal_Display.pretty_goals ctxt goal @ [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")]))); val extra_hyps = Assumption.extra_hyps ctxt goal; diff -r 9bac2f4cfd6e -r f45d332a90e3 src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Fri Sep 03 20:39:38 2010 +0200 +++ b/src/Pure/ProofGeneral/preferences.ML Fri Sep 03 21:13:53 2010 +0200 @@ -126,7 +126,7 @@ bool_pref show_brackets "show-brackets" "Show full bracketing in Isabelle terms", - bool_pref Proof.show_main_goal + bool_pref Goal_Display.show_main_goal_default "show-main-goal" "Show main goal in proof state display", bool_pref Syntax.eta_contract @@ -134,7 +134,7 @@ "Print terms eta-contracted"]; val advanced_display_preferences = - [nat_pref goals_limit + [nat_pref Goal_Display.goals_limit_default "goals-limit" "Setting for maximum number of goals printed", int_pref ProofContext.prems_limit diff -r 9bac2f4cfd6e -r f45d332a90e3 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Fri Sep 03 20:39:38 2010 +0200 +++ b/src/Pure/Thy/thy_output.ML Fri Sep 03 21:13:53 2010 +0200 @@ -459,7 +459,7 @@ val _ = add_option "margin" (add_wrapper o setmp_CRITICAL Pretty.margin_default o integer); val _ = add_option "indent" (Config.put indent o integer); val _ = add_option "source" (Config.put source o boolean); -val _ = add_option "goals_limit" (add_wrapper o setmp_CRITICAL goals_limit o integer); +val _ = add_option "goals_limit" (Config.put Goal_Display.goals_limit o integer); (* basic pretty printing *) @@ -582,7 +582,7 @@ | _ => error "No proof state"); fun goal_state name main_goal = antiquotation name (Scan.succeed ()) - (fn {state, context, ...} => fn () => output context + (fn {state, context = ctxt, ...} => fn () => output ctxt [Pretty.chunks (Proof.pretty_goals main_goal (proof_state state))]); in diff -r 9bac2f4cfd6e -r f45d332a90e3 src/Pure/display.ML --- a/src/Pure/display.ML Fri Sep 03 20:39:38 2010 +0200 +++ b/src/Pure/display.ML Fri Sep 03 21:13:53 2010 +0200 @@ -7,7 +7,6 @@ signature BASIC_DISPLAY = sig - val goals_limit: int Unsynchronized.ref val show_consts_default: bool Unsynchronized.ref val show_consts: bool Config.T val show_hyps: bool Unsynchronized.ref @@ -37,7 +36,6 @@ (** options **) -val goals_limit = Goal_Display.goals_limit; val show_consts_default = Goal_Display.show_consts_default; val show_consts = Goal_Display.show_consts; diff -r 9bac2f4cfd6e -r f45d332a90e3 src/Pure/goal.ML --- a/src/Pure/goal.ML Fri Sep 03 20:39:38 2010 +0200 +++ b/src/Pure/goal.ML Fri Sep 03 21:13:53 2010 +0200 @@ -83,7 +83,10 @@ 0 => () | n => raise THM ("Proof failed.\n" ^ Pretty.string_of (Pretty.chunks - (Goal_Display.pretty_goals ctxt {total = true, main = true, maxgoals = n} th)) ^ + (Goal_Display.pretty_goals + (ctxt + |> Config.put Goal_Display.goals_limit n + |> Config.put Goal_Display.show_main_goal true) th)) ^ "\n" ^ string_of_int n ^ " unsolved goal(s)!", 0, [th])); fun finish ctxt th = (check_finished ctxt th; conclude th); diff -r 9bac2f4cfd6e -r f45d332a90e3 src/Pure/goal_display.ML --- a/src/Pure/goal_display.ML Fri Sep 03 20:39:38 2010 +0200 +++ b/src/Pure/goal_display.ML Fri Sep 03 21:13:53 2010 +0200 @@ -7,22 +7,35 @@ signature GOAL_DISPLAY = sig - val goals_limit: int Unsynchronized.ref + val goals_limit_default: int Unsynchronized.ref + val goals_limit_value: Config.value Config.T + val goals_limit: int Config.T + val goals_total: bool Config.T + val show_main_goal_default: bool Unsynchronized.ref + val show_main_goal_value: Config.value Config.T + val show_main_goal: bool Config.T val show_consts_default: bool Unsynchronized.ref val show_consts_value: Config.value Config.T val show_consts: bool Config.T val pretty_flexpair: Proof.context -> term * term -> Pretty.T - val pretty_goals: Proof.context -> {total: bool, main: bool, maxgoals: int} -> - thm -> Pretty.T list - val pretty_goals_without_context: int -> thm -> Pretty.T list + val pretty_goals: Proof.context -> thm -> Pretty.T list + val pretty_goals_without_context: thm -> Pretty.T list end; structure Goal_Display: GOAL_DISPLAY = struct -val goals_limit = Unsynchronized.ref 10; (*max number of goals to print*) +val goals_limit_default = Unsynchronized.ref 10; +val goals_limit_value = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default)); +val goals_limit = Config.int goals_limit_value; + +val goals_total = Config.bool (Config.declare "goals_total" (fn _ => Config.Bool true)); -(*true: show consts with types in proof state output*) +val show_main_goal_default = Unsynchronized.ref false; +val show_main_goal_value = + Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default)); +val show_main_goal = Config.bool show_main_goal_value; + val show_consts_default = Unsynchronized.ref false; val show_consts_value = Config.declare "show_consts" (fn _ => Config.Bool (! show_consts_default)); val show_consts = Config.bool show_consts_value; @@ -62,10 +75,14 @@ in -fun pretty_goals ctxt0 {total, main, maxgoals} state = +fun pretty_goals ctxt0 state = let val ctxt = Config.put show_free_types false ctxt0; + val show_all_types = Config.get ctxt show_all_types; + val goals_limit = Config.get ctxt goals_limit; + val goals_total = Config.get ctxt goals_total; + val show_main_goal = Config.get ctxt show_main_goal; val prt_sort = Syntax.pretty_sort ctxt; val prt_typ = Syntax.pretty_typ ctxt; @@ -105,11 +122,11 @@ val ngoals = length As; fun pretty_gs (types, sorts) = - (if main then [prt_term B] else []) @ + (if show_main_goal then [prt_term B] else []) @ (if ngoals = 0 then [Pretty.str "No subgoals!"] - else if ngoals > maxgoals then - pretty_subgoals (take maxgoals As) @ - (if total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")] + else if ngoals > goals_limit then + pretty_subgoals (take goals_limit As) @ + (if goals_total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")] else []) else pretty_subgoals As) @ pretty_ffpairs tpairs @ @@ -122,9 +139,10 @@ (! show_types orelse ! show_sorts orelse show_all_types, ! show_sorts) end; -fun pretty_goals_without_context n th = - pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th)) - {total = true, main = true, maxgoals = n} th; +fun pretty_goals_without_context th = + let val ctxt = + Config.put show_main_goal true (Syntax.init_pretty_global (Thm.theory_of_thm th)) + in pretty_goals ctxt th end; end; diff -r 9bac2f4cfd6e -r f45d332a90e3 src/Pure/tactical.ML --- a/src/Pure/tactical.ML Fri Sep 03 20:39:38 2010 +0200 +++ b/src/Pure/tactical.ML Fri Sep 03 21:13:53 2010 +0200 @@ -191,8 +191,7 @@ (*Print the current proof state and pass it on.*) fun print_tac msg st = (tracing (msg ^ "\n" ^ - Pretty.string_of (Pretty.chunks - (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st))); + Pretty.string_of (Pretty.chunks (Goal_Display.pretty_goals_without_context st))); Seq.single st); (*Pause until a line is typed -- if non-empty then fail. *) @@ -231,7 +230,7 @@ fun tracify flag tac st = if !flag andalso not (!suppress_tracing) then (tracing (Pretty.string_of (Pretty.chunks - (Goal_Display.pretty_goals_without_context (! Goal_Display.goals_limit) st @ + (Goal_Display.pretty_goals_without_context st @ [Pretty.str "** Press RETURN to continue:"]))); exec_trace_command flag (tac, st)) else tac st;