# HG changeset patch
# User clasohm
# Date 817816927 -3600
# Node ID f800f533aa83b8c2e66070473b7699fe34729b37
# Parent  92f83b9d17e1a8b90b32557ba7144208da0ae1e0
simplified parser for constType

diff -r 92f83b9d17e1 -r f800f533aa83 src/Pure/Thy/thy_parse.ML
--- a/src/Pure/Thy/thy_parse.ML	Fri Dec 01 12:03:13 1995 +0100
+++ b/src/Pure/Thy/thy_parse.ML	Fri Dec 01 12:22:07 1995 +0100
@@ -259,53 +259,46 @@
 
 (* consts *)
 
-val simple_type = ident ||
-  (kind TypeVar -- optional ("::" $$-- ident >> cat "::") "" >>
-   (fn (tv, cl) => tv ^ cl));
+(*Parse an identifier, but only if it is not followed by colons or a comma;
+  the exclusion of a postfix comma can be controlled to allow expressions
+  like "(id, id)" but disallow ones like "'a => id id,id :: ..."*)
+fun ident_no_colon _ [] = eof_err()
+  | ident_no_colon allow_comma ((Ident, s, n) :: (rest as (Keyword, s2, n2) ::
+                                toks)) =
+      if s2 = "::" orelse (not allow_comma andalso 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;
 
-(*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
+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));
+
+      val appl_param =
+        simple_type || "(" $$-- const_type true --$$ ")" >> parens || 
+        "[" $$-- (list1 (const_type true)) --$$ "]" --$$ "=>" --
+          const_type allow_comma >>
+          (fn (src, dest) => mk_list src ^ " => " ^ dest);
+  in ("[" $$-- (list1 (const_type true)) --$$ "]" --$$ "=>" --
+        const_type allow_comma >>
+        (fn (src, dest) => mk_list src ^ " => " ^ dest) ||
+      repeat1 (appl_param --$$ "=>") -- const_type allow_comma >>
+        (fn (src, dest) => space_implode " => " (src@[dest])) ||
+      simple_type ||
+      "(" $$-- const_type true --$$ ")" >> parens) 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)) >>
+                    ((string || const_type false >> quote) -- opt_mixfix)) >>
                   (mk_big_list o map mk_triple2 o split_decls);