# HG changeset patch
# User wenzelm
# Date 1726080317 -7200
# Node ID 64dc09f7f189927ed32f9e01e232c00900b3eb53
# Parent  96c895da5d8c066385cb6147c2b18db0ee444dac
clarified YXML bootstrap;

diff -r 96c895da5d8c -r 64dc09f7f189 src/Pure/PIDE/xml0.ML
--- a/src/Pure/PIDE/xml0.ML	Wed Sep 11 20:06:12 2024 +0200
+++ b/src/Pure/PIDE/xml0.ML	Wed Sep 11 20:45:17 2024 +0200
@@ -1,9 +1,11 @@
 (*  Title:      Pure/PIDE/xml0.ML
     Author:     Makarius
 
-Untyped XML trees (bootstrap).
+Untyped XML trees and YXML notation: minimal bootstrap version.
 *)
 
+(** XML **)
+
 signature XML =
 sig
   type attributes = (string * string) list
@@ -70,3 +72,46 @@
   String.concat (rev (traverse_texts (fn x => fn xs => x :: xs) body []));
 
 end;
+
+
+
+(** YXML **)
+
+signature YXML =
+sig
+  val X_char: char
+  val Y_char: char
+  val X: string
+  val Y: string
+  val XY: string
+  val XYX: string
+  val detect: string -> bool
+  val output_markup: string * XML.attributes -> string * string
+end;
+
+structure YXML: YXML =
+struct
+
+(* markers *)
+
+val X_char = Char.chr 5;
+val Y_char = Char.chr 6;
+
+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;
+
+
+(* output markup *)
+
+fun output_markup ("", _) = ("", "")
+  | output_markup (name, atts) =
+      let
+        val bgs = XY :: name :: List.foldr (fn ((a, b), ps) => Y :: a :: "=" :: b :: ps) [X] atts;
+        val en = XYX;
+      in (String.concat bgs, en) end;
+
+end;
diff -r 96c895da5d8c -r 64dc09f7f189 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