--- a/NEWS Fri Mar 16 16:32:34 2012 +0000
+++ b/NEWS Fri Mar 16 18:21:22 2012 +0100
@@ -379,6 +379,10 @@
* Antiquotation @{keyword "name"} produces a parser for outer syntax
from a minor keyword introduced via theory header declaration.
+* Antiquotation @{command_spec "name"} produces the
+Outer_Syntax.command_spec from a major keyword introduced via theory
+header declaration; it can be passed to Outer_Syntax.command etc.
+
* Local_Theory.define no longer hard-wires default theorem name
"foo_def": definitional packages need to make this explicit, and may
choose to omit theorem bindings for definitions by using
--- a/src/HOL/Boogie/Tools/boogie_commands.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Boogie/Tools/boogie_commands.ML Fri Mar 16 18:21:22 2012 +0100
@@ -275,9 +275,8 @@
(Parse.string --| Args.colon -- Parse.nat))) []
val _ =
- Outer_Syntax.command "boogie_open"
+ Outer_Syntax.command @{command_spec "boogie_open"}
"open a new Boogie environment and load a Boogie-generated .b2i file"
- Keyword.thy_decl
(scan_opt "quiet" -- Parse.name -- vc_offsets >>
(Toplevel.theory o boogie_open))
@@ -303,9 +302,8 @@
Scan.succeed VC_Complete
val _ =
- Outer_Syntax.command "boogie_vc"
+ Outer_Syntax.command @{command_spec "boogie_vc"}
"enter into proof mode for a specific verification condition"
- Keyword.thy_goal
(vc_name -- vc_opts >> (fn args =>
(Toplevel.print o Toplevel.theory_to_proof (boogie_vc args))))
@@ -336,18 +334,16 @@
f (Toplevel.theory_of state))
val _ =
- Outer_Syntax.improper_command "boogie_status"
+ Outer_Syntax.improper_command @{command_spec "boogie_status"}
"show the name and state of all loaded verification conditions"
- Keyword.diag
(status_test >> status_cmd ||
status_vc >> status_cmd ||
Scan.succeed (status_cmd boogie_status))
val _ =
- Outer_Syntax.command "boogie_end"
+ Outer_Syntax.command @{command_spec "boogie_end"}
"close the current Boogie environment"
- Keyword.thy_decl
(Scan.succeed (Toplevel.theory boogie_end))
--- a/src/HOL/HOLCF/Tools/Domain/domain.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/HOLCF/Tools/Domain/domain.ML Fri Mar 16 18:21:22 2012 +0100
@@ -262,7 +262,7 @@
end
val _ =
- Outer_Syntax.command "domain" "define recursive domains (HOLCF)"
- Keyword.thy_decl (domains_decl >> (Toplevel.theory o mk_domain))
+ Outer_Syntax.command @{command_spec "domain"} "define recursive domains (HOLCF)"
+ (domains_decl >> (Toplevel.theory o mk_domain))
end
--- a/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/HOLCF/Tools/Domain/domain_isomorphism.ML Fri Mar 16 18:21:22 2012 +0100
@@ -771,8 +771,7 @@
in
val _ =
- Outer_Syntax.command "domain_isomorphism" "define domain isomorphisms (HOLCF)"
- Keyword.thy_decl
+ Outer_Syntax.command @{command_spec "domain_isomorphism"} "define domain isomorphisms (HOLCF)"
(parse_domain_isos >> (Toplevel.theory o domain_isomorphism_cmd))
end
--- a/src/HOL/HOLCF/Tools/cpodef.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/HOLCF/Tools/cpodef.ML Fri Mar 16 18:21:22 2012 +0100
@@ -357,14 +357,14 @@
((def, the_default t opt_name), (t, args, mx), A, morphs)
val _ =
- Outer_Syntax.command "pcpodef" "HOLCF type definition (requires admissibility proof)"
- Keyword.thy_goal
+ Outer_Syntax.command @{command_spec "pcpodef"}
+ "HOLCF type definition (requires admissibility proof)"
(typedef_proof_decl >>
(Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof true)))
val _ =
- Outer_Syntax.command "cpodef" "HOLCF type definition (requires admissibility proof)"
- Keyword.thy_goal
+ Outer_Syntax.command @{command_spec "cpodef"}
+ "HOLCF type definition (requires admissibility proof)"
(typedef_proof_decl >>
(Toplevel.print oo (Toplevel.theory_to_proof o mk_pcpodef_proof false)))
--- a/src/HOL/HOLCF/Tools/domaindef.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/HOLCF/Tools/domaindef.ML Fri Mar 16 18:21:22 2012 +0100
@@ -224,7 +224,7 @@
domaindef_cmd ((def, the_default t opt_name), (t, args, mx), A, morphs)
val _ =
- Outer_Syntax.command "domaindef" "HOLCF definition of domains from deflations" Keyword.thy_decl
+ Outer_Syntax.command @{command_spec "domaindef"} "HOLCF definition of domains from deflations"
(domaindef_decl >>
(Toplevel.print oo (Toplevel.theory o mk_domaindef)))
--- a/src/HOL/HOLCF/Tools/fixrec.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/HOLCF/Tools/fixrec.ML Fri Mar 16 18:21:22 2012 +0100
@@ -402,7 +402,7 @@
in Parse.enum1 "|" (spec' --| Scan.option (unexpected -- Parse.!!! (@{keyword "|"}))) end
val _ =
- Outer_Syntax.local_theory "fixrec" "define recursive functions (HOLCF)" Keyword.thy_decl
+ Outer_Syntax.local_theory @{command_spec "fixrec"} "define recursive functions (HOLCF)"
(Parse.fixes -- (Parse.where_ |-- Parse.!!! alt_specs')
>> (fn (fixes, specs) => add_fixrec_cmd fixes specs))
--- a/src/HOL/Import/import.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Import/import.ML Fri Mar 16 18:21:22 2012 +0100
@@ -238,51 +238,43 @@
val append_dump = (Parse.verbatim || Parse.string) >> add_dump
val _ =
- (Outer_Syntax.command "import_segment"
- "Set import segment name"
- Keyword.thy_decl (import_segment >> Toplevel.theory);
- Outer_Syntax.command "import_theory"
- "Set default external theory name"
- Keyword.thy_decl (import_theory >> Toplevel.theory);
- Outer_Syntax.command "end_import"
- "End external import"
- Keyword.thy_decl (end_import >> Toplevel.theory);
- Outer_Syntax.command "setup_theory"
- "Setup external theory replaying"
- Keyword.thy_decl (setup_theory >> Toplevel.theory);
- Outer_Syntax.command "end_setup"
- "End external setup"
- Keyword.thy_decl (end_setup >> Toplevel.theory);
- Outer_Syntax.command "setup_dump"
- "Setup the dump file name"
- Keyword.thy_decl (set_dump >> Toplevel.theory);
- Outer_Syntax.command "append_dump"
- "Add text to dump file"
- Keyword.thy_decl (append_dump >> Toplevel.theory);
- Outer_Syntax.command "flush_dump"
- "Write the dump to file"
- Keyword.thy_decl (fl_dump >> Toplevel.theory);
- Outer_Syntax.command "ignore_thms"
- "Theorems to ignore in next external theory import"
- Keyword.thy_decl (ignore_thms >> Toplevel.theory);
- Outer_Syntax.command "type_maps"
- "Map external type names to existing Isabelle/HOL type names"
- Keyword.thy_decl (type_maps >> Toplevel.theory);
- Outer_Syntax.command "def_maps"
- "Map external constant names to their primitive definitions"
- Keyword.thy_decl (def_maps >> Toplevel.theory);
- Outer_Syntax.command "thm_maps"
- "Map external theorem names to existing Isabelle/HOL theorem names"
- Keyword.thy_decl (thm_maps >> Toplevel.theory);
- Outer_Syntax.command "const_renames"
- "Rename external const names"
- Keyword.thy_decl (const_renames >> Toplevel.theory);
- Outer_Syntax.command "const_moves"
- "Rename external const names to other external constants"
- Keyword.thy_decl (const_moves >> Toplevel.theory);
- Outer_Syntax.command "const_maps"
- "Map external const names to existing Isabelle/HOL const names"
- Keyword.thy_decl (const_maps >> Toplevel.theory));
+ (Outer_Syntax.command @{command_spec "import_segment"} "set import segment name"
+ (import_segment >> Toplevel.theory);
+ Outer_Syntax.command @{command_spec "import_theory"} "set default external theory name"
+ (import_theory >> Toplevel.theory);
+ Outer_Syntax.command @{command_spec "end_import"} "end external import"
+ (end_import >> Toplevel.theory);
+ Outer_Syntax.command @{command_spec "setup_theory"} "setup external theory replaying"
+ (setup_theory >> Toplevel.theory);
+ Outer_Syntax.command @{command_spec "end_setup"} "end external setup"
+ (end_setup >> Toplevel.theory);
+ Outer_Syntax.command @{command_spec "setup_dump"} "setup the dump file name"
+ (set_dump >> Toplevel.theory);
+ Outer_Syntax.command @{command_spec "append_dump"} "add text to dump file"
+ (append_dump >> Toplevel.theory);
+ Outer_Syntax.command @{command_spec "flush_dump"} "write the dump to file"
+ (fl_dump >> Toplevel.theory);
+ Outer_Syntax.command @{command_spec "ignore_thms"}
+ "theorems to ignore in next external theory import"
+ (ignore_thms >> Toplevel.theory);
+ Outer_Syntax.command @{command_spec "type_maps"}
+ "map external type names to existing Isabelle/HOL type names"
+ (type_maps >> Toplevel.theory);
+ Outer_Syntax.command @{command_spec "def_maps"}
+ "map external constant names to their primitive definitions"
+ (def_maps >> Toplevel.theory);
+ Outer_Syntax.command @{command_spec "thm_maps"}
+ "map external theorem names to existing Isabelle/HOL theorem names"
+ (thm_maps >> Toplevel.theory);
+ Outer_Syntax.command @{command_spec "const_renames"}
+ "rename external const names"
+ (const_renames >> Toplevel.theory);
+ Outer_Syntax.command @{command_spec "const_moves"}
+ "rename external const names to other external constants"
+ (const_moves >> Toplevel.theory);
+ Outer_Syntax.command @{command_spec "const_maps"}
+ "map external const names to existing Isabelle/HOL const names"
+ (const_maps >> Toplevel.theory));
end
--- a/src/HOL/Nominal/nominal_atoms.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Nominal/nominal_atoms.ML Fri Mar 16 18:21:22 2012 +0100
@@ -1016,7 +1016,7 @@
(* syntax und parsing *)
val _ =
- Outer_Syntax.command "atom_decl" "declare new kinds of atoms" Keyword.thy_decl
+ Outer_Syntax.command @{command_spec "atom_decl"} "declare new kinds of atoms"
(Scan.repeat1 Parse.name >> (Toplevel.theory o create_nom_typedecls));
end;
--- a/src/HOL/Nominal/nominal_datatype.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Nominal/nominal_datatype.ML Fri Mar 16 18:21:22 2012 +0100
@@ -2044,7 +2044,7 @@
val nominal_datatype_cmd = gen_nominal_datatype Datatype.read_specs;
val _ =
- Outer_Syntax.command "nominal_datatype" "define nominal datatypes" Keyword.thy_decl
+ Outer_Syntax.command @{command_spec "nominal_datatype"} "define nominal datatypes"
(Parse.and_list1 Datatype.spec_cmd >>
(Toplevel.theory o nominal_datatype_cmd Datatype.default_config));
--- a/src/HOL/Nominal/nominal_inductive.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Nominal/nominal_inductive.ML Fri Mar 16 18:21:22 2012 +0100
@@ -670,16 +670,15 @@
(* outer syntax *)
val _ =
- Outer_Syntax.local_theory_to_proof "nominal_inductive"
+ Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive"}
"prove equivariance and strong induction theorem for inductive predicate involving nominal datatypes"
- Keyword.thy_goal
(Parse.xname -- Scan.optional (@{keyword "avoids"} |-- Parse.and_list1 (Parse.name --
(@{keyword ":"} |-- Scan.repeat1 Parse.name))) [] >> (fn (name, avoids) =>
prove_strong_ind name avoids));
val _ =
- Outer_Syntax.local_theory "equivariance"
- "prove equivariance for inductive predicate involving nominal datatypes" Keyword.thy_decl
+ Outer_Syntax.local_theory @{command_spec "equivariance"}
+ "prove equivariance for inductive predicate involving nominal datatypes"
(Parse.xname -- Scan.optional (@{keyword "["} |-- Parse.list1 Parse.name --| @{keyword "]"}) [] >>
(fn (name, atoms) => prove_eqvt name atoms));
--- a/src/HOL/Nominal/nominal_inductive2.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Nominal/nominal_inductive2.ML Fri Mar 16 18:21:22 2012 +0100
@@ -484,9 +484,8 @@
(* outer syntax *)
val _ =
- Outer_Syntax.local_theory_to_proof "nominal_inductive2"
+ Outer_Syntax.local_theory_to_proof @{command_spec "nominal_inductive2"}
"prove strong induction theorem for inductive predicate involving nominal datatypes"
- Keyword.thy_goal
(Parse.xname --
Scan.option (@{keyword "("} |-- Parse.!!! (Parse.name --| @{keyword ")"})) --
(Scan.optional (@{keyword "avoids"} |-- Parse.enum1 "|" (Parse.name --
--- a/src/HOL/Nominal/nominal_primrec.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Nominal/nominal_primrec.ML Fri Mar 16 18:21:22 2012 +0100
@@ -402,8 +402,8 @@
Scan.optional (@{keyword "("} |-- Parse.!!! (parser2 --| @{keyword ")"})) (NONE, NONE);
val _ =
- Outer_Syntax.local_theory_to_proof "nominal_primrec"
- "define primitive recursive functions on nominal datatypes" Keyword.thy_goal
+ Outer_Syntax.local_theory_to_proof @{command_spec "nominal_primrec"}
+ "define primitive recursive functions on nominal datatypes"
(options -- Parse.fixes -- Parse.for_fixes -- Parse_Spec.where_alt_specs
>> (fn ((((invs, fctxt), fixes), params), specs) =>
add_primrec_cmd invs fctxt fixes params specs));
--- a/src/HOL/Orderings.thy Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Orderings.thy Fri Mar 16 18:21:22 2012 +0100
@@ -409,8 +409,8 @@
(** Diagnostic command **)
val _ =
- Outer_Syntax.improper_command "print_orders"
- "print order structures available to transitivity reasoner" Keyword.diag
+ Outer_Syntax.improper_command @{command_spec "print_orders"}
+ "print order structures available to transitivity reasoner"
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
Toplevel.keep (print_structures o Toplevel.context_of)));
--- a/src/HOL/SPARK/Tools/spark_commands.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/SPARK/Tools/spark_commands.ML Fri Mar 16 18:21:22 2012 +0100
@@ -105,41 +105,36 @@
end);
val _ =
- Outer_Syntax.command "spark_open"
+ Outer_Syntax.command @{command_spec "spark_open"}
"open a new SPARK environment and load a SPARK-generated .vcg or .siv file"
- Keyword.thy_decl
(Parse.name -- Parse.parname >> (Toplevel.theory o spark_open));
val pfun_type = Scan.option
(Args.parens (Parse.list1 Parse.name) --| Args.colon -- Parse.name);
val _ =
- Outer_Syntax.command "spark_proof_functions"
+ Outer_Syntax.command @{command_spec "spark_proof_functions"}
"associate SPARK proof functions with terms"
- Keyword.thy_decl
(Scan.repeat1 (Parse.name -- (pfun_type --| Args.$$$ "=" -- Parse.term)) >>
- (Toplevel.theory o fold add_proof_fun_cmd));
+ (Toplevel.theory o fold add_proof_fun_cmd));
val _ =
- Outer_Syntax.command "spark_types"
+ Outer_Syntax.command @{command_spec "spark_types"}
"associate SPARK types with types"
- Keyword.thy_decl
(Scan.repeat1 (Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.typ --
Scan.optional (Args.parens (Parse.list1
(Parse.name -- Parse.!!! (Args.$$$ "=" |-- Parse.xname)))) [])) >>
(Toplevel.theory o fold add_spark_type_cmd));
val _ =
- Outer_Syntax.command "spark_vc"
+ Outer_Syntax.command @{command_spec "spark_vc"}
"enter into proof mode for a specific verification condition"
- Keyword.thy_goal
(Parse.name >> (fn name =>
(Toplevel.print o Toplevel.local_theory_to_proof NONE (prove_vc name))));
val _ =
- Outer_Syntax.improper_command "spark_status"
+ Outer_Syntax.improper_command @{command_spec "spark_status"}
"show the name and state of all loaded verification conditions"
- Keyword.diag
(Scan.optional
(Args.parens
( Args.$$$ "proved" >> K (is_some, K "")
@@ -147,9 +142,8 @@
(K true, string_of_status) >> show_status);
val _ =
- Outer_Syntax.command "spark_end"
+ Outer_Syntax.command @{command_spec "spark_end"}
"close the current SPARK environment"
- Keyword.thy_decl
(Scan.succeed (Toplevel.theory SPARK_VCs.close));
val setup = Theory.at_end (fn thy =>
--- a/src/HOL/Statespace/state_space.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Statespace/state_space.ML Fri Mar 16 18:21:22 2012 +0100
@@ -699,7 +699,7 @@
(plus1_unless comp parent --
Scan.optional (@{keyword "+"} |-- Parse.!!! (Scan.repeat1 comp)) [])));
val _ =
- Outer_Syntax.command "statespace" "define state space" Keyword.thy_decl
+ Outer_Syntax.command @{command_spec "statespace"} "define state space"
(statespace_decl >> (fn ((args, name), (parents, comps)) =>
Toplevel.theory (define_statespace args name parents comps)));
--- a/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/TPTP/TPTP_Parser/tptp_interpret.ML Fri Mar 16 18:21:22 2012 +0100
@@ -887,7 +887,7 @@
in TPTP_Data.map (cons ((prob_name, result))) thy' end
val _ =
- Outer_Syntax.improper_command "import_tptp" "import TPTP problem" Keyword.thy_decl
+ Outer_Syntax.improper_command @{command_spec "import_tptp"} "import TPTP problem"
(Parse.path >> (fn path =>
Toplevel.theory (fn thy => import_file true (Path.dir path) path [] [] thy)))
--- a/src/HOL/Tools/Datatype/datatype.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Datatype/datatype.ML Fri Mar 16 18:21:22 2012 +0100
@@ -792,7 +792,7 @@
>> (fn (((vs, t), mx), cons) => ((t, vs, mx), map Parse.triple1 cons));
val _ =
- Outer_Syntax.command "datatype" "define inductive datatypes" Keyword.thy_decl
+ Outer_Syntax.command @{command_spec "datatype"} "define inductive datatypes"
(Parse.and_list1 spec_cmd
>> (Toplevel.theory o (snd oo add_datatype_cmd Datatype_Aux.default_config)));
--- a/src/HOL/Tools/Datatype/primrec.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Datatype/primrec.ML Fri Mar 16 18:21:22 2012 +0100
@@ -310,8 +310,8 @@
(* outer syntax *)
val _ =
- Outer_Syntax.local_theory "primrec" "define primitive recursive functions on datatypes"
- Keyword.thy_decl
+ Outer_Syntax.local_theory @{command_spec "primrec"}
+ "define primitive recursive functions on datatypes"
(Parse.fixes -- Parse_Spec.where_alt_specs
>> (fn (fixes, specs) => add_primrec_cmd fixes specs #> snd));
--- a/src/HOL/Tools/Datatype/rep_datatype.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Datatype/rep_datatype.ML Fri Mar 16 18:21:22 2012 +0100
@@ -643,7 +643,7 @@
(* outer syntax *)
val _ =
- Outer_Syntax.command "rep_datatype" "represent existing types inductively" Keyword.thy_goal
+ Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing types inductively"
(Scan.repeat1 Parse.term >> (fn ts =>
Toplevel.print o
Toplevel.theory_to_proof (rep_datatype_cmd Datatype_Aux.default_config (K I) ts)));
--- a/src/HOL/Tools/Function/fun.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Function/fun.ML Fri Mar 16 18:21:22 2012 +0100
@@ -170,9 +170,9 @@
val _ =
- Outer_Syntax.local_theory' "fun" "define general recursive functions (short version)"
- Keyword.thy_decl
- (function_parser fun_config
- >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
+ Outer_Syntax.local_theory' @{command_spec "fun"}
+ "define general recursive functions (short version)"
+ (function_parser fun_config
+ >> (fn ((config, fixes), statements) => add_fun_cmd fixes statements config))
end
--- a/src/HOL/Tools/Function/function.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Function/function.ML Fri Mar 16 18:21:22 2012 +0100
@@ -277,15 +277,15 @@
(* outer syntax *)
val _ =
- Outer_Syntax.local_theory_to_proof' "function" "define general recursive functions"
- Keyword.thy_goal
- (function_parser default_config
- >> (fn ((config, fixes), statements) => function_cmd fixes statements config))
+ Outer_Syntax.local_theory_to_proof' @{command_spec "function"}
+ "define general recursive functions"
+ (function_parser default_config
+ >> (fn ((config, fixes), statements) => function_cmd fixes statements config))
val _ =
- Outer_Syntax.local_theory_to_proof "termination" "prove termination of a recursive function"
- Keyword.thy_goal
- (Scan.option Parse.term >> termination_cmd)
+ Outer_Syntax.local_theory_to_proof @{command_spec "termination"}
+ "prove termination of a recursive function"
+ (Scan.option Parse.term >> termination_cmd)
end
--- a/src/HOL/Tools/Function/partial_function.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Function/partial_function.ML Fri Mar 16 18:21:22 2012 +0100
@@ -281,10 +281,10 @@
val mode = @{keyword "("} |-- Parse.xname --| @{keyword ")"};
-val _ = Outer_Syntax.local_theory
- "partial_function" "define partial function" Keyword.thy_decl
- ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
- >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
+val _ =
+ Outer_Syntax.local_theory @{command_spec "partial_function"} "define partial function"
+ ((mode -- (Parse.fixes -- (Parse.where_ |-- Parse_Spec.spec)))
+ >> (fn (mode, (fixes, spec)) => add_partial_function_cmd mode fixes spec));
val setup = Mono_Rules.setup;
--- a/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Nitpick/nitpick_isar.ML Fri Mar 16 18:21:22 2012 +0100
@@ -390,16 +390,15 @@
params |> map string_for_raw_param
|> sort_strings |> cat_lines)))))
-val parse_nitpick_command =
- (parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans
-val parse_nitpick_params_command = parse_params #>> nitpick_params_trans
+val _ =
+ Outer_Syntax.improper_command @{command_spec "nitpick"}
+ "try to find a counterexample for a given subgoal using Nitpick"
+ ((parse_params -- Scan.optional Parse.nat 1) #>> nitpick_trans)
-val _ = Outer_Syntax.improper_command nitpickN
- "try to find a counterexample for a given subgoal using Nitpick"
- Keyword.diag parse_nitpick_command
-val _ = Outer_Syntax.command nitpick_paramsN
- "set and display the default parameters for Nitpick"
- Keyword.thy_decl parse_nitpick_params_command
+val _ =
+ Outer_Syntax.command @{command_spec "nitpick_params"}
+ "set and display the default parameters for Nitpick"
+ (parse_params #>> nitpick_params_trans)
fun try_nitpick auto = pick_nits [] (if auto then Auto_Try else Try) 1 0
--- a/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Predicate_Compile/code_prolog.ML Fri Mar 16 18:21:22 2012 +0100
@@ -1004,10 +1004,13 @@
val opt_print_modes =
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.xname --| @{keyword ")"})) [];
-val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag
- (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
- >> (fn ((print_modes, soln), t) => Toplevel.keep
- (values_cmd print_modes soln t))); (*FIXME does not preserve the previous functionality*)
+val _ =
+ Outer_Syntax.improper_command @{command_spec "values"}
+ "enumerate and print comprehensions"
+ (opt_print_modes -- Scan.optional (Parse.nat >> SOME) NONE -- Parse.term
+ >> (fn ((print_modes, soln), t) => Toplevel.keep
+ (values_cmd print_modes soln t))); (*FIXME does not preserve the previous functionality*)
+
(* quickcheck generator *)
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile.ML Fri Mar 16 18:21:22 2012 +0100
@@ -270,14 +270,16 @@
(* code_pred command and values command *)
-val _ = Outer_Syntax.local_theory_to_proof "code_pred"
- "prove equations for predicate specified by intro/elim rules"
- Keyword.thy_goal
- (opt_expected_modes -- opt_modes -- scan_options -- Parse.term_group >> code_pred_cmd)
+val _ =
+ Outer_Syntax.local_theory_to_proof @{command_spec "code_pred"}
+ "prove equations for predicate specified by intro/elim rules"
+ (opt_expected_modes -- opt_modes -- scan_options -- Parse.term_group >> code_pred_cmd)
-val _ = Outer_Syntax.improper_command "values" "enumerate and print comprehensions" Keyword.diag
- (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term
- >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep
- (Predicate_Compile_Core.values_cmd print_modes param_modes options k t)));
+val _ =
+ Outer_Syntax.improper_command @{command_spec "values"}
+ "enumerate and print comprehensions"
+ (opt_print_modes -- opt_param_modes -- value_options -- Scan.optional Parse.nat ~1 -- Parse.term
+ >> (fn ((((print_modes, param_modes), options), k), t) => Toplevel.keep
+ (Predicate_Compile_Core.values_cmd print_modes param_modes options k t)))
end
--- a/src/HOL/Tools/Quickcheck/abstract_generators.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Quickcheck/abstract_generators.ML Fri Mar 16 18:21:22 2012 +0100
@@ -64,8 +64,10 @@
val quickcheck_generator_cmd = gen_quickcheck_generator
(fn ctxt => fst o dest_Type o Proof_Context.read_type_name_proper ctxt false) Syntax.read_term
-val _ = Outer_Syntax.command "quickcheck_generator" "define quickcheck generators for abstract types"
- Keyword.thy_decl ((Parse.type_const --
+val _ =
+ Outer_Syntax.command @{command_spec "quickcheck_generator"}
+ "define quickcheck generators for abstract types"
+ ((Parse.type_const --
Scan.option (Args.$$$ "predicate" |-- @{keyword ":"} |-- Parse.term)) --
(Args.$$$ "constructors" |-- @{keyword ":"} |-- Parse.list1 Parse.term)
>> (fn ((tyco, opt_pred), constrs) =>
--- a/src/HOL/Tools/Quickcheck/find_unused_assms.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Quickcheck/find_unused_assms.ML Fri Mar 16 18:21:22 2012 +0100
@@ -104,8 +104,8 @@
val _ =
- Outer_Syntax.improper_command "find_unused_assms" "find theorems with superfluous assumptions"
- Keyword.diag
+ Outer_Syntax.improper_command @{command_spec "find_unused_assms"}
+ "find theorems with superfluous assumptions"
(Scan.option Parse.name
>> (fn opt_thy_name =>
Toplevel.no_timing o Toplevel.keep (fn state =>
--- a/src/HOL/Tools/Quotient/quotient_def.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Quotient/quotient_def.ML Fri Mar 16 18:21:22 2012 +0100
@@ -106,14 +106,13 @@
quotient_def (SOME (Binding.name qconst_name, NONE, mx), (Attrib.empty_binding, (lhs, rconst))) ctxt
end
-(* parser and command *)
-val quotdef_parser =
- Scan.option Parse_Spec.constdecl --
- Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term))
+(* command *)
val _ =
- Outer_Syntax.local_theory "quotient_definition"
+ Outer_Syntax.local_theory @{command_spec "quotient_definition"}
"definition for constants over the quotient type"
- Keyword.thy_decl (quotdef_parser >> (snd oo quotient_def_cmd))
+ (Scan.option Parse_Spec.constdecl --
+ Parse.!!! (Parse_Spec.opt_thm_name ":" -- (Parse.term --| @{keyword "is"} -- Parse.term))
+ >> (snd oo quotient_def_cmd))
end; (* structure *)
--- a/src/HOL/Tools/Quotient/quotient_info.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Quotient/quotient_info.ML Fri Mar 16 18:21:22 2012 +0100
@@ -291,15 +291,15 @@
(* outer syntax commands *)
val _ =
- Outer_Syntax.improper_command "print_quotmaps" "print quotient map functions" Keyword.diag
+ Outer_Syntax.improper_command @{command_spec "print_quotmaps"} "print quotient map functions"
(Scan.succeed (Toplevel.keep (print_quotmaps o Toplevel.context_of)))
val _ =
- Outer_Syntax.improper_command "print_quotients" "print quotients" Keyword.diag
+ Outer_Syntax.improper_command @{command_spec "print_quotients"} "print quotients"
(Scan.succeed (Toplevel.keep (print_quotients o Toplevel.context_of)))
val _ =
- Outer_Syntax.improper_command "print_quotconsts" "print quotient constants" Keyword.diag
+ Outer_Syntax.improper_command @{command_spec "print_quotconsts"} "print quotient constants"
(Scan.succeed (Toplevel.keep (print_quotconsts o Toplevel.context_of)))
end;
--- a/src/HOL/Tools/Quotient/quotient_type.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Quotient/quotient_type.ML Fri Mar 16 18:21:22 2012 +0100
@@ -264,17 +264,15 @@
val partial = Scan.optional (Parse.reserved "partial" -- @{keyword ":"} >> K true) false
-val quotspec_parser =
- Parse.and_list1
- ((Parse.type_args -- Parse.binding) --
- (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
- Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
- (@{keyword "/"} |-- (partial -- Parse.term)) --
- Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
-
val _ =
- Outer_Syntax.local_theory_to_proof "quotient_type"
+ Outer_Syntax.local_theory_to_proof @{command_spec "quotient_type"}
"quotient type definitions (require equivalence proofs)"
- Keyword.thy_goal (quotspec_parser >> quotient_type_cmd)
+ (Parse.and_list1
+ ((Parse.type_args -- Parse.binding) --
+ (* FIXME Parse.type_args_constrained and standard treatment of sort constraints *)
+ Parse.opt_mixfix -- (@{keyword "="} |-- Parse.typ) --
+ (@{keyword "/"} |-- (partial -- Parse.term)) --
+ Scan.option (@{keyword "morphisms"} |-- Parse.!!! (Parse.binding -- Parse.binding)))
+ >> quotient_type_cmd)
end;
--- a/src/HOL/Tools/SMT/smt_config.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/SMT/smt_config.ML Fri Mar 16 18:21:22 2012 +0100
@@ -247,10 +247,9 @@
end
val _ =
- Outer_Syntax.improper_command "smt_status"
- ("show the available SMT solvers, the currently selected SMT solver, " ^
- "and the values of SMT configuration options")
- Keyword.diag
+ Outer_Syntax.improper_command @{command_spec "smt_status"}
+ "show the available SMT solvers, the currently selected SMT solver, \
+ \and the values of SMT configuration options"
(Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
print_setup (Toplevel.context_of state))))
--- a/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/Sledgehammer/sledgehammer_isar.ML Fri Mar 16 18:21:22 2012 +0100
@@ -413,20 +413,16 @@
Scan.optional (Args.parens (Scan.repeat parse_relevance_chunk
>> merge_relevance_overrides))
no_relevance_override
-val parse_sledgehammer_command =
- (Scan.optional Parse.short_ident runN -- parse_params
- -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans
-val parse_sledgehammer_params_command =
- parse_params #>> sledgehammer_params_trans
val _ =
- Outer_Syntax.improper_command sledgehammerN
- "search for first-order proof using automatic theorem provers" Keyword.diag
- parse_sledgehammer_command
+ Outer_Syntax.improper_command @{command_spec "sledgehammer"}
+ "search for first-order proof using automatic theorem provers"
+ ((Scan.optional Parse.short_ident runN -- parse_params
+ -- parse_relevance_override -- Scan.option Parse.nat) #>> sledgehammer_trans)
val _ =
- Outer_Syntax.command sledgehammer_paramsN
- "set and display the default parameters for Sledgehammer" Keyword.thy_decl
- parse_sledgehammer_params_command
+ Outer_Syntax.command @{command_spec "sledgehammer_params"}
+ "set and display the default parameters for Sledgehammer"
+ (parse_params #>> sledgehammer_params_trans)
fun try_sledgehammer auto state =
let
--- a/src/HOL/Tools/choice_specification.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/choice_specification.ML Fri Mar 16 18:21:22 2012 +0100
@@ -237,25 +237,19 @@
val opt_name = Scan.optional (Parse.name --| @{keyword ":"}) ""
val opt_overloaded = Parse.opt_keyword "overloaded"
-val specification_decl =
- @{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
- Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
+val _ =
+ Outer_Syntax.command @{command_spec "specification"} "define constants by specification"
+ (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
+ Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop)
+ >> (fn (cos, alt_props) => Toplevel.print o
+ (Toplevel.theory_to_proof (process_spec NONE cos alt_props))))
val _ =
- Outer_Syntax.command "specification" "define constants by specification" Keyword.thy_goal
- (specification_decl >> (fn (cos,alt_props) =>
- Toplevel.print o (Toplevel.theory_to_proof
- (process_spec NONE cos alt_props))))
-
-val ax_specification_decl =
- Parse.name --
- (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
- Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop))
-
-val _ =
- Outer_Syntax.command "ax_specification" "define constants by specification" Keyword.thy_goal
- (ax_specification_decl >> (fn (axname,(cos,alt_props)) =>
- Toplevel.print o (Toplevel.theory_to_proof
- (process_spec (SOME axname) cos alt_props))))
+ Outer_Syntax.command @{command_spec "ax_specification"} "define constants by specification"
+ (Parse.name --
+ (@{keyword "("} |-- Scan.repeat1 (opt_name -- Parse.term -- opt_overloaded) --| @{keyword ")"} --
+ Scan.repeat1 ((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.prop))
+ >> (fn (axname, (cos, alt_props)) =>
+ Toplevel.print o (Toplevel.theory_to_proof (process_spec (SOME axname) cos alt_props))))
end
--- a/src/HOL/Tools/enriched_type.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/enriched_type.ML Fri Mar 16 18:21:22 2012 +0100
@@ -266,9 +266,10 @@
val enriched_type = gen_enriched_type Syntax.check_term;
val enriched_type_cmd = gen_enriched_type Syntax.read_term;
-val _ = Outer_Syntax.local_theory_to_proof "enriched_type"
- "register operations managing the functorial structure of a type"
- Keyword.thy_goal (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term
- >> (fn (prfx, t) => enriched_type_cmd prfx t));
+val _ =
+ Outer_Syntax.local_theory_to_proof @{command_spec "enriched_type"}
+ "register operations managing the functorial structure of a type"
+ (Scan.option (Parse.name --| @{keyword ":"}) -- Parse.term
+ >> (fn (prfx, t) => enriched_type_cmd prfx t));
end;
--- a/src/HOL/Tools/inductive.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/inductive.ML Fri Mar 16 18:21:22 2012 +0100
@@ -1144,21 +1144,21 @@
val ind_decl = gen_ind_decl add_ind_def;
val _ =
- Outer_Syntax.local_theory' "inductive" "define inductive predicates" Keyword.thy_decl
+ Outer_Syntax.local_theory' @{command_spec "inductive"} "define inductive predicates"
(ind_decl false);
val _ =
- Outer_Syntax.local_theory' "coinductive" "define coinductive predicates" Keyword.thy_decl
+ Outer_Syntax.local_theory' @{command_spec "coinductive"} "define coinductive predicates"
(ind_decl true);
val _ =
- Outer_Syntax.local_theory "inductive_cases"
- "create simplified instances of elimination rules (improper)" Keyword.thy_script
+ Outer_Syntax.local_theory @{command_spec "inductive_cases"}
+ "create simplified instances of elimination rules (improper)"
(Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_cases));
val _ =
- Outer_Syntax.local_theory "inductive_simps"
- "create simplification rules for inductive predicates" Keyword.thy_script
+ Outer_Syntax.local_theory @{command_spec "inductive_simps"}
+ "create simplification rules for inductive predicates"
(Parse.and_list1 Parse_Spec.specs >> (snd oo inductive_simps));
end;
--- a/src/HOL/Tools/inductive_set.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/inductive_set.ML Fri Mar 16 18:21:22 2012 +0100
@@ -575,11 +575,11 @@
val ind_set_decl = Inductive.gen_ind_decl add_ind_set_def;
val _ =
- Outer_Syntax.local_theory' "inductive_set" "define inductive sets" Keyword.thy_decl
+ Outer_Syntax.local_theory' @{command_spec "inductive_set"} "define inductive sets"
(ind_set_decl false);
val _ =
- Outer_Syntax.local_theory' "coinductive_set" "define coinductive sets" Keyword.thy_decl
+ Outer_Syntax.local_theory' @{command_spec "coinductive_set"} "define coinductive sets"
(ind_set_decl true);
end;
--- a/src/HOL/Tools/recdef.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/recdef.ML Fri Mar 16 18:21:22 2012 +0100
@@ -302,7 +302,7 @@
>> (fn ((((p, f), R), eqs), src) => #1 o add_recdef p f R (map Parse.triple_swap eqs) src);
val _ =
- Outer_Syntax.command "recdef" "define general recursive functions (TFL)" Keyword.thy_decl
+ Outer_Syntax.command @{command_spec "recdef"} "define general recursive functions (TFL)"
(recdef_decl >> Toplevel.theory);
@@ -313,12 +313,13 @@
>> (fn ((f, eqs), congs) => #1 o defer_recdef f eqs congs);
val _ =
- Outer_Syntax.command "defer_recdef" "defer general recursive functions (TFL)" Keyword.thy_decl
+ Outer_Syntax.command @{command_spec "defer_recdef"}
+ "defer general recursive functions (TFL)"
(defer_recdef_decl >> Toplevel.theory);
val _ =
- Outer_Syntax.local_theory_to_proof' "recdef_tc" "recommence proof of termination condition (TFL)"
- Keyword.thy_goal
+ Outer_Syntax.local_theory_to_proof' @{command_spec "recdef_tc"}
+ "recommence proof of termination condition (TFL)"
((Parse_Spec.opt_thm_name ":" >> apfst Binding.name_of) -- Parse.xname --
Scan.option (@{keyword "("} |-- Parse.nat --| @{keyword ")"})
>> (fn ((thm_name, name), i) => recdef_tc thm_name name i));
--- a/src/HOL/Tools/record.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/record.ML Fri Mar 16 18:21:22 2012 +0100
@@ -2311,7 +2311,7 @@
(* outer syntax *)
val _ =
- Outer_Syntax.command "record" "define extensible record" Keyword.thy_decl
+ Outer_Syntax.command @{command_spec "record"} "define extensible record"
(Parse.type_args_constrained -- Parse.binding --
(@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) --
Scan.repeat1 Parse.const_binding)
--- a/src/HOL/Tools/refute.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/refute.ML Fri Mar 16 18:21:22 2012 +0100
@@ -3198,8 +3198,8 @@
(* 'refute' command *)
val _ =
- Outer_Syntax.improper_command "refute"
- "try to find a model that refutes a given subgoal" Keyword.diag
+ Outer_Syntax.improper_command @{command_spec "refute"}
+ "try to find a model that refutes a given subgoal"
(scan_parms -- Scan.optional Parse.nat 1 >>
(fn (parms, i) =>
Toplevel.keep (fn state =>
@@ -3212,8 +3212,8 @@
(* 'refute_params' command *)
val _ =
- Outer_Syntax.command "refute_params"
- "show/store default parameters for the 'refute' command" Keyword.thy_decl
+ Outer_Syntax.command @{command_spec "refute_params"}
+ "show/store default parameters for the 'refute' command"
(scan_parms >> (fn parms =>
Toplevel.theory (fn thy =>
let
--- a/src/HOL/Tools/try0.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/try0.ML Fri Mar 16 18:21:22 2012 +0100
@@ -183,13 +183,10 @@
|| Scan.repeat parse_attr
>> (fn quad => fold merge_attrs quad ([], [], [], []))) x
-val parse_try0_command =
- Scan.optional parse_attrs ([], [], [], []) #>> try0_trans
-
val _ =
- Outer_Syntax.improper_command try0N
- "try a combination of proof methods" Keyword.diag
- parse_try0_command
+ Outer_Syntax.improper_command @{command_spec "try0"}
+ "try a combination of proof methods"
+ (Scan.optional parse_attrs ([], [], [], []) #>> try0_trans)
fun try_try0 auto =
do_try0 (if auto then Auto_Try else Try) NONE ([], [], [], [])
--- a/src/HOL/Tools/typedef.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/HOL/Tools/typedef.ML Fri Mar 16 18:21:22 2012 +0100
@@ -300,8 +300,8 @@
(** outer syntax **)
val _ =
- Outer_Syntax.local_theory_to_proof "typedef" "HOL type definition (requires non-emptiness proof)"
- Keyword.thy_goal
+ Outer_Syntax.local_theory_to_proof @{command_spec "typedef"}
+ "HOL type definition (requires non-emptiness proof)"
(Scan.optional (@{keyword "("} |--
((@{keyword "open"} >> K false) -- Scan.option Parse.binding ||
Parse.binding >> (fn s => (true, SOME s))) --| @{keyword ")"}) (true, NONE) --
--- a/src/Provers/classical.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Provers/classical.ML Fri Mar 16 18:21:22 2012 +0100
@@ -960,8 +960,7 @@
(** outer syntax **)
val _ =
- Outer_Syntax.improper_command "print_claset" "print context of Classical Reasoner"
- Keyword.diag
+ Outer_Syntax.improper_command @{command_spec "print_claset"} "print context of Classical Reasoner"
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
Toplevel.keep (fn state =>
let val ctxt = Toplevel.context_of state
--- a/src/Pure/Isar/isar_syn.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/Isar/isar_syn.ML Fri Mar 16 18:21:22 2012 +0100
@@ -25,14 +25,14 @@
(** init and exit **)
val _ =
- Outer_Syntax.command "theory" "begin theory" (Keyword.tag_theory Keyword.thy_begin)
+ Outer_Syntax.command ("theory", Keyword.tag_theory Keyword.thy_begin) "begin theory"
(Thy_Header.args >> (fn header =>
Toplevel.print o
Toplevel.init_theory
(fn () => Thy_Info.toplevel_begin_theory (Thy_Load.get_master_path ()) header)));
val _ =
- Outer_Syntax.command "end" "end (local) theory" (Keyword.tag_theory Keyword.thy_end)
+ Outer_Syntax.command ("end", Keyword.tag_theory Keyword.thy_end) "end (local) theory"
(Scan.succeed
(Toplevel.exit o Toplevel.end_local_theory o Toplevel.end_proof (K Proof.end_notepad)));
@@ -40,43 +40,65 @@
(** markup commands **)
-val _ = Outer_Syntax.markup_command Thy_Output.Markup "header" "theory header" Keyword.diag
- (Parse.doc_source >> Isar_Cmd.header_markup);
+val _ =
+ Outer_Syntax.markup_command Thy_Output.Markup
+ ("header", Keyword.diag) "theory header"
+ (Parse.doc_source >> Isar_Cmd.header_markup);
-val _ = Outer_Syntax.markup_command Thy_Output.Markup "chapter" "chapter heading"
- Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
+val _ =
+ Outer_Syntax.markup_command Thy_Output.Markup
+ ("chapter", Keyword.thy_heading) "chapter heading"
+ (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
-val _ = Outer_Syntax.markup_command Thy_Output.Markup "section" "section heading"
- Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
+val _ =
+ Outer_Syntax.markup_command Thy_Output.Markup
+ ("section", Keyword.thy_heading) "section heading"
+ (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
-val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsection" "subsection heading"
- Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
+val _ =
+ Outer_Syntax.markup_command Thy_Output.Markup
+ ("subsection", Keyword.thy_heading) "subsection heading"
+ (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
+
+val _ =
+ Outer_Syntax.markup_command Thy_Output.Markup
+ ("subsubsection", Keyword.thy_heading) "subsubsection heading"
+ (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
val _ =
- Outer_Syntax.markup_command Thy_Output.Markup "subsubsection" "subsubsection heading"
- Keyword.thy_heading (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
-
-val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv "text" "formal comment (theory)"
- Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
+ Outer_Syntax.markup_command Thy_Output.MarkupEnv
+ ("text", Keyword.thy_decl) "formal comment (theory)"
+ (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
-val _ = Outer_Syntax.markup_command Thy_Output.Verbatim "text_raw" "raw document preparation text"
- Keyword.thy_decl (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
+val _ =
+ Outer_Syntax.markup_command Thy_Output.Verbatim
+ ("text_raw", Keyword.thy_decl) "raw document preparation text"
+ (Parse.opt_target -- Parse.doc_source >> Isar_Cmd.local_theory_markup);
-val _ = Outer_Syntax.markup_command Thy_Output.Markup "sect" "formal comment (proof)"
- (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
+val _ =
+ Outer_Syntax.markup_command Thy_Output.Markup
+ ("sect", Keyword.tag_proof Keyword.prf_heading) "formal comment (proof)"
+ (Parse.doc_source >> Isar_Cmd.proof_markup);
-val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsect" "formal comment (proof)"
- (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
+val _ =
+ Outer_Syntax.markup_command Thy_Output.Markup
+ ("subsect", Keyword.tag_proof Keyword.prf_heading) "formal comment (proof)"
+ (Parse.doc_source >> Isar_Cmd.proof_markup);
-val _ = Outer_Syntax.markup_command Thy_Output.Markup "subsubsect" "formal comment (proof)"
- (Keyword.tag_proof Keyword.prf_heading) (Parse.doc_source >> Isar_Cmd.proof_markup);
+val _ =
+ Outer_Syntax.markup_command Thy_Output.Markup
+ ("subsubsect", Keyword.tag_proof Keyword.prf_heading) "formal comment (proof)"
+ (Parse.doc_source >> Isar_Cmd.proof_markup);
-val _ = Outer_Syntax.markup_command Thy_Output.MarkupEnv "txt" "formal comment (proof)"
- (Keyword.tag_proof Keyword.prf_decl) (Parse.doc_source >> Isar_Cmd.proof_markup);
+val _ =
+ Outer_Syntax.markup_command Thy_Output.MarkupEnv
+ ("txt", Keyword.tag_proof Keyword.prf_decl) "formal comment (proof)"
+ (Parse.doc_source >> Isar_Cmd.proof_markup);
-val _ = Outer_Syntax.markup_command Thy_Output.Verbatim "txt_raw"
- "raw document preparation text (proof)" (Keyword.tag_proof Keyword.prf_decl)
- (Parse.doc_source >> Isar_Cmd.proof_markup);
+val _ =
+ Outer_Syntax.markup_command Thy_Output.Verbatim
+ ("txt_raw", Keyword.tag_proof Keyword.prf_decl) "raw document preparation text (proof)"
+ (Parse.doc_source >> Isar_Cmd.proof_markup);
@@ -85,60 +107,60 @@
(* classes and sorts *)
val _ =
- Outer_Syntax.command "classes" "declare type classes" Keyword.thy_decl
+ Outer_Syntax.command ("classes", Keyword.thy_decl) "declare type classes"
(Scan.repeat1 (Parse.binding -- Scan.optional ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |--
Parse.!!! (Parse.list1 Parse.class)) [])
>> (Toplevel.theory o fold AxClass.axiomatize_class_cmd));
val _ =
- Outer_Syntax.command "classrel" "state inclusion of type classes (axiomatic!)" Keyword.thy_decl
+ Outer_Syntax.command ("classrel", Keyword.thy_decl) "state inclusion of type classes (axiomatic!)"
(Parse.and_list1 (Parse.class -- ((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<")
|-- Parse.!!! Parse.class))
>> (Toplevel.theory o AxClass.axiomatize_classrel_cmd));
val _ =
- Outer_Syntax.local_theory "default_sort" "declare default sort for explicit type variables"
- Keyword.thy_decl
+ Outer_Syntax.local_theory ("default_sort", Keyword.thy_decl)
+ "declare default sort for explicit type variables"
(Parse.sort >> (fn s => fn lthy => Local_Theory.set_defsort (Syntax.read_sort lthy s) lthy));
(* types *)
val _ =
- Outer_Syntax.local_theory "typedecl" "type declaration" Keyword.thy_decl
+ Outer_Syntax.local_theory ("typedecl", Keyword.thy_decl) "type declaration"
(Parse.type_args -- Parse.binding -- Parse.opt_mixfix
>> (fn ((args, a), mx) => Typedecl.typedecl (a, map (rpair dummyS) args, mx) #> snd));
val _ =
- Outer_Syntax.local_theory "type_synonym" "declare type abbreviation" Keyword.thy_decl
+ Outer_Syntax.local_theory ("type_synonym", Keyword.thy_decl) "declare type abbreviation"
(Parse.type_args -- Parse.binding --
(Parse.$$$ "=" |-- Parse.!!! (Parse.typ -- Parse.opt_mixfix'))
>> (fn ((args, a), (rhs, mx)) => snd o Typedecl.abbrev_cmd (a, args, mx) rhs));
val _ =
- Outer_Syntax.command "nonterminal"
- "declare syntactic type constructors (grammar nonterminal symbols)" Keyword.thy_decl
+ Outer_Syntax.command ("nonterminal", Keyword.thy_decl)
+ "declare syntactic type constructors (grammar nonterminal symbols)"
(Parse.and_list1 Parse.binding >> (Toplevel.theory o Sign.add_nonterminals_global));
val _ =
- Outer_Syntax.command "arities" "state type arities (axiomatic!)" Keyword.thy_decl
+ Outer_Syntax.command ("arities", Keyword.thy_decl) "state type arities (axiomatic!)"
(Scan.repeat1 Parse.arity >> (Toplevel.theory o fold AxClass.axiomatize_arity_cmd));
(* consts and syntax *)
val _ =
- Outer_Syntax.command "judgment" "declare object-logic judgment" Keyword.thy_decl
+ Outer_Syntax.command ("judgment", Keyword.thy_decl) "declare object-logic judgment"
(Parse.const_binding >> (Toplevel.theory o Object_Logic.add_judgment_cmd));
val _ =
- Outer_Syntax.command "consts" "declare constants" Keyword.thy_decl
+ Outer_Syntax.command ("consts", Keyword.thy_decl) "declare constants"
(Scan.repeat1 Parse.const_binding >> (Toplevel.theory o Sign.add_consts));
val opt_overloaded = Parse.opt_keyword "overloaded";
val _ =
- Outer_Syntax.command "finalconsts" "declare constants as final" Keyword.thy_decl
+ Outer_Syntax.command ("finalconsts", Keyword.thy_decl) "declare constants as final"
(opt_overloaded -- Scan.repeat1 Parse.term >> (uncurry (Toplevel.theory oo Theory.add_finals)));
val mode_spec =
@@ -149,11 +171,11 @@
Scan.optional (Parse.$$$ "(" |-- Parse.!!! (mode_spec --| Parse.$$$ ")")) Syntax.mode_default;
val _ =
- Outer_Syntax.command "syntax" "declare syntactic constants" Keyword.thy_decl
+ Outer_Syntax.command ("syntax", Keyword.thy_decl) "declare syntactic constants"
(opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.add_modesyntax));
val _ =
- Outer_Syntax.command "no_syntax" "delete syntax declarations" Keyword.thy_decl
+ Outer_Syntax.command ("no_syntax", Keyword.thy_decl) "delete syntax declarations"
(opt_mode -- Scan.repeat1 Parse.const_decl >> (Toplevel.theory o uncurry Sign.del_modesyntax));
@@ -174,18 +196,18 @@
>> (fn (left, (arr, right)) => arr (left, right));
val _ =
- Outer_Syntax.command "translations" "declare syntax translation rules" Keyword.thy_decl
+ Outer_Syntax.command ("translations", Keyword.thy_decl) "declare syntax translation rules"
(Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.translations));
val _ =
- Outer_Syntax.command "no_translations" "remove syntax translation rules" Keyword.thy_decl
+ Outer_Syntax.command ("no_translations", Keyword.thy_decl) "remove syntax translation rules"
(Scan.repeat1 trans_line >> (Toplevel.theory o Isar_Cmd.no_translations));
(* axioms and definitions *)
val _ =
- Outer_Syntax.command "axioms" "state arbitrary propositions (axiomatic!)" Keyword.thy_decl
+ Outer_Syntax.command ("axioms", Keyword.thy_decl) "state arbitrary propositions (axiomatic!)"
(Scan.repeat1 Parse_Spec.spec >>
(fn spec => Toplevel.theory (fn thy =>
(legacy_feature "Old 'axioms' command -- use 'axiomatization' instead";
@@ -197,7 +219,7 @@
Parse.$$$ "overloaded" >> K (false, true)) --| Parse.$$$ ")")) (false, false);
val _ =
- Outer_Syntax.command "defs" "define constants" Keyword.thy_decl
+ Outer_Syntax.command ("defs", Keyword.thy_decl) "define constants"
(opt_unchecked_overloaded --
Scan.repeat1 (Parse_Spec.thm_name ":" -- Parse.prop >> (fn ((x, y), z) => ((x, z), y)))
>> (Toplevel.theory o Isar_Cmd.add_defs));
@@ -206,35 +228,35 @@
(* constant definitions and abbreviations *)
val _ =
- Outer_Syntax.local_theory' "definition" "constant definition" Keyword.thy_decl
+ Outer_Syntax.local_theory' ("definition", Keyword.thy_decl) "constant definition"
(Parse_Spec.constdef >> (fn args => #2 oo Specification.definition_cmd args));
val _ =
- Outer_Syntax.local_theory' "abbreviation" "constant abbreviation" Keyword.thy_decl
+ Outer_Syntax.local_theory' ("abbreviation", Keyword.thy_decl) "constant abbreviation"
(opt_mode -- (Scan.option Parse_Spec.constdecl -- Parse.prop)
>> (fn (mode, args) => Specification.abbreviation_cmd mode args));
val _ =
- Outer_Syntax.local_theory "type_notation" "add concrete syntax for type constructors"
- Keyword.thy_decl
+ Outer_Syntax.local_theory ("type_notation", Keyword.thy_decl)
+ "add concrete syntax for type constructors"
(opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
>> (fn (mode, args) => Specification.type_notation_cmd true mode args));
val _ =
- Outer_Syntax.local_theory "no_type_notation" "delete concrete syntax for type constructors"
- Keyword.thy_decl
+ Outer_Syntax.local_theory ("no_type_notation", Keyword.thy_decl)
+ "delete concrete syntax for type constructors"
(opt_mode -- Parse.and_list1 (Parse.type_const -- Parse.mixfix)
>> (fn (mode, args) => Specification.type_notation_cmd false mode args));
val _ =
- Outer_Syntax.local_theory "notation" "add concrete syntax for constants / fixed variables"
- Keyword.thy_decl
+ Outer_Syntax.local_theory ("notation", Keyword.thy_decl)
+ "add concrete syntax for constants / fixed variables"
(opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
>> (fn (mode, args) => Specification.notation_cmd true mode args));
val _ =
- Outer_Syntax.local_theory "no_notation" "delete concrete syntax for constants / fixed variables"
- Keyword.thy_decl
+ Outer_Syntax.local_theory ("no_notation", Keyword.thy_decl)
+ "delete concrete syntax for constants / fixed variables"
(opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
>> (fn (mode, args) => Specification.notation_cmd false mode args));
@@ -242,7 +264,7 @@
(* constant specifications *)
val _ =
- Outer_Syntax.command "axiomatization" "axiomatic constant specification" Keyword.thy_decl
+ Outer_Syntax.command ("axiomatization", Keyword.thy_decl) "axiomatic constant specification"
(Scan.optional Parse.fixes [] --
Scan.optional (Parse.where_ |-- Parse.!!! (Parse.and_list1 Parse_Spec.specs)) []
>> (fn (x, y) => Toplevel.theory (#2 o Specification.axiomatization_cmd x y)));
@@ -255,13 +277,14 @@
>> (fn (facts, fixes) => #2 oo Specification.theorems_cmd kind facts fixes);
val _ =
- Outer_Syntax.local_theory' "theorems" "define theorems" Keyword.thy_decl (theorems Thm.theoremK);
+ Outer_Syntax.local_theory' ("theorems", Keyword.thy_decl) "define theorems"
+ (theorems Thm.theoremK);
val _ =
- Outer_Syntax.local_theory' "lemmas" "define lemmas" Keyword.thy_decl (theorems Thm.lemmaK);
+ Outer_Syntax.local_theory' ("lemmas", Keyword.thy_decl) "define lemmas" (theorems Thm.lemmaK);
val _ =
- Outer_Syntax.local_theory' "declare" "declare theorems" Keyword.thy_decl
+ Outer_Syntax.local_theory' ("declare", Keyword.thy_decl) "declare theorems"
(Parse.and_list1 Parse_Spec.xthms1 -- Parse.for_fixes
>> (fn (facts, fixes) =>
#2 oo Specification.theorems_cmd "" [(Attrib.empty_binding, flat facts)] fixes));
@@ -270,7 +293,7 @@
(* name space entry path *)
fun hide_names name hide what =
- Outer_Syntax.command name ("hide " ^ what ^ " from name space") Keyword.thy_decl
+ Outer_Syntax.command (name, Keyword.thy_decl) ("hide " ^ what ^ " from name space")
((Parse.opt_keyword "open" >> not) -- Scan.repeat1 Parse.xname >>
(Toplevel.theory o uncurry hide));
@@ -283,65 +306,66 @@
(* use ML text *)
val _ =
- Outer_Syntax.command "use" "ML text from file" (Keyword.tag_ml Keyword.thy_decl)
+ Outer_Syntax.command ("use", Keyword.tag_ml Keyword.thy_decl) "ML text from file"
(Parse.path >> (fn path => Toplevel.generic_theory (Thy_Load.exec_ml path)));
val _ =
- Outer_Syntax.command "ML" "ML text within theory or local theory"
- (Keyword.tag_ml Keyword.thy_decl)
+ Outer_Syntax.command ("ML", Keyword.tag_ml Keyword.thy_decl)
+ "ML text within theory or local theory"
(Parse.ML_source >> (fn (txt, pos) =>
Toplevel.generic_theory
(ML_Context.exec (fn () => ML_Context.eval_text true pos txt) #>
Local_Theory.propagate_ml_env)));
val _ =
- Outer_Syntax.command "ML_prf" "ML text within proof" (Keyword.tag_proof Keyword.prf_decl)
+ Outer_Syntax.command ("ML_prf", Keyword.tag_proof Keyword.prf_decl) "ML text within proof"
(Parse.ML_source >> (fn (txt, pos) =>
Toplevel.proof (Proof.map_context (Context.proof_map
(ML_Context.exec (fn () => ML_Context.eval_text true pos txt))) #> Proof.propagate_ml_env)));
val _ =
- Outer_Syntax.command "ML_val" "diagnostic ML text" (Keyword.tag_ml Keyword.diag)
+ Outer_Syntax.command ("ML_val", Keyword.tag_ml Keyword.diag) "diagnostic ML text"
(Parse.ML_source >> Isar_Cmd.ml_diag true);
val _ =
- Outer_Syntax.command "ML_command" "diagnostic ML text (silent)" (Keyword.tag_ml Keyword.diag)
+ Outer_Syntax.command ("ML_command", Keyword.tag_ml Keyword.diag) "diagnostic ML text (silent)"
(Parse.ML_source >> (Toplevel.no_timing oo Isar_Cmd.ml_diag false));
val _ =
- Outer_Syntax.command "setup" "ML theory setup" (Keyword.tag_ml Keyword.thy_decl)
+ Outer_Syntax.command ("setup", Keyword.tag_ml Keyword.thy_decl) "ML theory setup"
(Parse.ML_source >> (Toplevel.theory o Isar_Cmd.global_setup));
val _ =
- Outer_Syntax.local_theory "local_setup" "ML local theory setup" (Keyword.tag_ml Keyword.thy_decl)
+ Outer_Syntax.local_theory ("local_setup", Keyword.tag_ml Keyword.thy_decl) "ML local theory setup"
(Parse.ML_source >> Isar_Cmd.local_setup);
val _ =
- Outer_Syntax.command "attribute_setup" "define attribute in ML" (Keyword.tag_ml Keyword.thy_decl)
+ Outer_Syntax.command ("attribute_setup", Keyword.tag_ml Keyword.thy_decl) "define attribute in ML"
(Parse.position Parse.name --
Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Scan.optional Parse.text "")
>> (fn (name, (txt, cmt)) => Toplevel.theory (Attrib.attribute_setup name txt cmt)));
val _ =
- Outer_Syntax.command "method_setup" "define proof method in ML" (Keyword.tag_ml Keyword.thy_decl)
+ Outer_Syntax.command ("method_setup", Keyword.tag_ml Keyword.thy_decl) "define proof method in ML"
(Parse.position Parse.name --
Parse.!!! (Parse.$$$ "=" |-- Parse.ML_source -- Scan.optional Parse.text "")
>> (fn (name, (txt, cmt)) => Toplevel.theory (Method.method_setup name txt cmt)));
val _ =
- Outer_Syntax.local_theory "declaration" "generic ML declaration"
- (Keyword.tag_ml Keyword.thy_decl)
+ Outer_Syntax.local_theory ("declaration", Keyword.tag_ml Keyword.thy_decl)
+ "generic ML declaration"
(Parse.opt_keyword "pervasive" -- Parse.ML_source
>> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = false, pervasive = pervasive} txt));
val _ =
- Outer_Syntax.local_theory "syntax_declaration" "generic ML declaration"
- (Keyword.tag_ml Keyword.thy_decl)
+ Outer_Syntax.local_theory ("syntax_declaration", Keyword.tag_ml Keyword.thy_decl)
+ "generic ML declaration"
(Parse.opt_keyword "pervasive" -- Parse.ML_source
>> (fn (pervasive, txt) => Isar_Cmd.declaration {syntax = true, pervasive = pervasive} txt));
val _ =
- Outer_Syntax.local_theory "simproc_setup" "define simproc in ML" (Keyword.tag_ml Keyword.thy_decl)
+ Outer_Syntax.local_theory ("simproc_setup", Keyword.tag_ml Keyword.thy_decl)
+ "define simproc in ML"
(Parse.position Parse.name --
(Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")" --| Parse.$$$ "=") --
Parse.ML_source -- Scan.optional (Parse.$$$ "identifier" |-- Scan.repeat1 Parse.xname) []
@@ -353,35 +377,35 @@
val trfun = Parse.opt_keyword "advanced" -- Parse.ML_source;
val _ =
- Outer_Syntax.command "parse_ast_translation" "install parse ast translation functions"
- (Keyword.tag_ml Keyword.thy_decl)
+ Outer_Syntax.command ("parse_ast_translation", Keyword.tag_ml Keyword.thy_decl)
+ "install parse ast translation functions"
(trfun >> (Toplevel.theory o Isar_Cmd.parse_ast_translation));
val _ =
- Outer_Syntax.command "parse_translation" "install parse translation functions"
- (Keyword.tag_ml Keyword.thy_decl)
+ Outer_Syntax.command ("parse_translation", Keyword.tag_ml Keyword.thy_decl)
+ "install parse translation functions"
(trfun >> (Toplevel.theory o Isar_Cmd.parse_translation));
val _ =
- Outer_Syntax.command "print_translation" "install print translation functions"
- (Keyword.tag_ml Keyword.thy_decl)
+ Outer_Syntax.command ("print_translation", Keyword.tag_ml Keyword.thy_decl)
+ "install print translation functions"
(trfun >> (Toplevel.theory o Isar_Cmd.print_translation));
val _ =
- Outer_Syntax.command "typed_print_translation" "install typed print translation functions"
- (Keyword.tag_ml Keyword.thy_decl)
+ Outer_Syntax.command ("typed_print_translation", Keyword.tag_ml Keyword.thy_decl)
+ "install typed print translation functions"
(trfun >> (Toplevel.theory o Isar_Cmd.typed_print_translation));
val _ =
- Outer_Syntax.command "print_ast_translation" "install print ast translation functions"
- (Keyword.tag_ml Keyword.thy_decl)
+ Outer_Syntax.command ("print_ast_translation", Keyword.tag_ml Keyword.thy_decl)
+ "install print ast translation functions"
(trfun >> (Toplevel.theory o Isar_Cmd.print_ast_translation));
(* oracles *)
val _ =
- Outer_Syntax.command "oracle" "declare oracle" (Keyword.tag_ml Keyword.thy_decl)
+ Outer_Syntax.command ("oracle", Keyword.tag_ml Keyword.thy_decl) "declare oracle"
(Parse.position Parse.name -- (Parse.$$$ "=" |-- Parse.ML_source) >>
(fn (x, y) => Toplevel.theory (Isar_Cmd.oracle x y)));
@@ -389,7 +413,7 @@
(* local theories *)
val _ =
- Outer_Syntax.command "context" "enter local theory context" Keyword.thy_decl
+ Outer_Syntax.command ("context", Keyword.thy_decl) "enter local theory context"
(Parse.position Parse.name --| Parse.begin >> (fn name =>
Toplevel.print o Toplevel.begin_local_theory true (Named_Target.context_cmd name)));
@@ -402,7 +426,7 @@
Scan.repeat1 Parse_Spec.context_element >> pair ([], []);
val _ =
- Outer_Syntax.command "locale" "define named proof context" Keyword.thy_decl
+ Outer_Syntax.command ("locale", Keyword.thy_decl) "define named proof context"
(Parse.binding --
Scan.optional (Parse.$$$ "=" |-- Parse.!!! locale_val) (([], []), []) -- Parse.opt_begin
>> (fn ((name, (expr, elems)), begin) =>
@@ -415,24 +439,23 @@
(Parse.where_ |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)) [];
val _ =
- Outer_Syntax.command "sublocale"
- "prove sublocale relation between a locale and a locale expression" Keyword.thy_goal
+ Outer_Syntax.command ("sublocale", Keyword.thy_goal)
+ "prove sublocale relation between a locale and a locale expression"
(Parse.position Parse.xname --| (Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") --
parse_interpretation_arguments false
>> (fn (loc, (expr, equations)) =>
Toplevel.print o Toplevel.theory_to_proof (Expression.sublocale_cmd I loc expr equations)));
val _ =
- Outer_Syntax.command "interpretation"
- "prove interpretation of locale expression in theory" Keyword.thy_goal
+ Outer_Syntax.command ("interpretation", Keyword.thy_goal)
+ "prove interpretation of locale expression in theory"
(parse_interpretation_arguments true
>> (fn (expr, equations) => Toplevel.print o
Toplevel.theory_to_proof (Expression.interpretation_cmd expr equations)));
val _ =
- Outer_Syntax.command "interpret"
+ Outer_Syntax.command ("interpret", Keyword.tag_proof Keyword.prf_goal)
"prove interpretation of locale expression in proof context"
- (Keyword.tag_proof Keyword.prf_goal)
(parse_interpretation_arguments true
>> (fn (expr, equations) => Toplevel.print o
Toplevel.proof' (Expression.interpret_cmd expr equations)));
@@ -446,24 +469,24 @@
Scan.repeat1 Parse_Spec.context_element >> pair [];
val _ =
- Outer_Syntax.command "class" "define type class" Keyword.thy_decl
+ Outer_Syntax.command ("class", Keyword.thy_decl) "define type class"
(Parse.binding -- Scan.optional (Parse.$$$ "=" |-- class_val) ([], []) -- Parse.opt_begin
>> (fn ((name, (supclasses, elems)), begin) =>
(begin ? Toplevel.print) o Toplevel.begin_local_theory begin
(Class_Declaration.class_cmd I name supclasses elems #> snd)));
val _ =
- Outer_Syntax.local_theory_to_proof "subclass" "prove a subclass relation" Keyword.thy_goal
+ Outer_Syntax.local_theory_to_proof ("subclass", Keyword.thy_goal) "prove a subclass relation"
(Parse.class >> Class_Declaration.subclass_cmd I);
val _ =
- Outer_Syntax.command "instantiation" "instantiate and prove type arity" Keyword.thy_decl
+ Outer_Syntax.command ("instantiation", Keyword.thy_decl) "instantiate and prove type arity"
(Parse.multi_arity --| Parse.begin
>> (fn arities => Toplevel.print o
Toplevel.begin_local_theory true (Class.instantiation_cmd arities)));
val _ =
- Outer_Syntax.command "instance" "prove type arity or subclass relation" Keyword.thy_goal
+ Outer_Syntax.command ("instance", Keyword.thy_goal) "prove type arity or subclass relation"
((Parse.class --
((Parse.$$$ "\\<subseteq>" || Parse.$$$ "<") |-- Parse.!!! Parse.class) >> Class.classrel_cmd ||
Parse.multi_arity >> Class.instance_arity_cmd)
@@ -475,7 +498,7 @@
(* arbitrary overloading *)
val _ =
- Outer_Syntax.command "overloading" "overloaded definitions" Keyword.thy_decl
+ Outer_Syntax.command ("overloading", Keyword.thy_decl) "overloaded definitions"
(Scan.repeat1 (Parse.name --| (Parse.$$$ "\\<equiv>" || Parse.$$$ "==") -- Parse.term --
Scan.optional (Parse.$$$ "(" |-- (Parse.$$$ "unchecked" >> K false) --| Parse.$$$ ")") true
>> Parse.triple1) --| Parse.begin
@@ -486,7 +509,8 @@
(* code generation *)
val _ =
- Outer_Syntax.command "code_datatype" "define set of code datatype constructors" Keyword.thy_decl
+ Outer_Syntax.command ("code_datatype", Keyword.thy_decl)
+ "define set of code datatype constructors"
(Scan.repeat1 Parse.term >> (Toplevel.theory o Code.add_datatype_cmd));
@@ -497,9 +521,9 @@
fun gen_theorem schematic kind =
Outer_Syntax.local_theory_to_proof'
- (if schematic then "schematic_" ^ kind else kind)
+ (if schematic then ("schematic_" ^ kind, Keyword.thy_schematic_goal)
+ else (kind, Keyword.thy_goal))
("state " ^ (if schematic then "schematic " ^ kind else kind))
- (if schematic then Keyword.thy_schematic_goal else Keyword.thy_goal)
(Scan.optional (Parse_Spec.opt_thm_name ":" --|
Scan.ahead (Parse_Spec.locale_keyword || Parse_Spec.statement_keyword)) Attrib.empty_binding --
Parse_Spec.general_statement >> (fn (a, (elems, concl)) =>
@@ -514,28 +538,25 @@
val _ = gen_theorem true Thm.corollaryK;
val _ =
- Outer_Syntax.local_theory_to_proof "notepad"
- "Isar proof state as formal notepad, without any result" Keyword.thy_decl
+ Outer_Syntax.local_theory_to_proof ("notepad", Keyword.thy_decl)
+ "Isar proof state as formal notepad, without any result"
(Parse.begin >> K Proof.begin_notepad);
val _ =
- Outer_Syntax.command "have" "state local goal"
- (Keyword.tag_proof Keyword.prf_goal)
+ Outer_Syntax.command ("have", Keyword.tag_proof Keyword.prf_goal) "state local goal"
(Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.have));
val _ =
- Outer_Syntax.command "hence" "abbreviates \"then have\""
- (Keyword.tag_proof Keyword.prf_goal)
+ Outer_Syntax.command ("hence", Keyword.tag_proof Keyword.prf_goal) "abbreviates \"then have\""
(Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.hence));
val _ =
- Outer_Syntax.command "show" "state local goal, solving current obligation"
- (Keyword.tag_proof Keyword.prf_asm_goal)
+ Outer_Syntax.command ("show", Keyword.tag_proof Keyword.prf_asm_goal)
+ "state local goal, solving current obligation"
(Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.show));
val _ =
- Outer_Syntax.command "thus" "abbreviates \"then show\""
- (Keyword.tag_proof Keyword.prf_asm_goal)
+ Outer_Syntax.command ("thus", Keyword.tag_proof Keyword.prf_asm_goal) "abbreviates \"then show\""
(Parse_Spec.statement >> ((Toplevel.print oo Toplevel.proof') o Isar_Cmd.thus));
@@ -544,56 +565,51 @@
val facts = Parse.and_list1 Parse_Spec.xthms1;
val _ =
- Outer_Syntax.command "then" "forward chaining"
- (Keyword.tag_proof Keyword.prf_chain)
+ Outer_Syntax.command ("then", Keyword.tag_proof Keyword.prf_chain) "forward chaining"
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.chain));
val _ =
- Outer_Syntax.command "from" "forward chaining from given facts"
- (Keyword.tag_proof Keyword.prf_chain)
+ Outer_Syntax.command ("from", Keyword.tag_proof Keyword.prf_chain)
+ "forward chaining from given facts"
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.from_thmss_cmd)));
val _ =
- Outer_Syntax.command "with" "forward chaining from given and current facts"
- (Keyword.tag_proof Keyword.prf_chain)
+ Outer_Syntax.command ("with", Keyword.tag_proof Keyword.prf_chain)
+ "forward chaining from given and current facts"
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.with_thmss_cmd)));
val _ =
- Outer_Syntax.command "note" "define facts"
- (Keyword.tag_proof Keyword.prf_decl)
+ Outer_Syntax.command ("note", Keyword.tag_proof Keyword.prf_decl) "define facts"
(Parse_Spec.name_facts >> (Toplevel.print oo (Toplevel.proof o Proof.note_thmss_cmd)));
val _ =
- Outer_Syntax.command "using" "augment goal facts"
- (Keyword.tag_proof Keyword.prf_decl)
+ Outer_Syntax.command ("using", Keyword.tag_proof Keyword.prf_decl) "augment goal facts"
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.using_cmd)));
val _ =
- Outer_Syntax.command "unfolding" "unfold definitions in goal and facts"
- (Keyword.tag_proof Keyword.prf_decl)
+ Outer_Syntax.command ("unfolding", Keyword.tag_proof Keyword.prf_decl)
+ "unfold definitions in goal and facts"
(facts >> (Toplevel.print oo (Toplevel.proof o Proof.unfolding_cmd)));
(* proof context *)
val _ =
- Outer_Syntax.command "fix" "fix local variables (Skolem constants)"
- (Keyword.tag_proof Keyword.prf_asm)
+ Outer_Syntax.command ("fix", Keyword.tag_proof Keyword.prf_asm)
+ "fix local variables (Skolem constants)"
(Parse.fixes >> (Toplevel.print oo (Toplevel.proof o Proof.fix_cmd)));
val _ =
- Outer_Syntax.command "assume" "assume propositions"
- (Keyword.tag_proof Keyword.prf_asm)
+ Outer_Syntax.command ("assume", Keyword.tag_proof Keyword.prf_asm) "assume propositions"
(Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.assume_cmd)));
val _ =
- Outer_Syntax.command "presume" "assume propositions, to be established later"
- (Keyword.tag_proof Keyword.prf_asm)
+ Outer_Syntax.command ("presume", Keyword.tag_proof Keyword.prf_asm)
+ "assume propositions, to be established later"
(Parse_Spec.statement >> (Toplevel.print oo (Toplevel.proof o Proof.presume_cmd)));
val _ =
- Outer_Syntax.command "def" "local definition"
- (Keyword.tag_proof Keyword.prf_asm)
+ Outer_Syntax.command ("def", Keyword.tag_proof Keyword.prf_asm) "local definition"
(Parse.and_list1
(Parse_Spec.opt_thm_name ":" --
((Parse.binding -- Parse.opt_mixfix) --
@@ -601,25 +617,24 @@
>> (Toplevel.print oo (Toplevel.proof o Proof.def_cmd)));
val _ =
- Outer_Syntax.command "obtain" "generalized existence"
- (Keyword.tag_proof Keyword.prf_asm_goal)
+ Outer_Syntax.command ("obtain", Keyword.tag_proof Keyword.prf_asm_goal)
+ "generalized elimination"
(Parse.parname -- Scan.optional (Parse.fixes --| Parse.where_) [] -- Parse_Spec.statement
>> (fn ((x, y), z) => Toplevel.print o Toplevel.proof' (Obtain.obtain_cmd x y z)));
val _ =
- Outer_Syntax.command "guess" "wild guessing (unstructured)"
- (Keyword.tag_proof Keyword.prf_asm_goal)
+ Outer_Syntax.command ("guess", Keyword.tag_proof Keyword.prf_asm_goal)
+ "wild guessing (unstructured)"
(Scan.optional Parse.fixes [] >> (Toplevel.print oo (Toplevel.proof' o Obtain.guess_cmd)));
val _ =
- Outer_Syntax.command "let" "bind text variables"
- (Keyword.tag_proof Keyword.prf_decl)
+ Outer_Syntax.command ("let", Keyword.tag_proof Keyword.prf_decl) "bind text variables"
(Parse.and_list1 (Parse.and_list1 Parse.term -- (Parse.$$$ "=" |-- Parse.term))
>> (Toplevel.print oo (Toplevel.proof o Proof.let_bind_cmd)));
val _ =
- Outer_Syntax.command "write" "add concrete syntax for constants / fixed variables"
- (Keyword.tag_proof Keyword.prf_decl)
+ Outer_Syntax.command ("write", Keyword.tag_proof Keyword.prf_decl)
+ "add concrete syntax for constants / fixed variables"
(opt_mode -- Parse.and_list1 (Parse.const -- Parse_Spec.locale_mixfix)
>> (fn (mode, args) => Toplevel.print o Toplevel.proof (Proof.write_cmd mode args)));
@@ -629,92 +644,81 @@
Parse.xname >> rpair []) -- Parse_Spec.opt_attribs >> Parse.triple1;
val _ =
- Outer_Syntax.command "case" "invoke local context"
- (Keyword.tag_proof Keyword.prf_asm)
+ Outer_Syntax.command ("case", Keyword.tag_proof Keyword.prf_asm) "invoke local context"
(case_spec >> (Toplevel.print oo (Toplevel.proof o Proof.invoke_case_cmd)));
(* proof structure *)
val _ =
- Outer_Syntax.command "{" "begin explicit proof block"
- (Keyword.tag_proof Keyword.prf_open)
+ Outer_Syntax.command ("{", Keyword.tag_proof Keyword.prf_open) "begin explicit proof block"
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.begin_block));
val _ =
- Outer_Syntax.command "}" "end explicit proof block"
- (Keyword.tag_proof Keyword.prf_close)
+ Outer_Syntax.command ("}", Keyword.tag_proof Keyword.prf_close) "end explicit proof block"
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.end_block));
val _ =
- Outer_Syntax.command "next" "enter next proof block"
- (Keyword.tag_proof Keyword.prf_block)
+ Outer_Syntax.command ("next", Keyword.tag_proof Keyword.prf_block) "enter next proof block"
(Scan.succeed (Toplevel.print o Toplevel.proof Proof.next_block));
(* end proof *)
val _ =
- Outer_Syntax.command "qed" "conclude (sub-)proof"
- (Keyword.tag_proof Keyword.qed_block)
+ Outer_Syntax.command ("qed", Keyword.tag_proof Keyword.qed_block) "conclude (sub-)proof"
(Scan.option Method.parse >> Isar_Cmd.qed);
val _ =
- Outer_Syntax.command "by" "terminal backward proof"
- (Keyword.tag_proof Keyword.qed)
+ Outer_Syntax.command ("by", Keyword.tag_proof Keyword.qed) "terminal backward proof"
(Method.parse -- Scan.option Method.parse >> Isar_Cmd.terminal_proof);
val _ =
- Outer_Syntax.command ".." "default proof"
- (Keyword.tag_proof Keyword.qed)
+ Outer_Syntax.command ("..", Keyword.tag_proof Keyword.qed) "default proof"
(Scan.succeed Isar_Cmd.default_proof);
val _ =
- Outer_Syntax.command "." "immediate proof"
- (Keyword.tag_proof Keyword.qed)
+ Outer_Syntax.command (".", Keyword.tag_proof Keyword.qed) "immediate proof"
(Scan.succeed Isar_Cmd.immediate_proof);
val _ =
- Outer_Syntax.command "done" "done proof"
- (Keyword.tag_proof Keyword.qed)
+ Outer_Syntax.command ("done", Keyword.tag_proof Keyword.qed) "done proof"
(Scan.succeed Isar_Cmd.done_proof);
val _ =
- Outer_Syntax.command "sorry" "skip proof (quick-and-dirty mode only!)"
- (Keyword.tag_proof Keyword.qed)
+ Outer_Syntax.command ("sorry", Keyword.tag_proof Keyword.qed)
+ "skip proof (quick-and-dirty mode only!)"
(Scan.succeed Isar_Cmd.skip_proof);
val _ =
- Outer_Syntax.command "oops" "forget proof"
- (Keyword.tag_proof Keyword.qed_global)
+ Outer_Syntax.command ("oops", Keyword.tag_proof Keyword.qed_global) "forget proof"
(Scan.succeed Toplevel.forget_proof);
(* proof steps *)
val _ =
- Outer_Syntax.command "defer" "shuffle internal proof state"
- (Keyword.tag_proof Keyword.prf_script)
+ Outer_Syntax.command ("defer", Keyword.tag_proof Keyword.prf_script)
+ "shuffle internal proof state"
(Scan.option Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.defer)));
val _ =
- Outer_Syntax.command "prefer" "shuffle internal proof state"
- (Keyword.tag_proof Keyword.prf_script)
+ Outer_Syntax.command ("prefer", Keyword.tag_proof Keyword.prf_script)
+ "shuffle internal proof state"
(Parse.nat >> (Toplevel.print oo (Toplevel.proofs o Proof.prefer)));
val _ =
- Outer_Syntax.command "apply" "initial refinement step (unstructured)"
- (Keyword.tag_proof Keyword.prf_script)
+ Outer_Syntax.command ("apply", Keyword.tag_proof Keyword.prf_script)
+ "initial refinement step (unstructured)"
(Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply)));
val _ =
- Outer_Syntax.command "apply_end" "terminal refinement (unstructured)"
- (Keyword.tag_proof Keyword.prf_script)
+ Outer_Syntax.command ("apply_end", Keyword.tag_proof Keyword.prf_script)
+ "terminal refinement (unstructured)"
(Method.parse >> (Toplevel.print oo (Toplevel.proofs o Proof.apply_end)));
val _ =
- Outer_Syntax.command "proof" "backward proof"
- (Keyword.tag_proof Keyword.prf_block)
+ Outer_Syntax.command ("proof", Keyword.tag_proof Keyword.prf_block) "backward proof"
(Scan.option Method.parse >> (fn m => Toplevel.print o
Toplevel.actual_proof (Proof_Node.applys (Proof.proof m)) o
Toplevel.skip_proof (fn i => i + 1)));
@@ -726,31 +730,31 @@
Scan.option (Parse.$$$ "(" |-- Parse.!!! ((Parse_Spec.xthms1 --| Parse.$$$ ")")));
val _ =
- Outer_Syntax.command "also" "combine calculation and current facts"
- (Keyword.tag_proof Keyword.prf_decl)
+ Outer_Syntax.command ("also", Keyword.tag_proof Keyword.prf_decl)
+ "combine calculation and current facts"
(calc_args >> (Toplevel.proofs' o Calculation.also_cmd));
val _ =
- Outer_Syntax.command "finally" "combine calculation and current facts, exhibit result"
- (Keyword.tag_proof Keyword.prf_chain)
+ Outer_Syntax.command ("finally", Keyword.tag_proof Keyword.prf_chain)
+ "combine calculation and current facts, exhibit result"
(calc_args >> (Toplevel.proofs' o Calculation.finally_cmd));
val _ =
- Outer_Syntax.command "moreover" "augment calculation by current facts"
- (Keyword.tag_proof Keyword.prf_decl)
+ Outer_Syntax.command ("moreover", Keyword.tag_proof Keyword.prf_decl)
+ "augment calculation by current facts"
(Scan.succeed (Toplevel.proof' Calculation.moreover));
val _ =
- Outer_Syntax.command "ultimately" "augment calculation by current facts, exhibit result"
- (Keyword.tag_proof Keyword.prf_chain)
+ Outer_Syntax.command ("ultimately", Keyword.tag_proof Keyword.prf_chain)
+ "augment calculation by current facts, exhibit result"
(Scan.succeed (Toplevel.proof' Calculation.ultimately));
(* proof navigation *)
val _ =
- Outer_Syntax.command "back" "backtracking of proof command"
- (Keyword.tag_proof Keyword.prf_script)
+ Outer_Syntax.command ("back", Keyword.tag_proof Keyword.prf_script)
+ "backtracking of proof command"
(Scan.succeed (Toplevel.print o Toplevel.actual_proof Proof_Node.back o Toplevel.skip_proof I));
@@ -762,7 +766,7 @@
(Position.of_properties (Position.default_properties pos props), str));
val _ =
- Outer_Syntax.improper_command "Isabelle.command" "nested Isabelle command" Keyword.control
+ Outer_Syntax.improper_command ("Isabelle.command", Keyword.control) "nested Isabelle command"
(props_text :|-- (fn (pos, str) =>
(case Outer_Syntax.parse pos str of
[tr] => Scan.succeed (K tr)
@@ -779,152 +783,161 @@
val opt_bang = Scan.optional (Parse.$$$ "!" >> K true) false;
val _ =
- Outer_Syntax.improper_command "pretty_setmargin" "change default margin for pretty printing"
- Keyword.diag (Parse.nat >>
+ Outer_Syntax.improper_command ("pretty_setmargin", Keyword.diag)
+ "change default margin for pretty printing"
+ (Parse.nat >>
(fn n => Toplevel.no_timing o Toplevel.imperative (fn () => Pretty.margin_default := n)));
val _ =
- Outer_Syntax.improper_command "help" "print outer syntax commands" Keyword.diag
+ Outer_Syntax.improper_command ("help", Keyword.diag) "print outer syntax commands"
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative Outer_Syntax.print_outer_syntax));
val _ =
- Outer_Syntax.improper_command "print_commands" "print outer syntax commands" Keyword.diag
+ Outer_Syntax.improper_command ("print_commands", Keyword.diag) "print outer syntax commands"
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative Outer_Syntax.print_outer_syntax));
val _ =
- Outer_Syntax.improper_command "print_configs" "print configuration options" Keyword.diag
+ Outer_Syntax.improper_command ("print_configs", Keyword.diag) "print configuration options"
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_configs));
val _ =
- Outer_Syntax.improper_command "print_context" "print theory context name" Keyword.diag
+ Outer_Syntax.improper_command ("print_context", Keyword.diag) "print theory context name"
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_context));
val _ =
- Outer_Syntax.improper_command "print_theory" "print logical theory contents (verbose!)"
- Keyword.diag (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theory));
+ Outer_Syntax.improper_command ("print_theory", Keyword.diag)
+ "print logical theory contents (verbose!)"
+ (opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theory));
val _ =
- Outer_Syntax.improper_command "print_syntax" "print inner syntax of context (verbose!)"
- Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_syntax));
+ Outer_Syntax.improper_command ("print_syntax", Keyword.diag)
+ "print inner syntax of context (verbose!)"
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_syntax));
val _ =
- Outer_Syntax.improper_command "print_abbrevs" "print constant abbreviation of context"
- Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_abbrevs));
+ Outer_Syntax.improper_command ("print_abbrevs", Keyword.diag)
+ "print constant abbreviation of context"
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_abbrevs));
val _ =
- Outer_Syntax.improper_command "print_theorems"
- "print theorems of local theory or proof context" Keyword.diag
+ Outer_Syntax.improper_command ("print_theorems", Keyword.diag)
+ "print theorems of local theory or proof context"
(opt_bang >> (Toplevel.no_timing oo Isar_Cmd.print_theorems));
val _ =
- Outer_Syntax.improper_command "print_locales" "print locales of this theory" Keyword.diag
+ Outer_Syntax.improper_command ("print_locales", Keyword.diag)
+ "print locales of this theory"
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_locales));
val _ =
- Outer_Syntax.improper_command "print_classes" "print classes of this theory" Keyword.diag
+ Outer_Syntax.improper_command ("print_classes", Keyword.diag) "print classes of this theory"
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_theory o
Toplevel.keep (Class.print_classes o Toplevel.context_of)));
val _ =
- Outer_Syntax.improper_command "print_locale" "print locale of this theory" Keyword.diag
+ Outer_Syntax.improper_command ("print_locale", Keyword.diag) "print locale of this theory"
(opt_bang -- Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_locale));
val _ =
- Outer_Syntax.improper_command "print_interps"
- "print interpretations of locale for this theory or proof context" Keyword.diag
+ Outer_Syntax.improper_command ("print_interps", Keyword.diag)
+ "print interpretations of locale for this theory or proof context"
(Parse.position Parse.xname >> (Toplevel.no_timing oo Isar_Cmd.print_registrations));
val _ =
- Outer_Syntax.improper_command "print_dependencies"
- "print dependencies of locale expression" Keyword.diag
+ Outer_Syntax.improper_command ("print_dependencies", Keyword.diag)
+ "print dependencies of locale expression"
(opt_bang -- Parse_Spec.locale_expression true >>
(Toplevel.no_timing oo Isar_Cmd.print_dependencies));
val _ =
- Outer_Syntax.improper_command "print_attributes" "print attributes of this theory" Keyword.diag
+ Outer_Syntax.improper_command ("print_attributes", Keyword.diag)
+ "print attributes of this theory"
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_attributes));
val _ =
- Outer_Syntax.improper_command "print_simpset" "print context of Simplifier" Keyword.diag
+ Outer_Syntax.improper_command ("print_simpset", Keyword.diag)
+ "print context of Simplifier"
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_simpset));
val _ =
- Outer_Syntax.improper_command "print_rules" "print intro/elim rules" Keyword.diag
+ Outer_Syntax.improper_command ("print_rules", Keyword.diag) "print intro/elim rules"
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_rules));
val _ =
- Outer_Syntax.improper_command "print_trans_rules" "print transitivity rules" Keyword.diag
+ Outer_Syntax.improper_command ("print_trans_rules", Keyword.diag) "print transitivity rules"
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_trans_rules));
val _ =
- Outer_Syntax.improper_command "print_methods" "print methods of this theory" Keyword.diag
+ Outer_Syntax.improper_command ("print_methods", Keyword.diag) "print methods of this theory"
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_methods));
val _ =
- Outer_Syntax.improper_command "print_antiquotations" "print antiquotations (global)" Keyword.diag
+ Outer_Syntax.improper_command ("print_antiquotations", Keyword.diag)
+ "print antiquotations (global)"
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_antiquotations));
val _ =
- Outer_Syntax.improper_command "thy_deps" "visualize theory dependencies"
- Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.thy_deps));
+ Outer_Syntax.improper_command ("thy_deps", Keyword.diag) "visualize theory dependencies"
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.thy_deps));
val _ =
- Outer_Syntax.improper_command "class_deps" "visualize class dependencies"
- Keyword.diag (Scan.succeed (Toplevel.no_timing o Isar_Cmd.class_deps));
+ Outer_Syntax.improper_command ("class_deps", Keyword.diag) "visualize class dependencies"
+ (Scan.succeed (Toplevel.no_timing o Isar_Cmd.class_deps));
val _ =
- Outer_Syntax.improper_command "thm_deps" "visualize theorem dependencies"
- Keyword.diag (Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.thm_deps));
+ Outer_Syntax.improper_command ("thm_deps", Keyword.diag) "visualize theorem dependencies"
+ (Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.thm_deps));
val _ =
- Outer_Syntax.improper_command "print_binds" "print term bindings of proof context" Keyword.diag
+ Outer_Syntax.improper_command ("print_binds", Keyword.diag) "print term bindings of proof context"
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_binds));
val _ =
- Outer_Syntax.improper_command "print_facts" "print facts of proof context" Keyword.diag
+ Outer_Syntax.improper_command ("print_facts", Keyword.diag) "print facts of proof context"
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_facts));
val _ =
- Outer_Syntax.improper_command "print_cases" "print cases of proof context" Keyword.diag
+ Outer_Syntax.improper_command ("print_cases", Keyword.diag) "print cases of proof context"
(Scan.succeed (Toplevel.no_timing o Isar_Cmd.print_cases));
val _ =
- Outer_Syntax.improper_command "print_statement" "print theorems as long statements" Keyword.diag
+ Outer_Syntax.improper_command ("print_statement", Keyword.diag)
+ "print theorems as long statements"
(opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_stmts));
val _ =
- Outer_Syntax.improper_command "thm" "print theorems" Keyword.diag
+ Outer_Syntax.improper_command ("thm", Keyword.diag) "print theorems"
(opt_modes -- Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_thms));
val _ =
- Outer_Syntax.improper_command "prf" "print proof terms of theorems" Keyword.diag
+ Outer_Syntax.improper_command ("prf", Keyword.diag) "print proof terms of theorems"
(opt_modes -- Scan.option Parse_Spec.xthms1
>> (Toplevel.no_timing oo Isar_Cmd.print_prfs false));
val _ =
- Outer_Syntax.improper_command "full_prf" "print full proof terms of theorems" Keyword.diag
+ Outer_Syntax.improper_command ("full_prf", Keyword.diag) "print full proof terms of theorems"
(opt_modes -- Scan.option Parse_Spec.xthms1 >> (Toplevel.no_timing oo Isar_Cmd.print_prfs true));
val _ =
- Outer_Syntax.improper_command "prop" "read and print proposition" Keyword.diag
+ Outer_Syntax.improper_command ("prop", Keyword.diag) "read and print proposition"
(opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_prop));
val _ =
- Outer_Syntax.improper_command "term" "read and print term" Keyword.diag
+ Outer_Syntax.improper_command ("term", Keyword.diag) "read and print term"
(opt_modes -- Parse.term >> (Toplevel.no_timing oo Isar_Cmd.print_term));
val _ =
- Outer_Syntax.improper_command "typ" "read and print type" Keyword.diag
+ Outer_Syntax.improper_command ("typ", Keyword.diag) "read and print type"
(opt_modes -- Parse.typ >> (Toplevel.no_timing oo Isar_Cmd.print_type));
val _ =
- Outer_Syntax.improper_command "print_codesetup" "print code generator setup" Keyword.diag
+ Outer_Syntax.improper_command ("print_codesetup", Keyword.diag) "print code generator setup"
(Scan.succeed
(Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
(Code.print_codesetup o Toplevel.theory_of)));
val _ =
- Outer_Syntax.improper_command "unused_thms" "find unused theorems" Keyword.diag
+ Outer_Syntax.improper_command ("unused_thms", Keyword.diag) "find unused theorems"
(Scan.option ((Scan.repeat1 (Scan.unless Parse.minus Parse.name) --| Parse.minus) --
Scan.option (Scan.repeat1 (Scan.unless Parse.minus Parse.name))) >>
(Toplevel.no_timing oo Isar_Cmd.unused_thms));
@@ -934,39 +947,42 @@
(** system commands (for interactive mode only) **)
val _ =
- Outer_Syntax.improper_command "cd" "change current working directory" Keyword.control
+ Outer_Syntax.improper_command ("cd", Keyword.control) "change current working directory"
(Parse.path >> (fn path => Toplevel.no_timing o Toplevel.imperative (fn () => File.cd path)));
val _ =
- Outer_Syntax.improper_command "pwd" "print current working directory" Keyword.diag
+ Outer_Syntax.improper_command ("pwd", Keyword.diag) "print current working directory"
(Scan.succeed (Toplevel.no_timing o
Toplevel.imperative (fn () => writeln (Path.print (File.pwd ())))));
val _ =
- Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.control
+ Outer_Syntax.improper_command ("use_thy", Keyword.control) "use theory file"
(Parse.name >> (fn name =>
Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.use_thy name)));
val _ =
- Outer_Syntax.improper_command "remove_thy" "remove theory from loader database" Keyword.control
+ Outer_Syntax.improper_command ("remove_thy", Keyword.control) "remove theory from loader database"
(Parse.name >> (fn name =>
Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
val _ =
- Outer_Syntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
- Keyword.control (Parse.name >> (fn name =>
+ Outer_Syntax.improper_command ("kill_thy", Keyword.control)
+ "kill theory -- try to remove from loader database"
+ (Parse.name >> (fn name =>
Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
val _ =
- Outer_Syntax.improper_command "display_drafts" "display raw source files with symbols"
- Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.display_drafts));
+ Outer_Syntax.improper_command ("display_drafts", Keyword.diag)
+ "display raw source files with symbols"
+ (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.display_drafts));
val _ =
- Outer_Syntax.improper_command "print_drafts" "print raw source files with symbols"
- Keyword.diag (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));
+ Outer_Syntax.improper_command ("print_drafts", Keyword.diag)
+ "print raw source files with symbols"
+ (Scan.repeat1 Parse.path >> (Toplevel.no_timing oo Isar_Cmd.print_drafts));
val _ = (* FIXME tty only *)
- Outer_Syntax.improper_command "pr" "print current proof state (if present)" Keyword.diag
+ Outer_Syntax.improper_command ("pr", Keyword.diag) "print current proof state (if present)"
(opt_modes -- Scan.option Parse.nat >> (fn (modes, limit) =>
Toplevel.no_timing o Toplevel.keep (fn state =>
(case limit of NONE => () | SOME n => Goal_Display.goals_limit_default := n;
@@ -974,23 +990,26 @@
Print_Mode.with_modes modes (Toplevel.print_state true) state))));
val _ =
- Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.control
+ Outer_Syntax.improper_command ("disable_pr", Keyword.control)
+ "disable printing of toplevel state"
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := true)));
val _ =
- Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.control
+ Outer_Syntax.improper_command ("enable_pr", Keyword.control)
+ "enable printing of toplevel state"
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Toplevel.quiet := false)));
val _ =
- Outer_Syntax.improper_command "commit" "commit current session to ML database" Keyword.control
+ Outer_Syntax.improper_command ("commit", Keyword.control)
+ "commit current session to ML database"
(Parse.opt_unit >> K (Toplevel.no_timing o Toplevel.imperative Secure.commit));
val _ =
- Outer_Syntax.improper_command "quit" "quit Isabelle" Keyword.control
+ Outer_Syntax.improper_command ("quit", Keyword.control) "quit Isabelle"
(Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative quit)));
val _ =
- Outer_Syntax.improper_command "exit" "exit Isar loop" Keyword.control
+ Outer_Syntax.improper_command ("exit", Keyword.control) "exit Isar loop"
(Scan.succeed
(Toplevel.no_timing o Toplevel.keep (fn state =>
(Context.set_thread_data (try Toplevel.generic_theory_of state);
--- a/src/Pure/Isar/keyword.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/Isar/keyword.ML Fri Mar 16 18:21:22 2012 +0100
@@ -37,7 +37,9 @@
val tag_theory: T -> T
val tag_proof: T -> T
val tag_ml: T -> T
- val make: string * string list -> T
+ type spec = string * string list
+ val spec: spec -> T
+ val command_spec: string * spec -> string * T
val get_lexicons: unit -> Scan.lexicon * Scan.lexicon
val is_keyword: string -> bool
val command_keyword: string -> T option
@@ -65,7 +67,7 @@
(** keyword classification **)
-datatype T = Keyword of string * string list;
+datatype T = Keyword of string * string list; (*kind, tags (in canonical reverse order)*)
fun kind s = Keyword (s, []);
fun kind_of (Keyword (s, _)) = s;
@@ -141,11 +143,15 @@
("prf_asm_goal", prf_asm_goal),
("prf_script", prf_script)];
-fun make (kind, tags) =
+type spec = string * string list;
+
+fun spec (kind, tags) =
(case Symtab.lookup name_table kind of
SOME k => k |> fold tag tags
| NONE => error ("Unknown outer syntax keyword kind " ^ quote kind));
+fun command_spec (name, s) = (name, spec s);
+
(** global keyword tables **)
--- a/src/Pure/Isar/outer_syntax.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/Isar/outer_syntax.ML Fri Mar 16 18:21:22 2012 +0100
@@ -12,21 +12,20 @@
type outer_syntax
val is_markup: outer_syntax -> Thy_Output.markup -> string -> bool
val get_syntax: unit -> (Scan.lexicon * Scan.lexicon) * outer_syntax
- val command: string -> string -> Keyword.T ->
- (Toplevel.transition -> Toplevel.transition) parser -> unit
- val markup_command: Thy_Output.markup -> string -> string -> Keyword.T ->
+ type command_spec = string * Keyword.T
+ val command: command_spec -> string ->
(Toplevel.transition -> Toplevel.transition) parser -> unit
- val improper_command: string -> string -> Keyword.T ->
+ val markup_command: Thy_Output.markup -> command_spec -> string ->
(Toplevel.transition -> Toplevel.transition) parser -> unit
- val internal_command: string ->
+ val improper_command: command_spec -> string ->
(Toplevel.transition -> Toplevel.transition) parser -> unit
- val local_theory': string -> string -> Keyword.T ->
+ val local_theory': command_spec -> string ->
(bool -> local_theory -> local_theory) parser -> unit
- val local_theory: string -> string -> Keyword.T ->
+ val local_theory: command_spec -> string ->
(local_theory -> local_theory) parser -> unit
- val local_theory_to_proof': string -> string -> Keyword.T ->
+ val local_theory_to_proof': command_spec -> string ->
(bool -> local_theory -> Proof.state) parser -> unit
- val local_theory_to_proof: string -> string -> Keyword.T ->
+ val local_theory_to_proof: command_spec -> string ->
(local_theory -> Proof.state) parser -> unit
val print_outer_syntax: unit -> unit
val scan: Position.T -> string -> Token.T list
@@ -117,21 +116,24 @@
(** global outer syntax **)
+type command_spec = string * Keyword.T;
+
local
(*synchronized wrt. Keywords*)
val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
-fun add_command name kind cmd = CRITICAL (fn () =>
+fun add_command (name, kind) cmd = CRITICAL (fn () =>
let
val thy = ML_Context.the_global_context ();
val _ =
(case try (Thy_Header.the_keyword thy) name of
- SOME k =>
- if k = SOME kind then ()
+ SOME spec =>
+ if Option.map Keyword.spec spec = SOME kind then ()
else error ("Inconsistent outer syntax keyword declaration " ^ quote name)
| NONE =>
- if Context.theory_name thy = Context.PureN then Keyword.define (name, SOME kind)
+ if Context.theory_name thy = Context.PureN
+ then Keyword.define (name, SOME kind)
else error ("Undeclared outer syntax command " ^ quote name));
in
Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
@@ -146,25 +148,22 @@
fun lookup_commands_dynamic () = lookup_commands (! global_outer_syntax);
-fun command name comment kind parse =
- add_command name kind (make_command comment NONE false parse);
-
-fun markup_command markup name comment kind parse =
- add_command name kind (make_command comment (SOME markup) false parse);
+fun command command_spec comment parse =
+ add_command command_spec (make_command comment NONE false parse);
-fun improper_command name comment kind parse =
- add_command name kind (make_command comment NONE true parse);
+fun markup_command markup command_spec comment parse =
+ add_command command_spec (make_command comment (SOME markup) false parse);
-fun internal_command name parse =
- command name "(internal)" Keyword.control (parse >> (fn tr => Toplevel.no_timing o tr));
+fun improper_command command_spec comment parse =
+ add_command command_spec (make_command comment NONE true parse);
end;
(* local_theory commands *)
-fun local_theory_command do_print trans name comment kind parse =
- command name comment kind (Parse.opt_target -- parse
+fun local_theory_command do_print trans command_spec comment parse =
+ command command_spec comment (Parse.opt_target -- parse
>> (fn (loc, f) => (if do_print then Toplevel.print else I) o trans loc f));
val local_theory' = local_theory_command false Toplevel.local_theory';
--- a/src/Pure/ML/ml_antiquote.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/ML/ml_antiquote.ML Fri Mar 16 18:21:22 2012 +0100
@@ -66,8 +66,7 @@
inline (Binding.name "make_string") (Scan.succeed ml_make_string) #>
value (Binding.name "binding")
- (Scan.lift (Parse.position Args.name)
- >> (fn name => ML_Syntax.atomic (ML_Syntax.make_binding name))) #>
+ (Scan.lift (Parse.position Args.name) >> ML_Syntax.make_binding) #>
value (Binding.name "theory")
(Scan.lift Args.name >> (fn name =>
@@ -97,10 +96,10 @@
"Thm.ctyp_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_typ T))) #>
value (Binding.name "cterm") (Args.term >> (fn t =>
- "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
+ "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
value (Binding.name "cprop") (Args.prop >> (fn t =>
- "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
+ "Thm.cterm_of (ML_Context.the_global_context ()) " ^ ML_Syntax.atomic (ML_Syntax.print_term t))) #>
value (Binding.name "cpat")
(Args.context --
@@ -185,13 +184,24 @@
(* outer syntax *)
+fun with_keyword f =
+ Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
+ (f (name, Thy_Header.the_keyword thy name)
+ handle ERROR msg => error (msg ^ Position.str_of pos)));
+
val _ = Context.>> (Context.map_theory
- (value (Binding.name "keyword")
- (Args.theory -- Scan.lift (Parse.position Parse.string) >> (fn (thy, (name, pos)) =>
- (if is_none (Thy_Header.the_keyword thy name) then
- ML_Syntax.atomic ("Parse.$$$ " ^ ML_Syntax.print_string name)
- else error ("Unknown minor keyword " ^ quote name))
- handle ERROR msg => error (msg ^ Position.str_of pos)))));
+ (value (Binding.name "keyword")
+ (with_keyword
+ (fn (name, NONE) => "Parse.$$$ " ^ ML_Syntax.print_string name
+ | (name, SOME _) => error ("Expected minor keyword " ^ quote name))) #>
+ value (Binding.name "command_spec")
+ (with_keyword
+ (fn (name, SOME kind) =>
+ "Keyword.command_spec " ^ ML_Syntax.atomic
+ (ML_Syntax.print_pair ML_Syntax.print_string
+ (ML_Syntax.print_pair ML_Syntax.print_string
+ (ML_Syntax.print_list ML_Syntax.print_string)) (name, kind))
+ | (name, NONE) => error ("Expected command keyword " ^ quote name)))));
end;
--- a/src/Pure/Proof/extraction.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/Proof/extraction.ML Fri Mar 16 18:21:22 2012 +0100
@@ -820,25 +820,24 @@
val parse_vars = Scan.optional (Parse.$$$ "(" |-- Parse.list1 Parse.name --| Parse.$$$ ")") [];
val _ =
- Outer_Syntax.command "realizers"
- "specify realizers for primitive axioms / theorems, together with correctness proof"
- Keyword.thy_decl
+ Outer_Syntax.command ("realizers", Keyword.thy_decl)
+ "specify realizers for primitive axioms / theorems, together with correctness proof"
(Scan.repeat1 (Parse.xname -- parse_vars --| Parse.$$$ ":" -- Parse.string -- Parse.string) >>
(fn xs => Toplevel.theory (fn thy => add_realizers
(map (fn (((a, vs), s1), s2) => (Global_Theory.get_thm thy a, (vs, s1, s2))) xs) thy)));
val _ =
- Outer_Syntax.command "realizability"
- "add equations characterizing realizability" Keyword.thy_decl
- (Scan.repeat1 Parse.string >> (Toplevel.theory o add_realizes_eqns));
+ Outer_Syntax.command ("realizability", Keyword.thy_decl)
+ "add equations characterizing realizability"
+ (Scan.repeat1 Parse.string >> (Toplevel.theory o add_realizes_eqns));
val _ =
- Outer_Syntax.command "extract_type"
- "add equations characterizing type of extracted program" Keyword.thy_decl
- (Scan.repeat1 Parse.string >> (Toplevel.theory o add_typeof_eqns));
+ Outer_Syntax.command ("extract_type", Keyword.thy_decl)
+ "add equations characterizing type of extracted program"
+ (Scan.repeat1 Parse.string >> (Toplevel.theory o add_typeof_eqns));
val _ =
- Outer_Syntax.command "extract" "extract terms from proofs" Keyword.thy_decl
+ Outer_Syntax.command ("extract", Keyword.thy_decl) "extract terms from proofs"
(Scan.repeat1 (Parse.xname -- parse_vars) >> (fn xs => Toplevel.theory (fn thy =>
extract (map (apfst (Global_Theory.get_thm thy)) xs) thy)));
--- a/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/ProofGeneral/proof_general_emacs.ML Fri Mar 16 18:21:22 2012 +0100
@@ -189,31 +189,31 @@
(* additional outer syntax for Isar *)
val _ =
- Outer_Syntax.improper_command "ProofGeneral.pr" "print state (internal)" Keyword.diag
+ Outer_Syntax.improper_command ("ProofGeneral.pr", Keyword.diag) "print state (internal)"
(Scan.succeed (Toplevel.no_timing o Toplevel.keep (fn state =>
if Toplevel.is_toplevel state orelse Toplevel.is_theory state then tell_clear_goals ()
else (Toplevel.quiet := false; Toplevel.print_state true state))));
val _ = (*undo without output -- historical*)
- Outer_Syntax.improper_command "ProofGeneral.undo" "(internal)" Keyword.control
+ Outer_Syntax.improper_command ("ProofGeneral.undo", Keyword.control) "(internal)"
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative (fn () => Isar.undo 1)));
val _ =
- Outer_Syntax.improper_command "ProofGeneral.restart" "(internal)" Keyword.control
+ Outer_Syntax.improper_command ("ProofGeneral.restart", Keyword.control) "(internal)"
(Parse.opt_unit >> (Toplevel.no_timing oo K (Toplevel.imperative restart)));
val _ =
- Outer_Syntax.improper_command "ProofGeneral.kill_proof" "(internal)" Keyword.control
+ Outer_Syntax.improper_command ("ProofGeneral.kill_proof", Keyword.control) "(internal)"
(Scan.succeed (Toplevel.no_timing o
Toplevel.imperative (fn () => (Isar.kill_proof (); tell_clear_goals ()))));
val _ =
- Outer_Syntax.improper_command "ProofGeneral.inform_file_processed" "(internal)" Keyword.control
+ Outer_Syntax.improper_command ("ProofGeneral.inform_file_processed", Keyword.control) "(internal)"
(Parse.name >> (fn file =>
Toplevel.no_timing o Toplevel.imperative (fn () => inform_file_processed file)));
val _ =
- Outer_Syntax.improper_command "ProofGeneral.inform_file_retracted" "(internal)" Keyword.control
+ Outer_Syntax.improper_command ("ProofGeneral.inform_file_retracted", Keyword.control) "(internal)"
(Parse.name >> (Toplevel.no_timing oo
(fn file => Toplevel.imperative (fn () => inform_file_retracted file))));
--- a/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Fri Mar 16 18:21:22 2012 +0100
@@ -1032,7 +1032,7 @@
(* Extra command for embedding prover-control inside document (obscure/debug usage). *)
val _ =
- Outer_Syntax.improper_command "ProofGeneral.process_pgip" "(internal)" Keyword.control
+ Outer_Syntax.improper_command ("ProofGeneral.process_pgip", Keyword.control) "(internal)"
(Parse.text >> (Toplevel.no_timing oo
(fn txt => Toplevel.imperative (fn () =>
if print_mode_active proof_general_emacsN
--- a/src/Pure/System/isar.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/System/isar.ML Fri Mar 16 18:21:22 2012 +0100
@@ -164,35 +164,36 @@
(* global history *)
val _ =
- Outer_Syntax.improper_command "init_toplevel" "init toplevel point-of-interest" Keyword.control
+ Outer_Syntax.improper_command ("init_toplevel", Keyword.control) "init toplevel point-of-interest"
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative init));
val _ =
- Outer_Syntax.improper_command "linear_undo" "undo commands" Keyword.control
+ Outer_Syntax.improper_command ("linear_undo", Keyword.control) "undo commands"
(Scan.optional Parse.nat 1 >>
(fn n => Toplevel.no_timing o Toplevel.imperative (fn () => linear_undo n)));
val _ =
- Outer_Syntax.improper_command "undo" "undo commands (skipping closed proofs)" Keyword.control
+ Outer_Syntax.improper_command ("undo", Keyword.control) "undo commands (skipping closed proofs)"
(Scan.optional Parse.nat 1 >>
(fn n => Toplevel.no_timing o Toplevel.imperative (fn () => undo n)));
val _ =
- Outer_Syntax.improper_command "undos_proof" "undo commands (skipping closed proofs)"
- Keyword.control
+ Outer_Syntax.improper_command ("undos_proof", Keyword.control)
+ "undo commands (skipping closed proofs)"
(Scan.optional Parse.nat 1 >> (fn n => Toplevel.no_timing o
Toplevel.keep (fn state =>
if Toplevel.is_proof state then (undo n; print ()) else raise Toplevel.UNDEF)));
val _ =
- Outer_Syntax.improper_command "cannot_undo" "partial undo -- Proof General legacy"
- Keyword.control
+ Outer_Syntax.improper_command ("cannot_undo", Keyword.control)
+ "partial undo -- Proof General legacy"
(Parse.name >>
(fn "end" => Toplevel.no_timing o Toplevel.imperative (fn () => undo 1)
| txt => Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt))));
val _ =
- Outer_Syntax.improper_command "kill" "kill partial proof or theory development" Keyword.control
+ Outer_Syntax.improper_command ("kill", Keyword.control)
+ "kill partial proof or theory development"
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative kill));
end;
--- a/src/Pure/System/session.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/System/session.ML Fri Mar 16 18:21:22 2012 +0100
@@ -48,7 +48,7 @@
(if Distribution.changelog <> "" then "\nSee also " ^ Distribution.changelog else "");
val _ =
- Outer_Syntax.improper_command "welcome" "print welcome message" Keyword.diag
+ Outer_Syntax.improper_command ("welcome", Keyword.diag) "print welcome message"
(Scan.succeed (Toplevel.no_timing o Toplevel.imperative (writeln o welcome)));
--- a/src/Pure/Thy/thy_header.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/Thy/thy_header.ML Fri Mar 16 18:21:22 2012 +0100
@@ -8,13 +8,13 @@
sig
type header =
{name: string, imports: string list,
- keywords: (string * (string * string list) option) list,
+ keywords: (string * Keyword.spec option) list,
uses: (Path.T * bool) list}
- val make: string -> string list -> (string * (string * string list) option) list ->
+ val make: string -> string list -> (string * Keyword.spec option) list ->
(Path.T * bool) list -> header
val define_keywords: header -> unit
- val declare_keyword: string * (string * string list) option -> theory -> theory
- val the_keyword: theory -> string -> Keyword.T option
+ val declare_keyword: string * Keyword.spec option -> theory -> theory
+ val the_keyword: theory -> string -> Keyword.spec option
val args: header parser
val read: Position.T -> string -> header
end;
@@ -24,7 +24,7 @@
type header =
{name: string, imports: string list,
- keywords: (string * (string * string list) option) list,
+ keywords: (string * Keyword.spec option) list,
uses: (Path.T * bool) list};
fun make name imports keywords uses : header =
@@ -35,26 +35,27 @@
(** keyword declarations **)
fun define_keywords ({keywords, ...}: header) =
- List.app (fn (name, decl) => Keyword.define (name, Option.map Keyword.make decl)) keywords;
+ List.app (Keyword.define o apsnd (Option.map Keyword.spec)) keywords;
fun err_dup name = error ("Inconsistent declaration of outer syntax keyword " ^ quote name);
structure Data = Theory_Data
(
- type T = Keyword.T option Symtab.table;
+ type T = Keyword.spec option Symtab.table;
val empty = Symtab.empty;
val extend = I;
fun merge data : T = Symtab.merge (op =) data handle Symtab.DUP name => err_dup name;
);
-fun declare_keyword (name, decl) = Data.map (fn data =>
- let val kind = Option.map Keyword.make decl
- in Symtab.update_new (name, kind) data handle Symtab.DUP name => err_dup name end);
+fun declare_keyword (name, spec) =
+ Data.map (fn data =>
+ (Option.map Keyword.spec spec;
+ Symtab.update_new (name, spec) data handle Symtab.DUP dup => err_dup dup));
fun the_keyword thy name =
(case Symtab.lookup (Data.get thy) name of
- SOME kind => kind
- | NONE => error ("Unknown outer syntax keyword " ^ quote name));
+ SOME spec => spec
+ | NONE => error ("Undeclared outer syntax keyword " ^ quote name));
--- a/src/Pure/Tools/find_consts.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/Tools/find_consts.ML Fri Mar 16 18:21:22 2012 +0100
@@ -135,7 +135,7 @@
in
val _ =
- Outer_Syntax.improper_command "find_consts" "search constants by type pattern" Keyword.diag
+ Outer_Syntax.improper_command ("find_consts", Keyword.diag) "search constants by type pattern"
(Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
>> (fn spec => Toplevel.no_timing o
Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
--- a/src/Pure/Tools/find_theorems.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Pure/Tools/find_theorems.ML Fri Mar 16 18:21:22 2012 +0100
@@ -612,8 +612,8 @@
val query_parser = Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion));
val _ =
- Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria"
- Keyword.diag
+ Outer_Syntax.improper_command ("find_theorems", Keyword.diag)
+ "print theorems meeting specified criteria"
(options -- query_parser
>> (fn ((opt_lim, rem_dups), spec) =>
Toplevel.no_timing o
--- a/src/Tools/Code/code_haskell.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/Code/code_haskell.ML Fri Mar 16 18:21:22 2012 +0100
@@ -449,10 +449,9 @@
(** Isar setup **)
val _ =
- Outer_Syntax.command "code_monad" "define code syntax for monads" Keyword.thy_decl (
- Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
- Toplevel.theory (add_monad target raw_bind))
- );
+ Outer_Syntax.command @{command_spec "code_monad"} "define code syntax for monads"
+ (Parse.term_group -- Parse.name >> (fn (raw_bind, target) =>
+ Toplevel.theory (add_monad target raw_bind)));
val setup =
Code_Target.add_target
--- a/src/Tools/Code/code_preproc.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/Code/code_preproc.ML Fri Mar 16 18:21:22 2012 +0100
@@ -525,8 +525,8 @@
end;
val _ =
- Outer_Syntax.improper_command "print_codeproc" "print code preprocessor setup"
- Keyword.diag (Scan.succeed
+ Outer_Syntax.improper_command @{command_spec "print_codeproc"} "print code preprocessor setup"
+ (Scan.succeed
(Toplevel.no_timing o Toplevel.unknown_theory o Toplevel.keep
(print_codeproc o Toplevel.theory_of)));
--- a/src/Tools/Code/code_runtime.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/Code/code_runtime.ML Fri Mar 16 18:21:22 2012 +0100
@@ -352,13 +352,14 @@
in
val _ =
- Outer_Syntax.command "code_reflect" "enrich runtime environment with generated code"
- Keyword.thy_decl (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- (parse_datatype
+ Outer_Syntax.command @{command_spec "code_reflect"}
+ "enrich runtime environment with generated code"
+ (Parse.name -- Scan.optional (@{keyword "datatypes"} |-- (parse_datatype
::: Scan.repeat (@{keyword "and"} |-- parse_datatype))) []
-- Scan.optional (@{keyword "functions"} |-- Scan.repeat1 Parse.name) []
-- Scan.option (@{keyword "file"} |-- Parse.name)
- >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
- (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
+ >> (fn (((module_name, raw_datatypes), raw_functions), some_file) => Toplevel.theory
+ (code_reflect_cmd raw_datatypes raw_functions module_name some_file)));
end; (*local*)
--- a/src/Tools/Code/code_target.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/Code/code_target.ML Fri Mar 16 18:21:22 2012 +0100
@@ -680,57 +680,54 @@
-- code_expr_argsP) >> (fn seris => export_code_cmd raw_cs seris)));
val _ =
- Outer_Syntax.command "code_class" "define code syntax for class" Keyword.thy_decl (
- process_multi_syntax Parse.xname (Scan.option Parse.string)
- add_class_syntax_cmd);
+ Outer_Syntax.command @{command_spec "code_class"} "define code syntax for class"
+ (process_multi_syntax Parse.xname (Scan.option Parse.string)
+ add_class_syntax_cmd);
val _ =
- Outer_Syntax.command "code_instance" "define code syntax for instance" Keyword.thy_decl (
- process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname)
+ Outer_Syntax.command @{command_spec "code_instance"} "define code syntax for instance"
+ (process_multi_syntax (Parse.xname --| @{keyword "::"} -- Parse.xname)
(Scan.option (Parse.minus >> K ()))
- add_instance_syntax_cmd);
+ add_instance_syntax_cmd);
val _ =
- Outer_Syntax.command "code_type" "define code syntax for type constructor" Keyword.thy_decl (
- process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
- add_tyco_syntax_cmd);
+ Outer_Syntax.command @{command_spec "code_type"} "define code syntax for type constructor"
+ (process_multi_syntax Parse.xname Code_Printer.parse_tyco_syntax
+ add_tyco_syntax_cmd);
val _ =
- Outer_Syntax.command "code_const" "define code syntax for constant" Keyword.thy_decl (
- process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
- add_const_syntax_cmd);
+ Outer_Syntax.command @{command_spec "code_const"} "define code syntax for constant"
+ (process_multi_syntax Parse.term_group Code_Printer.parse_const_syntax
+ add_const_syntax_cmd);
val _ =
- Outer_Syntax.command "code_reserved" "declare words as reserved for target language"
- Keyword.thy_decl (
- Parse.name -- Scan.repeat1 Parse.name
- >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds)
- );
+ Outer_Syntax.command @{command_spec "code_reserved"}
+ "declare words as reserved for target language"
+ (Parse.name -- Scan.repeat1 Parse.name
+ >> (fn (target, reserveds) => (Toplevel.theory o fold (add_reserved target)) reserveds));
val _ =
- Outer_Syntax.command "code_include" "declare piece of code to be included in generated code"
- Keyword.thy_decl (
- Parse.name -- Parse.name -- (Parse.text :|-- (fn "-" => Scan.succeed NONE
- | s => Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
- >> (fn ((target, name), content_consts) =>
- (Toplevel.theory o add_include_cmd target) (name, content_consts))
- );
+ Outer_Syntax.command @{command_spec "code_include"}
+ "declare piece of code to be included in generated code"
+ (Parse.name -- Parse.name -- (Parse.text :|--
+ (fn "-" => Scan.succeed NONE
+ | s => Scan.optional (@{keyword "attach"} |-- Scan.repeat1 Parse.term) [] >> pair s >> SOME))
+ >> (fn ((target, name), content_consts) =>
+ (Toplevel.theory o add_include_cmd target) (name, content_consts)));
val _ =
- Outer_Syntax.command "code_modulename" "alias module to other name" Keyword.thy_decl (
- Parse.name -- Scan.repeat1 (Parse.name -- Parse.name)
- >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames)
- );
+ Outer_Syntax.command @{command_spec "code_modulename"} "alias module to other name"
+ (Parse.name -- Scan.repeat1 (Parse.name -- Parse.name)
+ >> (fn (target, modlnames) => (Toplevel.theory o fold (add_module_alias target)) modlnames));
val _ =
- Outer_Syntax.command "code_abort" "permit constant to be implemented as program abort"
- Keyword.thy_decl (
- Scan.repeat1 Parse.term_group >> (Toplevel.theory o fold allow_abort_cmd)
- );
+ Outer_Syntax.command @{command_spec "code_abort"}
+ "permit constant to be implemented as program abort"
+ (Scan.repeat1 Parse.term_group >> (Toplevel.theory o fold allow_abort_cmd));
val _ =
- Outer_Syntax.command "export_code" "generate executable code for constants"
- Keyword.diag (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
+ Outer_Syntax.command @{command_spec "export_code"} "generate executable code for constants"
+ (Parse.!!! code_exprP >> (fn f => Toplevel.keep (f o Toplevel.theory_of)));
end; (*local*)
--- a/src/Tools/Code/code_thingol.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/Code/code_thingol.ML Fri Mar 16 18:21:22 2012 +0100
@@ -1046,14 +1046,15 @@
in
val _ =
- Outer_Syntax.improper_command "code_thms" "print system of code equations for code" Keyword.diag
+ Outer_Syntax.improper_command @{command_spec "code_thms"}
+ "print system of code equations for code"
(Scan.repeat1 Parse.term_group
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
o Toplevel.keep ((fn thy => code_thms_cmd thy cs) o Toplevel.theory_of)));
val _ =
- Outer_Syntax.improper_command "code_deps" "visualize dependencies of code equations for code"
- Keyword.diag
+ Outer_Syntax.improper_command @{command_spec "code_deps"}
+ "visualize dependencies of code equations for code"
(Scan.repeat1 Parse.term_group
>> (fn cs => Toplevel.no_timing o Toplevel.unknown_theory
o Toplevel.keep ((fn thy => code_deps_cmd thy cs) o Toplevel.theory_of)));
--- a/src/Tools/induct.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/induct.ML Fri Mar 16 18:21:22 2012 +0100
@@ -259,8 +259,9 @@
end;
val _ =
- Outer_Syntax.improper_command "print_induct_rules" "print induction and cases rules"
- Keyword.diag (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
+ Outer_Syntax.improper_command @{command_spec "print_induct_rules"}
+ "print induction and cases rules"
+ (Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
Toplevel.keep (print_rules o Toplevel.context_of)));
--- a/src/Tools/interpretation_with_defs.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/interpretation_with_defs.ML Fri Mar 16 18:21:22 2012 +0100
@@ -80,8 +80,8 @@
end;
val _ =
- Outer_Syntax.command "interpretation"
- "prove interpretation of locale expression in theory" Keyword.thy_goal
+ Outer_Syntax.command @{command_spec "interpretation"}
+ "prove interpretation of locale expression in theory"
(Parse.!!! (Parse_Spec.locale_expression true) --
Scan.optional (@{keyword "defines"} |-- Parse.and_list1 (Parse_Spec.opt_thm_name ":"
-- ((Parse.binding -- Parse.opt_mixfix') --| @{keyword "is"} -- Parse.term))) [] --
--- a/src/Tools/quickcheck.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/quickcheck.ML Fri Mar 16 18:21:22 2012 +0100
@@ -83,7 +83,6 @@
struct
val quickcheckN = "quickcheck"
-val quickcheck_paramsN = "quickcheck_params"
val genuineN = "genuine"
val noneN = "none"
@@ -530,11 +529,12 @@
@{keyword "["} |-- Parse.list1 parse_arg --| @{keyword "]"} || Scan.succeed [];
val _ =
- Outer_Syntax.command quickcheck_paramsN "set parameters for random testing" Keyword.thy_decl
+ Outer_Syntax.command @{command_spec "quickcheck_params"} "set parameters for random testing"
(parse_args >> (fn args => Toplevel.theory (quickcheck_params_cmd args)));
val _ =
- Outer_Syntax.improper_command quickcheckN "try to find counterexample for subgoal" Keyword.diag
+ Outer_Syntax.improper_command @{command_spec "quickcheck"}
+ "try to find counterexample for subgoal"
(parse_args -- Scan.optional Parse.nat 1
>> (fn (args, i) => Toplevel.no_timing o Toplevel.keep (quickcheck_cmd args i)));
--- a/src/Tools/solve_direct.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/solve_direct.ML Fri Mar 16 18:21:22 2012 +0100
@@ -107,10 +107,9 @@
val solve_direct = do_solve_direct Normal
val _ =
- Outer_Syntax.improper_command solve_directN
- "try to solve conjectures directly with existing theorems" Keyword.diag
- (Scan.succeed
- (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
+ Outer_Syntax.improper_command @{command_spec "solve_direct"}
+ "try to solve conjectures directly with existing theorems"
+ (Scan.succeed (Toplevel.keep (ignore o solve_direct o Toplevel.proof_of)));
(* hook *)
--- a/src/Tools/subtyping.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/subtyping.ML Fri Mar 16 18:21:22 2012 +0100
@@ -1028,10 +1028,10 @@
(* outer syntax commands *)
val _ =
- Outer_Syntax.improper_command "print_coercions" "print all coercions" Keyword.diag
+ Outer_Syntax.improper_command @{command_spec "print_coercions"} "print all coercions"
(Scan.succeed (Toplevel.keep (print_coercions o Toplevel.context_of)))
val _ =
- Outer_Syntax.improper_command "print_coercion_maps" "print all coercion maps" Keyword.diag
+ Outer_Syntax.improper_command @{command_spec "print_coercion_maps"} "print all coercion maps"
(Scan.succeed (Toplevel.keep (print_coercion_maps o Toplevel.context_of)))
end;
--- a/src/Tools/try.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/try.ML Fri Mar 16 18:21:22 2012 +0100
@@ -88,9 +88,9 @@
|> tap (fn NONE => Output.urgent_message "Tried in vain." | _ => ())
val _ =
- Outer_Syntax.improper_command tryN
- "try a combination of automatic proving and disproving tools" Keyword.diag
- (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
+ Outer_Syntax.improper_command @{command_spec "try"}
+ "try a combination of automatic proving and disproving tools"
+ (Scan.succeed (Toplevel.keep (ignore o try_tools o Toplevel.proof_of)))
(* automatic try *)
--- a/src/Tools/value.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/Tools/value.ML Fri Mar 16 18:21:22 2012 +0100
@@ -63,7 +63,7 @@
Scan.option (@{keyword "["} |-- Parse.xname --| @{keyword "]"})
val _ =
- Outer_Syntax.improper_command "value" "evaluate and print term" Keyword.diag
+ Outer_Syntax.improper_command @{command_spec "value"} "evaluate and print term"
(opt_evaluator -- opt_modes -- Parse.term
>> (fn ((some_name, modes), t) => Toplevel.no_timing o Toplevel.keep
(value_cmd some_name modes t)));
--- a/src/ZF/Tools/datatype_package.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/ZF/Tools/datatype_package.ML Fri Mar 16 18:21:22 2012 +0100
@@ -430,19 +430,18 @@
Parse.name -- Scan.optional (@{keyword "("} |-- Parse.list1 Parse.term --| @{keyword ")"}) [] --
Parse.opt_mixfix >> Parse.triple1;
-val datatype_decl =
- (Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.!!! Parse.term) "") --
- Parse.and_list1 (Parse.term -- (@{keyword "="} |-- Parse.enum1 "|" con_decl)) --
- Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) [] --
- Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse_Spec.xthms1) [] --
- Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse_Spec.xthms1) []
- >> (Toplevel.theory o mk_datatype);
-
val coind_prefix = if coind then "co" else "";
val _ =
- Outer_Syntax.command (coind_prefix ^ "datatype")
- ("define " ^ coind_prefix ^ "datatype") Keyword.thy_decl datatype_decl;
+ Outer_Syntax.command
+ (if coind then @{command_spec "codatatype"} else @{command_spec "datatype"})
+ ("define " ^ coind_prefix ^ "datatype")
+ ((Scan.optional ((@{keyword "\<subseteq>"} || @{keyword "<="}) |-- Parse.!!! Parse.term) "") --
+ Parse.and_list1 (Parse.term -- (@{keyword "="} |-- Parse.enum1 "|" con_decl)) --
+ Scan.optional (@{keyword "monos"} |-- Parse.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (@{keyword "type_intros"} |-- Parse.!!! Parse_Spec.xthms1) [] --
+ Scan.optional (@{keyword "type_elims"} |-- Parse.!!! Parse_Spec.xthms1) []
+ >> (Toplevel.theory o mk_datatype));
end;
--- a/src/ZF/Tools/ind_cases.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/ZF/Tools/ind_cases.ML Fri Mar 16 18:21:22 2012 +0100
@@ -65,8 +65,8 @@
(* outer syntax *)
val _ =
- Outer_Syntax.command "inductive_cases"
- "create simplified instances of elimination rules (improper)" Keyword.thy_script
+ Outer_Syntax.command @{command_spec "inductive_cases"}
+ "create simplified instances of elimination rules (improper)"
(Parse.and_list1 (Parse_Spec.opt_thm_name ":" -- Scan.repeat1 Parse.prop)
>> (Toplevel.theory o inductive_cases));
--- a/src/ZF/Tools/induct_tacs.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/ZF/Tools/induct_tacs.ML Fri Mar 16 18:21:22 2012 +0100
@@ -188,16 +188,13 @@
(* outer syntax *)
-val rep_datatype_decl =
- (@{keyword "elimination"} |-- Parse.!!! Parse_Spec.xthm) --
- (@{keyword "induction"} |-- Parse.!!! Parse_Spec.xthm) --
- (@{keyword "case_eqns"} |-- Parse.!!! Parse_Spec.xthms1) --
- Scan.optional (@{keyword "recursor_eqns"} |-- Parse.!!! Parse_Spec.xthms1) []
- >> (fn (((x, y), z), w) => rep_datatype x y z w);
-
val _ =
- Outer_Syntax.command "rep_datatype" "represent existing set inductively" Keyword.thy_decl
- (rep_datatype_decl >> Toplevel.theory);
+ Outer_Syntax.command @{command_spec "rep_datatype"} "represent existing set inductively"
+ ((@{keyword "elimination"} |-- Parse.!!! Parse_Spec.xthm) --
+ (@{keyword "induction"} |-- Parse.!!! Parse_Spec.xthm) --
+ (@{keyword "case_eqns"} |-- Parse.!!! Parse_Spec.xthms1) --
+ Scan.optional (@{keyword "recursor_eqns"} |-- Parse.!!! Parse_Spec.xthms1) []
+ >> (fn (((x, y), z), w) => Toplevel.theory (rep_datatype x y z w)));
end;
--- a/src/ZF/Tools/inductive_package.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/ZF/Tools/inductive_package.ML Fri Mar 16 18:21:22 2012 +0100
@@ -591,8 +591,9 @@
>> (Toplevel.theory o mk_ind);
val _ =
- Outer_Syntax.command (co_prefix ^ "inductive")
- ("define " ^ co_prefix ^ "inductive sets") Keyword.thy_decl ind_decl;
+ Outer_Syntax.command
+ (if coind then @{command_spec "coinductive"} else @{command_spec "inductive"})
+ ("define " ^ co_prefix ^ "inductive sets") ind_decl;
end;
--- a/src/ZF/Tools/primrec_package.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/ZF/Tools/primrec_package.ML Fri Mar 16 18:21:22 2012 +0100
@@ -196,8 +196,7 @@
(* outer syntax *)
val _ =
- Outer_Syntax.command "primrec" "define primitive recursive functions on datatypes"
- Keyword.thy_decl
+ Outer_Syntax.command @{command_spec "primrec"} "define primitive recursive functions on datatypes"
(Scan.repeat1 (Parse_Spec.opt_thm_name ":" -- Parse.prop)
>> (Toplevel.theory o (#1 oo (add_primrec o map Parse.triple_swap))));
--- a/src/ZF/Tools/typechk.ML Fri Mar 16 16:32:34 2012 +0000
+++ b/src/ZF/Tools/typechk.ML Fri Mar 16 18:21:22 2012 +0100
@@ -121,7 +121,7 @@
"ZF type-checking";
val _ =
- Outer_Syntax.improper_command "print_tcset" "print context of ZF typecheck" Keyword.diag
+ Outer_Syntax.improper_command @{command_spec "print_tcset"} "print context of ZF typecheck"
(Scan.succeed (Toplevel.no_timing o Toplevel.unknown_context o
Toplevel.keep (print_tcset o Toplevel.context_of)));