# HG changeset patch
# User wenzelm
# Date 877603486 -7200
# Node ID 9b3cbfd6a93637b13fe4d14621150280e74e9c92
# Parent  1030dd79720bf8c33a704b15ee0b1a0481c994b5
improved typ parser, exported;

diff -r 1030dd79720b -r 9b3cbfd6a936 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Thu Oct 23 12:43:07 1997 +0200
+++ b/src/Pure/Thy/thy_parse.ML	Thu Oct 23 12:44:46 1997 +0200
@@ -14,7 +14,7 @@
 infix 0 ||;
 
 signature THY_PARSE =
-  sig
+sig
   type token
   val !! : ('a -> 'b * 'c) -> 'a -> 'b * 'c
   val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
@@ -46,6 +46,7 @@
     -> token list -> 'a list * token list
   val name: token list -> string * token list
   val sort: token list -> string * token list
+  val typ: token list -> string * token list
   val opt_infix: token list -> string * token list
   val opt_mixfix: token list -> string * token list
   val opt_witness: token list -> string * token list
@@ -70,7 +71,7 @@
   val mk_pair: string * string -> string
   val mk_triple: string * string * string -> string
   val strip_quotes: string -> string
-  end;
+end;
 
 
 structure ThyParse : THY_PARSE=
@@ -153,8 +154,9 @@
 fun enum1 sep parse = parse -- repeat (sep $$-- parse) >> op ::;
 fun enum sep parse = enum1 sep parse || empty;
 
-fun list  parse = enum  "," parse;
 fun list1 parse = enum1 "," parse;
+fun list parse = enum "," parse;
+
 
 
 (** theory parsers **)
@@ -235,6 +237,8 @@
 
 (* types *)
 
+(* FIXME clean!! *)
+
 (*Parse an identifier, but only if it is not followed by "::", "=" or ",";
   the exclusion of a postfix comma can be controlled to allow expressions
   like "(id, id)" but disallow ones like "'a => id id,id :: ..."*)
@@ -250,15 +254,14 @@
 
 (*type used in types, consts and syntax sections*)
 fun const_type allow_comma toks =
-  let val simple_type =
-        (ident ||
-         kind TypeVar -- optional ("::" $$-- ident >> cat "::") "" >>
-           (fn (tv, cl) => cat tv cl)) --
-           repeat (ident_no_colon allow_comma) >>
-           (fn (args, ts) => cat args (space_implode " " ts)) ||
-         ("(" $$-- (list1 (const_type true)) --$$ ")" >> (parens o commas)) --
-           repeat1 (ident_no_colon allow_comma) >>
-           (fn (args, ts) => cat args (space_implode " " ts));
+  let
+    val simple_type =
+      (ident || kind TypeVar ^^ optional ($$ "::" ^^ ident) "") --
+          repeat (ident_no_colon allow_comma)
+          >> (fn (args, ts) => cat args (space_implode " " ts)) ||
+        ("(" $$-- (list1 (const_type true)) --$$ ")" >> (parens o commas)) --
+          repeat1 (ident_no_colon allow_comma)
+          >> (fn (args, ts) => cat args (space_implode " " ts));
 
       val appl_param =
         simple_type || "(" $$-- const_type true --$$ ")" >> parens || 
@@ -274,6 +277,9 @@
       "(" $$-- const_type true --$$ ")" >> parens) toks
   end;
 
+val typ = string || (const_type false >> quote);
+
+
 fun mk_old_type_decl ((ts, n), syn) =
   map (fn t => (mk_triple (t, n, syn), false)) ts;
 
@@ -295,8 +301,7 @@
   empty >> K [];
 
 val type_decl = type_args -- name --
-  optional ("=" $$-- (string || (const_type false >> quote)) >> Some) None
-  -- opt_infix >> mk_type_decl;
+  optional ("=" $$-- typ >> Some) None -- opt_infix >> mk_type_decl;
 
 val type_decls =
   repeat1 (old_type_decl || type_decl) >> (mk_type_decls o flat);
@@ -305,8 +310,7 @@
 (* consts *)
 
 val const_decls =
-  repeat1
-    (names1 --$$ "::" -- !! ((string || const_type false >> quote) -- opt_mixfix))
+  repeat1 (names1 --$$ "::" -- !! (typ -- opt_mixfix))
   >> (mk_big_list o map mk_triple2 o split_decls);
 
 val opt_mode =
@@ -375,9 +379,8 @@
   end;
 
 val constaxiom_decls =
-  repeat1 (ident --$$ "::" -- !!
-           ((string || const_type false >> quote) -- opt_mixfix) -- !!
-           string) >> mk_constaxiom_decls;
+  repeat1 (ident --$$ "::" -- !! (typ -- opt_mixfix) -- !! string)
+  >> mk_constaxiom_decls;
 
 
 (* axclass *)