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;