--- 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"
--- 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
--- 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
--- 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
--- 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))));
--- 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 *)
--- 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"
--- 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
--- 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;
--- 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;