1.1 --- a/NEWS	Sat May 15 23:23:45 2010 +0200
     1.2 +++ b/NEWS	Sat May 15 23:32:15 2010 +0200
     1.3 @@ -507,6 +507,7 @@
     1.4  
     1.5    OuterKeyword  ~>  Keyword
     1.6    OuterParse    ~>  Parse
     1.7 +  SpecParse     ~>  Parse_Spec
     1.8  
     1.9  
    1.10  *** System ***

     2.1 --- a/src/Pure/IsaMakefile	Sat May 15 23:23:45 2010 +0200
     2.2 +++ b/src/Pure/IsaMakefile	Sat May 15 23:32:15 2010 +0200
     2.3 @@ -69,10 +69,10 @@
     2.4    Isar/local_syntax.ML Isar/local_theory.ML Isar/locale.ML		\
     2.5    Isar/method.ML Isar/object_logic.ML Isar/obtain.ML Isar/outer_lex.ML	\
     2.6    Isar/outer_syntax.ML Isar/overloading.ML Isar/parse.ML		\
     2.7 -  Isar/parse_value.ML Isar/proof.ML Isar/proof_context.ML		\
     2.8 -  Isar/proof_display.ML Isar/proof_node.ML Isar/rule_cases.ML		\
     2.9 -  Isar/rule_insts.ML Isar/runtime.ML Isar/skip_proof.ML			\
    2.10 -  Isar/spec_parse.ML Isar/spec_rules.ML Isar/specification.ML		\
    2.11 +  Isar/parse_spec.ML Isar/parse_value.ML Isar/proof.ML			\
    2.12 +  Isar/proof_context.ML Isar/proof_display.ML Isar/proof_node.ML	\
    2.13 +  Isar/rule_cases.ML Isar/rule_insts.ML Isar/runtime.ML			\
    2.14 +  Isar/skip_proof.ML Isar/spec_rules.ML Isar/specification.ML		\
    2.15    Isar/theory_target.ML Isar/toplevel.ML Isar/typedecl.ML		\
    2.16    ML/ml_antiquote.ML ML/ml_compiler.ML ML/ml_compiler_polyml-5.3.ML	\
    2.17    ML/ml_context.ML ML/ml_env.ML ML/ml_lex.ML ML/ml_parse.ML		\

     3.1 --- a/src/Pure/Isar/isar_syn.ML	Sat May 15 23:23:45 2010 +0200
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Sat May 15 23:32:15 2010 +0200
     3.3 @@ -183,7 +183,7 @@
     3.4  
     3.5  val _ =
     3.6    OuterSyntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl
     3.7 -    (Scan.repeat1 SpecParse.spec >>
     3.8 +    (Scan.repeat1 Parse_Spec.spec >>
     3.9        (Toplevel.theory o
    3.10          (IsarCmd.add_axioms o
    3.11            tap (fn _ => legacy_feature "Old 'axioms' command -- use 'axiomatization' instead"))));
    3.12 @@ -196,7 +196,7 @@
    3.13  val _ =
    3.14    OuterSyntax.command "defs" "define constants" Keyword.thy_decl
    3.15      (opt_unchecked_overloaded --
    3.16 -      Scan.repeat1 (SpecParse.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
    3.17 +      Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
    3.18        >> (Toplevel.theory o IsarCmd.add_defs));
    3.19  
    3.20  
    3.21 @@ -208,7 +208,7 @@
    3.22      --| Scan.option Parse.where_ >> Parse.triple1 ||
    3.23    Parse.binding -- (Parse.mixfix >> pair NONE) --| Scan.option Parse.where_ >> Parse.triple2;
    3.24  
    3.25 -val old_constdef = Scan.option old_constdecl -- (SpecParse.opt_thm_name ":" -- Parse.prop);
    3.26 +val old_constdef = Scan.option old_constdecl -- (Parse_Spec.opt_thm_name ":" -- Parse.prop);
    3.27  
    3.28  val structs =
    3.29    Scan.optional ((Parse.$$$ "(" -- Parse.$$$ "structure")
    3.30 @@ -223,11 +223,11 @@
    3.31  
    3.32  val _ =
    3.33    OuterSyntax.local_theory "definition" "constant definition" Keyword.thy_decl
    3.34 -    (SpecParse.constdef >> (fn args => #2 o Specification.definition_cmd args));
    3.35 +    (Parse_Spec.constdef >> (fn args => #2 o Specification.definition_cmd args));
    3.36  
    3.37  val _ =
    3.38    OuterSyntax.local_theory "abbreviation" "constant abbreviation" Keyword.thy_decl
    3.39 -    (opt_mode -- (Scan.option SpecParse.constdecl -- Parse.prop)
    3.40 +    (opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
    3.41        >> (fn (mode, args) => Specification.abbreviation_cmd mode args));
    3.42  
    3.43  val _ =
    3.44 @@ -245,13 +245,13 @@
    3.45  val _ =
    3.46    OuterSyntax.local_theory "notation" "add concrete syntax for constants / fixed variables"
    3.47      Keyword.thy_decl
    3.48 -    (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix)
    3.49 +    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
    3.50        >> (fn (mode, args) => Specification.notation_cmd true mode args));
    3.51  
    3.52  val _ =
    3.53    OuterSyntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables"
    3.54      Keyword.thy_decl
    3.55 -    (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix)
    3.56 +    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
    3.57        >> (fn (mode, args) => Specification.notation_cmd false mode args));
    3.58  
    3.59  
    3.60 @@ -260,14 +260,14 @@
    3.61  val _ =
    3.62    OuterSyntax.command "axiomatization" "axiomatic constant specification" Keyword.thy_decl
    3.63      (Scan.optional Parse.fixes [] --
    3.64 -      Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 SpecParse.specs)) []
    3.65 +      Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
    3.66        >> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
    3.67  
    3.68  
    3.69  (* theorems *)
    3.70  
    3.71  fun theorems kind =
    3.72 -  SpecParse.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args);
    3.73 +  Parse_Spec.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args);
    3.74  
    3.75  val _ =
    3.76    OuterSyntax.local_theory "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK);
    3.77 @@ -277,7 +277,7 @@
    3.78  
    3.79  val _ =
    3.80    OuterSyntax.local_theory "declare" "declare theorems" Keyword.thy_decl
    3.81 -    (Parse.and_list1 SpecParse.xthms1
    3.82 +    (Parse.and_list1 Parse_Spec.xthms1
    3.83        >> (fn args => #2 o Specification.theorems_cmd "" [(Attrib.empty_binding, flat args)]));
    3.84  
    3.85  
    3.86 @@ -416,9 +416,9 @@
    3.87  (* locales *)
    3.88  
    3.89  val locale_val =
    3.90 -  SpecParse.locale_expression false --
    3.91 -    Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
    3.92 -  Scan.repeat1 SpecParse.context_element >> pair ([], []);
    3.93 +  Parse_Spec.locale_expression false --
    3.94 +    Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
    3.95 +  Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
    3.96  
    3.97  val _ =
    3.98    OuterSyntax.command "locale" "define named proof context" Keyword.thy_decl
    3.99 @@ -432,15 +432,15 @@
   3.100    OuterSyntax.command "sublocale"
   3.101      "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal
   3.102      (Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
   3.103 -      Parse.!!! (SpecParse.locale_expression false)
   3.104 +      Parse.!!! (Parse_Spec.locale_expression false)
   3.105        >> (fn (loc, expr) =>
   3.106            Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd loc expr)));
   3.107  
   3.108  val _ =
   3.109    OuterSyntax.command "interpretation"
   3.110      "prove interpretation of locale expression in theory" Keyword.thy_goal
   3.111 -    (Parse.!!! (SpecParse.locale_expression true) --
   3.112 -      Scan.optional (Parse.where_ |-- Parse.and_list1 (SpecParse.opt_thm_name ":" -- Parse.prop)) []
   3.113 +    (Parse.!!! (Parse_Spec.locale_expression true) --
   3.114 +      Scan.optional (Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) []
   3.115        >> (fn (expr, equations) => Toplevel.print o
   3.116            Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations)));
   3.117  
   3.118 @@ -448,16 +448,16 @@
   3.119    OuterSyntax.command "interpret"
   3.120      "prove interpretation of locale expression in proof context"
   3.121      (Keyword.tag_proof Keyword.prf_goal)
   3.122 -    (Parse.!!! (SpecParse.locale_expression true)
   3.123 +    (Parse.!!! (Parse_Spec.locale_expression true)
   3.124        >> (fn expr => Toplevel.print o Toplevel.proof' (Expression.interpret_cmd expr)));
   3.125  
   3.126  
   3.127  (* classes *)
   3.128  
   3.129  val class_val =
   3.130 -  SpecParse.class_expr --
   3.131 -    Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 SpecParse.context_element)) [] ||
   3.132 -  Scan.repeat1 SpecParse.context_element >> pair [];
   3.133 +  Parse_Spec.class_expr --
   3.134 +    Scan.optional (Parse.$$$ "+" |-- Parse.!!! (Scan.repeat1 Parse_Spec.context_element)) [] ||
   3.135 +  Scan.repeat1 Parse_Spec.context_element >> pair [];
   3.136  
   3.137  val _ =
   3.138    OuterSyntax.command "class" "define type class" Keyword.thy_decl
   3.139 @@ -514,9 +514,9 @@
   3.140      (if schematic then "schematic_" ^ kind else kind)
   3.141      ("state " ^ (if schematic then "schematic " ^ kind else kind))
   3.142      (if schematic then Keyword.thy_schematic_goal else Keyword.thy_goal)
   3.143 -    (Scan.optional (SpecParse.opt_thm_name ":" --|
   3.144 -      Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) Attrib.empty_binding --
   3.145 -      SpecParse.general_statement >> (fn (a, (elems, concl)) =>
   3.146 +    (Scan.optional (Parse_Spec.opt_thm_name ":" --|
   3.147 +      Scan.ahead (Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --
   3.148 +      Parse_Spec.general_statement >> (fn (a, (elems, concl)) =>
   3.149          ((if schematic then Specification.schematic_theorem_cmd else Specification.theorem_cmd)
   3.150            kind NONE (K I) a elems concl)));
   3.151  
   3.152 @@ -537,27 +537,27 @@
   3.153  val _ =
   3.154    OuterSyntax.command "have" "state local goal"
   3.155      (Keyword.tag_proof Keyword.prf_goal)
   3.156 -    (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
   3.157 +    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.have));
   3.158  
   3.159  val _ =
   3.160    OuterSyntax.command "hence" "abbreviates \"then have\""
   3.161      (Keyword.tag_proof Keyword.prf_goal)
   3.162 -    (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
   3.163 +    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.hence));
   3.164  
   3.165  val _ =
   3.166    OuterSyntax.command "show" "state local goal, solving current obligation"
   3.167      (Keyword.tag_proof Keyword.prf_asm_goal)
   3.168 -    (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
   3.169 +    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.show));
   3.170  
   3.171  val _ =
   3.172    OuterSyntax.command "thus" "abbreviates \"then show\""
   3.173      (Keyword.tag_proof Keyword.prf_asm_goal)
   3.174 -    (SpecParse.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
   3.175 +    (Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o IsarCmd.thus));
   3.176  
   3.177  
   3.178  (* facts *)
   3.179  
   3.180 -val facts = Parse.and_list1 SpecParse.xthms1;
   3.181 +val facts = Parse.and_list1 Parse_Spec.xthms1;
   3.182  
   3.183  val _ =
   3.184    OuterSyntax.command "then" "forward chaining"
   3.185 @@ -577,7 +577,7 @@
   3.186  val _ =
   3.187    OuterSyntax.command "note" "define facts"
   3.188      (Keyword.tag_proof Keyword.prf_decl)
   3.189 -    (SpecParse.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
   3.190 +    (Parse_Spec.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
   3.191  
   3.192  val _ =
   3.193    OuterSyntax.command "using" "augment goal facts"
   3.194 @@ -600,18 +600,18 @@
   3.195  val _ =
   3.196    OuterSyntax.command "assume" "assume propositions"
   3.197      (Keyword.tag_proof Keyword.prf_asm)
   3.198 -    (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
   3.199 +    (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
   3.200  
   3.201  val _ =
   3.202    OuterSyntax.command "presume" "assume propositions, to be established later"
   3.203      (Keyword.tag_proof Keyword.prf_asm)
   3.204 -    (SpecParse.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
   3.205 +    (Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
   3.206  
   3.207  val _ =
   3.208    OuterSyntax.command "def" "local definition"
   3.209      (Keyword.tag_proof Keyword.prf_asm)
   3.210      (Parse.and_list1
   3.211 -      (SpecParse.opt_thm_name ":" --
   3.212 +      (Parse_Spec.opt_thm_name ":" --
   3.213          ((Parse.binding -- Parse.opt_mixfix) --
   3.214            ((Parse.$$$ "\\<equiv>" || Parse.$$$ "==") |-- Parse.!!! Parse.termp)))
   3.215      >> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
   3.216 @@ -619,7 +619,7 @@
   3.217  val _ =
   3.218    OuterSyntax.command "obtain" "generalized existence"
   3.219      (Keyword.tag_proof Keyword.prf_asm_goal)
   3.220 -    (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- SpecParse.statement
   3.221 +    (Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
   3.222        >> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
   3.223  
   3.224  val _ =
   3.225 @@ -636,13 +636,13 @@
   3.226  val _ =
   3.227    OuterSyntax.command "write" "add concrete syntax for constants / fixed variables"
   3.228      (Keyword.tag_proof Keyword.prf_decl)
   3.229 -    (opt_mode -- Parse.and_list1 (Parse.xname -- SpecParse.locale_mixfix)
   3.230 +    (opt_mode -- Parse.and_list1 (Parse.xname -- Parse_Spec.locale_mixfix)
   3.231      >> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
   3.232  
   3.233  val case_spec =
   3.234    (Parse.$$$ "(" |--
   3.235      Parse.!!! (Parse.xname -- Scan.repeat1 (Parse.maybe Parse.name) --| Parse.$$$ ")") ||
   3.236 -    Parse.xname >> rpair []) -- SpecParse.opt_attribs >> Parse.triple1;
   3.237 +    Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> Parse.triple1;
   3.238  
   3.239  val _ =
   3.240    OuterSyntax.command "case" "invoke local context"
   3.241 @@ -739,7 +739,7 @@
   3.242  (* calculational proof commands *)
   3.243  
   3.244  val calc_args =
   3.245 -  Scan.option (Parse.$$$ "(" |-- Parse.!!! ((SpecParse.xthms1 --| Parse.$$$ ")")));
   3.246 +  Scan.option (Parse.$$$ "(" |-- Parse.!!! ((Parse_Spec.xthms1 --| Parse.$$$ ")")));
   3.247  
   3.248  val _ =
   3.249    OuterSyntax.command "also" "combine calculation and current facts"
   3.250 @@ -883,7 +883,7 @@
   3.251  
   3.252  val _ =
   3.253    OuterSyntax.improper_command "thm_deps" "visualize theorem dependencies"
   3.254 -    Keyword.diag (SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
   3.255 +    Keyword.diag (Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.thm_deps));
   3.256  
   3.257  val _ =
   3.258    OuterSyntax.improper_command "print_binds" "print term bindings of proof context" Keyword.diag
   3.259 @@ -899,20 +899,20 @@
   3.260  
   3.261  val _ =
   3.262    OuterSyntax.improper_command "print_statement" "print theorems as long statements" Keyword.diag
   3.263 -    (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts));
   3.264 +    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_stmts));
   3.265  
   3.266  val _ =
   3.267    OuterSyntax.improper_command "thm" "print theorems" Keyword.diag
   3.268 -    (opt_modes -- SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
   3.269 +    (opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_thms));
   3.270  
   3.271  val _ =
   3.272    OuterSyntax.improper_command "prf" "print proof terms of theorems" Keyword.diag
   3.273 -    (opt_modes -- Scan.option SpecParse.xthms1
   3.274 +    (opt_modes -- Scan.option Parse_Spec.xthms1
   3.275        >> (Toplevel.no_timing oo IsarCmd.print_prfs false));
   3.276  
   3.277  val _ =
   3.278    OuterSyntax.improper_command "full_prf" "print full proof terms of theorems" Keyword.diag
   3.279 -    (opt_modes -- Scan.option SpecParse.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
   3.280 +    (opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo IsarCmd.print_prfs true));
   3.281  
   3.282  val _ =
   3.283    OuterSyntax.improper_command "prop" "read and print proposition" Keyword.diag

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Pure/Isar/parse_spec.ML	Sat May 15 23:32:15 2010 +0200
     4.3 @@ -0,0 +1,167 @@
     4.4 +(*  Title:      Pure/Isar/parse_spec.ML
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Parsers for complex specifications.
     4.8 +*)
     4.9 +
    4.10 +signature PARSE_SPEC =
    4.11 +sig
    4.12 +  val attrib: Attrib.src parser
    4.13 +  val attribs: Attrib.src list parser
    4.14 +  val opt_attribs: Attrib.src list parser
    4.15 +  val thm_name: string -> Attrib.binding parser
    4.16 +  val opt_thm_name: string -> Attrib.binding parser
    4.17 +  val spec: (Attrib.binding * string) parser
    4.18 +  val specs: (Attrib.binding * string list) parser
    4.19 +  val alt_specs: (Attrib.binding * string) list parser
    4.20 +  val where_alt_specs: (Attrib.binding * string) list parser
    4.21 +  val xthm: (Facts.ref * Attrib.src list) parser
    4.22 +  val xthms1: (Facts.ref * Attrib.src list) list parser
    4.23 +  val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
    4.24 +  val constdecl: (binding * string option * mixfix) parser
    4.25 +  val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
    4.26 +  val locale_mixfix: mixfix parser
    4.27 +  val locale_fixes: (binding * string option * mixfix) list parser
    4.28 +  val locale_insts: (string option list * (Attrib.binding * string) list) parser
    4.29 +  val class_expr: string list parser
    4.30 +  val locale_expression: bool -> Expression.expression parser
    4.31 +  val locale_keyword: string parser
    4.32 +  val context_element: Element.context parser
    4.33 +  val statement: (Attrib.binding * (string * string list) list) list parser
    4.34 +  val general_statement: (Element.context list * Element.statement) parser
    4.35 +  val statement_keyword: string parser
    4.36 +end;
    4.37 +
    4.38 +structure Parse_Spec: PARSE_SPEC =
    4.39 +struct
    4.40 +
    4.41 +(* theorem specifications *)
    4.42 +
    4.43 +val attrib =
    4.44 +  Parse.position ((Parse.keyword_ident_or_symbolic || Parse.xname) -- Parse.!!! Args.parse)
    4.45 +  >> Args.src;
    4.46 +
    4.47 +val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
    4.48 +val opt_attribs = Scan.optional attribs [];
    4.49 +
    4.50 +fun thm_name s = Parse.binding -- opt_attribs --| Parse.$$$ s;
    4.51 +
    4.52 +fun opt_thm_name s =
    4.53 +  Scan.optional ((Parse.binding -- opt_attribs || attribs >> pair Binding.empty) --| Parse.$$$ s)
    4.54 +    Attrib.empty_binding;
    4.55 +
    4.56 +val spec = opt_thm_name ":" -- Parse.prop;
    4.57 +val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
    4.58 +
    4.59 +val alt_specs =
    4.60 +  Parse.enum1 "|"
    4.61 +    (spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
    4.62 +
    4.63 +val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
    4.64 +
    4.65 +val xthm =
    4.66 +  Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
    4.67 +  (Parse.alt_string >> Facts.Fact ||
    4.68 +    Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
    4.69 +
    4.70 +val xthms1 = Scan.repeat1 xthm;
    4.71 +
    4.72 +val name_facts = Parse.and_list1 (opt_thm_name "=" -- xthms1);
    4.73 +
    4.74 +
    4.75 +(* basic constant specifications *)
    4.76 +
    4.77 +val constdecl =
    4.78 +  Parse.binding --
    4.79 +    (Parse.where_ >> K (NONE, NoSyn) ||
    4.80 +      Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) ||
    4.81 +      Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE))
    4.82 +  >> Parse.triple2;
    4.83 +
    4.84 +val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop);
    4.85 +
    4.86 +
    4.87 +(* locale and context elements *)
    4.88 +
    4.89 +val locale_mixfix =
    4.90 +  Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||
    4.91 +  Parse.mixfix;
    4.92 +
    4.93 +val locale_fixes =
    4.94 +  Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix
    4.95 +    >> (single o Parse.triple1) ||
    4.96 +  Parse.params >> map Syntax.no_syn) >> flat;
    4.97 +
    4.98 +val locale_insts =
    4.99 +  Scan.optional
   4.100 +    (Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] --
   4.101 +  Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) [];
   4.102 +
   4.103 +local
   4.104 +
   4.105 +val loc_element =
   4.106 +  Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes ||
   4.107 +  Parse.$$$ "constrains" |--
   4.108 +    Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ)))
   4.109 +    >> Element.Constrains ||
   4.110 +  Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp))
   4.111 +    >> Element.Assumes ||
   4.112 +  Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
   4.113 +    >> Element.Defines ||
   4.114 +  Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- xthms1))
   4.115 +    >> (curry Element.Notes "");
   4.116 +
   4.117 +fun plus1_unless test scan =
   4.118 +  scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
   4.119 +
   4.120 +fun prefix mandatory =
   4.121 +  Parse.name --
   4.122 +    (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
   4.123 +    Parse.$$$ ":";
   4.124 +
   4.125 +val instance = Parse.where_ |--
   4.126 +  Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
   4.127 +  Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
   4.128 +
   4.129 +in
   4.130 +
   4.131 +val locale_keyword =
   4.132 +  Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
   4.133 +  Parse.$$$ "defines" || Parse.$$$ "notes";
   4.134 +
   4.135 +val class_expr = plus1_unless locale_keyword Parse.xname;
   4.136 +
   4.137 +fun locale_expression mandatory =
   4.138 +  let
   4.139 +    val expr2 = Parse.xname;
   4.140 +    val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
   4.141 +      Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
   4.142 +    val expr0 = plus1_unless locale_keyword expr1;
   4.143 +  in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
   4.144 +
   4.145 +val context_element = Parse.group "context element" loc_element;
   4.146 +
   4.147 +end;
   4.148 +
   4.149 +
   4.150 +(* statements *)
   4.151 +
   4.152 +val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
   4.153 +
   4.154 +val obtain_case =
   4.155 +  Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] --
   4.156 +    (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
   4.157 +
   4.158 +val general_statement =
   4.159 +  statement >> (fn x => ([], Element.Shows x)) ||
   4.160 +  Scan.repeat context_element --
   4.161 +   (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains ||
   4.162 +    Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
   4.163 +
   4.164 +val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
   4.165 +
   4.166 +end;
   4.167 +
   4.168 +(*legacy alias*)
   4.169 +structure SpecParse = Parse_Spec;
   4.170 +

     5.1 --- a/src/Pure/Isar/spec_parse.ML	Sat May 15 23:23:45 2010 +0200
     5.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.3 @@ -1,163 +0,0 @@
     5.4 -(*  Title:      Pure/Isar/spec_parse.ML
     5.5 -    Author:     Makarius
     5.6 -
     5.7 -Parsers for complex specifications.
     5.8 -*)
     5.9 -
    5.10 -signature SPEC_PARSE =
    5.11 -sig
    5.12 -  val attrib: Attrib.src parser
    5.13 -  val attribs: Attrib.src list parser
    5.14 -  val opt_attribs: Attrib.src list parser
    5.15 -  val thm_name: string -> Attrib.binding parser
    5.16 -  val opt_thm_name: string -> Attrib.binding parser
    5.17 -  val spec: (Attrib.binding * string) parser
    5.18 -  val specs: (Attrib.binding * string list) parser
    5.19 -  val alt_specs: (Attrib.binding * string) list parser
    5.20 -  val where_alt_specs: (Attrib.binding * string) list parser
    5.21 -  val xthm: (Facts.ref * Attrib.src list) parser
    5.22 -  val xthms1: (Facts.ref * Attrib.src list) list parser
    5.23 -  val name_facts: (Attrib.binding * (Facts.ref * Attrib.src list) list) list parser
    5.24 -  val constdecl: (binding * string option * mixfix) parser
    5.25 -  val constdef: ((binding * string option * mixfix) option * (Attrib.binding * string)) parser
    5.26 -  val locale_mixfix: mixfix parser
    5.27 -  val locale_fixes: (binding * string option * mixfix) list parser
    5.28 -  val locale_insts: (string option list * (Attrib.binding * string) list) parser
    5.29 -  val class_expr: string list parser
    5.30 -  val locale_expression: bool -> Expression.expression parser
    5.31 -  val locale_keyword: string parser
    5.32 -  val context_element: Element.context parser
    5.33 -  val statement: (Attrib.binding * (string * string list) list) list parser
    5.34 -  val general_statement: (Element.context list * Element.statement) parser
    5.35 -  val statement_keyword: string parser
    5.36 -end;
    5.37 -
    5.38 -structure SpecParse: SPEC_PARSE =
    5.39 -struct
    5.40 -
    5.41 -(* theorem specifications *)
    5.42 -
    5.43 -val attrib =
    5.44 -  Parse.position ((Parse.keyword_ident_or_symbolic || Parse.xname) -- Parse.!!! Args.parse)
    5.45 -  >> Args.src;
    5.46 -
    5.47 -val attribs = Parse.$$$ "[" |-- Parse.list attrib --| Parse.$$$ "]";
    5.48 -val opt_attribs = Scan.optional attribs [];
    5.49 -
    5.50 -fun thm_name s = Parse.binding -- opt_attribs --| Parse.$$$ s;
    5.51 -
    5.52 -fun opt_thm_name s =
    5.53 -  Scan.optional ((Parse.binding -- opt_attribs || attribs >> pair Binding.empty) --| Parse.$$$ s)
    5.54 -    Attrib.empty_binding;
    5.55 -
    5.56 -val spec = opt_thm_name ":" -- Parse.prop;
    5.57 -val specs = opt_thm_name ":" -- Scan.repeat1 Parse.prop;
    5.58 -
    5.59 -val alt_specs =
    5.60 -  Parse.enum1 "|"
    5.61 -    (spec --| Scan.option (Scan.ahead (Parse.name || Parse.$$$ "[") -- Parse.!!! (Parse.$$$ "|")));
    5.62 -
    5.63 -val where_alt_specs = Parse.where_ |-- Parse.!!! alt_specs;
    5.64 -
    5.65 -val xthm =
    5.66 -  Parse.$$$ "[" |-- attribs --| Parse.$$$ "]" >> pair (Facts.named "") ||
    5.67 -  (Parse.alt_string >> Facts.Fact ||
    5.68 -    Parse.position Parse.xname -- Scan.option Attrib.thm_sel >> Facts.Named) -- opt_attribs;
    5.69 -
    5.70 -val xthms1 = Scan.repeat1 xthm;
    5.71 -
    5.72 -val name_facts = Parse.and_list1 (opt_thm_name "=" -- xthms1);
    5.73 -
    5.74 -
    5.75 -(* basic constant specifications *)
    5.76 -
    5.77 -val constdecl =
    5.78 -  Parse.binding --
    5.79 -    (Parse.where_ >> K (NONE, NoSyn) ||
    5.80 -      Parse.$$$ "::" |-- Parse.!!! ((Parse.typ >> SOME) -- Parse.opt_mixfix' --| Parse.where_) ||
    5.81 -      Scan.ahead (Parse.$$$ "(") |-- Parse.!!! (Parse.mixfix' --| Parse.where_ >> pair NONE))
    5.82 -  >> Parse.triple2;
    5.83 -
    5.84 -val constdef = Scan.option constdecl -- (opt_thm_name ":" -- Parse.prop);
    5.85 -
    5.86 -
    5.87 -(* locale and context elements *)
    5.88 -
    5.89 -val locale_mixfix =
    5.90 -  Parse.$$$ "(" -- Parse.$$$ "structure" -- Parse.!!! (Parse.$$$ ")") >> K Structure ||
    5.91 -  Parse.mixfix;
    5.92 -
    5.93 -val locale_fixes =
    5.94 -  Parse.and_list1 (Parse.binding -- Scan.option (Parse.$$$ "::" |-- Parse.typ) -- locale_mixfix
    5.95 -    >> (single o Parse.triple1) ||
    5.96 -  Parse.params >> map Syntax.no_syn) >> flat;
    5.97 -
    5.98 -val locale_insts =
    5.99 -  Scan.optional
   5.100 -    (Parse.$$$ "[" |-- Parse.!!! (Scan.repeat1 (Parse.maybe Parse.term) --| Parse.$$$ "]")) [] --
   5.101 -  Scan.optional (Parse.where_ |-- Parse.and_list1 (opt_thm_name ":" -- Parse.prop)) [];
   5.102 -
   5.103 -local
   5.104 -
   5.105 -val loc_element =
   5.106 -  Parse.$$$ "fixes" |-- Parse.!!! locale_fixes >> Element.Fixes ||
   5.107 -  Parse.$$$ "constrains" |--
   5.108 -    Parse.!!! (Parse.and_list1 (Parse.name -- (Parse.$$$ "::" |-- Parse.typ)))
   5.109 -    >> Element.Constrains ||
   5.110 -  Parse.$$$ "assumes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp))
   5.111 -    >> Element.Assumes ||
   5.112 -  Parse.$$$ "defines" |-- Parse.!!! (Parse.and_list1 (opt_thm_name ":" -- Parse.propp))
   5.113 -    >> Element.Defines ||
   5.114 -  Parse.$$$ "notes" |-- Parse.!!! (Parse.and_list1 (opt_thm_name "=" -- xthms1))
   5.115 -    >> (curry Element.Notes "");
   5.116 -
   5.117 -fun plus1_unless test scan =
   5.118 -  scan ::: Scan.repeat (Parse.$$$ "+" |-- Scan.unless test (Parse.!!! scan));
   5.119 -
   5.120 -fun prefix mandatory =
   5.121 -  Parse.name --
   5.122 -    (Parse.$$$ "!" >> K true || Parse.$$$ "?" >> K false || Scan.succeed mandatory) --|
   5.123 -    Parse.$$$ ":";
   5.124 -
   5.125 -val instance = Parse.where_ |--
   5.126 -  Parse.and_list1 (Parse.name -- (Parse.$$$ "=" |-- Parse.term)) >> Expression.Named ||
   5.127 -  Scan.repeat1 (Parse.maybe Parse.term) >> Expression.Positional;
   5.128 -
   5.129 -in
   5.130 -
   5.131 -val locale_keyword =
   5.132 -  Parse.$$$ "fixes" || Parse.$$$ "constrains" || Parse.$$$ "assumes" ||
   5.133 -  Parse.$$$ "defines" || Parse.$$$ "notes";
   5.134 -
   5.135 -val class_expr = plus1_unless locale_keyword Parse.xname;
   5.136 -
   5.137 -fun locale_expression mandatory =
   5.138 -  let
   5.139 -    val expr2 = Parse.xname;
   5.140 -    val expr1 = Scan.optional (prefix mandatory) ("", false) -- expr2 --
   5.141 -      Scan.optional instance (Expression.Named []) >> (fn ((p, l), i) => (l, (p, i)));
   5.142 -    val expr0 = plus1_unless locale_keyword expr1;
   5.143 -  in expr0 -- Scan.optional (Parse.$$$ "for" |-- Parse.!!! locale_fixes) [] end;
   5.144 -
   5.145 -val context_element = Parse.group "context element" loc_element;
   5.146 -
   5.147 -end;
   5.148 -
   5.149 -
   5.150 -(* statements *)
   5.151 -
   5.152 -val statement = Parse.and_list1 (opt_thm_name ":" -- Scan.repeat1 Parse.propp);
   5.153 -
   5.154 -val obtain_case =
   5.155 -  Parse.parbinding -- (Scan.optional (Parse.simple_fixes --| Parse.where_) [] --
   5.156 -    (Parse.and_list1 (Scan.repeat1 Parse.prop) >> flat));
   5.157 -
   5.158 -val general_statement =
   5.159 -  statement >> (fn x => ([], Element.Shows x)) ||
   5.160 -  Scan.repeat context_element --
   5.161 -   (Parse.$$$ "obtains" |-- Parse.!!! (Parse.enum1 "|" obtain_case) >> Element.Obtains ||
   5.162 -    Parse.$$$ "shows" |-- Parse.!!! statement >> Element.Shows);
   5.163 -
   5.164 -val statement_keyword = Parse.$$$ "obtains" || Parse.$$$ "shows";
   5.165 -
   5.166 -end;

     6.1 --- a/src/Pure/ROOT.ML	Sat May 15 23:23:45 2010 +0200
     6.2 +++ b/src/Pure/ROOT.ML	Sat May 15 23:32:15 2010 +0200
     6.3 @@ -220,7 +220,7 @@
     6.4  use "Isar/code.ML";
     6.5  
     6.6  (*specifications*)
     6.7 -use "Isar/spec_parse.ML";
     6.8 +use "Isar/parse_spec.ML";
     6.9  use "Isar/spec_rules.ML";
    6.10  use "Isar/specification.ML";
    6.11  use "Isar/typedecl.ML";