# HG changeset patch
# User clasohm
# Date 815745440 -3600
# Node ID 9a6e7bd2bfaf37446eae985ee7c9622d9c62a201
# Parent  b94ef890dbf2a4a14b0e184eb16ff1f5d1d0cba5
types in consts section of .thy files can now be specified without quotes

diff -r b94ef890dbf2 -r 9a6e7bd2bfaf src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Fri Nov 03 12:00:46 1995 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Tue Nov 07 12:57:20 1995 +0100
@@ -68,7 +68,7 @@
   val strip_quotes: string -> string
 end;
 
-functor ThyParseFun(structure Symtab: SYMTAB and ThyScan: THY_SCAN): THY_PARSE =
+functor ThyParseFun(structure Symtab: SYMTAB and ThyScan: THY_SCAN): THY_PARSE=
 struct
 
 open ThyScan;
@@ -253,13 +253,58 @@
 val type_decl = type_args -- name -- optional ("=" $$-- !! string >> Some) None
   -- opt_infix >> mk_type_decl;
 
-val type_decls = repeat1 (old_type_decl || type_decl) >> (mk_type_decls o flat);
+val type_decls = repeat1 (old_type_decl || type_decl) >>
+                 (mk_type_decls o flat);
 
 
 (* consts *)
 
-val const_decls = repeat1 (names1 --$$ "::" -- !! (string -- opt_mixfix))
-  >> (mk_big_list o map mk_triple2 o split_decls);
+val simple_type = ident || kind TypeVar;
+
+(*Types with type arguments, like e.g. "'a list list"*)
+fun complex_type toks =
+  let val typ = simple_type || "(" $$-- complex_type --$$ ")" >> parens;
+      val typ2 = complex_type || "(" $$-- complex_type --$$ ")" >> parens;
+  in
+   (typ -- repeat ident >> (fn (t, ts) => space_implode " " (t::ts)) ||
+    "(" $$-- !! (list1 typ2) --$$ ")" -- !! (repeat1 ident) >>
+      (fn (tas, ts) => space_implode " " (parens (commas tas) :: ts))) toks
+  end;
+
+(*Const type which is limited at the end by "=>", ")", "]" or ","*)
+fun param_type toks =
+  ((complex_type || "(" $$-- param_type --$$ ")" >> parens ||
+    "[" $$-- !! (list1 param_type) --$$ "]" >> mk_list) --
+     repeat ("=>" $$-- param_type >> cat " =>") >>
+     (fn (t, ts) => t ^ implode ts)) toks;
+
+(*Parse an identifier, but only if it is not followed by colons or a comma*)
+fun ident_no_colon [] = eof_err()
+  | ident_no_colon ((Ident, s, n) :: (rest as (Keyword, s2, n2) :: toks)) =
+      if s2 = "::" orelse s2 = "," then
+        syn_err (name_of_kind Ident) (quote s2) n2
+      else (s, rest)
+  | ident_no_colon ((Ident, s, n) :: toks) = (s, toks)
+  | ident_no_colon ((k, s, n) :: _) =
+      syn_err (name_of_kind Ident) (quote s) n;
+
+(*Type after last "=>"*)
+val appl_last =
+  (simple_type || "(" $$-- param_type --$$ ")" >> parens) --
+  repeat ident_no_colon >> (fn (t, ts) => space_implode " " (t::ts));
+
+(*Type specified before "=>"*)
+val appl_param =
+  (complex_type || "(" $$-- param_type --$$ ")" >> parens ||
+   "[" $$-- !! (list1 param_type) --$$ "]" >> (brackets o commas)) --$$ "=>";
+
+(*Top level const type*)
+val const_type = repeat appl_param -- appl_last >>
+  (fn (ts, t) => space_implode " => " (ts@[t]));
+
+val const_decls = repeat1 (names1 --$$ "::" -- !!
+                    ((string || const_type>>quote) -- opt_mixfix)) >>
+                  (mk_big_list o map mk_triple2 o split_decls);
 
 
 (* translations *)