# HG changeset patch
# User wenzelm
# Date 1368441617 -7200
# Node ID bca32217b304b8999c7cd0ea2ace40ea1efaf557
# Parent  ae755fd6c8835752cddb9532f8c2a02db7f778cf
retain goal display options when printing error messages, to avoid breakdown for huge goals;

diff -r ae755fd6c883 -r bca32217b304 src/HOL/Tools/Function/lexicographic_order.ML
--- 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
diff -r ae755fd6c883 -r bca32217b304 src/Pure/Isar/proof_display.ML
--- 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 *)
diff -r ae755fd6c883 -r bca32217b304 src/Pure/Thy/thy_output.ML
--- 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
 
diff -r ae755fd6c883 -r bca32217b304 src/Pure/goal.ML
--- 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;
 
diff -r ae755fd6c883 -r bca32217b304 src/Pure/goal_display.ML
--- 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;