1.1 --- a/etc/options Mon May 13 15:22:19 2013 +0200
1.2 +++ b/etc/options Mon May 13 16:40:59 2013 +0200
1.3 @@ -14,6 +14,9 @@
1.4 option document_graph : bool = false
1.5 -- "generate session graph image for document"
1.6
1.7 +option goals_limit : int = 10
1.8 + -- "maximum number of subgoals to be printed"
1.9 +
1.10 option show_question_marks : bool = true
1.11 -- "show leading question mark of schematic variables"
1.12
2.1 --- a/src/Doc/IsarRef/Document_Preparation.thy Mon May 13 15:22:19 2013 +0200
2.2 +++ b/src/Doc/IsarRef/Document_Preparation.thy Mon May 13 16:40:59 2013 +0200
2.3 @@ -358,7 +358,7 @@
2.4 or indentation for pretty printing of display material.
2.5
2.6 \item @{antiquotation_option_def goals_limit}~@{text "= nat"}
2.7 - determines the maximum number of goals to be printed (for goal-based
2.8 + determines the maximum number of subgoals to be printed (for goal-based
2.9 antiquotation).
2.10
2.11 \item @{antiquotation_option_def source}~@{text "= bool"} prints the
3.1 --- a/src/Doc/IsarRef/Inner_Syntax.thy Mon May 13 15:22:19 2013 +0200
3.2 +++ b/src/Doc/IsarRef/Inner_Syntax.thy Mon May 13 16:40:59 2013 +0200
3.3 @@ -213,7 +213,7 @@
3.4 might look at terms more discretely.
3.5
3.6 \item @{attribute goals_limit} controls the maximum number of
3.7 - subgoals to be shown in goal output.
3.8 + subgoals to be printed.
3.9
3.10 \item @{attribute show_main_goal} controls whether the main result
3.11 to be proven should be displayed. This information might be
4.1 --- a/src/HOL/Tools/Function/lexicographic_order.ML Mon May 13 15:22:19 2013 +0200
4.2 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Mon May 13 16:40:59 2013 +0200
4.3 @@ -120,22 +120,21 @@
4.4
4.5 (** Error reporting **)
4.6
4.7 -fun pr_goals ctxt st =
4.8 - Pretty.string_of
4.9 - (Goal_Display.pretty_goal
4.10 - {main = Config.get ctxt Goal_Display.show_main_goal, limit = false} ctxt st)
4.11 -
4.12 fun row_index i = chr (i + 97) (* FIXME not scalable wrt. chr range *)
4.13 fun col_index j = string_of_int (j + 1) (* FIXME not scalable wrt. table layout *)
4.14
4.15 fun pr_unprovable_cell _ ((i,j), Less _) = []
4.16 | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) =
4.17 - ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st]
4.18 + ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
4.19 + Goal_Display.string_of_goal ctxt st]
4.20 | pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) =
4.21 - ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st_less ^
4.22 - "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^ pr_goals ctxt st_leq]
4.23 + ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
4.24 + Goal_Display.string_of_goal ctxt st_less ^
4.25 + "\n(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):\n" ^
4.26 + Goal_Display.string_of_goal ctxt st_leq]
4.27 | pr_unprovable_cell ctxt ((i,j), False st) =
4.28 - ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^ pr_goals ctxt st]
4.29 + ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
4.30 + Goal_Display.string_of_goal ctxt st]
4.31
4.32 fun pr_unprovable_subgoals ctxt table =
4.33 table
5.1 --- a/src/Pure/Isar/isar_syn.ML Mon May 13 15:22:19 2013 +0200
5.2 +++ b/src/Pure/Isar/isar_syn.ML Mon May 13 16:40:59 2013 +0200
5.3 @@ -975,7 +975,7 @@
5.4 Outer_Syntax.improper_command @{command_spec "pr"} "print current proof state (if present)"
5.5 (opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
5.6 Toplevel.keep (fn state =>
5.7 - (case limit of NONE => () | SOME n => Goal_Display.goals_limit_default := n;
5.8 + (case limit of NONE => () | SOME n => Options.default_put_int "goals_limit" n;
5.9 Toplevel.quiet := false;
5.10 Print_Mode.with_modes modes (Toplevel.print_state true) state))));
5.11
6.1 --- a/src/Pure/Isar/proof_display.ML Mon May 13 15:22:19 2013 +0200
6.2 +++ b/src/Pure/Isar/proof_display.ML Mon May 13 16:40:59 2013 +0200
6.3 @@ -105,8 +105,7 @@
6.4 end;
6.5
6.6 fun string_of_goal ctxt goal =
6.7 - Pretty.string_of (Pretty.chunks
6.8 - [pretty_goal_header goal, Goal_Display.pretty_goal {main = true, limit = false} ctxt goal]);
6.9 + Pretty.string_of (Pretty.chunks [pretty_goal_header goal, Goal_Display.pretty_goal ctxt goal]);
6.10
6.11
6.12 (* goal facts *)
7.1 --- a/src/Pure/ProofGeneral/preferences.ML Mon May 13 15:22:19 2013 +0200
7.2 +++ b/src/Pure/ProofGeneral/preferences.ML Mon May 13 16:40:59 2013 +0200
7.3 @@ -159,9 +159,9 @@
7.4 "Print terms eta-contracted"];
7.5
7.6 val advanced_display_preferences =
7.7 - [nat_pref Goal_Display.goals_limit_default
7.8 + [options_pref "goals_limit"
7.9 "goals-limit"
7.10 - "Setting for maximum number of goals printed",
7.11 + "Setting for maximum number of subgoals to be printed",
7.12 print_depth_pref,
7.13 options_pref "show_question_marks"
7.14 "show-question-marks"
8.1 --- a/src/Pure/Thy/thy_output.ML Mon May 13 15:22:19 2013 +0200
8.2 +++ b/src/Pure/Thy/thy_output.ML Mon May 13 16:40:59 2013 +0200
8.3 @@ -612,7 +612,8 @@
8.4
8.5 fun goal_state name main = antiquotation name (Scan.succeed ())
8.6 (fn {state, context = ctxt, ...} => fn () => output ctxt
8.7 - [Goal_Display.pretty_goal {main = main, limit = true} ctxt (proof_state state)]);
8.8 + [Goal_Display.pretty_goal
8.9 + (Config.put Goal_Display.show_main_goal main ctxt) (proof_state state)]);
8.10
8.11 in
8.12
9.1 --- a/src/Pure/goal.ML Mon May 13 15:22:19 2013 +0200
9.2 +++ b/src/Pure/goal.ML Mon May 13 16:40:59 2013 +0200
9.3 @@ -97,8 +97,7 @@
9.4 fun check_finished ctxt th =
9.5 if Thm.no_prems th then th
9.6 else
9.7 - raise THM ("Proof failed.\n" ^
9.8 - Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt th), 0, [th]);
9.9 + raise THM ("Proof failed.\n" ^ Pretty.string_of (Goal_Display.pretty_goal ctxt th), 0, [th]);
9.10
9.11 fun finish ctxt = check_finished ctxt #> conclude;
9.12
10.1 --- a/src/Pure/goal_display.ML Mon May 13 15:22:19 2013 +0200
10.2 +++ b/src/Pure/goal_display.ML Mon May 13 16:40:59 2013 +0200
10.3 @@ -7,10 +7,8 @@
10.4
10.5 signature GOAL_DISPLAY =
10.6 sig
10.7 - val goals_limit_default: int Unsynchronized.ref
10.8 val goals_limit_raw: Config.raw
10.9 val goals_limit: int Config.T
10.10 - val goals_total: bool Config.T
10.11 val show_main_goal_default: bool Unsynchronized.ref
10.12 val show_main_goal_raw: Config.raw
10.13 val show_main_goal: bool Config.T
10.14 @@ -20,18 +18,16 @@
10.15 val pretty_flexpair: Proof.context -> term * term -> Pretty.T
10.16 val pretty_goals: Proof.context -> thm -> Pretty.T list
10.17 val pretty_goals_without_context: thm -> Pretty.T list
10.18 - val pretty_goal: {main: bool, limit: bool} -> Proof.context -> thm -> Pretty.T
10.19 + val pretty_goal: Proof.context -> thm -> Pretty.T
10.20 + val string_of_goal: Proof.context -> thm -> string
10.21 end;
10.22
10.23 structure Goal_Display: GOAL_DISPLAY =
10.24 struct
10.25
10.26 -val goals_limit_default = Unsynchronized.ref 10;
10.27 -val goals_limit_raw = Config.declare "goals_limit" (fn _ => Config.Int (! goals_limit_default));
10.28 +val goals_limit_raw = Config.declare_option "goals_limit";
10.29 val goals_limit = Config.int goals_limit_raw;
10.30
10.31 -val goals_total = Config.bool (Config.declare "goals_total" (fn _ => Config.Bool true));
10.32 -
10.33 val show_main_goal_default = Unsynchronized.ref false;
10.34 val show_main_goal_raw =
10.35 Config.declare "show_main_goal" (fn _ => Config.Bool (! show_main_goal_default));
10.36 @@ -91,7 +87,6 @@
10.37 val show_consts = Config.get ctxt show_consts
10.38 val show_main_goal = Config.get ctxt show_main_goal;
10.39 val goals_limit = Config.get ctxt goals_limit;
10.40 - val goals_total = Config.get ctxt goals_total;
10.41
10.42 val prt_sort = Syntax.pretty_sort ctxt;
10.43 val prt_typ = Syntax.pretty_typ ctxt;
10.44 @@ -134,8 +129,7 @@
10.45 (if ngoals = 0 then [Pretty.str "No subgoals!"]
10.46 else if ngoals > goals_limit then
10.47 pretty_subgoals (take goals_limit As) @
10.48 - (if goals_total then [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
10.49 - else [])
10.50 + [Pretty.str ("A total of " ^ string_of_int ngoals ^ " subgoals...")]
10.51 else pretty_subgoals As) @
10.52 pretty_ffpairs tpairs @
10.53 (if show_consts then pretty_consts prop else []) @
10.54 @@ -148,12 +142,8 @@
10.55 Config.put show_main_goal true (Syntax.init_pretty_global (Thm.theory_of_thm th))
10.56 in pretty_goals ctxt th end;
10.57
10.58 -fun pretty_goal {main, limit} ctxt th =
10.59 - Pretty.chunks (pretty_goals
10.60 - (ctxt
10.61 - |> Config.put show_main_goal main
10.62 - |> not limit ? Config.put goals_limit (Thm.nprems_of th)
10.63 - |> Config.put goals_total false) th);
10.64 +val pretty_goal = Pretty.chunks oo pretty_goals;
10.65 +val string_of_goal = Pretty.string_of oo pretty_goal;
10.66
10.67 end;
10.68