src/Pure/Isar/outer_parse.ML
changeset 14646 f5f2340398f9
parent 14605 9de4d64eee3b
child 14835 695ee8ad0bb6
     1.1 --- a/src/Pure/Isar/outer_parse.ML	Thu Apr 22 10:57:12 2004 +0200
     1.2 +++ b/src/Pure/Isar/outer_parse.ML	Thu Apr 22 10:58:54 2004 +0200
     1.3 @@ -34,6 +34,7 @@
     1.4    val eof: token list -> string * token list
     1.5    val not_eof: token list -> token * token list
     1.6    val opt_unit: token list -> unit * token list
     1.7 +  val opt_keyword: string -> token list -> bool * token list
     1.8    val nat: token list -> int * token list
     1.9    val enum: string -> (token list -> 'a * token list) -> token list -> 'a list * token list
    1.10    val enum1: string -> (token list -> 'a * token list) -> token list -> 'a list * token list
    1.11 @@ -53,6 +54,7 @@
    1.12    val opt_mixfix: token list -> Syntax.mixfix * token list
    1.13    val opt_infix': token list -> Syntax.mixfix * token list
    1.14    val opt_mixfix': token list -> Syntax.mixfix * token list
    1.15 +  val mixfix': token list -> Syntax.mixfix * token list
    1.16    val const: token list -> (bstring * string * Syntax.mixfix) * token list
    1.17    val term: token list -> string * token list
    1.18    val prop: token list -> string * token list
    1.19 @@ -153,6 +155,8 @@
    1.20  
    1.21  val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
    1.22  
    1.23 +fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
    1.24 +
    1.25  
    1.26  (* enumerations *)
    1.27  
    1.28 @@ -173,8 +177,7 @@
    1.29  val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
    1.30  
    1.31  val uname = underscore >> K None || name >> Some;
    1.32 -  (* CB: underscore yields None, any other name Some with that string.
    1.33 -     Used, for example, in the renaming of locale parameters.  *)
    1.34 +
    1.35  
    1.36  (* sorts and arities *)
    1.37  
    1.38 @@ -215,14 +218,14 @@
    1.39    (string -- !!! (opt_pris -- Scan.optional nat Syntax.max_pri))
    1.40    >> (Syntax.Mixfix o triple2);
    1.41  
    1.42 -fun opt_fix guard fix =
    1.43 -  Scan.optional ($$$ "(" |-- guard (fix --| $$$ ")")) Syntax.NoSyn;
    1.44 +fun fix_decl guard fix = $$$ "(" |-- guard (fix --| $$$ ")");
    1.45 +fun opt_fix guard fix = Scan.optional (fix_decl guard fix) Syntax.NoSyn;
    1.46  
    1.47  val opt_infix = opt_fix !!! (infxl || infxr || infx);
    1.48  val opt_mixfix = opt_fix !!! (mixfix || binder || infxl || infxr || infx);
    1.49 -
    1.50  val opt_infix' = opt_fix I (infxl || infxr || infx);
    1.51  val opt_mixfix' = opt_fix I (mixfix || binder || infxl || infxr || infx);
    1.52 +val mixfix' = fix_decl !!! (mixfix || binder || infxl || infxr || infx);
    1.53  
    1.54  
    1.55  (* consts *)