# HG changeset patch
# User berghofe
# Date 1086342691 -7200
# Node ID 8b9a372b3e9008f05b9c4e8e2d7a77178157c6b4
# Parent  419b45cdb400ea4c2dc961c02badd883ef32bddf
Tuned parse_att.

diff -r 419b45cdb400 -r 8b9a372b3e90 src/Pure/General/xml.ML
--- a/src/Pure/General/xml.ML	Wed Jun 02 17:35:08 2004 +0200
+++ b/src/Pure/General/xml.ML	Fri Jun 04 11:51:31 2004 +0200
@@ -89,14 +89,9 @@
     implode) --| scan_lit "]]>";
 
 val parse_att =
-  Symbol.scan_id --| scan_whspc --| $$ "=" --| scan_whspc --| $$ "\"" --
-  (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) --| $$ "'";
+  Symbol.scan_id --| scan_whspc --| $$ "=" --| scan_whspc --
+  (($$ "\"" || $$ "'") :-- (fn s => (Scan.repeat (Scan.unless ($$ s)
+    (scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ s) >> snd);
 
 val parse_comment = scan_lit "<!--" --
   Scan.repeat (Scan.unless (scan_lit "-->") (Scan.one Symbol.not_eof)) --
@@ -118,7 +113,7 @@
 
 and parse_elem xs =
   ($$ "<" |-- Symbol.scan_id --
-    Scan.repeat (scan_whspc |-- (parse_att || parse_att2)) --| scan_whspc :-- (fn (s, _) =>
+    Scan.repeat (scan_whspc |-- parse_att) --| scan_whspc :-- (fn (s, _) =>
       !! (err "Expected > or />")
         (scan_lit "/>" >> K []
          || $$ ">" |-- parse_content --|