--- a/src/Pure/PIDE/yxml.ML Wed Sep 11 20:45:17 2024 +0200
+++ b/src/Pure/PIDE/yxml.ML Wed Sep 11 21:25:15 2024 +0200
@@ -27,7 +27,6 @@
val write_body: Path.T -> XML.body -> unit
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
val parse_body_bytes: Bytes.T -> XML.body
val parse: string -> XML.tree
@@ -85,8 +84,6 @@
let val [bg1, bg2, en] = space_explode Z (string_of (XML.wrap_elem ((markup, Z_text), Z_text)))
in ((bg1, bg2), en) end;
-val markup_ops: Markup.ops = {output = output_markup};
-
(** efficient YXML parsing **)