src/Pure/Tools/xml.ML
changeset 24022 ab76c73b3b58
parent 23784 75e6b9dd5336
     1.1 --- a/src/Pure/Tools/xml.ML	Sat Jul 28 20:40:26 2007 +0200
     1.2 +++ b/src/Pure/Tools/xml.ML	Sat Jul 28 20:40:27 2007 +0200
     1.3 @@ -132,8 +132,8 @@
     1.4  
     1.5  val parse_att =
     1.6    Symbol.scan_id --| scan_whspc --| $$ "=" --| scan_whspc --
     1.7 -  (($$ "\"" || $$ "'") :-- (fn s => (Scan.repeat (Scan.unless ($$ s)
     1.8 -    (scan_special || Scan.one Symbol.is_regular)) >> implode) --| $$ s) >> snd);
     1.9 +  (($$ "\"" || $$ "'") :|-- (fn s => (Scan.repeat (Scan.unless ($$ s)
    1.10 +    (scan_special || Scan.one Symbol.is_regular)) >> implode) --| $$ s));
    1.11  
    1.12  val parse_comment = Scan.this_string "<!--" --
    1.13    Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.is_regular)) --