# HG changeset patch # User wenzelm # Date 1211659492 -7200 # Node ID 742e262132129bc225058dca9e11dd0bd409af2c # Parent 978cefd606ad3e89ca88dcc998c3ac641c59e01b more uniform treatment of OuterSyntax.local_theory commands; diff -r 978cefd606ad -r 742e26213212 src/HOL/Tools/inductive_package.ML --- a/src/HOL/Tools/inductive_package.ML Sat May 24 22:04:48 2008 +0200 +++ b/src/HOL/Tools/inductive_package.ML Sat May 24 22:04:52 2008 +0200 @@ -75,9 +75,8 @@ (string * string option * mixfix) list -> ((bstring * Attrib.src list) * string) list -> (Facts.ref * Attrib.src list) list -> local_theory -> inductive_result * local_theory - val gen_ind_decl: add_ind_def -> - bool -> OuterParse.token list -> - (Toplevel.transition -> Toplevel.transition) * OuterParse.token list + val gen_ind_decl: add_ind_def -> bool -> + OuterParse.token list -> (local_theory -> local_theory) * OuterParse.token list end; structure InductivePackage: INDUCTIVE_PACKAGE = @@ -945,25 +944,21 @@ | (a, _) => error ("Illegal local specification parameters for " ^ quote a)); fun gen_ind_decl mk_def coind = - P.opt_target -- P.fixes -- P.for_fixes -- Scan.optional (P.$$$ "where" |-- P.!!! SpecParse.specification) [] -- Scan.optional (P.$$$ "monos" |-- P.!!! SpecParse.xthms1) [] - >> (fn ((((loc, preds), params), specs), monos) => - Toplevel.local_theory loc - (fn lthy => lthy |> gen_add_inductive mk_def true coind preds params - (flatten_specification specs) monos |> snd)); + >> (fn (((preds, params), specs), monos) => + (snd o gen_add_inductive mk_def true coind preds params (flatten_specification specs) monos)); val ind_decl = gen_ind_decl add_ind_def; -val _ = OuterSyntax.command "inductive" "define inductive predicates" K.thy_decl (ind_decl false); -val _ = OuterSyntax.command "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true); +val _ = OuterSyntax.local_theory "inductive" "define inductive predicates" K.thy_decl (ind_decl false); +val _ = OuterSyntax.local_theory "coinductive" "define coinductive predicates" K.thy_decl (ind_decl true); val _ = - OuterSyntax.command "inductive_cases" + OuterSyntax.local_theory "inductive_cases" "create simplified instances of elimination rules (improper)" K.thy_script - (P.opt_target -- P.and_list1 SpecParse.spec - >> (fn (loc, specs) => Toplevel.local_theory loc (snd o inductive_cases specs))); + (P.and_list1 SpecParse.spec >> (fn specs => snd o inductive_cases specs)); end; diff -r 978cefd606ad -r 742e26213212 src/HOL/Tools/inductive_set_package.ML --- a/src/HOL/Tools/inductive_set_package.ML Sat May 24 22:04:48 2008 +0200 +++ b/src/HOL/Tools/inductive_set_package.ML Sat May 24 22:04:52 2008 +0200 @@ -545,10 +545,10 @@ val ind_set_decl = InductivePackage.gen_ind_decl add_ind_set_def; val _ = - OuterSyntax.command "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false); + OuterSyntax.local_theory "inductive_set" "define inductive sets" K.thy_decl (ind_set_decl false); val _ = - OuterSyntax.command "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true); + OuterSyntax.local_theory "coinductive_set" "define coinductive sets" K.thy_decl (ind_set_decl true); end; diff -r 978cefd606ad -r 742e26213212 src/HOL/Tools/recdef_package.ML --- a/src/HOL/Tools/recdef_package.ML Sat May 24 22:04:48 2008 +0200 +++ b/src/HOL/Tools/recdef_package.ML Sat May 24 22:04:52 2008 +0200 @@ -316,11 +316,10 @@ (defer_recdef_decl >> Toplevel.theory); val _ = - OuterSyntax.command "recdef_tc" "recommence proof of termination condition (TFL)" K.thy_goal - (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))); + OuterSyntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)" + K.thy_goal + (SpecParse.opt_thm_name ":" -- P.xname -- Scan.option (P.$$$ "(" |-- P.nat --| P.$$$ ")") + >> (fn ((thm_name, name), i) => recdef_tc thm_name name i)); end; diff -r 978cefd606ad -r 742e26213212 src/Pure/Isar/isar_syn.ML --- a/src/Pure/Isar/isar_syn.ML Sat May 24 22:04:48 2008 +0200 +++ b/src/Pure/Isar/isar_syn.ML Sat May 24 22:04:52 2008 +0200 @@ -232,55 +232,49 @@ val constdef = Scan.option constdecl -- (SpecParse.opt_thm_name ":" -- P.prop); val _ = - OuterSyntax.command "definition" "constant definition" K.thy_decl - (P.opt_target -- constdef - >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.definition_cmd args))); + OuterSyntax.local_theory "definition" "constant definition" K.thy_decl + (constdef >> (fn args => #2 o Specification.definition_cmd args)); val _ = - OuterSyntax.command "abbreviation" "constant abbreviation" K.thy_decl - (P.opt_target -- opt_mode -- (Scan.option constdecl -- P.prop) - >> (fn ((loc, mode), args) => - Toplevel.local_theory loc (Specification.abbreviation_cmd mode args))); + OuterSyntax.local_theory "abbreviation" "constant abbreviation" K.thy_decl + (opt_mode -- (Scan.option constdecl -- P.prop) + >> (fn (mode, args) => Specification.abbreviation_cmd mode args)); val _ = - OuterSyntax.command "notation" "add notation for constants / fixed variables" K.thy_decl - (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix) - >> (fn ((loc, mode), args) => - Toplevel.local_theory loc (Specification.notation_cmd true mode args))); + OuterSyntax.local_theory "notation" "add notation for constants / fixed variables" K.thy_decl + (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix) + >> (fn (mode, args) => Specification.notation_cmd true mode args)); val _ = - OuterSyntax.command "no_notation" "delete notation for constants / fixed variables" K.thy_decl - (P.opt_target -- opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix) - >> (fn ((loc, mode), args) => - Toplevel.local_theory loc (Specification.notation_cmd false mode args))); + OuterSyntax.local_theory "no_notation" "delete notation for constants / fixed variables" K.thy_decl + (opt_mode -- P.and_list1 (P.xname -- SpecParse.locale_mixfix) + >> (fn (mode, args) => Specification.notation_cmd false mode args)); (* constant specifications *) val _ = - OuterSyntax.command "axiomatization" "axiomatic constant specification" K.thy_decl - (P.opt_target -- - (Scan.optional P.fixes [] -- - Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.spec)) []) - >> (fn (loc, (x, y)) => Toplevel.local_theory loc (#2 o Specification.axiomatization_cmd x y))); + OuterSyntax.local_theory "axiomatization" "axiomatic constant specification" K.thy_decl + (Scan.optional P.fixes [] -- + Scan.optional (P.where_ |-- P.!!! (P.and_list1 SpecParse.spec)) [] + >> (fn (x, y) => #2 o Specification.axiomatization_cmd x y)); (* theorems *) -fun theorems kind = P.opt_target -- SpecParse.name_facts - >> (fn (loc, args) => Toplevel.local_theory loc (#2 o Specification.theorems_cmd kind args)); +fun theorems kind = + SpecParse.name_facts >> (fn args => #2 o Specification.theorems_cmd kind args); val _ = - OuterSyntax.command "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK); + OuterSyntax.local_theory "theorems" "define theorems" K.thy_decl (theorems Thm.theoremK); val _ = - OuterSyntax.command "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK); + OuterSyntax.local_theory "lemmas" "define lemmas" K.thy_decl (theorems Thm.lemmaK); val _ = - OuterSyntax.command "declare" "declare theorems (improper)" K.thy_decl - (P.opt_target -- (P.and_list1 SpecParse.xthms1 >> flat) - >> (fn (loc, args) => Toplevel.local_theory loc - (#2 o Specification.theorems_cmd "" [(("", []), args)]))); + OuterSyntax.local_theory "declare" "declare theorems (improper)" K.thy_decl + (P.and_list1 SpecParse.xthms1 + >> (fn args => #2 o Specification.theorems_cmd "" [(("", []), flat args)])); (* name space entry path *) @@ -328,16 +322,14 @@ >> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt))); val _ = - OuterSyntax.command "declaration" "generic ML declaration" (K.tag_ml K.thy_decl) - (P.opt_target -- P.position P.text - >> (fn (loc, txt) => Toplevel.local_theory loc (IsarCmd.declaration txt))); + OuterSyntax.local_theory "declaration" "generic ML declaration" (K.tag_ml K.thy_decl) + (P.position P.text >> IsarCmd.declaration); val _ = - OuterSyntax.command "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl) - (P.opt_target -- - P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") -- + OuterSyntax.local_theory "simproc_setup" "define simproc in ML" (K.tag_ml K.thy_decl) + (P.name -- (P.$$$ "(" |-- P.enum1 "|" P.term --| P.$$$ ")" --| P.$$$ "=") -- P.position P.text -- Scan.optional (P.$$$ "identifier" |-- Scan.repeat1 P.xname) [] - >> (fn ((((loc, a), b), c), d) => Toplevel.local_theory loc (IsarCmd.simproc_setup a b c d))); + >> (fn (((a, b), c), d) => IsarCmd.simproc_setup a b c d)); (* translation functions *) @@ -439,9 +431,8 @@ (Class.class_cmd name supclasses elems #-> TheoryTarget.begin))); val _ = - OuterSyntax.command "subclass" "prove a subclass relation" K.thy_goal - (P.opt_target -- P.xname >> (fn (loc, class) => - Toplevel.print o Toplevel.local_theory_to_proof loc (Subclass.subclass_cmd class))); + OuterSyntax.local_theory_to_proof "subclass" "prove a subclass relation" K.thy_goal + (P.xname >> Subclass.subclass_cmd); val _ = OuterSyntax.command "instantiation" "instantiate and prove type arity" K.thy_decl @@ -482,13 +473,11 @@ (* statements *) fun gen_theorem kind = - OuterSyntax.command kind ("state " ^ kind) K.thy_goal - (P.opt_target -- Scan.optional (SpecParse.opt_thm_name ":" --| + OuterSyntax.local_theory_to_proof' kind ("state " ^ kind) K.thy_goal + (Scan.optional (SpecParse.opt_thm_name ":" --| Scan.ahead (SpecParse.locale_keyword || SpecParse.statement_keyword)) ("", []) -- - SpecParse.general_statement >> (fn ((loc, a), (elems, concl)) => - (Toplevel.print o - Toplevel.local_theory_to_proof' loc - (Specification.theorem_cmd kind NONE (K I) a elems concl)))); + SpecParse.general_statement >> (fn (a, (elems, concl)) => + (Specification.theorem_cmd kind NONE (K I) a elems concl))); val _ = gen_theorem Thm.theoremK; val _ = gen_theorem Thm.lemmaK;