1.1 --- a/src/Pure/General/xml.ML	Sat May 29 15:10:56 2004 +0200
     1.2 +++ b/src/Pure/General/xml.ML	Sat May 29 15:11:06 2004 +0200
     1.3 @@ -77,29 +77,29 @@
     1.4  
     1.5  val scan_whspc = Scan.any Symbol.is_blank;
     1.6  
     1.7 -fun scan_string s = Scan.list (Symbol.explode s) >> K s;
     1.8 +fun scan_lit s = Scan.this (Symbol.explode s) >> K s;
     1.9  
    1.10  val scan_special = $$ "&" ^^ Symbol.scan_id ^^ $$ ";" >> decode;
    1.11  
    1.12  val parse_chars = Scan.repeat1 (Scan.unless (scan_whspc -- $$ "<")
    1.13    (scan_special || Scan.one Symbol.not_eof)) >> implode;
    1.14  
    1.15 -val parse_cdata = scan_string "<![CDATA[" |--
    1.16 -  (Scan.repeat (Scan.unless (scan_string "]]>") (Scan.one Symbol.not_eof)) >>
    1.17 -    implode) --| scan_string "]]>";
    1.18 +val parse_cdata = scan_lit "<![CDATA[" |--
    1.19 +  (Scan.repeat (Scan.unless (scan_lit "]]>") (Scan.one Symbol.not_eof)) >>
    1.20 +    implode) --| scan_lit "]]>";
    1.21  
    1.22  val parse_att =
    1.23    Symbol.scan_id --| scan_whspc --| $$ "=" --| scan_whspc --| $$ "\"" --
    1.24    (Scan.repeat (Scan.unless ($$ "\"")
    1.25      (scan_special || Scan.one Symbol.not_eof)) >> implode) --| $$ "\"";
    1.26  
    1.27 -val parse_comment = scan_string "<!--" --
    1.28 -  Scan.repeat (Scan.unless (scan_string "-->") (Scan.one Symbol.not_eof)) --
    1.29 -  scan_string "-->";
    1.30 +val parse_comment = scan_lit "<!--" --
    1.31 +  Scan.repeat (Scan.unless (scan_lit "-->") (Scan.one Symbol.not_eof)) --
    1.32 +  scan_lit "-->";
    1.33  
    1.34 -val parse_pi = scan_string "<?" |--
    1.35 -  Scan.repeat (Scan.unless (scan_string "?>") (Scan.one Symbol.not_eof)) --|
    1.36 -  scan_string "?>";
    1.37 +val parse_pi = scan_lit "<?" |--
    1.38 +  Scan.repeat (Scan.unless (scan_lit "?>") (Scan.one Symbol.not_eof)) --|
    1.39 +  scan_lit "?>";
    1.40  
    1.41  fun parse_content xs =
    1.42    ((Scan.optional (scan_whspc |-- parse_chars >> (single o Text)) [] --
    1.43 @@ -115,14 +115,14 @@
    1.44    ($$ "<" |-- Symbol.scan_id --
    1.45      Scan.repeat (scan_whspc |-- parse_att) --| scan_whspc :-- (fn (s, _) =>
    1.46        !! (err "Expected > or />")
    1.47 -        (scan_string "/>" >> K []
    1.48 +        (scan_lit "/>" >> K []
    1.49           || $$ ">" |-- parse_content --|
    1.50              !! (err ("Expected </" ^ s ^ ">"))
    1.51 -              (scan_string ("</" ^ s) --| scan_whspc --| $$ ">"))) >>
    1.52 +              (scan_lit ("</" ^ s) --| scan_whspc --| $$ ">"))) >>
    1.53      (fn ((s, atts), ts) => Elem (s, atts, ts))) xs;
    1.54  
    1.55  val parse_document =
    1.56 -  Scan.option (scan_string "<!DOCTYPE" -- scan_whspc |--
    1.57 +  Scan.option (scan_lit "<!DOCTYPE" -- scan_whspc |--
    1.58      (Scan.repeat (Scan.unless ($$ ">")
    1.59        (Scan.one Symbol.not_eof)) >> implode) --| $$ ">" --| scan_whspc) --
    1.60    parse_elem;