1.1 --- a/src/Pure/General/xml.ML	Wed Jun 02 17:35:08 2004 +0200
     1.2 +++ b/src/Pure/General/xml.ML	Fri Jun 04 11:51:31 2004 +0200
     1.3 @@ -89,14 +89,9 @@
     1.4      implode) --| scan_lit "]]>";
     1.5  
     1.6  val parse_att =
     1.7 -  Symbol.scan_id --| scan_whspc --| $$ "=" --| scan_whspc --| $$ "\"" --
     1.8 -  (Scan.repeat (Scan.unless ($$ "\"")
     1.9 -    (scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ "\"";
    1.10 -
    1.11 -val parse_att2 = 
    1.12 -  Symbol.scan_id --| scan_whspc --| $$ "=" --| scan_whspc --| $$ "'" --
    1.13 -  (Scan.repeat (Scan.unless ($$ "'")
    1.14 -    (scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ "'";
    1.15 +  Symbol.scan_id --| scan_whspc --| $$ "=" --| scan_whspc --
    1.16 +  (($$ "\"" || $$ "'") :-- (fn s => (Scan.repeat (Scan.unless ($$ s)
    1.17 +    (scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ s) >> snd);
    1.18  
    1.19  val parse_comment = scan_lit "<!--" --
    1.20    Scan.repeat (Scan.unless (scan_lit "-->") (Scan.one Symbol.not_eof)) --
    1.21 @@ -118,7 +113,7 @@
    1.22  
    1.23  and parse_elem xs =
    1.24    ($$ "<" |-- Symbol.scan_id --
    1.25 -    Scan.repeat (scan_whspc |-- (parse_att || parse_att2)) --| scan_whspc :-- (fn (s, _) =>
    1.26 +    Scan.repeat (scan_whspc |-- parse_att) --| scan_whspc :-- (fn (s, _) =>
    1.27        !! (err "Expected > or />")
    1.28          (scan_lit "/>" >> K []
    1.29           || $$ ">" |-- parse_content --|