src/Pure/Isar/outer_parse.ML

 
 signature OUTER_PARSE =
 sig
   type token = OuterLex.token
   type 'a parser = token list -> 'a * token list
+  type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list)
   val group: string -> (token list -> 'a) -> token list -> 'a
   val !!! : (token list -> 'a) -> token list -> 'a
   val !!!! : (token list -> 'a) -> token list -> 'a
   val triple1: ('a * 'b) * 'c -> 'a * 'b * 'c
   val triple2: 'a * ('b * 'c) -> 'a * 'b * 'c

   val int: int parser
   val enum: string -> 'a parser -> 'a list parser
   val enum1: string -> 'a parser -> 'a list parser
   val and_list: 'a parser -> 'a list parser
   val and_list1: 'a parser -> 'a list parser
-  val enum': string -> ('a * token list -> 'b * ('a * token list)) ->
-    'a * token list -> 'b list * ('a * token list)
-  val enum1': string -> ('a * token list -> 'b * ('a * token list)) ->
-    'a * token list -> 'b list * ('a * token list)
-  val and_list': ('a * token list -> 'b * ('a * token list)) ->
-    'a * token list -> 'b list * ('a * token list)
-  val and_list1': ('a * token list -> 'b * ('a * token list)) ->
-    'a * token list -> 'b list * ('a * token list)
+  val enum': string -> 'a context_parser -> 'a list context_parser
+  val enum1': string -> 'a context_parser -> 'a list context_parser
+  val and_list': 'a context_parser -> 'a list context_parser
+  val and_list1': 'a context_parser -> 'a list context_parser
   val list: 'a parser -> 'a list parser
   val list1: 'a parser -> 'a list parser
   val name: bstring parser
   val binding: binding parser
   val xname: xstring parser

 
 structure T = OuterLex;
 type token = T.token;
 
 type 'a parser = token list -> 'a * token list;
+type 'a context_parser = Context.generic * token list -> 'a * (Context.generic * token list);
 
 
 (** error handling **)
 
 (* group atomic parsers (no cuts!) *)

 
 val target = ($$$ "(" -- $$$ "in") |-- !!! (xname --| $$$ ")");
 val opt_target = Scan.option target;
 
 end;
+
+type 'a parser = 'a OuterParse.parser;
+type 'a context_parser = 'a OuterParse.context_parser;
+