--- a/src/Pure/General/xml.ML Tue Jun 01 18:51:55 2004 +0200
+++ b/src/Pure/General/xml.ML Tue Jun 01 18:52:38 2004 +0200
@@ -93,6 +93,11 @@
(Scan.repeat (Scan.unless ($$ "\"")
(scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ "\"";
+val parse_att2 =
+ Symbol.scan_id --| scan_whspc --| $$ "=" --| scan_whspc --| $$ "'" --
+ (Scan.repeat (Scan.unless ($$ "'")
+ (scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ "'";
+
val parse_comment = scan_lit "<!--" --
Scan.repeat (Scan.unless (scan_lit "-->") (Scan.one Symbol.not_eof)) --
scan_lit "-->";
@@ -113,7 +118,7 @@
and parse_elem xs =
($$ "<" |-- Symbol.scan_id --
- Scan.repeat (scan_whspc |-- parse_att) --| scan_whspc :-- (fn (s, _) =>
+ Scan.repeat (scan_whspc |-- (parse_att || parse_att2)) --| scan_whspc :-- (fn (s, _) =>
!! (err "Expected > or />")
(scan_lit "/>" >> K []
|| $$ ">" |-- parse_content --|