src/Pure/Isar/spec_parse.ML
changeset 33287 0f99569d23e1
parent 30726 67388cc4ccb4
child 36950 75b8f26f2f07
     1.1 --- a/src/Pure/Isar/spec_parse.ML	Wed Oct 28 20:49:09 2009 +0100
     1.2 +++ b/src/Pure/Isar/spec_parse.ML	Wed Oct 28 22:00:35 2009 +0100
     1.3 @@ -18,6 +18,8 @@
     1.4    val xthm: (Facts.ref * Attrib.src list) parser
     1.5    val xthms1: (Facts.ref * Attrib.src list) list parser
     1.6    val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
     1.7 +  val constdecl: (binding * string option * mixfix) parser
     1.8 +  val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
     1.9    val locale_mixfix: mixfix parser
    1.10    val locale_fixes: (binding * string option * mixfix) list parser
    1.11    val locale_insts: (string option list * (Attrib.binding * string) list) parser
    1.12 @@ -66,6 +68,18 @@
    1.13  val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1);
    1.14  
    1.15  
    1.16 +(* basic constant specifications *)
    1.17 +
    1.18 +val constdecl =
    1.19 +  P.binding --
    1.20 +    (P.where_ >> K (NONE, NoSyn) ||
    1.21 +      P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
    1.22 +      Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
    1.23 +  >> P.triple2;
    1.24 +
    1.25 +val constdef = Scan.option constdecl -- (opt_thm_name ":" -- P.prop);
    1.26 +
    1.27 +
    1.28  (* locale and context elements *)
    1.29  
    1.30  val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix;