1.1 --- a/src/Pure/General/xml.ML Tue Jun 01 18:51:55 2004 +0200
1.2 +++ b/src/Pure/General/xml.ML Tue Jun 01 18:52:38 2004 +0200
1.3 @@ -93,6 +93,11 @@
1.4 (Scan.repeat (Scan.unless ($$ "\"")
1.5 (scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ "\"";
1.6
1.7 +val parse_att2 =
1.8 + Symbol.scan_id --| scan_whspc --| $$ "=" --| scan_whspc --| $$ "'" --
1.9 + (Scan.repeat (Scan.unless ($$ "'")
1.10 + (scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ "'";
1.11 +
1.12 val parse_comment = scan_lit "<!--" --
1.13 Scan.repeat (Scan.unless (scan_lit "-->") (Scan.one Symbol.not_eof)) --
1.14 scan_lit "-->";
1.15 @@ -113,7 +118,7 @@
1.16
1.17 and parse_elem xs =
1.18 ($$ "<" |-- Symbol.scan_id --
1.19 - Scan.repeat (scan_whspc |-- parse_att) --| scan_whspc :-- (fn (s, _) =>
1.20 + Scan.repeat (scan_whspc |-- (parse_att || parse_att2)) --| scan_whspc :-- (fn (s, _) =>
1.21 !! (err "Expected > or />")
1.22 (scan_lit "/>" >> K []
1.23 || $$ ">" |-- parse_content --|