# HG changeset patch
# User wenzelm
# Date 1007818748 -3600
# Node ID 9b3e7a35da30561230fb0650354c6fe258c95714
# Parent  74977582a585c8b7303f2f6bb744ba9cd670c8c1
Basic support for XML output.

diff -r 74977582a585 -r 9b3e7a35da30 src/Pure/General/xml.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/xml.ML	Sat Dec 08 14:39:08 2001 +0100
@@ -0,0 +1,43 @@
+(*  Title:      Pure/General/xml.ML
+    ID:         $Id$
+    Author:     Markus Wenzel, LMU München
+    License:    GPL (GNU GENERAL PUBLIC LICENSE)
+
+Basic support for XML output.
+*)
+
+signature XML =
+sig
+  val element: string -> (string * string) list -> string list -> string
+  val text: string -> string
+  val header: string
+end;
+
+structure XML: XML =
+struct
+
+(* character data *)
+
+fun encode "<" = "&lt;"
+  | encode ">" = "&gt;"
+  | encode "&" = "&amp;"
+  | encode "'" = "&apos;"
+  | encode "\"" = "&quot;"
+  | encode c = c;
+
+val text = implode o map encode o explode;
+
+
+(* elements *)
+
+fun attribute (a, x) = a ^ " = " ^ quote (text x);
+
+fun element name atts cs =
+  let val elem = space_implode " " (name :: map attribute atts) in
+    if null cs then enclose "<" "/>" elem
+    else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name
+  end;
+
+val header = "<?xml version=\"1.0\"?>\n";
+
+end;