# HG changeset patch
# User aspinall
# Date 1165247708 -3600
# Node ID 88b815dca68d6d3ca459c7615a6666d37b036316
# Parent  32f3e1127de2773ba0b6410211b8103d92cde594
Add parse_string for attribute values and other string content

diff -r 32f3e1127de2 -r 88b815dca68d src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Mon Dec 04 15:15:59 2006 +0100
+++ b/src/Pure/General/xml.ML	Mon Dec 04 16:55:08 2006 +0100
@@ -22,6 +22,7 @@
   type element = string * attributes * tree list
   val string_of_tree: tree -> string
   val buffer_of_tree: tree -> Buffer.T
+  val parse_string : string -> string option
   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
@@ -121,6 +122,8 @@
 val parse_chars = Scan.repeat1 (Scan.unless ((* scan_whspc -- *)$$ "<")
   (scan_special || Scan.one Symbol.not_eof)) >> implode;
 
+val parse_string = Scan.read Symbol.stopper parse_chars o explode;
+
 val parse_cdata = Scan.this_string "<![CDATA[" |--
   (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.not_eof)) >>
     implode) --| Scan.this_string "]]>";