# HG changeset patch
# User wenzelm
# Date 1725903618 -7200
# Node ID 7feaa04d332b7ea429ea9e209190b55b6b949566
# Parent  b866d1510bd041da0c3519c6292e34011660b4ab
prefer static YXML.output_markup_only (without print_mode): Output.status is only relevant for PIDE (with print_mode "isabelle_process");

diff -r b866d1510bd0 -r 7feaa04d332b src/Pure/PIDE/command.ML
--- a/src/Pure/PIDE/command.ML	Mon Sep 09 19:00:53 2024 +0200
+++ b/src/Pure/PIDE/command.ML	Mon Sep 09 19:40:18 2024 +0200
@@ -213,14 +213,14 @@
             NONE => ()
           | SOME 0 => ()
           | SOME n =>
-              let val report = Markup.markup_only (Markup.command_indent (n - 1));
+              let val report = YXML.output_markup_only (Markup.command_indent (n - 1));
               in Toplevel.setmp_thread_position tr (fn () => Output.report [report]) () end)
         else ()
       end
   | NONE => ());
 
 fun status tr m =
-  Toplevel.setmp_thread_position tr (fn () => Output.status [Markup.markup_only m]) ();
+  Toplevel.setmp_thread_position tr (fn () => Output.status [YXML.output_markup_only m]) ();
 
 fun eval_state keywords span tr ({state, ...}: eval_state) =
   let
diff -r b866d1510bd0 -r 7feaa04d332b src/Pure/PIDE/document.ML
--- a/src/Pure/PIDE/document.ML	Mon Sep 09 19:00:53 2024 +0200
+++ b/src/Pure/PIDE/document.ML	Mon Sep 09 19:40:18 2024 +0200
@@ -635,7 +635,7 @@
     val _ = List.app (fn (thy, r) => Context_Position.reports_global thy [r]) parents_reports;
 
     val thy = Resources.begin_theory master_dir header parents;
-    val _ = Output.status [Markup.markup_only Markup.initialized];
+    val _ = Output.status [YXML.output_markup_only Markup.initialized];
   in thy end;
 
 fun get_special_parent node =
@@ -785,10 +785,10 @@
             val consolidate =
               Command.print0 {pri = Task_Queue.urgent_pri + 1, print_fn = fn _ => fn _ =>
                 let
-                  val _ = Output.status [Markup.markup_only Markup.consolidating];
+                  val _ = Output.status [YXML.output_markup_only Markup.consolidating];
                   val result = Exn.capture (Thy_Info.apply_presentation context) thy;
                   val _ = Lazy.force (get_consolidated node);
-                  val _ = Output.status [Markup.markup_only Markup.consolidated];
+                  val _ = Output.status [YXML.output_markup_only Markup.consolidated];
                 in Exn.release result end};
             val result_entry =
               (case lookup_entry node id of
diff -r b866d1510bd0 -r 7feaa04d332b src/Pure/PIDE/execution.ML
--- a/src/Pure/PIDE/execution.ML	Mon Sep 09 19:00:53 2024 +0200
+++ b/src/Pure/PIDE/execution.ML	Mon Sep 09 19:40:18 2024 +0200
@@ -141,7 +141,7 @@
     val props =
       if ! Multithreading.trace >= 2
       then [(Markup.taskN, Task_Queue.str_of_task task)] else [];
-  in Output.status (map (Markup.markup_only o Markup.properties props) markups) end;
+  in Output.status (map (YXML.output_markup_only o Markup.properties props) markups) end;
 
 type params = {name: string, pos: Position.T, pri: int};
 
diff -r b866d1510bd0 -r 7feaa04d332b src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Mon Sep 09 19:00:53 2024 +0200
+++ b/src/Pure/PIDE/markup.ML	Mon Sep 09 19:40:18 2024 +0200
@@ -285,7 +285,6 @@
   val enclose: T -> Output.output -> Output.output
   val markup: T -> string -> string
   val markups: T list -> string -> string
-  val markup_only: T -> string
   val markup_report: string -> string
 end;
 
@@ -874,8 +873,6 @@
 
 val markups = fold_rev markup;
 
-fun markup_only m = markup m "";
-
 fun markup_report "" = ""
   | markup_report txt = markup report txt;
 
diff -r b866d1510bd0 -r 7feaa04d332b src/Pure/PIDE/query_operation.ML
--- a/src/Pure/PIDE/query_operation.ML	Mon Sep 09 19:00:53 2024 +0200
+++ b/src/Pure/PIDE/query_operation.ML	Mon Sep 09 19:40:18 2024 +0200
@@ -22,7 +22,7 @@
         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 (Markup.markup_only m);
+            fun status m = output_result (YXML.output_markup_only m);
             fun writeln_result s = output_result (Markup.markup Markup.writeln s);
             fun toplevel_error exn =
               output_result (Markup.markup Markup.error (Runtime.exn_message exn));
diff -r b866d1510bd0 -r 7feaa04d332b src/Pure/PIDE/yxml.ML
--- a/src/Pure/PIDE/yxml.ML	Mon Sep 09 19:00:53 2024 +0200
+++ b/src/Pure/PIDE/yxml.ML	Mon Sep 09 19:40:18 2024 +0200
@@ -28,6 +28,7 @@
   val bytes_of: XML.tree -> Bytes.T
   val write_body: Path.T -> XML.body -> unit
   val output_markup: Markup.T -> string * string
+  val output_markup_only: Markup.T -> string
   val output_markup_elem: Markup.T -> (string * string) * string
   val markup_ops: Markup.ops
   val parse_body: string -> XML.body
@@ -95,6 +96,8 @@
   if Markup.is_empty markup then Markup.no_output
   else (XY ^ name ^ implode (map (fn p => Y ^ Properties.print_eq p) atts) ^ X, XYX);
 
+val output_markup_only = op ^ o output_markup;
+
 fun output_markup_elem markup =
   let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text)))
   in ((bg1, bg2), en) end;