# HG changeset patch # User wenzelm # Date 1003185202 -7200 # Node ID 311eee3d63b64891a69f9815a394b707f5ac7c4d # Parent 2c201f3b018efb0bdd7f26aff3d9956653a0570b parser for underscore (actually a symbolic identifier!); diff -r 2c201f3b018e -r 311eee3d63b6 src/Pure/Isar/outer_parse.ML --- a/src/Pure/Isar/outer_parse.ML Tue Oct 16 00:32:34 2001 +0200 +++ b/src/Pure/Isar/outer_parse.ML Tue Oct 16 00:33:22 2001 +0200 @@ -14,6 +14,7 @@ val !!!! : (token list -> 'a) -> token list -> 'a val $$$ : string -> token list -> string * token list val semicolon: token list -> string * token list + val underscore: token list -> string * token list val position: (token list -> 'a * 'b) -> token list -> ('a * Position.T) * 'b val command: token list -> string * token list val keyword: token list -> string * token list @@ -143,6 +144,8 @@ val semicolon = $$$ ";"; +val underscore = sym_ident :-- (fn "_" => Scan.succeed () | _ => Scan.fail) >> #1; + val nat = number >> (fst o Term.read_int o Symbol.explode); val not_eof = Scan.one T.not_eof;