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