# HG changeset patch
# User wenzelm
# Date 1745572945 -7200
# Node ID 7415414bd9d85f20aa23df5f9a8d73506480489f
# Parent  46591222e4fc68e0f81dfe916db9b551014bb35c
more scalable: discontinue odd shortcuts from 6b3739fee456, which produce bulky strings internally;

diff -r 46591222e4fc -r 7415414bd9d8 src/HOL/Library/code_lazy.ML
--- a/src/HOL/Library/code_lazy.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/HOL/Library/code_lazy.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -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 46591222e4fc -r 7415414bd9d8 src/HOL/SPARK/Tools/spark_commands.ML
--- a/src/HOL/SPARK/Tools/spark_commands.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/HOL/SPARK/Tools/spark_commands.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -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 46591222e4fc -r 7415414bd9d8 src/HOL/Tools/Quickcheck/find_unused_assms.ML
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -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 46591222e4fc -r 7415414bd9d8 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/HOL/Tools/inductive.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -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 46591222e4fc -r 7415414bd9d8 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Provers/classical.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -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 46591222e4fc -r 7415414bd9d8 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Pure/General/pretty.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -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 =
@@ -553,19 +551,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 46591222e4fc -r 7415414bd9d8 src/Pure/Isar/attrib.ML
--- a/src/Pure/Isar/attrib.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Pure/Isar/attrib.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -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 46591222e4fc -r 7415414bd9d8 src/Pure/Isar/bundle.ML
--- a/src/Pure/Isar/bundle.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Pure/Isar/bundle.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -110,8 +110,8 @@
   end;
 
 fun print_bundles verbose ctxt =
-  Pretty.writeln_chunks
-    (map (pretty_bundle ctxt) (Name_Space.markup_table verbose ctxt (get_all ctxt)));
+  Pretty.writeln (Pretty.chunks
+    (map (pretty_bundle ctxt) (Name_Space.markup_table verbose ctxt (get_all ctxt))));
 
 
 
diff -r 46591222e4fc -r 7415414bd9d8 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Pure/Isar/calculation.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -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 46591222e4fc -r 7415414bd9d8 src/Pure/Isar/class.ML
--- a/src/Pure/Isar/class.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Pure/Isar/class.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -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 46591222e4fc -r 7415414bd9d8 src/Pure/Isar/code.ML
--- a/src/Pure/Isar/code.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Pure/Isar/code.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -1252,7 +1252,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 +1265,7 @@
         Pretty.str "cases:" :: Pretty.fbrk
         :: (Pretty.fbreaks o map pretty_case) cases
       )
-    ]
+    ])
   end;
 
 
diff -r 46591222e4fc -r 7415414bd9d8 src/Pure/Isar/context_rules.ML
--- a/src/Pure/Isar/context_rules.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Pure/Isar/context_rules.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -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 46591222e4fc -r 7415414bd9d8 src/Pure/Isar/method.ML
--- a/src/Pure/Isar/method.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Pure/Isar/method.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -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 46591222e4fc -r 7415414bd9d8 src/Pure/Isar/outer_syntax.ML
--- a/src/Pure/Isar/outer_syntax.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Pure/Isar/outer_syntax.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -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 46591222e4fc -r 7415414bd9d8 src/Pure/Isar/proof_context.ML
--- a/src/Pure/Isar/proof_context.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Pure/Isar/proof_context.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -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 46591222e4fc -r 7415414bd9d8 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Pure/Pure.thy	Fri Apr 25 11:22:25 2025 +0200
@@ -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>
@@ -1411,7 +1412,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 46591222e4fc -r 7415414bd9d8 src/Pure/Syntax/syntax.ML
--- a/src/Pure/Syntax/syntax.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Pure/Syntax/syntax.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -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 46591222e4fc -r 7415414bd9d8 src/Pure/Syntax/syntax_phases.ML
--- a/src/Pure/Syntax/syntax_phases.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Pure/Syntax/syntax_phases.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -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 46591222e4fc -r 7415414bd9d8 src/Pure/Thy/document_antiquotation.ML
--- a/src/Pure/Thy/document_antiquotation.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -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 46591222e4fc -r 7415414bd9d8 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Tools/Code/code_preproc.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -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 46591222e4fc -r 7415414bd9d8 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Tools/induct.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -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 46591222e4fc -r 7415414bd9d8 src/Tools/subtyping.ML
--- a/src/Tools/subtyping.ML	Fri Apr 25 09:46:21 2025 +0200
+++ b/src/Tools/subtyping.ML	Fri Apr 25 11:22:25 2025 +0200
@@ -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 *)