src/Pure/PIDE/yxml.ML

--- a/src/Pure/PIDE/yxml.ML	Wed Sep 11 20:06:12 2024 +0200
+++ b/src/Pure/PIDE/yxml.ML	Wed Sep 11 20:45:17 2024 +0200
@@ -16,9 +16,7 @@
 
 signature YXML =
 sig
-  val X: Symbol.symbol
-  val Y: Symbol.symbol
-  val detect: string -> bool
+  include YXML
   val traverse: (string -> 'a -> 'a) -> XML.tree -> 'a -> 'a
   val tree_size: XML.tree -> int
   val body_size: XML.body -> int
@@ -27,7 +25,6 @@
   val bytes_of_body: XML.body -> Bytes.T
   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
@@ -41,20 +38,10 @@
 structure YXML: YXML =
 struct
 
-(** string representation **)
-
-(* markers *)
-
-val X_char = Char.chr 5;
-val Y_char = Char.chr 6;
+open YXML;
 
-val X = String.str X_char;
-val Y = String.str Y_char;
-val XY = X ^ Y;
-val XYX = XY ^ X;
 
-fun detect s = Char.contains s X_char orelse Char.contains s Y_char;
-
+(** string representation **)
 
 (* traverse *)
 
@@ -92,14 +79,6 @@
 val Z = chr 0;
 val Z_text = [XML.Text Z];
 
-fun output_markup (markup as (name, atts)) =
-  if Markup.is_empty markup then Markup.no_output
-  else
-    let
-      val bgs = XY :: name :: fold_rev (fn p => cons Y o cons (Properties.print_eq p)) atts [X];
-      val en = XYX;
-    in (implode bgs, en) end;
-
 val output_markup_only = op ^ o output_markup;
 
 fun output_markup_elem markup =
@@ -109,6 +88,7 @@
 val markup_ops: Markup.ops = {output = output_markup};
 
 
+
 (** efficient YXML parsing **)
 
 local