# HG changeset patch
# User wenzelm
# Date 1726049909 -7200
# Node ID 885343964b7f2247bd7e863f2ca0026d53105d40
# Parent  e3a419073736037c67c40a77f3a701f3a86f9a57
clarified files;

diff -r e3a419073736 -r 885343964b7f src/Pure/PIDE/xml0.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/xml0.ML	Wed Sep 11 12:18:29 2024 +0200
@@ -0,0 +1,70 @@
+(*  Title:      Pure/PIDE/xml0.ML
+    Author:     Makarius
+
+Untyped XML trees (bootstrap).
+*)
+
+signature XML =
+sig
+  type attributes = (string * string) list
+  datatype tree =
+      Elem of (string * attributes) * tree list
+    | Text of string
+  type body = tree list
+  val xml_elemN: string
+  val xml_nameN: string
+  val xml_bodyN: string
+  val wrap_elem: ((string * attributes) * body) * body -> tree
+  val unwrap_elem: tree -> (((string * attributes) * body) * body) option
+  val unwrap_elem_body: tree -> body option
+  val content_of: body -> string
+end
+
+structure XML: XML =
+struct
+
+type attributes = (string * string) list;
+
+datatype tree =
+    Elem of (string * attributes) * tree list
+  | Text of string;
+
+type body = tree list;
+
+
+(* wrapped elements *)
+
+val xml_elemN = "xml_elem";
+val xml_nameN = "xml_name";
+val xml_bodyN = "xml_body";
+
+fun wrap_elem (((a, atts), body1), body2) =
+  Elem ((xml_elemN, (xml_nameN, a) :: atts), Elem ((xml_bodyN, []), body1) :: body2);
+
+fun unwrap_elem (Elem ((name, (n, a) :: atts), Elem ((name', []), body1) :: body2)) =
+      if name = xml_elemN andalso n = xml_nameN andalso name' = xml_bodyN
+      then SOME (((a, atts), body1), body2) else NONE
+  | unwrap_elem _ = NONE;
+
+fun unwrap_elem_body (Elem ((name, (n, _) :: _), Elem ((name', []), _) :: body)) =
+      if name = xml_elemN andalso n = xml_nameN andalso name' = xml_bodyN
+      then SOME body else NONE
+  | unwrap_elem_body _ = NONE;
+
+
+(* text content *)
+
+fun add_contents [] res = res
+  | add_contents (t :: ts) res = add_contents ts (add_content t res)
+and add_content tree res =
+  (case unwrap_elem_body tree of
+    SOME ts => add_contents ts res
+  | NONE =>
+      (case tree of
+        Elem (_, ts) => add_contents ts res
+      | Text s => s :: res));
+
+fun content_of body =
+  String.concat (rev (add_contents body []));
+
+end;
diff -r e3a419073736 -r 885343964b7f src/Pure/PIDE/xml_type.ML
--- a/src/Pure/PIDE/xml_type.ML	Wed Sep 11 12:11:47 2024 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,70 +0,0 @@
-(*  Title:      Pure/PIDE/xml_type.ML
-    Author:     Makarius
-
-Untyped XML trees: minimal type definitions.
-*)
-
-signature XML =
-sig
-  type attributes = (string * string) list
-  datatype tree =
-      Elem of (string * attributes) * tree list
-    | Text of string
-  type body = tree list
-  val xml_elemN: string
-  val xml_nameN: string
-  val xml_bodyN: string
-  val wrap_elem: ((string * attributes) * body) * body -> tree
-  val unwrap_elem: tree -> (((string * attributes) * body) * body) option
-  val unwrap_elem_body: tree -> body option
-  val content_of: body -> string
-end
-
-structure XML: XML =
-struct
-
-type attributes = (string * string) list;
-
-datatype tree =
-    Elem of (string * attributes) * tree list
-  | Text of string;
-
-type body = tree list;
-
-
-(* wrapped elements *)
-
-val xml_elemN = "xml_elem";
-val xml_nameN = "xml_name";
-val xml_bodyN = "xml_body";
-
-fun wrap_elem (((a, atts), body1), body2) =
-  Elem ((xml_elemN, (xml_nameN, a) :: atts), Elem ((xml_bodyN, []), body1) :: body2);
-
-fun unwrap_elem (Elem ((name, (n, a) :: atts), Elem ((name', []), body1) :: body2)) =
-      if name = xml_elemN andalso n = xml_nameN andalso name' = xml_bodyN
-      then SOME (((a, atts), body1), body2) else NONE
-  | unwrap_elem _ = NONE;
-
-fun unwrap_elem_body (Elem ((name, (n, _) :: _), Elem ((name', []), _) :: body)) =
-      if name = xml_elemN andalso n = xml_nameN andalso name' = xml_bodyN
-      then SOME body else NONE
-  | unwrap_elem_body _ = NONE;
-
-
-(* text content *)
-
-fun add_contents [] res = res
-  | add_contents (t :: ts) res = add_contents ts (add_content t res)
-and add_content tree res =
-  (case unwrap_elem_body tree of
-    SOME ts => add_contents ts res
-  | NONE =>
-      (case tree of
-        Elem (_, ts) => add_contents ts res
-      | Text s => s :: res));
-
-fun content_of body =
-  String.concat (rev (add_contents body []));
-
-end;
diff -r e3a419073736 -r 885343964b7f src/Pure/ROOT0.ML
--- a/src/Pure/ROOT0.ML	Wed Sep 11 12:11:47 2024 +0200
+++ b/src/Pure/ROOT0.ML	Wed Sep 11 12:18:29 2024 +0200
@@ -2,8 +2,9 @@
 
 ML_file "ML/ml_statistics.ML";
 
+ML_file "PIDE/xml0.ML";
+
 ML_file "General/exn.ML";
-ML_file "PIDE/xml_type.ML";
 ML_file "General/output_primitives.ML";
 
 ML_file "Concurrent/thread_attributes.ML";