# HG changeset patch # User wenzelm # Date 1368456059 -7200 # Node ID 4ccc75f17bb7c1494c4a5d41ec35e99edd1d628c # Parent 68c163598f07e0754dd4421d28f53dccffc19cc2# Parent 61ac1efe02c30ffdba99cdd5dd05079905e65b20 merged diff -r 68c163598f07 -r 4ccc75f17bb7 etc/options --- a/etc/options Mon May 13 15:22:19 2013 +0200 +++ b/etc/options Mon May 13 16:40:59 2013 +0200 @@ -14,6 +14,9 @@ option document_graph : bool = false -- "generate session graph image for document" +option goals_limit : int = 10 + -- "maximum number of subgoals to be printed" + option show_question_marks : bool = true -- "show leading question mark of schematic variables" diff -r 68c163598f07 -r 4ccc75f17bb7 src/Doc/IsarRef/Document_Preparation.thy --- a/src/Doc/IsarRef/Document_Preparation.thy Mon May 13 15:22:19 2013 +0200 +++ b/src/Doc/IsarRef/Document_Preparation.thy Mon May 13 16:40:59 2013 +0200 @@ -358,7 +358,7 @@ or indentation for pretty printing of display material. \item @{antiquotation_option_def goals_limit}~@{text "= nat"} - determines the maximum number of goals to be printed (for goal-based + determines the maximum number of subgoals to be printed (for goal-based antiquotation). \item @{antiquotation_option_def source}~@{text "= bool"} prints the diff -r 68c163598f07 -r 4ccc75f17bb7 src/Doc/IsarRef/Inner_Syntax.thy --- a/src/Doc/IsarRef/Inner_Syntax.thy Mon May 13 15:22:19 2013 +0200 +++ b/src/Doc/IsarRef/Inner_Syntax.thy Mon May 13 16:40:59 2013 +0200 @@ -213,7 +213,7 @@ might look at terms more discretely. \item @{attribute goals_limit} controls the maximum number of - subgoals to be shown in goal output. + subgoals to be printed. \item @{attribute show_main_goal} controls whether the main result to be proven should be displayed. This information might be diff -r 68c163598f07 -r 4ccc75f17bb7 src/HOL/Tools/Function/lexicographic_order.ML --- a/src/HOL/Tools/Function/lexicographic_order.ML Mon May 13 15:22:19 2013 +0200 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Mon May 13 16:40:59 2013 +0200 @@ -120,22 +120,21 @@ (** Error reporting **) -fun pr_goals ctxt st = - Pretty.string_of - (Goal_Display.pretty_goal - {main = Config.get ctxt Goal_Display.show_main_goal, limit = false} ctxt st) - fun row_index i = chr (i + 97) (* FIXME not scalable wrt. chr range *) fun col_index j = string_of_int (j + 1) (* FIXME not scalable wrt. table layout *) fun pr_unprovable_cell _ ((i,j), Less _) = [] | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) = - ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st] + ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ + Goal_Display.string_of_goal ctxt st] | pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) = - ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less ^ - "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq] + ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ + Goal_Display.string_of_goal ctxt st_less ^ + "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ + Goal_Display.string_of_goal ctxt st_leq] | pr_unprovable_cell ctxt ((i,j), False st) = - ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st] + ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ + Goal_Display.string_of_goal ctxt st] fun pr_unprovable_subgoals ctxt table = table diff -r 68c163598f07 -r 4ccc75f17bb7 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Mon May 13 15:22:19 2013 +0200 +++ b/src/Pure/Isar/isar_syn.ML Mon May 13 16:40:59 2013 +0200 @@ -975,7 +975,7 @@ Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)" (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) => Toplevel.keep (fn state => - (case limit of NONE => () | SOME n => Goal_Display.goals_limit_default := n; + (case limit of NONE => () | SOME n => Options.default_put_int "goals_limit" n; Toplevel.quiet := false; Print_Mode.with_modes modes (Toplevel.print_state true) state)))); diff -r 68c163598f07 -r 4ccc75f17bb7 src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Mon May 13 15:22:19 2013 +0200 +++ b/src/Pure/Isar/proof_display.ML Mon May 13 16:40:59 2013 +0200 @@ -105,8 +105,7 @@ end; fun string_of_goal ctxt goal = - Pretty.string_of (Pretty.chunks - [pretty_goal_header goal, Goal_Display.pretty_goal {main = true, limit = false} ctxt goal]); + Pretty.string_of (Pretty.chunks [pretty_goal_header goal, Goal_Display.pretty_goal ctxt goal]); (* goal facts *) diff -r 68c163598f07 -r 4ccc75f17bb7 src/Pure/ProofGeneral/preferences.ML --- a/src/Pure/ProofGeneral/preferences.ML Mon May 13 15:22:19 2013 +0200 +++ b/src/Pure/ProofGeneral/preferences.ML Mon May 13 16:40:59 2013 +0200 @@ -159,9 +159,9 @@ "Print terms eta-contracted"]; val advanced_display_preferences = - [nat_pref Goal_Display.goals_limit_default + [options_pref "goals_limit" "goals-limit" - "Setting for maximum number of goals printed", + "Setting for maximum number of subgoals to be printed", print_depth_pref, options_pref "show_question_marks" "show-question-marks" diff -r 68c163598f07 -r 4ccc75f17bb7 src/Pure/Thy/thy_output.ML --- a/src/Pure/Thy/thy_output.ML Mon May 13 15:22:19 2013 +0200 +++ b/src/Pure/Thy/thy_output.ML Mon May 13 16:40:59 2013 +0200 @@ -612,7 +612,8 @@ fun goal_state name main = antiquotation name (Scan.succeed ()) (fn {state, context = ctxt, ...} => fn () => output ctxt - [Goal_Display.pretty_goal {main = main, limit = true} ctxt (proof_state state)]); + [Goal_Display.pretty_goal + (Config.put Goal_Display.show_main_goal main ctxt) (proof_state state)]); in diff -r 68c163598f07 -r 4ccc75f17bb7 src/Pure/goal.ML --- a/src/Pure/goal.ML Mon May 13 15:22:19 2013 +0200 +++ b/src/Pure/goal.ML Mon May 13 16:40:59 2013 +0200 @@ -97,8 +97,7 @@ fun check_finished ctxt th = if Thm.no_prems th then th else - raise THM ("Proof failed.\n" ^ - Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt th), 0, [th]); + raise THM ("Proof failed.\n" ^ Pretty.string_of (Goal_Display.pretty_goal ctxt th), 0, [th]); fun finish ctxt = check_finished ctxt #> conclude; diff -r 68c163598f07 -r 4ccc75f17bb7 src/Pure/goal_display.ML --- a/src/Pure/goal_display.ML Mon May 13 15:22:19 2013 +0200 +++ b/src/Pure/goal_display.ML Mon May 13 16:40:59 2013 +0200 @@ -7,10 +7,8 @@ signature GOAL_DISPLAY = sig - val goals_limit_default: int Unsynchronized.ref val goals_limit_raw: Config.raw val goals_limit: int Config.T - val goals_total: bool Config.T val show_main_goal_default: bool Unsynchronized.ref val show_main_goal_raw: Config.raw val show_main_goal: bool Config.T @@ -20,18 +18,16 @@ val pretty_flexpair: Proof.context -> term * term -> Pretty.T val pretty_goals: Proof.context -> thm -> Pretty.T list val pretty_goals_without_context: thm -> Pretty.T list - val pretty_goal: {main: bool, limit: bool} -> Proof.context -> thm -> Pretty.T + val pretty_goal: Proof.context -> thm -> Pretty.T + val string_of_goal: Proof.context -> thm -> string end; structure Goal_Display: GOAL_DISPLAY = struct -val goals_limit_default = Unsynchronized.ref 10; -val goals_limit_raw = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default)); +val goals_limit_raw = Config.declare_option "goals_limit"; val goals_limit = Config.int goals_limit_raw; -val goals_total = Config.bool (Config.declare "goals_total" (fn _ => Config.Bool true)); - val show_main_goal_default = Unsynchronized.ref false; val show_main_goal_raw = Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default)); @@ -91,7 +87,6 @@ val show_consts = Config.get ctxt show_consts val show_main_goal = Config.get ctxt show_main_goal; val goals_limit = Config.get ctxt goals_limit; - val goals_total = Config.get ctxt goals_total; val prt_sort = Syntax.pretty_sort ctxt; val prt_typ = Syntax.pretty_typ ctxt; @@ -134,8 +129,7 @@ (if ngoals = 0 then [Pretty.str "No 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 []) + [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")] else pretty_subgoals As) @ pretty_ffpairs tpairs @ (if show_consts then pretty_consts prop else []) @ @@ -148,12 +142,8 @@ Config.put show_main_goal true (Syntax.init_pretty_global (Thm.theory_of_thm th)) in pretty_goals ctxt th end; -fun pretty_goal {main, limit} ctxt th = - Pretty.chunks (pretty_goals - (ctxt - |> Config.put show_main_goal main - |> not limit ? Config.put goals_limit (Thm.nprems_of th) - |> Config.put goals_total false) th); +val pretty_goal = Pretty.chunks oo pretty_goals; +val string_of_goal = Pretty.string_of oo pretty_goal; end;