--- 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;