# HG changeset patch
# User wenzelm
# Date 1725283392 -7200
# Node ID 090adcdceaaefc77057e698d23fff3ae6f89263e
# Parent  f52eb69564a404806bfe06427eb875e7b3aec63e
clarified modules;

diff -r f52eb69564a4 -r 090adcdceaae src/Pure/General/output_primitives.ML
--- a/src/Pure/General/output_primitives.ML	Mon Sep 02 14:36:35 2024 +0200
+++ b/src/Pure/General/output_primitives.ML	Mon Sep 02 15:23:12 2024 +0200
@@ -6,14 +6,6 @@
 
 signature OUTPUT_PRIMITIVES =
 sig
-  structure XML:
-  sig
-    type attributes = (string * string) list
-    datatype tree =
-        Elem of (string * attributes) * tree list
-      | Text of string
-    type body = tree list
-  end
   type output = string
   type serial = int
   type properties = (string * string) list
@@ -37,22 +29,6 @@
 structure Output_Primitives: OUTPUT_PRIMITIVES =
 struct
 
-(** XML trees **)
-
-structure XML =
-struct
-
-type attributes = (string * string) list;
-
-datatype tree =
-    Elem of (string * attributes) * tree list
-  | Text of string;
-
-type body = tree list;
-
-end;
-
-
 (* output *)
 
 type output = string;
diff -r f52eb69564a4 -r 090adcdceaae src/Pure/PIDE/xml.ML
--- a/src/Pure/PIDE/xml.ML	Mon Sep 02 14:36:35 2024 +0200
+++ b/src/Pure/PIDE/xml.ML	Mon Sep 02 15:23:12 2024 +0200
@@ -15,8 +15,8 @@
   val int_atom: int A
   val bool_atom: bool A
   val unit_atom: unit A
-  val self: Output_Primitives.XML.body T
-  val tree: Output_Primitives.XML.tree T
+  val self: XML.body T
+  val tree: XML.tree T
   val properties: Properties.T T
   val string: string T
   val int: int T
@@ -31,11 +31,7 @@
 
 signature XML =
 sig
-  type attributes = (string * string) list
-  datatype tree =
-      Elem of (string * attributes) * tree list
-    | Text of string
-  type body = tree list
+  include XML
   val blob: string list -> body
   val is_empty: tree -> bool
   val is_empty_body: body -> bool
@@ -71,7 +67,7 @@
 
 (** XML trees **)
 
-open Output_Primitives.XML;
+open XML;
 
 val blob =
   let
diff -r f52eb69564a4 -r 090adcdceaae src/Pure/PIDE/xml_type.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/xml_type.ML	Mon Sep 02 15:23:12 2024 +0200
@@ -0,0 +1,27 @@
+(*  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
+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;
+
+end;
diff -r f52eb69564a4 -r 090adcdceaae src/Pure/ROOT0.ML
--- a/src/Pure/ROOT0.ML	Mon Sep 02 14:36:35 2024 +0200
+++ b/src/Pure/ROOT0.ML	Mon Sep 02 15:23:12 2024 +0200
@@ -3,6 +3,7 @@
 ML_file "ML/ml_statistics.ML";
 
 ML_file "General/exn.ML";
+ML_file "PIDE/xml_type.ML";
 ML_file "General/output_primitives.ML";
 
 ML_file "Concurrent/thread_attributes.ML";