added reserved;
authorwenzelm
Sun May 22 16:51:18 2005 +0200 (2005-05-22)
changeset 16030bbfb2f1378b3
parent 16029 070ed43b86f8
child 16031 fbf3471214d6
added reserved;
src/Pure/Isar/outer_parse.ML
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Sun May 22 16:51:17 2005 +0200
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Sun May 22 16:51:18 2005 +0200
     1.3 @@ -31,6 +31,7 @@
     1.4    val sync: token list -> string * token list
     1.5    val eof: token list -> string * token list
     1.6    val $$$ : string -> token list -> string * token list
     1.7 +  val reserved : string -> token list -> string * token list
     1.8    val semicolon: token list -> string * token list
     1.9    val underscore: token list -> string * token list
    1.10    val maybe: (token list -> 'a * token list) -> token list -> 'a option * token list
    1.11 @@ -148,6 +149,10 @@
    1.12    group (T.str_of_kind T.Keyword ^ " " ^ quote x)
    1.13      (Scan.one (T.keyword_with (equal x)) >> T.val_of);
    1.14  
    1.15 +fun reserved x =
    1.16 +  group ("Reserved identifier " ^ quote x)
    1.17 +    (Scan.one (T.ident_with (equal x)) >> T.val_of);
    1.18 +
    1.19  val semicolon = $$$ ";";
    1.20  
    1.21  val minus = sym_ident :-- (fn "-" => Scan.succeed () | _ => Scan.fail) >> #1;