# HG changeset patch # User wenzelm # Date 1169240888 -3600 # Node ID 6d13239d5f52a13bcca966c4b88c172e13fd37fc # Parent 33d7468302bb86a4daf696cdeeb1c62b527909a1 moved parts of OuterParse to SpecParse; diff -r 33d7468302bb -r 6d13239d5f52 src/HOL/Nominal/nominal_primrec.ML --- a/src/HOL/Nominal/nominal_primrec.ML Fri Jan 19 22:08:07 2007 +0100 +++ b/src/HOL/Nominal/nominal_primrec.ML Fri Jan 19 22:08:08 2007 +0100 @@ -426,7 +426,7 @@ (parser4 --| P.$$$ ")")) (false, ("", (NONE, NONE))); val primrec_decl = - options -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop); + options -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop); val primrecP = OuterSyntax.command "nominal_primrec" "define primitive recursive functions on nominal datatypes" K.thy_goal diff -r 33d7468302bb -r 6d13239d5f52 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Fri Jan 19 22:08:07 2007 +0100 +++ b/src/HOL/Tools/datatype_package.ML Fri Jan 19 22:08:08 2007 +0100 @@ -1030,9 +1030,9 @@ val rep_datatype_decl = Scan.option (Scan.repeat1 P.name) -- - Scan.optional (P.$$$ "distinct" |-- P.!!! (P.and_list1 P.xthms1)) [[]] -- - Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 P.xthms1)) [[]] -- - (P.$$$ "induction" |-- P.!!! P.xthm); + Scan.optional (P.$$$ "distinct" |-- P.!!! (P.and_list1 SpecParse.xthms1)) [[]] -- + Scan.optional (P.$$$ "inject" |-- P.!!! (P.and_list1 SpecParse.xthms1)) [[]] -- + (P.$$$ "induction" |-- P.!!! SpecParse.xthm); fun mk_rep_datatype (((opt_ts, dss), iss), ind) = #2 o rep_datatype opt_ts dss iss ind; diff -r 33d7468302bb -r 6d13239d5f52 src/HOL/Tools/old_inductive_package.ML --- a/src/HOL/Tools/old_inductive_package.ML Fri Jan 19 22:08:07 2007 +0100 +++ b/src/HOL/Tools/old_inductive_package.ML Fri Jan 19 22:08:08 2007 +0100 @@ -888,8 +888,8 @@ fun ind_decl coind = Scan.repeat1 P.term -- (P.$$$ "intros" |-- - P.!!! (Scan.repeat (P.opt_thm_name ":" -- P.prop))) -- - Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] + P.!!! (Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop))) -- + Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] >> (Toplevel.theory o mk_ind coind); val inductiveP = @@ -900,7 +900,7 @@ val ind_cases = - P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop) + P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop) >> (Toplevel.theory o inductive_cases); val inductive_casesP = diff -r 33d7468302bb -r 6d13239d5f52 src/HOL/Tools/primrec_package.ML --- a/src/HOL/Tools/primrec_package.ML Fri Jan 19 22:08:07 2007 +0100 +++ b/src/HOL/Tools/primrec_package.ML Fri Jan 19 22:08:08 2007 +0100 @@ -321,7 +321,7 @@ P.name >> pair false) --| P.$$$ ")")) (false, ""); val primrec_decl = - opt_unchecked_name -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop); + opt_unchecked_name -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop); val primrecP = OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl diff -r 33d7468302bb -r 6d13239d5f52 src/HOL/Tools/recdef_package.ML --- a/src/HOL/Tools/recdef_package.ML Fri Jan 19 22:08:07 2007 +0100 +++ b/src/HOL/Tools/recdef_package.ML Fri Jan 19 22:08:08 2007 +0100 @@ -314,7 +314,7 @@ val recdef_decl = Scan.optional (P.$$$ "(" -- P.!!! (P.$$$ "permissive" -- P.$$$ ")") >> K false) true -- - P.name -- P.term -- Scan.repeat1 (P.opt_thm_name ":" -- P.prop) -- Scan.option hints + P.name -- P.term -- Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop) -- Scan.option hints >> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map P.triple_swap eqs) src); val recdefP = @@ -324,7 +324,7 @@ val defer_recdef_decl = P.name -- Scan.repeat1 P.prop -- - Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (P.xthms1 --| P.$$$ ")")) [] + Scan.optional (P.$$$ "(" |-- P.$$$ "congs" |-- P.!!! (SpecParse.xthms1 --| P.$$$ ")")) [] >> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs); val defer_recdefP = @@ -333,8 +333,8 @@ val recdef_tcP = OuterSyntax.command "recdef_tc" "recommence proof of termination condition (TFL)" K.thy_goal - (P.opt_locale_target -- - P.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") + (P.opt_target -- + SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") >> (fn (((loc, thm_name), name), i) => Toplevel.print o Toplevel.local_theory_to_proof loc (recdef_tc thm_name name i))); diff -r 33d7468302bb -r 6d13239d5f52 src/HOL/Tools/specification_package.ML --- a/src/HOL/Tools/specification_package.ML Fri Jan 19 22:08:07 2007 +0100 +++ b/src/HOL/Tools/specification_package.ML Fri Jan 19 22:08:08 2007 +0100 @@ -241,7 +241,7 @@ val specification_decl = P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" -- - Scan.repeat1 (P.opt_thm_name ":" -- P.prop) + Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop) val specificationP = OuterSyntax.command "specification" "define constants by specification" K.thy_goal @@ -252,7 +252,7 @@ val ax_specification_decl = P.name -- (P.$$$ "(" |-- Scan.repeat1 (opt_name -- P.term -- opt_overloaded) --| P.$$$ ")" -- - Scan.repeat1 (P.opt_thm_name ":" -- P.prop)) + Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop)) val ax_specificationP = OuterSyntax.command "ax_specification" "define constants by specification" K.thy_goal diff -r 33d7468302bb -r 6d13239d5f52 src/HOLCF/fixrec_package.ML --- a/src/HOLCF/fixrec_package.ML Fri Jan 19 22:08:07 2007 +0100 +++ b/src/HOLCF/fixrec_package.ML Fri Jan 19 22:08:08 2007 +0100 @@ -291,7 +291,7 @@ local structure P = OuterParse and K = OuterKeyword in -val fixrec_eqn = P.opt_thm_name ":" -- P.prop; +val fixrec_eqn = SpecParse.opt_thm_name ":" -- P.prop; val fixrec_strict = P.opt_keyword "permissive" >> not; @@ -304,7 +304,7 @@ (fixrec_decl >> (Toplevel.theory o uncurry add_fixrec)); (* fixpat parser *) -val fixpat_decl = P.opt_thm_name ":" -- Scan.repeat1 P.prop; +val fixpat_decl = SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop; val fixpatP = OuterSyntax.command "fixpat" "define rewrites for fixrec functions" K.thy_decl diff -r 33d7468302bb -r 6d13239d5f52 src/Pure/ProofGeneral/parsing.ML --- a/src/Pure/ProofGeneral/parsing.ML Fri Jan 19 22:08:07 2007 +0100 +++ b/src/Pure/ProofGeneral/parsing.ML Fri Jan 19 22:08:08 2007 +0100 @@ -129,8 +129,8 @@ val thmnameP = (* see isar_syn.ML/theoremsP *) let - val name_facts = P.and_list1 ((P.opt_thm_name "=" --| P.xthms1) >> #1) - val theoremsP = P.opt_locale_target |-- name_facts >> (fn [] => "" | x::_ => x) + val name_facts = P.and_list1 ((SpecParse.opt_thm_name "=" --| SpecParse.xthms1) >> #1) + val theoremsP = P.opt_target |-- name_facts >> (fn [] => "" | x::_ => x) in theoremsP end @@ -150,8 +150,8 @@ | "classes" => named_item P.name "class" | "classrel" => named_item P.name "class" | "consts" => named_item (P.const >> #1) "term" - | "axioms" => named_item (P.spec_name >> (#1 o #1)) "theorem" - | "defs" => named_item (opt_overloaded |-- P.spec_name >> (#1 o #1)) "theorem" + | "axioms" => named_item (SpecParse.spec_name >> (#1 o #1)) "theorem" + | "defs" => named_item (opt_overloaded |-- SpecParse.spec_name >> (#1 o #1)) "theorem" | "constdefs" => named_item P.name (* FIXME: heavily simplified/wrong *) "term" | "theorems" => named_item thmnameP "thmset" | "lemmas" => named_item thmnameP "thmset" @@ -164,17 +164,17 @@ fun xmls_of_thy_goal (name,toks,str) = let (* see isar_syn.ML/gen_theorem *) - val statement = P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.propp); + val statement = P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.propp); val general_statement = - statement >> pair [] || Scan.repeat P.locale_element -- (P.$$$ "shows" |-- statement); + statement >> pair [] || Scan.repeat SpecParse.locale_element -- (P.$$$ "shows" |-- statement); val gen_theoremP = - P.opt_locale_target -- Scan.optional (P.opt_thm_name ":" --| - Scan.ahead (P.locale_keyword || P.$$$ "shows")) ("", []) -- + P.opt_target -- Scan.optional (SpecParse.opt_thm_name ":" --| + Scan.ahead (SpecParse.locale_keyword || P.$$$ "shows")) ("", []) -- general_statement >> (fn ((locale, a), (elems, concl)) => fst a) (* a : (bstring * Args.src list) *) - val nameP = P.opt_locale_target |-- (Scan.optional ((P.opt_thm_name ":") >> #1) "") + val nameP = P.opt_target |-- (Scan.optional ((SpecParse.opt_thm_name ":") >> #1) "") val thmname = nameparse "opengoal" "theorem" nameP toks in [D.Opengoal {thmname=SOME thmname, text=str}, diff -r 33d7468302bb -r 6d13239d5f52 src/Pure/Tools/class_package.ML --- a/src/Pure/Tools/class_package.ML Fri Jan 19 22:08:07 2007 +0100 +++ b/src/Pure/Tools/class_package.ML Fri Jan 19 22:08:08 2007 +0100 @@ -560,7 +560,7 @@ val (classK, instanceK, print_classesK) = ("class", "instance", "print_classes") val class_subP = P.name -- Scan.repeat (P.$$$ "+" |-- P.name) >> (op ::); -val class_bodyP = P.!!! (Scan.repeat1 P.locale_element); +val class_bodyP = P.!!! (Scan.repeat1 SpecParse.locale_element); val parse_arity = (P.xname --| P.$$$ "::" -- P.!!! P.arity) @@ -582,7 +582,7 @@ OuterSyntax.command instanceK "prove type arity or subclass relation" K.thy_goal (( P.xname -- ((P.$$$ "\\" || P.$$$ "<") |-- P.!!! P.xname) >> instance_sort_e - || P.and_list1 parse_arity -- Scan.repeat (P.opt_thm_name ":" -- P.prop) + || P.and_list1 parse_arity -- Scan.repeat (SpecParse.opt_thm_name ":" -- P.prop) >> (fn (arities, defs) => instance_arity_e arities defs) ) >> (Toplevel.print oo Toplevel.theory_to_proof)); diff -r 33d7468302bb -r 6d13239d5f52 src/Pure/Tools/invoke.ML --- a/src/Pure/Tools/invoke.ML Fri Jan 19 22:08:07 2007 +0100 +++ b/src/Pure/Tools/invoke.ML Fri Jan 19 22:08:08 2007 +0100 @@ -119,7 +119,7 @@ OuterSyntax.command "invoke" "schematic invocation of locale expression in proof context" (K.tag_proof K.prf_goal) - (P.opt_thm_name ":" -- P.locale_expr -- P.locale_insts -- P.for_fixes + (SpecParse.opt_thm_name ":" -- SpecParse.locale_expr -- SpecParse.locale_insts -- P.for_fixes >> (fn (((name, expr), insts), fixes) => Toplevel.print o Toplevel.proof' (invoke name expr insts fixes))); diff -r 33d7468302bb -r 6d13239d5f52 src/ZF/Tools/datatype_package.ML --- a/src/ZF/Tools/datatype_package.ML Fri Jan 19 22:08:07 2007 +0100 +++ b/src/ZF/Tools/datatype_package.ML Fri Jan 19 22:08:08 2007 +0100 @@ -417,9 +417,9 @@ val datatype_decl = (Scan.optional ((P.$$$ "\\" || P.$$$ "<=") |-- P.!!! P.term) "") -- P.and_list1 (P.term -- (P.$$$ "=" |-- P.enum1 "|" con_decl)) -- - Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] -- - Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1) [] -- - Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1) [] + Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] -- + Scan.optional (P.$$$ "type_intros" |-- P.!!! SpecParse.xthms1) [] -- + Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) [] >> (Toplevel.theory o mk_datatype); val coind_prefix = if coind then "co" else ""; diff -r 33d7468302bb -r 6d13239d5f52 src/ZF/Tools/ind_cases.ML --- a/src/ZF/Tools/ind_cases.ML Fri Jan 19 22:08:07 2007 +0100 +++ b/src/ZF/Tools/ind_cases.ML Fri Jan 19 22:08:08 2007 +0100 @@ -82,7 +82,7 @@ local structure P = OuterParse and K = OuterKeyword in val ind_cases = - P.and_list1 (P.opt_thm_name ":" -- Scan.repeat1 P.prop) + P.and_list1 (SpecParse.opt_thm_name ":" -- Scan.repeat1 P.prop) >> (Toplevel.theory o inductive_cases); val inductive_casesP = diff -r 33d7468302bb -r 6d13239d5f52 src/ZF/Tools/induct_tacs.ML --- a/src/ZF/Tools/induct_tacs.ML Fri Jan 19 22:08:07 2007 +0100 +++ b/src/ZF/Tools/induct_tacs.ML Fri Jan 19 22:08:08 2007 +0100 @@ -199,10 +199,10 @@ local structure P = OuterParse and K = OuterKeyword in val rep_datatype_decl = - (P.$$$ "elimination" |-- P.!!! P.xthm) -- - (P.$$$ "induction" |-- P.!!! P.xthm) -- - (P.$$$ "case_eqns" |-- P.!!! P.xthms1) -- - Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! P.xthms1) [] + (P.$$$ "elimination" |-- P.!!! SpecParse.xthm) -- + (P.$$$ "induction" |-- P.!!! SpecParse.xthm) -- + (P.$$$ "case_eqns" |-- P.!!! SpecParse.xthms1) -- + Scan.optional (P.$$$ "recursor_eqns" |-- P.!!! SpecParse.xthms1) [] >> (fn (((x, y), z), w) => rep_datatype x y z w); val rep_datatypeP = diff -r 33d7468302bb -r 6d13239d5f52 src/ZF/Tools/inductive_package.ML --- a/src/ZF/Tools/inductive_package.ML Fri Jan 19 22:08:07 2007 +0100 +++ b/src/ZF/Tools/inductive_package.ML Fri Jan 19 22:08:08 2007 +0100 @@ -590,11 +590,11 @@ (P.$$$ "domains" |-- P.!!! (P.enum1 "+" P.term -- ((P.$$$ "\\" || P.$$$ "<=") |-- P.term))) -- (P.$$$ "intros" |-- - P.!!! (Scan.repeat1 (P.opt_thm_name ":" -- P.prop))) -- - Scan.optional (P.$$$ "monos" |-- P.!!! P.xthms1) [] -- - Scan.optional (P.$$$ "con_defs" |-- P.!!! P.xthms1) [] -- - Scan.optional (P.$$$ "type_intros" |-- P.!!! P.xthms1) [] -- - Scan.optional (P.$$$ "type_elims" |-- P.!!! P.xthms1) [] + P.!!! (Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop))) -- + Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] -- + Scan.optional (P.$$$ "con_defs" |-- P.!!! SpecParse.xthms1) [] -- + Scan.optional (P.$$$ "type_intros" |-- P.!!! SpecParse.xthms1) [] -- + Scan.optional (P.$$$ "type_elims" |-- P.!!! SpecParse.xthms1) [] >> (Toplevel.theory o mk_ind); val inductiveP = OuterSyntax.command (co_prefix ^ "inductive") diff -r 33d7468302bb -r 6d13239d5f52 src/ZF/Tools/primrec_package.ML --- a/src/ZF/Tools/primrec_package.ML Fri Jan 19 22:08:07 2007 +0100 +++ b/src/ZF/Tools/primrec_package.ML Fri Jan 19 22:08:08 2007 +0100 @@ -205,7 +205,7 @@ local structure P = OuterParse and K = OuterKeyword in -val primrec_decl = Scan.repeat1 (P.opt_thm_name ":" -- P.prop); +val primrec_decl = Scan.repeat1 (SpecParse.opt_thm_name ":" -- P.prop); val primrecP = OuterSyntax.command "primrec" "define primitive recursive functions on datatypes" K.thy_decl