provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
authorwenzelm
Wed Oct 28 22:00:35 2009 +0100 (2009-10-28)
changeset 332870f99569d23e1
parent 33286 1807921b6268
child 33288 bd3f30da7bc1
provide SpecParse.constdecl/constdef, e.g. for quotient_definition;
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/spec_parse.ML
     1.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Oct 28 20:49:09 2009 +0100
     1.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Oct 28 22:00:35 2009 +0100
     1.3 @@ -222,22 +222,13 @@
     1.4  
     1.5  (* constant definitions and abbreviations *)
     1.6  
     1.7 -val constdecl =
     1.8 -  P.binding --
     1.9 -    (P.where_ >> K (NONE, NoSyn) ||
    1.10 -      P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
    1.11 -      Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
    1.12 -  >> P.triple2;
    1.13 -
    1.14 -val constdef = Scan.option constdecl -- (SpecParse.opt_thm_name ":" -- P.prop);
    1.15 -
    1.16  val _ =
    1.17    OuterSyntax.local_theory "definition" "constant definition" K.thy_decl
    1.18 -    (constdef >> (fn args => #2 o Specification.definition_cmd args));
    1.19 +    (SpecParse.constdef >> (fn args => #2 o Specification.definition_cmd args));
    1.20  
    1.21  val _ =
    1.22    OuterSyntax.local_theory "abbreviation" "constant abbreviation" K.thy_decl
    1.23 -    (opt_mode -- (Scan.option constdecl -- P.prop)
    1.24 +    (opt_mode -- (Scan.option SpecParse.constdecl -- P.prop)
    1.25      >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
    1.26  
    1.27  val _ =
     2.1 --- a/src/Pure/Isar/spec_parse.ML	Wed Oct 28 20:49:09 2009 +0100
     2.2 +++ b/src/Pure/Isar/spec_parse.ML	Wed Oct 28 22:00:35 2009 +0100
     2.3 @@ -18,6 +18,8 @@
     2.4    val xthm: (Facts.ref * Attrib.src list) parser
     2.5    val xthms1: (Facts.ref * Attrib.src list) list parser
     2.6    val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
     2.7 +  val constdecl: (binding * string option * mixfix) parser
     2.8 +  val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
     2.9    val locale_mixfix: mixfix parser
    2.10    val locale_fixes: (binding * string option * mixfix) list parser
    2.11    val locale_insts: (string option list * (Attrib.binding * string) list) parser
    2.12 @@ -66,6 +68,18 @@
    2.13  val name_facts = P.and_list1 (opt_thm_name "=" -- xthms1);
    2.14  
    2.15  
    2.16 +(* basic constant specifications *)
    2.17 +
    2.18 +val constdecl =
    2.19 +  P.binding --
    2.20 +    (P.where_ >> K (NONE, NoSyn) ||
    2.21 +      P.$$$ "::" |-- P.!!! ((P.typ >> SOME) -- P.opt_mixfix' --| P.where_) ||
    2.22 +      Scan.ahead (P.$$$ "(") |-- P.!!! (P.mixfix' --| P.where_ >> pair NONE))
    2.23 +  >> P.triple2;
    2.24 +
    2.25 +val constdef = Scan.option constdecl -- (opt_thm_name ":" -- P.prop);
    2.26 +
    2.27 +
    2.28  (* locale and context elements *)
    2.29  
    2.30  val locale_mixfix = P.$$$ "(" -- P.$$$ "structure" -- P.!!! (P.$$$ ")") >> K Structure || P.mixfix;