1.1 --- a/src/Pure/General/xml.ML	Fri Jun 18 20:07:42 2004 +0200
     1.2 +++ b/src/Pure/General/xml.ML	Fri Jun 18 20:07:51 2004 +0200
     1.3 @@ -3,29 +3,41 @@
     1.4      Author:     David Aspinall, Stefan Berghofer and Markus Wenzel
     1.5      License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.6  
     1.7 -Basic support for XML input and output.
     1.8 +Basic support for XML.
     1.9  *)
    1.10  
    1.11  signature XML =
    1.12  sig
    1.13 +  val header: string
    1.14 +  val text: string -> string
    1.15 +  val cdata: string -> string
    1.16 +  val element: string -> (string * string) list -> string list -> string
    1.17    datatype tree =
    1.18        Elem of string * (string * string) list * tree list
    1.19      | Text of string
    1.20 -  val element: string -> (string * string) list -> string list -> string
    1.21 -  val text: string -> string
    1.22 -  val cdata: string -> string
    1.23 -  val header: string
    1.24    val string_of_tree: tree -> string
    1.25 -  val tree_of_string: string -> tree
    1.26    val parse_content: string list -> tree list * string list
    1.27    val parse_elem: string list -> tree * string list
    1.28    val parse_document: string list -> (string option * tree) * string list
    1.29 +  val tree_of_string: string -> tree
    1.30  end;
    1.31  
    1.32  structure XML: XML =
    1.33  struct
    1.34  
    1.35 -(* character data *)
    1.36 +(** string based representation (small scale) **)
    1.37 +
    1.38 +val header = "<?xml version=\"1.0\"?>\n";
    1.39 +
    1.40 +
    1.41 +(* text and character data *)
    1.42 +
    1.43 +fun decode "&lt;" = "<"
    1.44 +  | decode "&gt;" = ">"
    1.45 +  | decode "&amp;" = "&"
    1.46 +  | decode "&apos;" = "'"
    1.47 +  | decode "&quot;" = "\""
    1.48 +  | decode c = c;
    1.49  
    1.50  fun encode "<" = "&lt;"
    1.51    | encode ">" = "&gt;"
    1.52 @@ -34,27 +46,13 @@
    1.53    | encode "\"" = "&quot;"
    1.54    | encode c = c;
    1.55  
    1.56 -fun decode "&lt;" = "<"
    1.57 -  | decode "&gt;" = ">"
    1.58 -  | decode "&amp;" = "&"
    1.59 -  | decode "&apos;" = "'"
    1.60 -  | decode "&quot;" = "\""
    1.61 -  | decode c = c;
    1.62 -
    1.63  val text = Library.translate_string encode;
    1.64  
    1.65 -val cdata_open  = "<![CDATA["
    1.66 -val cdata_close = "]]>"
    1.67 -
    1.68 -fun cdata s = cdata_open ^ s ^ cdata_close;
    1.69 +val cdata = enclose "<![CDATA[" "]]>";
    1.70  
    1.71  
    1.72  (* elements *)
    1.73  
    1.74 -datatype tree =
    1.75 -    Elem of string * (string * string) list * tree list
    1.76 -  | Text of string;
    1.77 -
    1.78  fun attribute (a, x) = a ^ " = \"" ^ text x ^ "\"";
    1.79  
    1.80  fun element name atts cs =
    1.81 @@ -63,14 +61,34 @@
    1.82      else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name
    1.83    end;
    1.84  
    1.85 -fun string_of_tree (Elem (name, atts, ts)) =
    1.86 -      element name atts (map string_of_tree ts)
    1.87 -  | string_of_tree (Text s) = s;
    1.88  
    1.89 -val header = "<?xml version=\"1.0\"?>\n";
    1.90  
    1.91 +(** explicit XML trees **)
    1.92  
    1.93 -(* parser *)
    1.94 +datatype tree =
    1.95 +    Elem of string * (string * string) list * tree list
    1.96 +  | Text of string;
    1.97 +
    1.98 +fun string_of_tree tree =
    1.99 +  let
   1.100 +    fun string_of (Elem (name, atts, ts)) buf =
   1.101 +        let val buf' =
   1.102 +          buf |> Buffer.add "<"
   1.103 +          |> fold Buffer.add (separate " " (name :: map attribute atts))
   1.104 +        in
   1.105 +          if null ts then
   1.106 +            buf' |> Buffer.add "/>"
   1.107 +          else
   1.108 +            buf' |> Buffer.add ">"
   1.109 +            |> fold string_of ts
   1.110 +            |> Buffer.add "</" |> Buffer.add name |> Buffer.add ">"
   1.111 +        end
   1.112 +      | string_of (Text s) buf = Buffer.add (text s) buf;
   1.113 +  in Buffer.content (string_of tree Buffer.empty) end;
   1.114 +
   1.115 +
   1.116 +
   1.117 +(** XML parsing **)
   1.118  
   1.119  fun err s (xs, _) =
   1.120    "XML parsing error: " ^ s ^ "\nfound: " ^ quote (Symbol.beginning 100 xs);