# HG changeset patch
# User paulson
# Date 1745749264 -3600
# Node ID 0af7fe946bfd9543697a6736ce244f1b2e004060
# Parent  a151c934824cce83e0aec762b1d7e1af686ce5c8# Parent  88043331f1662f8196be3bfd70779d5ee8106403
merged

diff -r 88043331f166 -r 0af7fe946bfd src/HOL/Library/code_lazy.ML
--- a/src/HOL/Library/code_lazy.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/HOL/Library/code_lazy.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -629,7 +629,7 @@
     fun cmp ((name1, _), (name2, _)) = string_ord (name1, name2)
     val infos = Laziness_Data.get thy |> Symtab.dest |> map (apfst Long_Name.base_name) |> sort cmp
   in
-    Pretty.writeln_chunks (map (print_lazy_type thy) infos)
+    Pretty.writeln (Pretty.chunks (map (print_lazy_type thy) infos))
   end;
 
 
diff -r 88043331f166 -r 0af7fe946bfd src/HOL/Library/conditional_parametricity.ML
--- a/src/HOL/Library/conditional_parametricity.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/HOL/Library/conditional_parametricity.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -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 88043331f166 -r 0af7fe946bfd src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -88,7 +88,7 @@
          Pretty.big_list (name ^ " " ^ f status)
            (Element.pretty_ctxt ctxt context' @
             Element.pretty_stmt ctxt stmt)) vcs'') vcs')] |>
-    Pretty.writeln_chunks2
+    Pretty.chunks2 |> Pretty.writeln
   end;
 
 val _ =
diff -r 88043331f166 -r 0af7fe946bfd src/HOL/Tools/Function/lexicographic_order.ML
--- a/src/HOL/Tools/Function/lexicographic_order.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/HOL/Tools/Function/lexicographic_order.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -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 88043331f166 -r 0af7fe946bfd src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -114,7 +114,7 @@
     [Pretty.str (msg ^ ":"), Pretty.str ""] @
     map (pretty_thm ctxt) with_superfluous_assumptions @
     [Pretty.str "", Pretty.str end_msg]
-  end |> Pretty.writeln_chunks
+  end |> Pretty.chunks |> Pretty.writeln
 
 end
 
diff -r 88043331f166 -r 0af7fe946bfd src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/HOL/Tools/inductive.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -241,7 +241,7 @@
           map (Pretty.mark_str o #1)
             (Name_Space.markup_entries verbose ctxt space consts))),
      Pretty.big_list "monotonicity rules:" (map (Thm.pretty_thm_item ctxt) monos)]
-  end |> Pretty.writeln_chunks;
+  end |> Pretty.chunks |> Pretty.writeln;
 
 
 (* inductive info *)
diff -r 88043331f166 -r 0af7fe946bfd src/Provers/classical.ML
--- a/src/Provers/classical.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Provers/classical.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -643,7 +643,7 @@
       Pretty.big_list "elimination rules (elim):" (pretty_thms unsafeEs),
       Pretty.strs ("safe wrappers:" :: map #1 swrappers),
       Pretty.strs ("unsafe wrappers:" :: map #1 uwrappers)]
-    |> Pretty.writeln_chunks
+    |> Pretty.chunks |> Pretty.writeln
   end;
 
 
diff -r 88043331f166 -r 0af7fe946bfd src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/General/output.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -25,7 +25,7 @@
   val writelns: string list -> unit
   val writelns_urgent: string list -> unit
   val writeln_urgent: string -> unit
-  val state: string -> unit
+  val state: string list-> unit
   val information: string -> unit
   val error_message': serial * string -> unit
   val error_message: string -> unit
@@ -117,7 +117,7 @@
 fun writeln s = writelns [s];
 fun writelns_urgent ss = ! writeln_urgent_fn ss;
 fun writeln_urgent s = writelns_urgent [s];
-fun state s = ! state_fn [s];
+fun state ss = ! state_fn ss;
 fun information s = ! information_fn [s];
 fun tracing s = ! tracing_fn [s];
 fun warning s = ! warning_fn [s];
diff -r 88043331f166 -r 0af7fe946bfd src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/General/pretty.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -95,8 +95,6 @@
   val chunks: T list -> T
   val chunks2: T list -> T
   val block_enclose: T * T -> T list -> T
-  val writeln_chunks: T list -> unit
-  val writeln_chunks2: T list -> unit
 end;
 
 structure Pretty: PRETTY =
@@ -239,6 +237,17 @@
 
 (** formatting **)
 
+(* robust string output, with potential data loss *)
+
+fun robust_string_of out prt =
+  let
+    val bs = out prt;
+    val bs' =
+      if Bytes.size bs <= String.maxSize then bs
+      else out (from_ML (ML_Pretty.no_markup (to_ML prt)));
+  in Bytes.content bs' end;
+
+
 (* output operations *)
 
 type output_ops =
@@ -503,7 +512,7 @@
       | output (Str (s, _)) = Bytes.add s;
   in Bytes.build o output o output_tree ops false end;
 
-val symbolic_string_of = Bytes.content o symbolic_output;
+val symbolic_string_of = robust_string_of symbolic_output;
 
 
 (* unformatted output: other markup only *)
@@ -518,14 +527,14 @@
   in Bytes.build o output o output_tree ops false end;
 
 fun unformatted_string_of prt =
-  Bytes.content (unformatted (output_ops NONE) prt);
+  robust_string_of (unformatted (output_ops NONE)) prt;
 
 
 (* output interfaces *)
 
 fun output ops = if #symbolic ops then symbolic_output else format_tree ops;
 
-fun string_of_ops ops = Bytes.content o output ops;
+fun string_of_ops ops = robust_string_of (output ops);
 fun string_of prt = string_of_ops (output_ops NONE) prt;
 
 fun strings_of prt = Bytes.contents (output (output_ops NONE) prt);
@@ -553,19 +562,6 @@
 
 fun block_enclose (prt1, prt2) prts = chunks [block (fbreaks (prt1 :: prts)), prt2];
 
-fun string_of_text_fold prt = string_of prt |> Markup.markup Markup.text_fold;
-
-fun writeln_chunks prts =
-  Output.writelns (Library.separate "\n" (map string_of_text_fold prts));
-
-fun writeln_chunks2 prts =
-  (case try split_last prts of
-    NONE => ()
-  | SOME (prefix, last) =>
-      (map (fn prt => Markup.markup Markup.text_fold (string_of prt ^ "\n") ^ "\n") prefix @
-        [string_of_text_fold last])
-      |> Output.writelns);
-
 end;
 
 
diff -r 88043331f166 -r 0af7fe946bfd src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/Isar/attrib.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -114,7 +114,7 @@
             (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
   in
     [Pretty.big_list "attributes:" (map prt_attr (Name_Space.markup_table verbose ctxt attribs))]
-    |> Pretty.writeln_chunks
+    |> Pretty.chunks |> Pretty.writeln
   end;
 
 val attribute_space = Name_Space.space_of_table o Attributes.get;
diff -r 88043331f166 -r 0af7fe946bfd src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/Isar/bundle.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -110,8 +110,10 @@
   end;
 
 fun print_bundles verbose ctxt =
-  Pretty.writeln_chunks
-    (map (pretty_bundle ctxt) (Name_Space.markup_table verbose ctxt (get_all ctxt)));
+  Name_Space.markup_table verbose ctxt (get_all ctxt)
+  |> map (pretty_bundle ctxt)
+  |> Pretty.chunks
+  |> Pretty.writeln;
 
 
 
diff -r 88043331f166 -r 0af7fe946bfd src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/Isar/calculation.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -47,7 +47,7 @@
   let val pretty_thm = Thm.pretty_thm_item ctxt in
    [Pretty.big_list "transitivity rules:" (map pretty_thm (get_trans_rules ctxt)),
     Pretty.big_list "symmetry rules:" (map pretty_thm (get_sym_rules ctxt))]
-  end |> Pretty.writeln_chunks;
+  end |> Pretty.chunks |> Pretty.writeln;
 
 
 (* access calculation *)
diff -r 88043331f166 -r 0af7fe946bfd src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/Isar/class.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -210,7 +210,8 @@
     Sorts.all_classes algebra
     |> sort (Name_Space.extern_ord ctxt class_space)
     |> map prt_entry
-    |> Pretty.writeln_chunks2
+    |> Pretty.chunks2
+    |> Pretty.writeln
   end;
 
 
diff -r 88043331f166 -r 0af7fe946bfd src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/Isar/code.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -1111,8 +1111,9 @@
 
 fun apply_functrans ctxt functrans =
   let
-    fun trace_eqns s eqns = (Pretty.writeln o Pretty.chunks)
-      (Pretty.str s :: map (Thm.pretty_thm ctxt o fst) eqns);
+    fun trace_eqns s eqns =
+      Pretty.writeln (Pretty.chunks
+        (Pretty.str s :: map (Thm.pretty_thm ctxt o fst) eqns));
     val tracing = if Config.get ctxt simp_trace then trace_eqns else (K o K) ();
   in
     tap (tracing "before function transformation")
@@ -1252,7 +1253,7 @@
       |> filter (fn (_, No_Case) => false | _ => true)
       |> sort (string_ord o apply2 fst);
   in
-    Pretty.writeln_chunks [
+    Pretty.writeln (Pretty.chunks [
       Pretty.block (
         Pretty.str "types:" :: Pretty.fbrk
         :: (Pretty.fbreaks o map pretty_type_spec) types
@@ -1265,7 +1266,7 @@
         Pretty.str "cases:" :: Pretty.fbrk
         :: (Pretty.fbreaks o map pretty_case) cases
       )
-    ]
+    ])
   end;
 
 
@@ -1390,10 +1391,7 @@
     fun matches_args args' =
       let
         val k = length args' - length args
-      in if k >= 0
-        then Pattern.matchess thy (args, (map incr_idx o drop k) args')
-        else false
-      end;
+      in k >= 0 andalso Pattern.matchess thy (args, (map incr_idx o drop k) args') end;
     fun drop (thm', proper') = if (proper orelse not proper')
       andalso matches_args (args_of thm') then
         (if verbose then warning ("Code generator: dropping subsumed code equation\n" ^
diff -r 88043331f166 -r 0af7fe946bfd src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/Isar/context_rules.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -122,7 +122,7 @@
         (map_filter (fn (_, (k, th)) =>
             if k = (i, b) then SOME (Thm.pretty_thm_item ctxt th) else NONE)
           (sort (int_ord o apply2 fst) rules));
-  in Pretty.writeln_chunks (map prt_kind rule_kinds) end;
+  in Pretty.writeln (Pretty.chunks (map prt_kind rule_kinds)) end;
 
 
 (* access data *)
diff -r 88043331f166 -r 0af7fe946bfd src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/Isar/method.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -396,7 +396,7 @@
             (Pretty.mark_str name :: Pretty.str ":" :: Pretty.brk 2 :: Pretty.text comment);
   in
     [Pretty.big_list "methods:" (map prt_meth (Name_Space.markup_table verbose ctxt meths))]
-    |> Pretty.writeln_chunks
+    |> Pretty.chunks |> Pretty.writeln
   end;
 
 
diff -r 88043331f166 -r 0af7fe946bfd src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/Isar/outer_syntax.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -95,7 +95,8 @@
   dest_commands thy
   |> filter (fn (name, _) => forall (fn pat => match_string pat name) pats)
   |> map pretty_command
-  |> Pretty.writeln_chunks;
+  |> Pretty.chunks
+  |> Pretty.writeln;
 
 fun print_commands thy =
   let
@@ -105,7 +106,8 @@
   in
     [Pretty.strs ("keywords:" :: map quote minor),
       Pretty.big_list "commands:" (map pretty_command commands)]
-    |> Pretty.writeln_chunks
+    |> Pretty.chunks
+    |> Pretty.writeln
   end;
 
 
diff -r 88043331f166 -r 0af7fe946bfd src/Pure/Isar/proof.ML
--- a/src/Pure/Isar/proof.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/Isar/proof.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -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 88043331f166 -r 0af7fe946bfd src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/Isar/proof_context.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -1563,7 +1563,7 @@
     else [Pretty.big_list "abbreviations:" (map (pretty_term_abbrev ctxt o #2) abbrevs)]
   end;
 
-fun print_abbrevs verbose = Pretty.writeln_chunks o pretty_abbrevs verbose true;
+fun print_abbrevs verbose = Pretty.writeln o Pretty.chunks o pretty_abbrevs verbose true;
 
 
 (* term bindings *)
@@ -1595,7 +1595,7 @@
   end;
 
 fun print_local_facts verbose ctxt =
-  Pretty.writeln_chunks (pretty_local_facts verbose ctxt);
+  Pretty.writeln (Pretty.chunks (pretty_local_facts verbose ctxt));
 
 
 (* named local contexts *)
diff -r 88043331f166 -r 0af7fe946bfd src/Pure/Isar/proof_display.ML
--- a/src/Pure/Isar/proof_display.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/Isar/proof_display.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -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 88043331f166 -r 0af7fe946bfd src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/Isar/toplevel.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -27,7 +27,6 @@
   val presentation_state: Proof.context -> state
   val pretty_context: state -> Pretty.T list
   val pretty_state: state -> Pretty.T list
-  val string_of_state: state -> string
   val pretty_abstract: state -> Pretty.T
   type presentation = state -> Latex.text
   type transition
@@ -243,8 +242,6 @@
   | Proof (prf, _) => Proof.pretty_state (Proof_Node.current prf)
   | Skipped_Proof (d, _) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]);
 
-val string_of_state = pretty_state #> Pretty.chunks #> Pretty.string_of;
-
 fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">");
 
 val _ = ML_system_pp (fn _ => fn _ => Pretty.to_ML o pretty_abstract);
@@ -624,7 +621,7 @@
     val enabled = is_none opt_err andalso Options.default_bool \<^system_option>\<open>show_states\<close>;
     val opt_err' =
       if enabled then
-        (case Exn.capture (Output.state o string_of_state) st' of
+        (case Exn.capture (Output.state o Pretty.strings_of o Pretty.chunks o pretty_state) st' of
           Exn.Exn exn => SOME exn
         | Exn.Res _ => opt_err)
       else opt_err;
diff -r 88043331f166 -r 0af7fe946bfd src/Pure/ML/ml_pretty.ML
--- a/src/Pure/ML/ml_pretty.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/ML/ml_pretty.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -9,9 +9,11 @@
   datatype context = datatype PolyML.context
   val markup_get: PolyML.context list -> string * string
   val markup_context: string * string -> PolyML.context list
+  val no_markup_context: PolyML.context list -> PolyML.context list
   val open_block_detect: PolyML.context list -> bool
   val open_block_context: bool -> PolyML.context list
   datatype pretty = datatype PolyML.pretty
+  val no_markup: pretty -> pretty
   val block: pretty list -> pretty
   val str: string -> pretty
   val brk: FixedInt.int -> pretty
@@ -58,6 +60,9 @@
   (if bg = "" then [] else [ContextProperty (markup_bg, bg)]) @
   (if en = "" then [] else [ContextProperty (markup_en, en)]);
 
+val no_markup_context =
+  List.filter (fn ContextProperty (a, _) => a <> markup_bg andalso a <> markup_en | _ => true);
+
 
 (* open_block flag *)
 
@@ -77,6 +82,9 @@
 
 datatype pretty = datatype PolyML.pretty;
 
+fun no_markup (PrettyBlock (a, b, c, d)) = PrettyBlock (a, b, no_markup_context c, map no_markup d)
+  | no_markup a = a;
+
 fun block prts = PrettyBlock (2, false, [], prts);
 val str = PrettyString;
 fun brk width = PrettyBreak (width, 0);
diff -r 88043331f166 -r 0af7fe946bfd src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/PIDE/command.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -482,6 +482,7 @@
       then
         SOME {delay = NONE, pri = Task_Queue.urgent_pri + 1, persistent = false, strict = false,
           print_fn = fn _ => fn st =>
-            if Toplevel.is_proof st then Output.state (Toplevel.string_of_state st)
+            if Toplevel.is_proof st
+            then Output.state (Pretty.strings_of (Pretty.chunks (Toplevel.pretty_state st)))
             else ()}
       else NONE);
diff -r 88043331f166 -r 0af7fe946bfd src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/Pure.thy	Sun Apr 27 11:21:04 2025 +0100
@@ -1155,7 +1155,7 @@
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_context\<close>
     "print context of local theory target"
-    (Scan.succeed (Toplevel.keep (Pretty.writeln_chunks o Toplevel.pretty_context)));
+    (Scan.succeed (Toplevel.keep (Pretty.writeln o Pretty.chunks o Toplevel.pretty_context)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_theory\<close>
@@ -1275,7 +1275,7 @@
     "print term bindings of proof context"
     (Scan.succeed
       (Toplevel.keep
-        (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
+        (Pretty.writeln o Pretty.chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_facts\<close> "print facts of proof context"
@@ -1285,7 +1285,8 @@
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_cases\<close> "print cases of proof context"
     (Scan.succeed
-      (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
+      (Toplevel.keep
+        (Pretty.writeln o Pretty.chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>print_statement\<close>
@@ -1340,7 +1341,9 @@
   Outer_Syntax.command \<^command_keyword>\<open>print_state\<close>
     "print current proof state (if present)"
     (opt_modes >> (fn modes =>
-      Toplevel.keep (Print_Mode.with_modes modes (Output.writeln o Toplevel.string_of_state))));
+      Toplevel.keep
+        (Print_Mode.with_modes modes
+          (Output.writelns o Pretty.strings_of o Pretty.chunks o Toplevel.pretty_state))));
 
 val _ =
   Outer_Syntax.command \<^command_keyword>\<open>welcome\<close> "print welcome message"
@@ -1411,7 +1414,7 @@
                 NONE => (Theory.parents_of thy, [thy])
               | SOME (xs, NONE) => (map check xs, [thy])
               | SOME (xs, SOME ys) => (map check xs, map check ys))
-            |> map pretty_thm |> Pretty.writeln_chunks
+            |> map pretty_thm |> Pretty.chunks |> Pretty.writeln
           end)));
 
 in end\<close>
diff -r 88043331f166 -r 0af7fe946bfd src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/Syntax/syntax.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -714,9 +714,9 @@
 
 in
 
-fun print_gram syn = Pretty.writeln_chunks (pretty_gram syn);
-fun print_trans syn = Pretty.writeln_chunks (pretty_trans syn);
-fun print_syntax syn = Pretty.writeln_chunks (pretty_gram syn @ pretty_trans syn);
+fun print_gram syn = Pretty.writeln (Pretty.chunks (pretty_gram syn));
+fun print_trans syn = Pretty.writeln (Pretty.chunks (pretty_trans syn));
+fun print_syntax syn = Pretty.writeln (Pretty.chunks (pretty_gram syn @ pretty_trans syn));
 
 end;
 
diff -r 88043331f166 -r 0af7fe946bfd src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/Syntax/syntax_phases.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -927,7 +927,7 @@
     pretty_checks "term_checks" term_checks @
     pretty_checks "typ_unchecks" typ_unchecks @
     pretty_checks "term_unchecks" term_unchecks
-  end |> Pretty.writeln_chunks;
+  end |> Pretty.chunks |> Pretty.writeln;
 
 
 local
diff -r 88043331f166 -r 0af7fe946bfd src/Pure/Thy/document_antiquotation.ML
--- a/src/Pure/Thy/document_antiquotation.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/Thy/document_antiquotation.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -116,7 +116,7 @@
   in
     [Pretty.big_list "document antiquotations:" (map Pretty.mark_str command_names),
      Pretty.big_list "document antiquotation options:" (map Pretty.mark_str option_names)]
-  end |> Pretty.writeln_chunks;
+  end |> Pretty.chunks |> Pretty.writeln;
 
 fun check ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#1 (get_antiquotations ctxt));
 fun check_option ctxt = #1 o Name_Space.check (Context.Proof ctxt) (#2 (get_antiquotations ctxt));
diff -r 88043331f166 -r 0af7fe946bfd src/Pure/goal.ML
--- a/src/Pure/goal.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/goal.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -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 88043331f166 -r 0af7fe946bfd src/Pure/goal_display.ML
--- a/src/Pure/goal_display.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/goal_display.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -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 88043331f166 -r 0af7fe946bfd src/Pure/tactical.ML
--- a/src/Pure/tactical.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Pure/tactical.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -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;
diff -r 88043331f166 -r 0af7fe946bfd src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Tools/Code/code_preproc.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -262,7 +262,7 @@
     val post = (#post o the_thmproc) thy;
     val functrans = (map fst o #functrans o the_thmproc) thy;
   in
-    Pretty.writeln_chunks [
+    Pretty.writeln (Pretty.chunks [
       Pretty.block [
         Pretty.str "preprocessing simpset:",
         Pretty.fbrk,
@@ -278,7 +278,7 @@
         :: Pretty.fbrk
         :: (Pretty.fbreaks o map Pretty.str) functrans
       )
-    ]
+    ])
   end;
 
 fun simple_functrans f ctxt eqns = case f ctxt (map fst eqns)
diff -r 88043331f166 -r 0af7fe946bfd src/Tools/induct.ML
--- a/src/Tools/induct.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Tools/induct.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -259,7 +259,7 @@
     pretty_rules ctxt "induct pred:" inductP,
     pretty_rules ctxt "cases type:" casesT,
     pretty_rules ctxt "cases pred:" casesP]
-    |> Pretty.writeln_chunks
+    |> Pretty.chunks |> Pretty.writeln
   end;
 
 val _ =
diff -r 88043331f166 -r 0af7fe946bfd src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Sun Apr 27 11:20:39 2025 +0100
+++ b/src/Tools/subtyping.ML	Sun Apr 27 11:21:04 2025 +0100
@@ -1086,7 +1086,7 @@
    [Pretty.big_list "coercions between base types:" (map show_coercion simple),
     Pretty.big_list "other coercions:" (map show_coercion complex),
     Pretty.big_list "coercion maps:" (map show_map tmaps)]
-  end |> Pretty.writeln_chunks;
+  end |> Pretty.chunks |> Pretty.writeln;
 
 
 (* attribute setup *)