# HG changeset patch
# User wenzelm
# Date 1745592879 -7200
# Node ID 255dcbe53c5003e75ecf365726d328a33daeee43
# Parent  62b4b9f336c5f5c7150ac2fb9e381bd6bee6b6f7
clarified signature: more scalable output;

diff -r 62b4b9f336c5 -r 255dcbe53c50 src/Pure/General/output.ML
--- a/src/Pure/General/output.ML	Fri Apr 25 11:34:29 2025 +0200
+++ b/src/Pure/General/output.ML	Fri Apr 25 16:54:39 2025 +0200
@@ -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 62b4b9f336c5 -r 255dcbe53c50 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Fri Apr 25 11:34:29 2025 +0200
+++ b/src/Pure/Isar/toplevel.ML	Fri Apr 25 16:54:39 2025 +0200
@@ -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 62b4b9f336c5 -r 255dcbe53c50 src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Fri Apr 25 11:34:29 2025 +0200
+++ b/src/Pure/PIDE/command.ML	Fri Apr 25 16:54:39 2025 +0200
@@ -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 62b4b9f336c5 -r 255dcbe53c50 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Fri Apr 25 11:34:29 2025 +0200
+++ b/src/Pure/Pure.thy	Fri Apr 25 16:54:39 2025 +0200
@@ -1341,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"