# HG changeset patch
# User aspinall
# Date 1165178814 -3600
# Node ID c762bdc2b504db2b0d69008af46aa79427b2f4f0
# Parent  7ab9ad8d67576cc7e9cda7c5277f15b524517460
Add string buffer getter.  Add Rawtext constructor to allow XML-escaped strings in tree.

diff -r 7ab9ad8d6757 -r c762bdc2b504 src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Sun Dec 03 16:25:33 2006 +0100
+++ b/src/Pure/General/xml.ML	Sun Dec 03 21:46:54 2006 +0100
@@ -7,22 +7,27 @@
 
 signature XML =
 sig
-  type attributes = (string * string) list
-  datatype tree =
-      Elem of string * attributes * tree list
-    | Text of string
-  type element = string * attributes * tree list
+  (* string functions *)
   val header: string
   val text: string -> string
   val text_charref: string -> string
   val cdata: string -> string
+  type attributes = (string * string) list
   val element: string -> attributes -> string list -> string
+  (* tree functions *)
+  datatype tree =
+      Elem of string * attributes * tree list
+    | Text of string    (* native string, subject to XML.text on output *)
+    | Rawtext of string (* XML string: not parsed and output directly   *)
+  type element = string * attributes * tree list
   val string_of_tree: tree -> string
+  val buffer_of_tree: tree -> Buffer.T
   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
+  (* scanner for stream parser in proof_general.ML *)				
   val scan_comment_whspc : string list -> unit * string list
-  val tree_of_string: string -> tree
 end;
 
 structure XML: XML =
@@ -77,11 +82,12 @@
 
 datatype tree =
     Elem of string * attributes * tree list
-  | Text of string;
+  | Text of string      
+  | Rawtext of string;  
 
 type element = string * attributes * tree list
 
-fun string_of_tree tree =
+fun buffer_of_tree tree =
   let
     fun string_of (Elem (name, atts, ts)) buf =
         let val buf' =
@@ -95,8 +101,11 @@
             |> fold string_of ts
             |> Buffer.add "</" |> Buffer.add name |> Buffer.add ">"
         end
-      | string_of (Text s) buf = Buffer.add (text s) buf;
-  in Buffer.content (string_of tree Buffer.empty) end;
+      | string_of (Text s) buf = Buffer.add (text s) buf
+      | string_of (Rawtext s) buf = Buffer.add s buf;
+  in string_of tree Buffer.empty end;
+
+val string_of_tree = Buffer.content o buffer_of_tree;