tuned;
authorwenzelm
Fri, 14 Feb 2014 20:58:48 +0100
changeset 55496 5d2835453ad3
parent 55495 b389f65edc44
child 55497 c0f8aebfb43d
tuned;
src/Pure/ML/ml_lex.ML
--- a/src/Pure/ML/ml_lex.ML	Fri Feb 14 16:27:29 2014 +0100
+++ b/src/Pure/ML/ml_lex.ML	Fri Feb 14 20:58:48 2014 +0100
@@ -142,12 +142,6 @@
 fun !!! msg = Symbol_Pos.!!! (fn () => err_prefix ^ msg);
 
 
-(* blanks *)
-
-val scan_blank = Scan.one (Symbol.is_ascii_blank o Symbol_Pos.symbol);
-val scan_blanks1 = Scan.repeat1 scan_blank;
-
-
 (* keywords *)
 
 val keywords = ["#", "(", ")", ",", "->", "...", ":", ":>", ";", "=",
@@ -167,9 +161,7 @@
 local
 
 val scan_letdigs =
-  Scan.many
-    ((Symbol.is_ascii_letter orf Symbol.is_ascii_digit orf Symbol.is_ascii_quasi) o
-      Symbol_Pos.symbol);
+  Scan.many (Symbol.is_ascii_letdig o Symbol_Pos.symbol);
 
 val scan_alphanumeric =
   Scan.one (Symbol.is_ascii_letter o Symbol_Pos.symbol) -- scan_letdigs >> op ::;
@@ -181,10 +173,10 @@
 
 val scan_ident = scan_alphanumeric || scan_symbolic;
 
-val scan_longident =
+val scan_long_ident =
   (Scan.repeat1 (scan_alphanumeric @@@ $$$ ".") >> flat) @@@ (scan_ident || $$$ "=");
 
-val scan_typevar = $$$ "'" @@@ scan_letdigs;
+val scan_type_var = $$$ "'" @@@ scan_letdigs;
 
 end;
 
@@ -197,6 +189,7 @@
 val scan_hex = Scan.many1 (Symbol.is_ascii_hex o Symbol_Pos.symbol);
 val scan_sign = Scan.optional ($$$ "~") [];
 val scan_decint = scan_sign @@@ scan_dec;
+val scan_exp = ($$$ "E" || $$$ "e") @@@ scan_decint;
 
 in
 
@@ -206,8 +199,6 @@
 
 val scan_int = scan_sign @@@ ($$$ "0" @@@ $$$ "x" @@@ scan_hex || scan_dec);
 
-val scan_exp = ($$$ "E" || $$$ "e") @@@ scan_decint;
-
 val scan_real =
   scan_decint @@@ $$$ "." @@@ scan_dec @@@ Scan.optional scan_exp [] ||
   scan_decint @@@ scan_exp;
@@ -217,6 +208,8 @@
 
 (* chars and strings *)
 
+val scan_blanks1 = Scan.many1 (Symbol.is_ascii_blank o Symbol_Pos.symbol);
+
 local
 
 val scan_escape =
@@ -269,9 +262,9 @@
    (scan_word >> token Word ||
     scan_real >> token Real ||
     scan_int >> token Int ||
-    scan_longident >> token LongIdent ||
+    scan_long_ident >> token LongIdent ||
     scan_ident >> token Ident ||
-    scan_typevar >> token TypeVar));
+    scan_type_var >> token TypeVar));
 
 val scan_antiq = Antiquote.scan_antiq >> Antiquote.Antiq || scan_ml >> Antiquote.Text;