declare command keywords via theory header, including strict checking outside Pure;
--- a/src/FOL/FOL.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/FOL/FOL.thy Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,7 @@
theory FOL
imports IFOL
+keywords "print_claset" "print_induct_rules" :: diag
uses
"~~/src/Provers/classical.ML"
"~~/src/Provers/blast.ML"
--- a/src/HOL/Boogie/Boogie.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Boogie/Boogie.thy Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,8 @@
theory Boogie
imports Word
+keywords
+ "boogie_open" "boogie_end" :: thy_decl and "boogie_vc" :: thy_goal and "boogie_status" :: diag
uses
("Tools/boogie_vcs.ML")
("Tools/boogie_loader.ML")
--- a/src/HOL/Datatype.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Datatype.thy Thu Mar 15 22:08:53 2012 +0100
@@ -7,6 +7,7 @@
theory Datatype
imports Product_Type Sum_Type Nat
+keywords "datatype" :: thy_decl
uses
("Tools/Datatype/datatype.ML")
("Tools/inductive_realizer.ML")
--- a/src/HOL/Fun.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Fun.thy Thu Mar 15 22:08:53 2012 +0100
@@ -7,6 +7,7 @@
theory Fun
imports Complete_Lattices
+keywords "enriched_type" :: thy_goal
uses ("Tools/enriched_type.ML")
begin
--- a/src/HOL/FunDef.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/FunDef.thy Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,7 @@
theory FunDef
imports Partial_Function Wellfounded
+keywords "function" "termination" :: thy_goal and "fun" :: thy_decl
uses
"Tools/prop_logic.ML"
"Tools/sat_solver.ML"
--- a/src/HOL/HOL.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/HOL.thy Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,8 @@
theory HOL
imports Pure "~~/src/Tools/Code_Generator"
+keywords
+ "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag
uses
("Tools/hologic.ML")
"~~/src/Tools/IsaPlanner/zipper.ML"
--- a/src/HOL/HOLCF/Cpodef.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/HOLCF/Cpodef.thy Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,7 @@
theory Cpodef
imports Adm
+keywords "pcpodef" "cpodef" :: thy_goal
uses ("Tools/cpodef.ML")
begin
--- a/src/HOL/HOLCF/Domain.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/HOLCF/Domain.thy Thu Mar 15 22:08:53 2012 +0100
@@ -6,7 +6,9 @@
theory Domain
imports Representable Domain_Aux
-keywords "lazy" "unsafe"
+keywords
+ "domaindef" :: thy_decl and "lazy" "unsafe" and
+ "domain_isomorphism" "domain" :: thy_decl
uses
("Tools/domaindef.ML")
("Tools/Domain/domain_isomorphism.ML")
--- a/src/HOL/HOLCF/Fixrec.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/HOLCF/Fixrec.thy Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,7 @@
theory Fixrec
imports Plain_HOLCF
+keywords "fixrec" :: thy_decl
uses
("Tools/holcf_library.ML")
("Tools/fixrec.ML")
--- a/src/HOL/Hilbert_Choice.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Hilbert_Choice.thy Thu Mar 15 22:08:53 2012 +0100
@@ -7,6 +7,7 @@
theory Hilbert_Choice
imports Nat Wellfounded Plain
+keywords "specification" "ax_specification" :: thy_goal
uses ("Tools/choice_specification.ML")
begin
--- a/src/HOL/Import/Importer.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Import/Importer.thy Thu Mar 15 22:08:53 2012 +0100
@@ -4,7 +4,10 @@
theory Importer
imports Main
-keywords ">"
+keywords
+ "import_segment" "import_theory" "end_import" "setup_theory" "end_setup"
+ "setup_dump" "append_dump" "flush_dump" "ignore_thms" "type_maps"
+ "def_maps" "thm_maps" "const_renames" "const_moves" "const_maps" :: thy_decl and ">"
uses "shuffler.ML" "import_rews.ML" ("proof_kernel.ML") ("replay.ML") ("import.ML")
begin
--- a/src/HOL/Inductive.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Inductive.thy Thu Mar 15 22:08:53 2012 +0100
@@ -6,7 +6,11 @@
theory Inductive
imports Complete_Lattices
-keywords "monos"
+keywords
+ "inductive" "coinductive" :: thy_decl and
+ "inductive_cases" "inductive_simps" :: thy_script and "monos" and
+ "rep_datatype" :: thy_goal and
+ "primrec" :: thy_decl
uses
"Tools/dseq.ML"
("Tools/inductive.ML")
--- a/src/HOL/Library/Old_Recdef.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Library/Old_Recdef.thy Thu Mar 15 22:08:53 2012 +0100
@@ -6,7 +6,10 @@
theory Old_Recdef
imports Wfrec
-keywords "recdef" :: thy_decl and "permissive" "congs" "hints"
+keywords
+ "recdef" "defer_recdef" :: thy_decl and
+ "recdef_tc" :: thy_goal and
+ "permissive" "congs" "hints"
uses
("~~/src/HOL/Tools/TFL/casesplit.ML")
("~~/src/HOL/Tools/TFL/utils.ML")
--- a/src/HOL/Metis.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Metis.thy Thu Mar 15 22:08:53 2012 +0100
@@ -8,6 +8,7 @@
theory Metis
imports ATP
+keywords "try0" :: diag
uses "~~/src/Tools/Metis/metis.ML"
("Tools/Metis/metis_generate.ML")
("Tools/Metis/metis_reconstruct.ML")
--- a/src/HOL/Nitpick.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Nitpick.thy Thu Mar 15 22:08:53 2012 +0100
@@ -9,6 +9,7 @@
theory Nitpick
imports Map Quotient SAT Record
+keywords "nitpick" :: diag and "nitpick_params" :: thy_decl
uses ("Tools/Nitpick/kodkod.ML")
("Tools/Nitpick/kodkod_sat.ML")
("Tools/Nitpick/nitpick_util.ML")
--- a/src/HOL/Nominal/Nominal.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Nominal/Nominal.thy Thu Mar 15 22:08:53 2012 +0100
@@ -1,6 +1,9 @@
theory Nominal
imports Main "~~/src/HOL/Library/Infinite_Set"
-keywords "avoids"
+keywords
+ "atom_decl" "nominal_datatype" "equivariance" :: thy_decl and
+ "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal and
+ "avoids"
uses
("nominal_thmdecls.ML")
("nominal_atoms.ML")
--- a/src/HOL/Orderings.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Orderings.thy Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,7 @@
theory Orderings
imports HOL
+keywords "print_orders" :: diag
uses
"~~/src/Provers/order.ML"
"~~/src/Provers/quasi.ML" (* FIXME unused? *)
--- a/src/HOL/Partial_Function.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Partial_Function.thy Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,7 @@
theory Partial_Function
imports Complete_Partial_Order Option
+keywords "partial_function" :: thy_decl
uses
"Tools/Function/function_lib.ML"
"Tools/Function/partial_function.ML"
--- a/src/HOL/Predicate_Compile.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Predicate_Compile.thy Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,7 @@
theory Predicate_Compile
imports Predicate New_Random_Sequence Quickcheck_Exhaustive
+keywords "code_pred" :: thy_goal and "values" :: diag
uses
"Tools/Predicate_Compile/predicate_compile_aux.ML"
"Tools/Predicate_Compile/predicate_compile_compilations.ML"
--- a/src/HOL/Product_Type.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Product_Type.thy Thu Mar 15 22:08:53 2012 +0100
@@ -7,6 +7,7 @@
theory Product_Type
imports Typedef Inductive Fun
+keywords "inductive_set" "coinductive_set" :: thy_decl
uses
("Tools/split_rule.ML")
("Tools/inductive_set.ML")
--- a/src/HOL/Quickcheck_Exhaustive.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Quickcheck_Exhaustive.thy Thu Mar 15 22:08:53 2012 +0100
@@ -4,6 +4,7 @@
theory Quickcheck_Exhaustive
imports Quickcheck
+keywords "quickcheck_generator" :: thy_decl
uses
("Tools/Quickcheck/exhaustive_generators.ML")
("Tools/Quickcheck/abstract_generators.ML")
--- a/src/HOL/Quickcheck_Narrowing.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Quickcheck_Narrowing.thy Thu Mar 15 22:08:53 2012 +0100
@@ -4,6 +4,7 @@
theory Quickcheck_Narrowing
imports Quickcheck_Exhaustive
+keywords "find_unused_assms" :: diag
uses
("Tools/Quickcheck/PNF_Narrowing_Engine.hs")
("Tools/Quickcheck/Narrowing_Engine.hs")
--- a/src/HOL/Quotient.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Quotient.thy Thu Mar 15 22:08:53 2012 +0100
@@ -6,7 +6,10 @@
theory Quotient
imports Plain Hilbert_Choice Equiv_Relations
-keywords "/"
+keywords
+ "print_quotmaps" "print_quotients" "print_quotconsts" :: diag and
+ "quotient_type" :: thy_goal and "/" and
+ "quotient_definition" :: thy_decl
uses
("Tools/Quotient/quotient_info.ML")
("Tools/Quotient/quotient_type.ML")
--- a/src/HOL/Record.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Record.thy Thu Mar 15 22:08:53 2012 +0100
@@ -10,6 +10,7 @@
theory Record
imports Plain Quickcheck_Narrowing
+keywords "record" :: thy_decl
uses ("Tools/record.ML")
begin
--- a/src/HOL/Refute.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Refute.thy Thu Mar 15 22:08:53 2012 +0100
@@ -9,6 +9,7 @@
theory Refute
imports Hilbert_Choice List Sledgehammer
+keywords "refute" :: diag and "refute_params" :: thy_decl
uses "Tools/refute.ML"
begin
--- a/src/HOL/SMT.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/SMT.thy Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,7 @@
theory SMT
imports Record
+keywords "smt_status" :: diag
uses
"Tools/SMT/smt_utils.ML"
"Tools/SMT/smt_failure.ML"
--- a/src/HOL/SPARK/SPARK_Setup.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/SPARK/SPARK_Setup.thy Thu Mar 15 22:08:53 2012 +0100
@@ -7,6 +7,9 @@
theory SPARK_Setup
imports Word
+keywords
+ "spark_open" "spark_proof_functions" "spark_types" "spark_end" :: thy_decl and
+ "spark_vc" :: thy_goal and "spark_status" :: diag
uses
"Tools/fdl_lexer.ML"
"Tools/fdl_parser.ML"
--- a/src/HOL/Sledgehammer.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Sledgehammer.thy Thu Mar 15 22:08:53 2012 +0100
@@ -8,6 +8,7 @@
theory Sledgehammer
imports ATP SMT
+keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
uses "Tools/Sledgehammer/async_manager.ML"
"Tools/Sledgehammer/sledgehammer_util.ML"
"Tools/Sledgehammer/sledgehammer_filter.ML"
--- a/src/HOL/Statespace/StateSpaceLocale.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Statespace/StateSpaceLocale.thy Thu Mar 15 22:08:53 2012 +0100
@@ -5,6 +5,7 @@
header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*}
theory StateSpaceLocale imports StateFun
+keywords "statespace" :: thy_decl
uses "state_space.ML" "state_fun.ML"
begin
--- a/src/HOL/TPTP/TPTP_Parser.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/TPTP/TPTP_Parser.thy Thu Mar 15 22:08:53 2012 +0100
@@ -9,6 +9,7 @@
theory TPTP_Parser
imports Main
+keywords "import_tptp" :: diag (* FIXME !? *)
uses
"TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*)
--- a/src/HOL/Typedef.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/Typedef.thy Thu Mar 15 22:08:53 2012 +0100
@@ -6,7 +6,7 @@
theory Typedef
imports Set
-keywords "morphisms"
+keywords "typedef" :: thy_goal and "morphisms"
uses ("Tools/typedef.ML")
begin
--- a/src/HOL/ex/Interpretation_with_Defs.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/HOL/ex/Interpretation_with_Defs.thy Thu Mar 15 22:08:53 2012 +0100
@@ -6,6 +6,7 @@
theory Interpretation_with_Defs
imports Pure
+keywords "interpretation" :: thy_goal
uses "~~/src/Tools/interpretation_with_defs.ML"
begin
--- a/src/Pure/Isar/isar_syn.ML Thu Mar 15 20:07:00 2012 +0100
+++ b/src/Pure/Isar/isar_syn.ML Thu Mar 15 22:08:53 2012 +0100
@@ -21,7 +21,7 @@
"constrains", "defines", "fixes", "for", "identifier", "if",
"imports", "in", "infix", "infixl", "infixr", "is", "keywords",
"notes", "obtains", "open", "output", "overloaded", "pervasive",
- "shows", "structure", "unchecked", "uses", "where", "|", "by"]));
+ "shows", "structure", "unchecked", "uses", "where", "|"]));
--- a/src/Pure/Isar/keyword.ML Thu Mar 15 20:07:00 2012 +0100
+++ b/src/Pure/Isar/keyword.ML Thu Mar 15 22:08:53 2012 +0100
@@ -48,7 +48,7 @@
val status: unit -> unit
val keyword: string -> unit
val command: string -> T -> unit
- val declare: string * (string * string list) option -> unit
+ val declare: string -> T option -> unit
val is_diag: string -> bool
val is_control: string -> bool
val is_regular: string -> bool
@@ -215,8 +215,8 @@
change_commands (Symtab.update (name, kind));
command_status (name, kind));
-fun declare (name, NONE) = keyword name
- | declare (name, SOME kind) = command name (make kind);
+fun declare name NONE = keyword name
+ | declare name (SOME kind) = command name kind;
(* command categories *)
--- a/src/Pure/Isar/outer_syntax.ML Thu Mar 15 20:07:00 2012 +0100
+++ b/src/Pure/Isar/outer_syntax.ML Thu Mar 15 22:08:53 2012 +0100
@@ -123,11 +123,23 @@
val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
fun add_command name kind cmd = CRITICAL (fn () =>
- (Keyword.command name kind;
- Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
- (if not (Symtab.defined commands name) then ()
- else warning ("Redefining outer syntax command " ^ quote name);
- Symtab.update (name, cmd) commands)))));
+ 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 ()
+ else error ("Inconsistent outer syntax keyword declaration " ^ quote name)
+ | NONE =>
+ (Keyword.command name kind;
+ if Context.theory_name thy = Context.PureN then ()
+ else error ("Undeclared outer syntax command " ^ quote name)));
+ in
+ Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
+ (if not (Symtab.defined commands name) then ()
+ else warning ("Redefining outer syntax command " ^ quote name);
+ Symtab.update (name, cmd) commands)))
+ end);
in
--- a/src/Pure/PIDE/document.ML Thu Mar 15 20:07:00 2012 +0100
+++ b/src/Pure/PIDE/document.ML Thu Mar 15 22:08:53 2012 +0100
@@ -215,7 +215,8 @@
val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
val keywords = (case header of Exn.Res (_, {keywords, ...}) => keywords | _ => []);
val header' =
- (List.app Keyword.declare keywords; header)
+ (List.app (fn (name, decl) =>
+ Keyword.declare name (Option.map Keyword.make decl)) keywords; header)
handle exn as ERROR _ => Exn.Exn exn;
val nodes1 = nodes
|> default_node name
--- a/src/Pure/Thy/thy_header.ML Thu Mar 15 20:07:00 2012 +0100
+++ b/src/Pure/Thy/thy_header.ML Thu Mar 15 22:08:53 2012 +0100
@@ -43,15 +43,15 @@
fun merge data : T = Symtab.merge (op =) data handle Symtab.DUP name => err_dup name;
);
-fun declare_keyword (name, kind) =
- Data.map (fn data =>
- (if is_none kind then Keyword.keyword name else ();
- Symtab.update_new (name, Option.map Keyword.make kind) 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;
+ val _ = Keyword.declare name kind;
+ in Symtab.update_new (name, kind) data handle Symtab.DUP name => err_dup name end);
fun the_keyword thy name =
(case Symtab.lookup (Data.get thy) name of
- SOME decl => decl
+ SOME kind => kind
| NONE => error ("Unknown outer syntax keyword " ^ quote name));
--- a/src/Pure/Thy/thy_output.ML Thu Mar 15 20:07:00 2012 +0100
+++ b/src/Pure/Thy/thy_output.ML Thu Mar 15 22:08:53 2012 +0100
@@ -626,6 +626,8 @@
(* embedded lemma *)
+val _ = Keyword.keyword "by";
+
val _ =
Context.>> (Context.map_theory
(antiquotation (Binding.name "lemma")
--- a/src/Tools/Code_Generator.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/Tools/Code_Generator.thy Thu Mar 15 22:08:53 2012 +0100
@@ -6,7 +6,13 @@
theory Code_Generator
imports Pure
-keywords "datatypes" "functions" "module_name" "file" "checking"
+keywords
+ "try" "solve_direct" "quickcheck" "value" "print_codeproc"
+ "code_thms" "code_deps" "export_code" :: diag and
+ "quickcheck_params" "code_class" "code_instance" "code_type"
+ "code_const" "code_reserved" "code_include" "code_modulename"
+ "code_abort" "code_monad" "code_reflect" :: thy_decl and
+ "datatypes" "functions" "module_name" "file" "checking"
uses
"~~/src/Tools/misc_legacy.ML"
"~~/src/Tools/cache_io.ML"
--- a/src/ZF/Datatype_ZF.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/ZF/Datatype_ZF.thy Thu Mar 15 22:08:53 2012 +0100
@@ -7,6 +7,7 @@
theory Datatype_ZF
imports Inductive_ZF Univ QUniv
+keywords "datatype" "codatatype" :: thy_decl
uses "Tools/datatype_package.ML"
begin
--- a/src/ZF/Inductive_ZF.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/ZF/Inductive_ZF.thy Thu Mar 15 22:08:53 2012 +0100
@@ -14,8 +14,10 @@
theory Inductive_ZF
imports Fixedpt QPair Nat_ZF
keywords
+ "inductive" "coinductive" "rep_datatype" "primrec" :: thy_decl and
+ "inductive_cases" :: thy_script and
+ "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
"elimination" "induction" "case_eqns" "recursor_eqns"
- "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
uses
("ind_syntax.ML")
("Tools/cartprod.ML")
--- a/src/ZF/upair.thy Thu Mar 15 20:07:00 2012 +0100
+++ b/src/ZF/upair.thy Thu Mar 15 22:08:53 2012 +0100
@@ -11,8 +11,11 @@
header{*Unordered Pairs*}
-theory upair imports ZF
-uses "Tools/typechk.ML" begin
+theory upair
+imports ZF
+keywords "print_tcset" :: diag
+uses "Tools/typechk.ML"
+begin
setup TypeCheck.setup