added detect;
authorwenzelm
Thu Apr 03 16:03:55 2008 +0200 (2008-04-03)
changeset 2652514a56f013469
parent 26524 63953bec4c98
child 26526 d1557acb9ef9
added detect;
removed auxiliary buffer_of_tree;
tuned;
src/Pure/General/xml.ML
     1.1 --- a/src/Pure/General/xml.ML	Thu Apr 03 16:03:54 2008 +0200
     1.2 +++ b/src/Pure/General/xml.ML	Thu Apr 03 16:03:55 2008 +0200
     1.3 @@ -8,6 +8,7 @@
     1.4  signature XML =
     1.5  sig
     1.6    (*string functions*)
     1.7 +  val detect: string -> bool
     1.8    val header: string
     1.9    val text: string -> string
    1.10    type attributes = (string * string) list
    1.11 @@ -20,7 +21,6 @@
    1.12      | Output of output
    1.13    type content = tree list
    1.14    type element = string * attributes * content
    1.15 -  val buffer_of_tree: tree -> Buffer.T
    1.16    val string_of_tree: tree -> string
    1.17    val plain_content: tree -> string
    1.18    val parse_string : string -> string option
    1.19 @@ -34,8 +34,10 @@
    1.20  structure XML: XML =
    1.21  struct
    1.22  
    1.23 -(** string based representation (small scale) **)
    1.24  
    1.25 +(** string representation **)
    1.26 +
    1.27 +val detect = String.isPrefix "<?xml";
    1.28  val header = "<?xml version=\"1.0\"?>\n";
    1.29  
    1.30  
    1.31 @@ -62,10 +64,13 @@
    1.32  
    1.33  fun attribute (a, x) = a ^ " = \"" ^ text x ^ "\"";
    1.34  
    1.35 -fun element name atts cs =
    1.36 -  let val elem = space_implode " " (name :: map attribute atts) in
    1.37 -    if null cs then enclose "<" "/>" elem
    1.38 -    else enclose "<" ">" elem ^ implode cs ^ enclose "</" ">" name
    1.39 +fun element name atts body =
    1.40 +  let
    1.41 +    val elem = space_implode " " (name :: map attribute atts);
    1.42 +    val b = implode body;
    1.43 +  in
    1.44 +    if b = "" then enclose "<" "/>" elem
    1.45 +    else enclose "<" ">" elem ^ b ^ enclose "</" ">" name
    1.46    end;
    1.47  
    1.48  
    1.49 @@ -82,25 +87,18 @@
    1.50  type content = tree list;
    1.51  type element = string * attributes * content;
    1.52  
    1.53 -fun buffer_of_tree tree =
    1.54 +fun string_of_tree t =
    1.55    let
    1.56 -    fun string_of (Elem (name, atts, ts)) buf =
    1.57 -        let val buf' =
    1.58 -          buf |> Buffer.add "<"
    1.59 -          |> fold Buffer.add (separate " " (name :: map attribute atts))
    1.60 -        in
    1.61 -          if null ts then
    1.62 -            buf' |> Buffer.add "/>"
    1.63 -          else
    1.64 -            buf' |> Buffer.add ">"
    1.65 -            |> fold string_of ts
    1.66 -            |> Buffer.add "</" |> Buffer.add name |> Buffer.add ">"
    1.67 -        end
    1.68 -      | string_of (Text s) buf = Buffer.add (text s) buf
    1.69 -      | string_of (Output s) buf = Buffer.add s buf;
    1.70 -  in string_of tree Buffer.empty end;
    1.71 -
    1.72 -val string_of_tree = Buffer.content o buffer_of_tree;
    1.73 +    fun name_atts name atts = fold Buffer.add (separate " " (name :: map attribute atts));
    1.74 +    fun tree (Elem (name, atts, [])) =
    1.75 +          Buffer.add "<" #> name_atts name atts #> Buffer.add "/>"
    1.76 +      | tree (Elem (name, atts, ts)) =
    1.77 +          Buffer.add "<" #> name_atts name atts #> Buffer.add ">" #>
    1.78 +          fold tree ts #>
    1.79 +          Buffer.add "</" #> Buffer.add name #> Buffer.add ">"
    1.80 +      | tree (Text s) = Buffer.add (text s)
    1.81 +      | tree (Output s) = Buffer.add s;
    1.82 +  in Buffer.empty |> tree t |> Buffer.content end;
    1.83  
    1.84  fun plain_content tree =
    1.85    let