ML_Lex.keywords;
authorwenzelm
Sat Sep 15 19:26:17 2007 +0200 (2007-09-15)
changeset 2458257599da58045
parent 24581 6491d89ba76c
child 24583 d77e4d48e497
ML_Lex.keywords;
tuned comments;
src/Pure/ML/ml_syntax.ML
     1.1 --- a/src/Pure/ML/ml_syntax.ML	Sat Sep 15 19:26:06 2007 +0200
     1.2 +++ b/src/Pure/ML/ml_syntax.ML	Sat Sep 15 19:26:17 2007 +0200
     1.3 @@ -1,4 +1,4 @@
     1.4 -(*  Title:      Pure/General/ml_syntax.ML
     1.5 +(*  Title:      Pure/ML/ml_syntax.ML
     1.6      ID:         $Id$
     1.7      Author:     Makarius
     1.8  
     1.9 @@ -31,14 +31,7 @@
    1.10  
    1.11  (* reserved words *)
    1.12  
    1.13 -val reserved_names =
    1.14 - ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else",
    1.15 -  "end", "exception", "fn", "fun", "handle", "if", "in", "infix",
    1.16 -  "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse",
    1.17 -  "raise", "rec", "then", "type", "val", "with", "withtype", "while",
    1.18 -  "eqtype", "functor", "include", "sharing", "sig", "signature",
    1.19 -  "struct", "structure", "where"];
    1.20 -
    1.21 +val reserved_names = filter Syntax.is_ascii_identifier ML_Lex.keywords;
    1.22  val reserved = Name.make_context reserved_names;
    1.23  val is_reserved = Name.is_declared reserved;
    1.24