# HG changeset patch
# User wenzelm
# Date 1745523580 -7200
# Node ID bcee022fbe3063d8338e633def89647b156a8b2a
# Parent  0133fe6a1f55ecb66c0f47fdbde81e00e8fd6ff8
more scalable;

diff -r 0133fe6a1f55 -r bcee022fbe30 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 24 20:42:04 2025 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Apr 24 21:39:40 2025 +0200
@@ -244,55 +244,53 @@
 
 local
 
-fun string_of_stmts ctxt args =
+fun pretty_stmts ctxt args =
   Attrib.eval_thms ctxt args
   |> map (Element.pretty_statement ctxt Thm.theoremK)
-  |> Pretty.chunks2 |> Pretty.string_of;
+  |> Pretty.chunks2;
 
-fun string_of_thms ctxt args =
-  Pretty.string_of (Proof_Context.pretty_fact ctxt ("", Attrib.eval_thms ctxt args));
+fun pretty_thms ctxt args =
+  Proof_Context.pretty_fact ctxt ("", Attrib.eval_thms ctxt args);
 
-fun string_of_prfs full state arg =
-  Pretty.string_of
-    (case arg of
-      NONE =>
-        let
-          val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state);
-          val thy = Proof_Context.theory_of ctxt;
-          val prf = Thm.proof_of thm;
-          val prop = Thm.full_prop_of thm;
-          val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
-        in
-          Proof_Syntax.pretty_proof ctxt
-            (if full then Proofterm.reconstruct_proof thy prop prf' else prf')
-        end
-    | SOME srcs =>
-        let
-          val ctxt = Toplevel.context_of state;
-          val pretty_proof = Proof_Syntax.pretty_standard_proof_of ctxt full;
-        in Pretty.chunks (map pretty_proof (Attrib.eval_thms ctxt srcs)) end);
+fun pretty_prfs full state arg =
+  (case arg of
+    NONE =>
+      let
+        val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state);
+        val thy = Proof_Context.theory_of ctxt;
+        val prf = Thm.proof_of thm;
+        val prop = Thm.full_prop_of thm;
+        val prf' = Proofterm.rewrite_proof_notypes ([], []) prf;
+      in
+        Proof_Syntax.pretty_proof ctxt
+          (if full then Proofterm.reconstruct_proof thy prop prf' else prf')
+      end
+  | SOME srcs =>
+      let
+        val ctxt = Toplevel.context_of state;
+        val pretty_proof = Proof_Syntax.pretty_standard_proof_of ctxt full;
+      in Pretty.chunks (map pretty_proof (Attrib.eval_thms ctxt srcs)) end);
 
-fun string_of_prop ctxt s =
+fun pretty_prop ctxt s =
   let
     val prop = Syntax.read_prop ctxt s;
     val ctxt' = Proof_Context.augment prop ctxt;
-  in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end;
+  in Pretty.quote (Syntax.pretty_term ctxt' prop) end;
 
-fun string_of_term ctxt s =
+fun pretty_term ctxt s =
   let
     val t = Syntax.read_term ctxt s;
     val T = Term.type_of t;
     val ctxt' = Proof_Context.augment t ctxt;
   in
-    Pretty.string_of
-      (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk,
-        Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)])
+    Pretty.block [Pretty.quote (Syntax.pretty_term ctxt' t), Pretty.fbrk,
+      Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt' T)]
   end;
 
-fun string_of_type ctxt (s, NONE) =
+fun pretty_type ctxt (s, NONE) =
       let val T = Syntax.read_typ ctxt s
-      in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end
-  | string_of_type ctxt (s1, SOME s2) =
+      in Pretty.quote (Syntax.pretty_typ ctxt T) end
+  | pretty_type ctxt (s1, SOME s2) =
       let
         val ctxt' = Config.put show_sorts true ctxt;
         val raw_T = Syntax.parse_typ ctxt' s1;
@@ -301,19 +299,19 @@
           Syntax.check_term ctxt'
             (Logic.mk_type raw_T |> Type.constraint (Term.itselfT (Type_Infer.anyT S)))
           |> Logic.dest_type;
-      in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt' T)) end;
+      in Pretty.quote (Syntax.pretty_typ ctxt' T) end;
 
-fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
-  Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ());
+fun print_item pretty (modes, arg) = Toplevel.keep (fn state =>
+  Print_Mode.with_modes modes (fn () => Pretty.writeln (pretty state arg)) ());
 
 in
 
-val print_stmts = print_item (string_of_stmts o Toplevel.context_of);
-val print_thms = print_item (string_of_thms o Toplevel.context_of);
-val print_prfs = print_item o string_of_prfs;
-val print_prop = print_item (string_of_prop o Toplevel.context_of);
-val print_term = print_item (string_of_term o Toplevel.context_of);
-val print_type = print_item (string_of_type o Toplevel.context_of);
+val print_stmts = print_item (pretty_stmts o Toplevel.context_of);
+val print_thms = print_item (pretty_thms o Toplevel.context_of);
+val print_prfs = print_item o pretty_prfs;
+val print_prop = print_item (pretty_prop o Toplevel.context_of);
+val print_term = print_item (pretty_term o Toplevel.context_of);
+val print_type = print_item (pretty_type o Toplevel.context_of);
 
 end;