# HG changeset patch # User wenzelm # Date 1165683942 -3600 # Node ID 88661e47147d4e80dcc5919d7d21f44e084021e9 # Parent 25239591e732212093e9f6e1705f6261eb8ab519 renamed reserved to reserved_names; added reserved: Name.context; diff -r 25239591e732 -r 88661e47147d src/Pure/General/ml_syntax.ML --- a/src/Pure/General/ml_syntax.ML Sat Dec 09 18:05:41 2006 +0100 +++ b/src/Pure/General/ml_syntax.ML Sat Dec 09 18:05:42 2006 +0100 @@ -7,7 +7,8 @@ signature ML_SYNTAX = sig - val reserved: string list + val reserved_names: string list + val reserved: Name.context val is_reserved: string -> bool val is_identifier: string -> bool val str_of_pair: ('a -> string) -> ('b -> string) -> 'a * 'b -> string @@ -21,7 +22,7 @@ (* reserved words *) -val reserved = +val reserved_names = ["abstype", "and", "andalso", "as", "case", "do", "datatype", "else", "end", "exception", "fn", "fun", "handle", "if", "in", "infix", "infixr", "let", "local", "nonfix", "of", "op", "open", "orelse", @@ -29,7 +30,8 @@ "eqtype", "functor", "include", "sharing", "sig", "signature", "struct", "structure", "where"]; -val is_reserved = member (op =) reserved; +val reserved = Name.make_context reserved_names; +val is_reserved = Name.is_declared reserved; (* identifiers *)