src/Pure/Tools/xml.ML
changeset 23784 75e6b9dd5336
parent 23723 4fff46d5faaa
child 24022 ab76c73b3b58
     1.1 --- a/src/Pure/Tools/xml.ML	Wed Jul 11 12:23:34 2007 +0200
     1.2 +++ b/src/Pure/Tools/xml.ML	Wed Jul 11 17:47:45 2007 +0200
     1.3 @@ -122,28 +122,28 @@
     1.4  val scan_special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
     1.5  
     1.6  val parse_chars = Scan.repeat1 (Scan.unless ((* scan_whspc -- *)$$ "<")
     1.7 -  (scan_special || Scan.one Symbol.not_eof)) >> implode;
     1.8 +  (scan_special || Scan.one Symbol.is_regular)) >> implode;
     1.9  
    1.10  val parse_string = Scan.read Symbol.stopper parse_chars o explode;
    1.11  
    1.12  val parse_cdata = Scan.this_string "<![CDATA[" |--
    1.13 -  (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.not_eof)) >>
    1.14 +  (Scan.repeat (Scan.unless (Scan.this_string "]]>") (Scan.one Symbol.is_regular)) >>
    1.15      implode) --| Scan.this_string "]]>";
    1.16  
    1.17  val parse_att =
    1.18    Symbol.scan_id --| scan_whspc --| $$ "=" --| scan_whspc --
    1.19    (($$ "\"" || $$ "'") :-- (fn s => (Scan.repeat (Scan.unless ($$ s)
    1.20 -    (scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ s) >> snd);
    1.21 +    (scan_special || Scan.one Symbol.is_regular)) >> implode) --| $$ s) >> snd);
    1.22  
    1.23  val parse_comment = Scan.this_string "<!--" --
    1.24 -  Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.not_eof)) --
    1.25 +  Scan.repeat (Scan.unless (Scan.this_string "-->") (Scan.one Symbol.is_regular)) --
    1.26    Scan.this_string "-->";
    1.27  
    1.28  val scan_comment_whspc =
    1.29    (scan_whspc >> K()) --| (Scan.repeat (parse_comment |-- (scan_whspc >> K())));
    1.30  
    1.31  val parse_pi = Scan.this_string "<?" |--
    1.32 -  Scan.repeat (Scan.unless (Scan.this_string "?>") (Scan.one Symbol.not_eof)) --|
    1.33 +  Scan.repeat (Scan.unless (Scan.this_string "?>") (Scan.one Symbol.is_regular)) --|
    1.34    Scan.this_string "?>";
    1.35  
    1.36  fun parse_content xs =
    1.37 @@ -169,7 +169,7 @@
    1.38  val parse_document =
    1.39    Scan.option (Scan.this_string "<!DOCTYPE" -- scan_whspc |--
    1.40      (Scan.repeat (Scan.unless ($$ ">")
    1.41 -      (Scan.one Symbol.not_eof)) >> implode) --| $$ ">" --| scan_whspc) --
    1.42 +      (Scan.one Symbol.is_regular)) >> implode) --| $$ ">" --| scan_whspc) --
    1.43    parse_elem;
    1.44  
    1.45  fun tree_of_string s =