# HG changeset patch # User wenzelm # Date 1392407928 -3600 # Node ID 5d2835453ad3ee422a2312a318ce746f5151df0a # Parent b389f65edc44ab9ca7b04cf7355ee537fb444512 tuned; diff -r b389f65edc44 -r 5d2835453ad3 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;