--- a/src/Pure/Isar/outer_parse.ML Thu Apr 22 10:57:12 2004 +0200
+++ b/src/Pure/Isar/outer_parse.ML Thu Apr 22 10:58:54 2004 +0200
@@ -34,6 +34,7 @@
val eof: token list -> string * token list
val not_eof: token list -> token * token list
val opt_unit: token list -> unit * token list
+ val opt_keyword: string -> token list -> bool * token list
val nat: token list -> int * token list
val enum: string -> (token list -> 'a * token list) -> token list -> 'a list * token list
val enum1: string -> (token list -> 'a * token list) -> token list -> 'a list * token list
@@ -53,6 +54,7 @@
val opt_mixfix: token list -> Syntax.mixfix * token list
val opt_infix': token list -> Syntax.mixfix * token list
val opt_mixfix': token list -> Syntax.mixfix * token list
+ val mixfix': token list -> Syntax.mixfix * token list
val const: token list -> (bstring * string * Syntax.mixfix) * token list
val term: token list -> string * token list
val prop: token list -> string * token list
@@ -153,6 +155,8 @@
val opt_unit = Scan.optional ($$$ "(" -- $$$ ")" >> (K ())) ();
+fun opt_keyword s = Scan.optional ($$$ "(" |-- !!! (($$$ s >> K true) --| $$$ ")")) false;
+
(* enumerations *)
@@ -173,8 +177,7 @@
val text = group "text" (short_ident || long_ident || sym_ident || string || number || verbatim);
val uname = underscore >> K None || name >> Some;
- (* CB: underscore yields None, any other name Some with that string.
- Used, for example, in the renaming of locale parameters. *)
+
(* sorts and arities *)
@@ -215,14 +218,14 @@
(string -- !!! (opt_pris -- Scan.optional nat Syntax.max_pri))
>> (Syntax.Mixfix o triple2);
-fun opt_fix guard fix =
- Scan.optional ($$$ "(" |-- guard (fix --| $$$ ")")) Syntax.NoSyn;
+fun fix_decl guard fix = $$$ "(" |-- guard (fix --| $$$ ")");
+fun opt_fix guard fix = Scan.optional (fix_decl guard fix) Syntax.NoSyn;
val opt_infix = opt_fix !!! (infxl || infxr || infx);
val opt_mixfix = opt_fix !!! (mixfix || binder || infxl || infxr || infx);
-
val opt_infix' = opt_fix I (infxl || infxr || infx);
val opt_mixfix' = opt_fix I (mixfix || binder || infxl || infxr || infx);
+val mixfix' = fix_decl !!! (mixfix || binder || infxl || infxr || infx);
(* consts *)