src/Pure/ML/ml_lex.ML
changeset 40627 becf5d5187cc
parent 40525 14a2e686bdac
child 41502 967cbbc77abd
     1.1 --- a/src/Pure/ML/ml_lex.ML	Fri Nov 19 23:48:07 2010 +0100
     1.2 +++ b/src/Pure/ML/ml_lex.ML	Sat Nov 20 00:53:26 2010 +0100
     1.3 @@ -149,7 +149,7 @@
     1.4    "sharing", "sig", "signature", "struct", "structure", "then", "type",
     1.5    "val", "where", "while", "with", "withtype"];
     1.6  
     1.7 -val lex = Scan.make_lexicon (map explode keywords);
     1.8 +val lex = Scan.make_lexicon (map raw_explode keywords);
     1.9  fun scan_keyword x = Scan.literal lex x;
    1.10  
    1.11  
    1.12 @@ -166,7 +166,7 @@
    1.13    Scan.one (Symbol.is_ascii_letter o Symbol_Pos.symbol) -- scan_letdigs >> op ::;
    1.14  
    1.15  val scan_symbolic =
    1.16 -  Scan.many1 (member (op =) (explode "!#$%&*+-/:<=>?@\\^`|~") o Symbol_Pos.symbol);
    1.17 +  Scan.many1 (member (op =) (raw_explode "!#$%&*+-/:<=>?@\\^`|~") o Symbol_Pos.symbol);
    1.18  
    1.19  in
    1.20  
    1.21 @@ -211,7 +211,7 @@
    1.22  local
    1.23  
    1.24  val scan_escape =
    1.25 -  Scan.one (member (op =) (explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single ||
    1.26 +  Scan.one (member (op =) (raw_explode "\"\\abtnvfr") o Symbol_Pos.symbol) >> single ||
    1.27    $$$ "^" @@@ (Scan.one (fn (s, _) => ord "@" <= ord s andalso ord s <= ord "_") >> single) ||
    1.28    Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --
    1.29      Scan.one (Symbol.is_ascii_digit o Symbol_Pos.symbol) --