# HG changeset patch
# User wenzelm
# Date 1350150784 -7200
# Node ID ed5080c031651d60185826ef91c387b96d499a4c
# Parent  8fae089f5a0c30ddd2098e4795d3e26ee35e5a59
some attempts to unify/simplify pretty_goal;

diff -r 8fae089f5a0c -r ed5080c03165 src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Sat Oct 13 18:04:11 2012 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Sat Oct 13 19:53:04 2012 +0200
@@ -122,10 +122,9 @@
 (** Error reporting **)
 
 fun pr_goals ctxt st =
-  Goal_Display.pretty_goals
-    (Config.put Goal_Display.goals_limit (Thm.nprems_of st) ctxt) st
-  |> Pretty.chunks
-  |> Pretty.string_of
+  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)
 fun col_index j = string_of_int (j + 1)
diff -r 8fae089f5a0c -r ed5080c03165 src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sat Oct 13 18:04:11 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Sat Oct 13 19:53:04 2012 +0200
@@ -33,7 +33,6 @@
   val enter_forward: state -> state
   val goal_message: (unit -> Pretty.T) -> state -> state
   val pretty_state: int -> state -> Pretty.T list
-  val pretty_goals: bool -> state -> Pretty.T list
   val refine: Method.text -> state -> state Seq.seq
   val refine_end: Method.text -> state -> state Seq.seq
   val refine_insert: thm list -> state -> state
@@ -378,14 +377,6 @@
      else prt_goal (try find_goal state))
   end;
 
-fun pretty_goals main state =
-  let
-    val (_, (_, goal)) = get_goal state;
-    val ctxt = context_of state
-      |> Config.put Goal_Display.show_main_goal main
-      |> Config.put Goal_Display.goals_total false;
-  in Goal_Display.pretty_goals ctxt goal end;
-
 
 
 (** proof steps **)
@@ -490,18 +481,14 @@
 
 (* conclude goal *)
 
-fun unfinished_goal_msg ctxt goal =
-  Pretty.string_of (Pretty.chunks
-    (Goal_Display.pretty_goals ctxt goal @
-      [Pretty.str (string_of_int (Thm.nprems_of goal) ^ " unsolved goal(s)")]));
-
 fun conclude_goal ctxt goal propss =
   let
     val thy = Proof_Context.theory_of ctxt;
     val string_of_term = Syntax.string_of_term ctxt;
     val string_of_thm = Display.string_of_thm ctxt;
 
-    val _ = Thm.no_prems goal orelse error (unfinished_goal_msg ctxt goal);
+    val _ = Thm.no_prems goal orelse
+      error (Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt goal));
 
     val extra_hyps = Assumption.extra_hyps ctxt goal;
     val _ = null extra_hyps orelse
@@ -535,7 +522,10 @@
         else
           (case Seq.pull (Seq.filter (Thm.no_prems o #2 o #2 o get_goal o #2) rest) of
             SOME ((f, state), _) => f state
-          | NONE => error ("Failed to finish proof:\n" ^ unfinished_goal_msg ctxt1 goal1))
+          | NONE =>
+              error ("Failed to finish proof:\n" ^
+                Pretty.string_of
+                  (Goal_Display.pretty_goal {main = true, limit = false} ctxt1 goal1)))
       end
   | NONE => error "Failed to finish proof");
 
diff -r 8fae089f5a0c -r ed5080c03165 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Sat Oct 13 18:04:11 2012 +0200
+++ b/src/Pure/Thy/thy_output.ML	Sat Oct 13 19:53:04 2012 +0200
@@ -609,14 +609,13 @@
 local
 
 fun proof_state state =
-  (case try Toplevel.proof_of state of
-    SOME prf => prf
+  (case try (Proof.goal o Toplevel.proof_of) state of
+    SOME {goal, ...} => goal
   | _ => error "No proof state");
 
-fun goal_state name main_goal = antiquotation name (Scan.succeed ())
+fun goal_state name main = antiquotation name (Scan.succeed ())
   (fn {state, context = ctxt, ...} => fn () => output ctxt
-    [Pretty.chunks
-      (Proof.pretty_goals main_goal (Proof.map_context (K ctxt) (proof_state state)))]);
+    [Goal_Display.pretty_goal {main = main, limit = true} ctxt (proof_state state)]);
 
 in
 
diff -r 8fae089f5a0c -r ed5080c03165 src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sat Oct 13 18:04:11 2012 +0200
+++ b/src/Pure/goal.ML	Sat Oct 13 19:53:04 2012 +0200
@@ -87,12 +87,7 @@
   (case Thm.nprems_of th of
     0 => th
   | n => raise THM ("Proof failed.\n" ^
-      Pretty.string_of (Pretty.chunks
-        (Goal_Display.pretty_goals
-          (ctxt
-            |> Config.put Goal_Display.goals_limit n
-            |> Config.put Goal_Display.show_main_goal true) th)) ^
-      "\n" ^ string_of_int n ^ " unsolved goal(s)!", 0, [th]));
+      Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt th), 0, [th]));
 
 fun finish ctxt = check_finished ctxt #> conclude;
 
diff -r 8fae089f5a0c -r ed5080c03165 src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Sat Oct 13 18:04:11 2012 +0200
+++ b/src/Pure/goal_display.ML	Sat Oct 13 19:53:04 2012 +0200
@@ -20,6 +20,7 @@
   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
 end;
 
 structure Goal_Display: GOAL_DISPLAY =
@@ -148,6 +149,13 @@
     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);
+
 end;
 
 end;