# HG changeset patch
# User wenzelm
# Date 1745597172 -7200
# Node ID d08f5b5ead0a294d42ccfe75f05575103c3fd065
# Parent  255dcbe53c5003e75ecf365726d328a33daeee43
clarified signature: more scalable output --- avoid adhoc string concatenations after Pretty.string_of;

diff -r 255dcbe53c50 -r d08f5b5ead0a src/HOL/Library/conditional_parametricity.ML
--- a/src/HOL/Library/conditional_parametricity.ML	Fri Apr 25 16:54:39 2025 +0200
+++ b/src/HOL/Library/conditional_parametricity.ML	Fri Apr 25 18:06:12 2025 +0200
@@ -110,7 +110,7 @@
 (* Tactics  *)
 (* helper tactics for printing *)
 fun error_tac ctxt msg st =
-  (error (msg ^ "\n" ^ Goal_Display.string_of_goal ctxt st); Seq.single st);
+  (error (Goal_Display.print_goal ctxt msg st); Seq.single st);
 
 fun error_tac' ctxt msg = SELECT_GOAL (error_tac ctxt msg);
 
diff -r 255dcbe53c50 -r d08f5b5ead0a src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Fri Apr 25 16:54:39 2025 +0200
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Fri Apr 25 18:06:12 2025 +0200
@@ -124,16 +124,12 @@
 
 fun pr_unprovable_cell _ ((i,j), Less _) = []
   | pr_unprovable_cell ctxt ((i,j), LessEq (_, st)) =
-      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
-       Goal_Display.string_of_goal ctxt st]
+      [Goal_Display.print_goal ctxt ("(" ^ row_index i ^ ", " ^ col_index j ^ ", <):") st]
   | pr_unprovable_cell ctxt ((i,j), None (st_leq, st_less)) =
-      ["(" ^ 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]
+      [Goal_Display.print_goal ctxt ("(" ^ row_index i ^ ", " ^ col_index j ^ ", <):") st_less ^ "\n" ^
+       Goal_Display.print_goal ctxt ("(" ^ row_index i ^ ", " ^ col_index j ^ ", <=):") st_leq]
   | pr_unprovable_cell ctxt ((i,j), False st) =
-      ["(" ^ row_index i ^ ", " ^ col_index j ^ ", <):\n" ^
-       Goal_Display.string_of_goal ctxt st]
+      [Goal_Display.print_goal ctxt ("(" ^ row_index i ^ ", " ^ col_index j ^ ", <):") st]
 
 fun pr_unprovable_subgoals ctxt table =
   table
diff -r 255dcbe53c50 -r d08f5b5ead0a src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Fri Apr 25 16:54:39 2025 +0200
+++ b/src/Pure/Isar/proof.ML	Fri Apr 25 18:06:12 2025 +0200
@@ -492,7 +492,8 @@
     val _ =
       Context.subthy_id (Thm.theory_id goal, Context.theory_id thy) orelse
         error "Bad background theory of goal state";
-    val _ = Thm.no_prems goal orelse error (Proof_Display.string_of_goal ctxt goal);
+    val _ = Thm.no_prems goal orelse
+      error (Pretty.string_of (Proof_Display.pretty_goal ctxt goal));
 
     fun err_lost () = error ("Lost goal structure:\n" ^ Thm.string_of_thm ctxt goal);
 
@@ -521,13 +522,16 @@
 
 val finished_goal_error = "Failed to finish proof";
 
+fun finished_goal_error_pos pos =
+  Pretty.block0 (Pretty.str finished_goal_error :: Pretty.here pos @ [Pretty.str ":"]);
+
 fun finished_goal pos state =
   let val (ctxt, {goal, ...}) = find_goal state in
     if Thm.no_prems goal then Seq.Result state
     else
       Seq.Error (fn () =>
-        finished_goal_error ^ Position.here pos ^ ":\n" ^
-          Proof_Display.string_of_goal ctxt goal)
+        Pretty.string_of (Pretty.chunks
+          [finished_goal_error_pos pos, Proof_Display.pretty_goal ctxt goal]))
   end;
 
 
diff -r 255dcbe53c50 -r d08f5b5ead0a src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Fri Apr 25 16:54:39 2025 +0200
+++ b/src/Pure/Isar/proof_display.ML	Fri Apr 25 18:06:12 2025 +0200
@@ -12,7 +12,7 @@
   val pretty_theorems: bool -> Proof.context -> Pretty.T list
   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 pretty_goal: Proof.context -> thm -> Pretty.T
   val pretty_goal_facts: Proof.context -> string -> thm list option -> Pretty.T list
   val pretty_goal_inst: Proof.context -> term list list -> thm -> Pretty.T list
   val method_error: string -> Position.T ->
@@ -200,10 +200,10 @@
 fun pretty_goal_header goal =
   Pretty.block ([Pretty.keyword1 "goal"] @ subgoals (Thm.nprems_of goal) @ [Pretty.str ":"]);
 
-end;
+fun pretty_goal ctxt goal =
+  Pretty.chunks [pretty_goal_header goal, Goal_Display.pretty_goal ctxt goal];
 
-fun string_of_goal ctxt goal =
-  Pretty.string_of (Pretty.chunks [pretty_goal_header goal, Goal_Display.pretty_goal ctxt goal]);
+end;
 
 
 (* goal facts *)
@@ -282,13 +282,14 @@
 fun method_error kind pos {context = ctxt, facts, goal} = Seq.Error (fn () =>
   let
     val pr_header =
-      "Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^
-      "proof method" ^ Position.here pos ^ ":\n";
+      Pretty.block0
+       ([Pretty.str ("Failed to apply " ^ (if kind = "" then "" else kind ^ " ") ^ "proof method")]
+         @ Pretty.here pos @ [Pretty.str ":"]);
     val pr_facts =
-      if null facts then ""
-      else Pretty.string_of (Pretty.chunks (pretty_goal_facts ctxt "using" (SOME facts))) ^ "\n";
-    val pr_goal = string_of_goal ctxt goal;
-  in pr_header ^ pr_facts ^ pr_goal end);
+      if null facts then []
+      else [Pretty.chunks (pretty_goal_facts ctxt "using" (SOME facts))];
+    val pr_goal = pretty_goal ctxt goal;
+  in Pretty.string_of (Pretty.chunks ([pr_header] @ pr_facts @ [pr_goal])) end);
 
 
 (* results *)
diff -r 255dcbe53c50 -r d08f5b5ead0a src/Pure/goal.ML
--- a/src/Pure/goal.ML	Fri Apr 25 16:54:39 2025 +0200
+++ b/src/Pure/goal.ML	Fri Apr 25 18:06:12 2025 +0200
@@ -80,7 +80,7 @@
 *)
 fun check_finished ctxt th =
   if Thm.no_prems th then th
-  else raise THM ("Proof failed.\n" ^ Goal_Display.string_of_goal ctxt th, 0, [th]);
+  else raise THM (Goal_Display.print_goal ctxt "Proof failed." th, 0, [th]);
 
 fun finish ctxt = check_finished ctxt #> conclude;
 
diff -r 255dcbe53c50 -r d08f5b5ead0a src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Fri Apr 25 16:54:39 2025 +0200
+++ b/src/Pure/goal_display.ML	Fri Apr 25 18:06:12 2025 +0200
@@ -11,7 +11,7 @@
   val show_main_goal: bool Config.T
   val pretty_goals: Proof.context -> thm -> Pretty.T list
   val pretty_goal: Proof.context -> thm -> Pretty.T
-  val string_of_goal: Proof.context -> thm -> string
+  val print_goal: Proof.context -> string -> thm -> string
 end;
 
 structure Goal_Display: GOAL_DISPLAY =
@@ -117,7 +117,10 @@
   end;
 
 val pretty_goal = Pretty.chunks oo pretty_goals;
-val string_of_goal = Pretty.string_of oo pretty_goal;
+
+fun print_goal ctxt header state =
+  (Pretty.string_of o Pretty.chunks)
+    ((if header = "" then [] else [Pretty.str header]) @ pretty_goals ctxt state);
 
 end;
 
diff -r 255dcbe53c50 -r d08f5b5ead0a src/Pure/tactical.ML
--- a/src/Pure/tactical.ML	Fri Apr 25 16:54:39 2025 +0200
+++ b/src/Pure/tactical.ML	Fri Apr 25 18:06:12 2025 +0200
@@ -176,7 +176,7 @@
 
 (*Print the current proof state and pass it on.*)
 fun print_tac ctxt msg st =
-  (tracing (msg ^ "\n" ^ Goal_Display.string_of_goal ctxt st); Seq.single st);
+  (tracing (Goal_Display.print_goal ctxt msg st); Seq.single st);
 
 
 (*Deterministic REPEAT: only retains the first outcome;