src/Pure/PIDE/query_operation.ML

--- a/src/Pure/PIDE/query_operation.ML	Thu Apr 24 21:39:40 2025 +0200
+++ b/src/Pure/PIDE/query_operation.ML	Thu Apr 24 22:45:04 2025 +0200
@@ -9,7 +9,9 @@
 sig
   val register: {name: string, pri: int} ->
     ({state: Toplevel.state, args: string list,
-      output_result: string -> unit, writeln_result: string -> unit} -> unit) -> unit
+      output_result: string list -> unit,
+      writelns_result: string list -> unit,
+      writeln_result: string -> unit} -> unit) -> unit
 end;
 
 structure Query_Operation: QUERY_OPERATION =
@@ -21,16 +23,17 @@
       SOME {delay = NONE, pri = pri, persistent = false, strict = false,
         print_fn = fn _ => Thread_Attributes.uninterruptible (fn run => fn state =>
           let
-            fun output_result s = Output.result [(Markup.instanceN, instance)] [s];
-            fun status m = output_result (YXML.output_markup_only m);
-            fun writeln_result s = output_result (Markup.markup Markup.writeln s);
+            fun output_result ss = Output.result [(Markup.instanceN, instance)] ss;
+            fun status m = output_result [YXML.output_markup_only m];
+            fun writelns_result ss = output_result (Markup.markup_strings Markup.writeln ss);
+            val writeln_result = writelns_result o single;
             fun toplevel_error exn =
-              output_result (Markup.markup Markup.error (Runtime.exn_message exn));
+              output_result [Markup.markup Markup.error (Runtime.exn_message exn)];
 
             val _ = status Markup.running;
             fun main () =
               f {state = state, args = args, output_result = output_result,
-                  writeln_result = writeln_result};
+                  writelns_result = writelns_result, writeln_result = writeln_result};
             val _ =
               (case Exn.capture_body (*sic!*) (run main) of
                 Exn.Res () => ()
@@ -47,5 +50,10 @@
   Query_Operation.register {name = "print_state", pri = Task_Queue.urgent_pri}
     (fn {state = st, output_result, ...} =>
       if Toplevel.is_proof st
-      then output_result (Markup.markup Markup.state (Toplevel.string_of_state st))
+      then
+        Toplevel.pretty_state st
+        |> Pretty.chunks
+        |> Pretty.strings_of
+        |> Markup.markup_strings Markup.state
+        |> output_result
       else ());