1.1 --- a/src/Pure/Thy/thy_parse.ML	Thu Oct 23 12:43:07 1997 +0200
     1.2 +++ b/src/Pure/Thy/thy_parse.ML	Thu Oct 23 12:44:46 1997 +0200
     1.3 @@ -14,7 +14,7 @@
     1.4  infix 0 ||;
     1.5  
     1.6  signature THY_PARSE =
     1.7 -  sig
     1.8 +sig
     1.9    type token
    1.10    val !! : ('a -> 'b * 'c) -> 'a -> 'b * 'c
    1.11    val >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
    1.12 @@ -46,6 +46,7 @@
    1.13      -> token list -> 'a list * token list
    1.14    val name: token list -> string * token list
    1.15    val sort: token list -> string * token list
    1.16 +  val typ: token list -> string * token list
    1.17    val opt_infix: token list -> string * token list
    1.18    val opt_mixfix: token list -> string * token list
    1.19    val opt_witness: token list -> string * token list
    1.20 @@ -70,7 +71,7 @@
    1.21    val mk_pair: string * string -> string
    1.22    val mk_triple: string * string * string -> string
    1.23    val strip_quotes: string -> string
    1.24 -  end;
    1.25 +end;
    1.26  
    1.27  
    1.28  structure ThyParse : THY_PARSE=
    1.29 @@ -153,8 +154,9 @@
    1.30  fun enum1 sep parse = parse -- repeat (sep $$-- parse) >> op ::;
    1.31  fun enum sep parse = enum1 sep parse || empty;
    1.32  
    1.33 -fun list  parse = enum  "," parse;
    1.34  fun list1 parse = enum1 "," parse;
    1.35 +fun list parse = enum "," parse;
    1.36 +
    1.37  
    1.38  
    1.39  (** theory parsers **)
    1.40 @@ -235,6 +237,8 @@
    1.41  
    1.42  (* types *)
    1.43  
    1.44 +(* FIXME clean!! *)
    1.45 +
    1.46  (*Parse an identifier, but only if it is not followed by "::", "=" or ",";
    1.47    the exclusion of a postfix comma can be controlled to allow expressions
    1.48    like "(id, id)" but disallow ones like "'a => id id,id :: ..."*)
    1.49 @@ -250,15 +254,14 @@
    1.50  
    1.51  (*type used in types, consts and syntax sections*)
    1.52  fun const_type allow_comma toks =
    1.53 -  let val simple_type =
    1.54 -        (ident ||
    1.55 -         kind TypeVar -- optional ("::" $$-- ident >> cat "::") "" >>
    1.56 -           (fn (tv, cl) => cat tv cl)) --
    1.57 -           repeat (ident_no_colon allow_comma) >>
    1.58 -           (fn (args, ts) => cat args (space_implode " " ts)) ||
    1.59 -         ("(" $$-- (list1 (const_type true)) --$$ ")" >> (parens o commas)) --
    1.60 -           repeat1 (ident_no_colon allow_comma) >>
    1.61 -           (fn (args, ts) => cat args (space_implode " " ts));
    1.62 +  let
    1.63 +    val simple_type =
    1.64 +      (ident || kind TypeVar ^^ optional ($$ "::" ^^ ident) "") --
    1.65 +          repeat (ident_no_colon allow_comma)
    1.66 +          >> (fn (args, ts) => cat args (space_implode " " ts)) ||
    1.67 +        ("(" $$-- (list1 (const_type true)) --$$ ")" >> (parens o commas)) --
    1.68 +          repeat1 (ident_no_colon allow_comma)
    1.69 +          >> (fn (args, ts) => cat args (space_implode " " ts));
    1.70  
    1.71        val appl_param =
    1.72          simple_type || "(" $$-- const_type true --$$ ")" >> parens || 
    1.73 @@ -274,6 +277,9 @@
    1.74        "(" $$-- const_type true --$$ ")" >> parens) toks
    1.75    end;
    1.76  
    1.77 +val typ = string || (const_type false >> quote);
    1.78 +
    1.79 +
    1.80  fun mk_old_type_decl ((ts, n), syn) =
    1.81    map (fn t => (mk_triple (t, n, syn), false)) ts;
    1.82  
    1.83 @@ -295,8 +301,7 @@
    1.84    empty >> K [];
    1.85  
    1.86  val type_decl = type_args -- name --
    1.87 -  optional ("=" $$-- (string || (const_type false >> quote)) >> Some) None
    1.88 -  -- opt_infix >> mk_type_decl;
    1.89 +  optional ("=" $$-- typ >> Some) None -- opt_infix >> mk_type_decl;
    1.90  
    1.91  val type_decls =
    1.92    repeat1 (old_type_decl || type_decl) >> (mk_type_decls o flat);
    1.93 @@ -305,8 +310,7 @@
    1.94  (* consts *)
    1.95  
    1.96  val const_decls =
    1.97 -  repeat1
    1.98 -    (names1 --$$ "::" -- !! ((string || const_type false >> quote) -- opt_mixfix))
    1.99 +  repeat1 (names1 --$$ "::" -- !! (typ -- opt_mixfix))
   1.100    >> (mk_big_list o map mk_triple2 o split_decls);
   1.101  
   1.102  val opt_mode =
   1.103 @@ -375,9 +379,8 @@
   1.104    end;
   1.105  
   1.106  val constaxiom_decls =
   1.107 -  repeat1 (ident --$$ "::" -- !!
   1.108 -           ((string || const_type false >> quote) -- opt_mixfix) -- !!
   1.109 -           string) >> mk_constaxiom_decls;
   1.110 +  repeat1 (ident --$$ "::" -- !! (typ -- opt_mixfix) -- !! string)
   1.111 +  >> mk_constaxiom_decls;
   1.112  
   1.113  
   1.114  (* axclass *)