# HG changeset patch
# User wenzelm
# Date 1236975765 -3600
# Node ID 5c628a39b7cb845ae70e50f05535a698294bd3f2
# Parent  4120fc59dd8591021cc7794619b694d69f44a19b
pervasive types 'a parser and 'a context_parser;

diff -r 4120fc59dd85 -r 5c628a39b7cb src/Pure/Isar/outer_parse.ML
--- a/src/Pure/Isar/outer_parse.ML	Fri Mar 13 19:58:26 2009 +0100
+++ b/src/Pure/Isar/outer_parse.ML	Fri Mar 13 21:22:45 2009 +0100
@@ -8,6 +8,7 @@
 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
@@ -50,14 +51,10 @@
   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
@@ -106,6 +103,7 @@
 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 **)
@@ -339,3 +337,7 @@
 val opt_target = Scan.option target;
 
 end;
+
+type 'a parser = 'a OuterParse.parser;
+type 'a context_parser = 'a OuterParse.context_parser;
+