# HG changeset patch
# User aspinall
# Date 1086108758 -7200
# Node ID 49afb368f4bed2944339528d14342c1909ee1fe9
# Parent  a43f9e2c633263becb8be1305889ffb84dc72ae6
Add alternative syntax for attributes

diff -r a43f9e2c6332 -r 49afb368f4be src/Pure/General/xml.ML
--- 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 --|