retain goal display options when printing error messages, to avoid breakdown for huge goals;
--- a/src/HOL/Tools/Function/lexicographic_order.ML Mon May 13 06:50:37 2013 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML Mon May 13 12:40:17 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/proof_display.ML Mon May 13 06:50:37 2013 +0200
+++ b/src/Pure/Isar/proof_display.ML Mon May 13 12:40:17 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/Thy/thy_output.ML Mon May 13 06:50:37 2013 +0200
+++ b/src/Pure/Thy/thy_output.ML Mon May 13 12:40:17 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 06:50:37 2013 +0200
+++ b/src/Pure/goal.ML Mon May 13 12:40:17 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 06:50:37 2013 +0200
+++ b/src/Pure/goal_display.ML Mon May 13 12:40:17 2013 +0200
@@ -20,7 +20,8 @@
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 =
@@ -148,12 +149,10 @@
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);
+fun pretty_goal ctxt th =
+ Pretty.chunks (pretty_goals (Config.put goals_total false ctxt) th);
+
+val string_of_goal = Pretty.string_of oo pretty_goal;
end;