added begin parser;
authorwenzelm
Wed Oct 11 22:55:20 2006 +0200 (2006-10-11)
changeset 20983d4500b9b220e
parent 20982 fade54fde622
child 20984 d09f388fa9db
added begin parser;
src/Pure/Isar/outer_parse.ML
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Wed Oct 11 22:55:19 2006 +0200
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Wed Oct 11 22:55:20 2006 +0200
     1.3 @@ -39,6 +39,7 @@
     1.4    val tags: token list -> string list * token list
     1.5    val opt_unit: token list -> unit * token list
     1.6    val opt_keyword: string -> token list -> bool * token list
     1.7 +  val begin: token list -> string * token list
     1.8    val opt_begin: token list -> bool * token list
     1.9    val nat: token list -> int * token list
    1.10    val enum: string -> (token list -> 'a * token list) -> token list -> 'a list * token list
    1.11 @@ -191,7 +192,8 @@
    1.12  val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
    1.13  fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
    1.14  
    1.15 -val opt_begin = Scan.optional ($$$ "begin" >> K true) false;
    1.16 +val begin = $$$ "begin";
    1.17 +val opt_begin = Scan.optional (begin >> K true) false;
    1.18  
    1.19  
    1.20  (* enumerations *)