added output_markup (from Tools/isabelle_process.ML);
major cleanup of signature;

--- a/src/Pure/General/xml.ML	Thu Apr 03 18:42:36 2008 +0200
+++ b/src/Pure/General/xml.ML	Thu Apr 03 18:42:37 2008 +0200
@@ -11,9 +11,9 @@
   val detect: string -> bool
   val header: string
   val text: string -> string
-  type attributes = (string * string) list
-  val attribute: string * string -> string
+  type attributes = Markup.property list
   val element: string -> attributes -> string list -> string
+  val output_markup: Markup.T -> output * output
   (*tree functions*)
   datatype tree =
       Elem of string * attributes * tree list
@@ -21,14 +21,14 @@
     | Output of output
   type content = tree list
   type element = string * attributes * content
-  val string_of_tree: tree -> string
+  val string_of: tree -> string
   val plain_content: tree -> string
   val parse_string : string -> string option
+  val parse_comment_whspc: string list -> unit * string list
   val parse_content: string list -> tree list * string list
   val parse_elem: string list -> tree * string list
   val parse_document: string list -> (string option * tree) * string list
-  val tree_of_string: string -> tree
-  val scan_comment_whspc: string list -> unit * string list
+  val parse: string -> tree
 end;
 
 structure XML: XML =
@@ -62,23 +62,25 @@
 
 (* elements *)
 
-fun attribute (a, x) = a ^ " = \"" ^ text x ^ "\"";
+type attributes = Markup.property list;
+
+fun elem name atts =
+  space_implode " " (name :: map (fn (a, x) => a ^ " = \"" ^ text x ^ "\"") atts);
 
 fun element name atts body =
-  let
-    val elem = space_implode " " (name :: map attribute atts);
-    val b = implode body;
-  in
-    if b = "" then enclose "<" "/>" elem
-    else enclose "<" ">" elem ^ b ^ enclose "</" ">" name
+  let val b = implode body in
+    if b = "" then enclose "<" "/>" (elem name atts)
+    else enclose "<" ">" (elem name atts) ^ b ^ enclose "</" ">" name
   end;
 
+fun output_markup (name, atts) =
+ (enclose "<" ">" (elem name atts),
+  enclose "</" ">" name);
+
 
 
 (** explicit XML trees **)
 
-type attributes = (string * string) list;
-
 datatype tree =
     Elem of string * attributes * tree list
   | Text of string
@@ -87,13 +89,12 @@
 type content = tree list;
 type element = string * attributes * content;
 
-fun string_of_tree t =
+fun string_of t =
   let
-    fun name_atts name atts = fold Buffer.add (separate " " (name :: map attribute atts));
     fun tree (Elem (name, atts, [])) =
-          Buffer.add "<" #> name_atts name atts #> Buffer.add "/>"
+          Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add "/>"
       | tree (Elem (name, atts, ts)) =
-          Buffer.add "<" #> name_atts name atts #> Buffer.add ">" #>
+          Buffer.add "<" #> Buffer.add (elem name atts) #> Buffer.add ">" #>
           fold tree ts #>
           Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
       | tree (Text s) = Buffer.add (text s)
@@ -136,7 +137,7 @@
   Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.is_regular)) --
   Scan.this_string "-->";
 
-val scan_comment_whspc =
+val parse_comment_whspc =
   (scan_whspc >> K()) --| (Scan.repeat (parse_comment |-- (scan_whspc >> K())));
 
 val parse_pi = Scan.this_string "<?" |--
@@ -169,7 +170,7 @@
       (Scan.one Symbol.is_regular)) >> implode) --| $$ ">" --| scan_whspc) --
   parse_elem;
 
-fun tree_of_string s =
+fun parse s =
   (case Scan.finite Symbol.stopper (Scan.error (!! (err "Malformed element")
       (scan_whspc |-- parse_elem --| scan_whspc))) (Symbol.explode s) of
     (x, []) => x