1.1 --- a/src/Pure/General/xml.ML	Mon Dec 04 15:15:59 2006 +0100
     1.2 +++ b/src/Pure/General/xml.ML	Mon Dec 04 16:55:08 2006 +0100
     1.3 @@ -22,6 +22,7 @@
     1.4    type element = string * attributes * tree list
     1.5    val string_of_tree: tree -> string
     1.6    val buffer_of_tree: tree -> Buffer.T
     1.7 +  val parse_string : string -> string option
     1.8    val parse_content: string list -> tree list * string list
     1.9    val parse_elem: string list -> tree * string list
    1.10    val parse_document: string list -> (string option * tree) * string list
    1.11 @@ -121,6 +122,8 @@
    1.12  val parse_chars = Scan.repeat1 (Scan.unless ((* scan_whspc -- *)$$ "<")
    1.13    (scan_special || Scan.one Symbol.not_eof)) >> implode;
    1.14  
    1.15 +val parse_string = Scan.read Symbol.stopper parse_chars o explode;
    1.16 +
    1.17  val parse_cdata = Scan.this_string "<![CDATA[" |--
    1.18    (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.not_eof)) >>
    1.19      implode) --| Scan.this_string "]]>";