further attempts to unify/simplify goal output;

--- a/src/Pure/Isar/proof.ML	Tue Oct 16 13:06:40 2012 +0200
+++ b/src/Pure/Isar/proof.ML	Tue Oct 16 14:02:02 2012 +0200
@@ -333,32 +333,20 @@
 
 fun pretty_facts _ _ NONE = []
   | pretty_facts s ctxt (SOME ths) =
-      [Pretty.big_list (s ^ "this:") (map (Display.pretty_thm ctxt) ths), Pretty.str ""];
+      [Pretty.chunks
+        (Pretty.block [Pretty.command s, Pretty.brk 1, Pretty.str "this:"] ::
+          map (Display.pretty_thm ctxt) ths), Pretty.str ""];
 
 fun pretty_state nr state =
   let
     val {context = ctxt, facts, mode, goal = _} = top state;
     val verbose = Config.get ctxt Proof_Context.verbose;
 
-    fun levels_up 0 = ""
-      | levels_up 1 = "1 level up"
-      | levels_up i = string_of_int i ^ " levels up";
-
-    fun subgoals 0 = ""
-      | subgoals 1 = "1 subgoal"
-      | subgoals n = string_of_int n ^ " subgoals";
-
-    fun description strs =
-      (case filter_out (fn s => s = "") strs of [] => ""
-      | strs' => enclose " (" ")" (commas strs'));
-
-    fun prt_goal (SOME (_, (i,
+    fun prt_goal (SOME (_, (_,
       {statement = ((_, pos), _, _), messages, using, goal, before_qed = _, after_qed = _}))) =
           pretty_facts "using " ctxt
             (if mode <> Backward orelse null using then NONE else SOME using) @
-          [Pretty.str ("goal" ^
-            description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @
-          Goal_Display.pretty_goals ctxt goal @
+          [Proof_Display.pretty_goal_header goal] @ Goal_Display.pretty_goals ctxt goal @
           (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages))
       | prt_goal NONE = [];
 
@@ -487,8 +475,7 @@
     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 (Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt goal));
+    val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);
 
     val extra_hyps = Assumption.extra_hyps ctxt goal;
     val _ = null extra_hyps orelse
@@ -519,10 +506,7 @@
 fun finished_goal state =
   let val (ctxt, (_, goal)) = get_goal state in
     if Thm.no_prems goal then Seq.Result state
-    else
-      Seq.Error (fn () =>
-        finished_goal_error ^ ":\n" ^
-          Pretty.string_of (Goal_Display.pretty_goal {main = true, limit = false} ctxt goal))
+    else Seq.Error (fn () => finished_goal_error ^ ":\n" ^ Proof_Display.string_of_goal ctxt goal)
   end;
 
 
@@ -980,29 +964,14 @@
 
 (* concluding steps *)
 
-fun method_error name state = Seq.Error (fn () =>
-  let
-    val (ctxt, (facts, goal)) = get_goal state;
-    val pr_header =
-      "Failure of " ^ (if name = "" then "" else name ^ " ") ^ "proof method on goal state:\n";
-    val pr_facts =
-      if null facts then ""
-      else Pretty.string_of (Pretty.big_list "facts:" (map (Display.pretty_thm ctxt) facts)) ^ "\n";
-    val pr_goal =
-      "goal:\n" ^ Pretty.string_of (Goal_Display.pretty_goal {main = false, limit = false} ctxt goal);
-  in pr_header ^ pr_facts ^ pr_goal end);
-
-local
-
+fun method_error name state = Seq.single (Proof_Display.method_error name (raw_goal state));
 val op APPEND = Seq.APPEND;
 
 fun terminal_proof qeds initial terminal =
-  ((proof (SOME initial) #> Seq.map Seq.Result) APPEND (Seq.single o method_error "initial"))
-  #> Seq.maps_results (qeds terminal APPEND (Seq.single o method_error "terminal"))
+  ((proof (SOME initial) #> Seq.map Seq.Result) APPEND method_error "initial")
+  #> Seq.maps_results (qeds terminal APPEND method_error "terminal")
   #> Seq.the_result "";
 
-in
-
 fun local_terminal_proof (text, opt_text) = terminal_proof local_qeds text (opt_text, true);
 val local_default_proof = local_terminal_proof (Method.default_text, NONE);
 val local_immediate_proof = local_terminal_proof (Method.this_text, NONE);
@@ -1015,8 +984,6 @@
 fun global_skip_proof int = global_terminal_proof (Method.sorry_text int, NONE);
 val global_done_proof = terminal_proof global_qeds Method.done_text (NONE, false);
 
-end;
-
 
 (* common goal statements *)
 

--- a/src/Pure/Isar/proof_display.ML	Tue Oct 16 13:06:40 2012 +0200
+++ b/src/Pure/Isar/proof_display.ML	Tue Oct 16 14:02:02 2012 +0200
@@ -17,6 +17,9 @@
   val pretty_full_theory: bool -> theory -> Pretty.T
   val print_theory: theory -> unit
   val string_of_rule: Proof.context -> string -> thm -> string
+  val pretty_goal_header: thm -> Pretty.T
+  val string_of_goal: Proof.context -> thm -> string
+  val method_error: string -> {context: Proof.context, facts: thm list, goal: thm} -> 'a Seq.result
   val print_results: Markup.T -> bool -> Proof.context ->
     ((string * string) * (string * thm list) list) -> unit
   val print_consts: bool -> Proof.context -> (string * typ -> bool) -> (string * typ) list -> unit
@@ -86,6 +89,42 @@
 val string_of_rule = Pretty.string_of ooo pretty_rule;
 
 
+(* goals *)
+
+local
+
+fun subgoals 0 = []
+  | subgoals 1 = [Pretty.brk 1, Pretty.str "(1 subgoal)"]
+  | subgoals n = [Pretty.brk 1, Pretty.str ("(" ^ string_of_int n ^ " subgoals)")];
+
+in
+
+fun pretty_goal_header goal =
+  Pretty.block ([Pretty.command "goal"] @ subgoals (Thm.nprems_of goal) @ [Pretty.str ":"]);
+
+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]);
+
+
+(* method_error *)
+
+fun method_error name {context = ctxt, facts, goal} = Seq.Error (fn () =>
+  let
+    val pr_header = "Failure of " ^ (if name = "" then "" else name ^ " ") ^ "proof method:\n";
+    val pr_facts =
+      if null facts then ""
+      else
+        Pretty.string_of
+          (Pretty.chunks
+            (Pretty.block [Pretty.command "using", Pretty.brk 1, Pretty.str "this:"] ::
+              map (Display.pretty_thm ctxt) facts)) ^ "\n";
+    val pr_goal = string_of_goal ctxt goal;
+  in pr_header ^ pr_facts ^ pr_goal end);
+
+
 (* results *)
 
 local