declare command keywords via theory header, including strict checking outside Pure;
authorwenzelm
Thu Mar 15 22:08:53 2012 +0100 (2012-03-15)
changeset 46950d0181abdbdac
parent 46949 94aa7b81bcf6
child 46951 4e032ac36134
declare command keywords via theory header, including strict checking outside Pure;
src/FOL/FOL.thy
src/HOL/Boogie/Boogie.thy
src/HOL/Datatype.thy
src/HOL/Fun.thy
src/HOL/FunDef.thy
src/HOL/HOL.thy
src/HOL/HOLCF/Cpodef.thy
src/HOL/HOLCF/Domain.thy
src/HOL/HOLCF/Fixrec.thy
src/HOL/Hilbert_Choice.thy
src/HOL/Import/Importer.thy
src/HOL/Inductive.thy
src/HOL/Library/Old_Recdef.thy
src/HOL/Metis.thy
src/HOL/Nitpick.thy
src/HOL/Nominal/Nominal.thy
src/HOL/Orderings.thy
src/HOL/Partial_Function.thy
src/HOL/Predicate_Compile.thy
src/HOL/Product_Type.thy
src/HOL/Quickcheck_Exhaustive.thy
src/HOL/Quickcheck_Narrowing.thy
src/HOL/Quotient.thy
src/HOL/Record.thy
src/HOL/Refute.thy
src/HOL/SMT.thy
src/HOL/SPARK/SPARK_Setup.thy
src/HOL/Sledgehammer.thy
src/HOL/Statespace/StateSpaceLocale.thy
src/HOL/TPTP/TPTP_Parser.thy
src/HOL/Typedef.thy
src/HOL/ex/Interpretation_with_Defs.thy
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/keyword.ML
src/Pure/Isar/outer_syntax.ML
src/Pure/PIDE/document.ML
src/Pure/Thy/thy_header.ML
src/Pure/Thy/thy_output.ML
src/Tools/Code_Generator.thy
src/ZF/Datatype_ZF.thy
src/ZF/Inductive_ZF.thy
src/ZF/upair.thy
     1.1 --- a/src/FOL/FOL.thy	Thu Mar 15 20:07:00 2012 +0100
     1.2 +++ b/src/FOL/FOL.thy	Thu Mar 15 22:08:53 2012 +0100
     1.3 @@ -6,6 +6,7 @@
     1.4  
     1.5  theory FOL
     1.6  imports IFOL
     1.7 +keywords "print_claset" "print_induct_rules" :: diag
     1.8  uses
     1.9    "~~/src/Provers/classical.ML"
    1.10    "~~/src/Provers/blast.ML"
     2.1 --- a/src/HOL/Boogie/Boogie.thy	Thu Mar 15 20:07:00 2012 +0100
     2.2 +++ b/src/HOL/Boogie/Boogie.thy	Thu Mar 15 22:08:53 2012 +0100
     2.3 @@ -6,6 +6,8 @@
     2.4  
     2.5  theory Boogie
     2.6  imports Word
     2.7 +keywords
     2.8 +  "boogie_open" "boogie_end" :: thy_decl and "boogie_vc" :: thy_goal and "boogie_status" :: diag
     2.9  uses
    2.10    ("Tools/boogie_vcs.ML")
    2.11    ("Tools/boogie_loader.ML")
     3.1 --- a/src/HOL/Datatype.thy	Thu Mar 15 20:07:00 2012 +0100
     3.2 +++ b/src/HOL/Datatype.thy	Thu Mar 15 22:08:53 2012 +0100
     3.3 @@ -7,6 +7,7 @@
     3.4  
     3.5  theory Datatype
     3.6  imports Product_Type Sum_Type Nat
     3.7 +keywords "datatype" :: thy_decl
     3.8  uses
     3.9    ("Tools/Datatype/datatype.ML")
    3.10    ("Tools/inductive_realizer.ML")
     4.1 --- a/src/HOL/Fun.thy	Thu Mar 15 20:07:00 2012 +0100
     4.2 +++ b/src/HOL/Fun.thy	Thu Mar 15 22:08:53 2012 +0100
     4.3 @@ -7,6 +7,7 @@
     4.4  
     4.5  theory Fun
     4.6  imports Complete_Lattices
     4.7 +keywords "enriched_type" :: thy_goal
     4.8  uses ("Tools/enriched_type.ML")
     4.9  begin
    4.10  
     5.1 --- a/src/HOL/FunDef.thy	Thu Mar 15 20:07:00 2012 +0100
     5.2 +++ b/src/HOL/FunDef.thy	Thu Mar 15 22:08:53 2012 +0100
     5.3 @@ -6,6 +6,7 @@
     5.4  
     5.5  theory FunDef
     5.6  imports Partial_Function Wellfounded
     5.7 +keywords "function" "termination" :: thy_goal and "fun" :: thy_decl
     5.8  uses
     5.9    "Tools/prop_logic.ML"
    5.10    "Tools/sat_solver.ML"
     6.1 --- a/src/HOL/HOL.thy	Thu Mar 15 20:07:00 2012 +0100
     6.2 +++ b/src/HOL/HOL.thy	Thu Mar 15 22:08:53 2012 +0100
     6.3 @@ -6,6 +6,8 @@
     6.4  
     6.5  theory HOL
     6.6  imports Pure "~~/src/Tools/Code_Generator"
     6.7 +keywords
     6.8 +  "print_coercions" "print_coercion_maps" "print_claset" "print_induct_rules" :: diag
     6.9  uses
    6.10    ("Tools/hologic.ML")
    6.11    "~~/src/Tools/IsaPlanner/zipper.ML"
     7.1 --- a/src/HOL/HOLCF/Cpodef.thy	Thu Mar 15 20:07:00 2012 +0100
     7.2 +++ b/src/HOL/HOLCF/Cpodef.thy	Thu Mar 15 22:08:53 2012 +0100
     7.3 @@ -6,6 +6,7 @@
     7.4  
     7.5  theory Cpodef
     7.6  imports Adm
     7.7 +keywords "pcpodef" "cpodef" :: thy_goal
     7.8  uses ("Tools/cpodef.ML")
     7.9  begin
    7.10  
     8.1 --- a/src/HOL/HOLCF/Domain.thy	Thu Mar 15 20:07:00 2012 +0100
     8.2 +++ b/src/HOL/HOLCF/Domain.thy	Thu Mar 15 22:08:53 2012 +0100
     8.3 @@ -6,7 +6,9 @@
     8.4  
     8.5  theory Domain
     8.6  imports Representable Domain_Aux
     8.7 -keywords "lazy" "unsafe"
     8.8 +keywords
     8.9 +  "domaindef" :: thy_decl and "lazy" "unsafe" and
    8.10 +  "domain_isomorphism" "domain" :: thy_decl
    8.11  uses
    8.12    ("Tools/domaindef.ML")
    8.13    ("Tools/Domain/domain_isomorphism.ML")
     9.1 --- a/src/HOL/HOLCF/Fixrec.thy	Thu Mar 15 20:07:00 2012 +0100
     9.2 +++ b/src/HOL/HOLCF/Fixrec.thy	Thu Mar 15 22:08:53 2012 +0100
     9.3 @@ -6,6 +6,7 @@
     9.4  
     9.5  theory Fixrec
     9.6  imports Plain_HOLCF
     9.7 +keywords "fixrec" :: thy_decl
     9.8  uses
     9.9    ("Tools/holcf_library.ML")
    9.10    ("Tools/fixrec.ML")
    10.1 --- a/src/HOL/Hilbert_Choice.thy	Thu Mar 15 20:07:00 2012 +0100
    10.2 +++ b/src/HOL/Hilbert_Choice.thy	Thu Mar 15 22:08:53 2012 +0100
    10.3 @@ -7,6 +7,7 @@
    10.4  
    10.5  theory Hilbert_Choice
    10.6  imports Nat Wellfounded Plain
    10.7 +keywords "specification" "ax_specification" :: thy_goal
    10.8  uses ("Tools/choice_specification.ML")
    10.9  begin
   10.10  
    11.1 --- a/src/HOL/Import/Importer.thy	Thu Mar 15 20:07:00 2012 +0100
    11.2 +++ b/src/HOL/Import/Importer.thy	Thu Mar 15 22:08:53 2012 +0100
    11.3 @@ -4,7 +4,10 @@
    11.4  
    11.5  theory Importer
    11.6  imports Main
    11.7 -keywords ">"
    11.8 +keywords
    11.9 +  "import_segment" "import_theory" "end_import" "setup_theory" "end_setup"
   11.10 +  "setup_dump" "append_dump" "flush_dump" "ignore_thms" "type_maps"
   11.11 +  "def_maps" "thm_maps" "const_renames" "const_moves" "const_maps" :: thy_decl and ">"
   11.12  uses "shuffler.ML" "import_rews.ML" ("proof_kernel.ML") ("replay.ML") ("import.ML")
   11.13  begin
   11.14  
    12.1 --- a/src/HOL/Inductive.thy	Thu Mar 15 20:07:00 2012 +0100
    12.2 +++ b/src/HOL/Inductive.thy	Thu Mar 15 22:08:53 2012 +0100
    12.3 @@ -6,7 +6,11 @@
    12.4  
    12.5  theory Inductive 
    12.6  imports Complete_Lattices
    12.7 -keywords "monos"
    12.8 +keywords
    12.9 +  "inductive" "coinductive" :: thy_decl and
   12.10 +  "inductive_cases" "inductive_simps" :: thy_script and "monos" and
   12.11 +  "rep_datatype" :: thy_goal and
   12.12 +  "primrec" :: thy_decl
   12.13  uses
   12.14    "Tools/dseq.ML"
   12.15    ("Tools/inductive.ML")
    13.1 --- a/src/HOL/Library/Old_Recdef.thy	Thu Mar 15 20:07:00 2012 +0100
    13.2 +++ b/src/HOL/Library/Old_Recdef.thy	Thu Mar 15 22:08:53 2012 +0100
    13.3 @@ -6,7 +6,10 @@
    13.4  
    13.5  theory Old_Recdef
    13.6  imports Wfrec
    13.7 -keywords "recdef" :: thy_decl and "permissive" "congs" "hints"
    13.8 +keywords
    13.9 +  "recdef" "defer_recdef" :: thy_decl and
   13.10 +  "recdef_tc" :: thy_goal and
   13.11 +  "permissive" "congs" "hints"
   13.12  uses
   13.13    ("~~/src/HOL/Tools/TFL/casesplit.ML")
   13.14    ("~~/src/HOL/Tools/TFL/utils.ML")
    14.1 --- a/src/HOL/Metis.thy	Thu Mar 15 20:07:00 2012 +0100
    14.2 +++ b/src/HOL/Metis.thy	Thu Mar 15 22:08:53 2012 +0100
    14.3 @@ -8,6 +8,7 @@
    14.4  
    14.5  theory Metis
    14.6  imports ATP
    14.7 +keywords "try0" :: diag
    14.8  uses "~~/src/Tools/Metis/metis.ML"
    14.9       ("Tools/Metis/metis_generate.ML")
   14.10       ("Tools/Metis/metis_reconstruct.ML")
    15.1 --- a/src/HOL/Nitpick.thy	Thu Mar 15 20:07:00 2012 +0100
    15.2 +++ b/src/HOL/Nitpick.thy	Thu Mar 15 22:08:53 2012 +0100
    15.3 @@ -9,6 +9,7 @@
    15.4  
    15.5  theory Nitpick
    15.6  imports Map Quotient SAT Record
    15.7 +keywords "nitpick" :: diag and "nitpick_params" :: thy_decl
    15.8  uses ("Tools/Nitpick/kodkod.ML")
    15.9       ("Tools/Nitpick/kodkod_sat.ML")
   15.10       ("Tools/Nitpick/nitpick_util.ML")
    16.1 --- a/src/HOL/Nominal/Nominal.thy	Thu Mar 15 20:07:00 2012 +0100
    16.2 +++ b/src/HOL/Nominal/Nominal.thy	Thu Mar 15 22:08:53 2012 +0100
    16.3 @@ -1,6 +1,9 @@
    16.4  theory Nominal 
    16.5  imports Main "~~/src/HOL/Library/Infinite_Set"
    16.6 -keywords "avoids"
    16.7 +keywords
    16.8 +  "atom_decl" "nominal_datatype" "equivariance" :: thy_decl and
    16.9 +  "nominal_primrec" "nominal_inductive" "nominal_inductive2" :: thy_goal and
   16.10 +  "avoids"
   16.11  uses
   16.12    ("nominal_thmdecls.ML")
   16.13    ("nominal_atoms.ML")
    17.1 --- a/src/HOL/Orderings.thy	Thu Mar 15 20:07:00 2012 +0100
    17.2 +++ b/src/HOL/Orderings.thy	Thu Mar 15 22:08:53 2012 +0100
    17.3 @@ -6,6 +6,7 @@
    17.4  
    17.5  theory Orderings
    17.6  imports HOL
    17.7 +keywords "print_orders" :: diag
    17.8  uses
    17.9    "~~/src/Provers/order.ML"
   17.10    "~~/src/Provers/quasi.ML"  (* FIXME unused? *)
    18.1 --- a/src/HOL/Partial_Function.thy	Thu Mar 15 20:07:00 2012 +0100
    18.2 +++ b/src/HOL/Partial_Function.thy	Thu Mar 15 22:08:53 2012 +0100
    18.3 @@ -6,6 +6,7 @@
    18.4  
    18.5  theory Partial_Function
    18.6  imports Complete_Partial_Order Option
    18.7 +keywords "partial_function" :: thy_decl
    18.8  uses 
    18.9    "Tools/Function/function_lib.ML" 
   18.10    "Tools/Function/partial_function.ML" 
    19.1 --- a/src/HOL/Predicate_Compile.thy	Thu Mar 15 20:07:00 2012 +0100
    19.2 +++ b/src/HOL/Predicate_Compile.thy	Thu Mar 15 22:08:53 2012 +0100
    19.3 @@ -6,6 +6,7 @@
    19.4  
    19.5  theory Predicate_Compile
    19.6  imports Predicate New_Random_Sequence Quickcheck_Exhaustive
    19.7 +keywords "code_pred" :: thy_goal and "values" :: diag
    19.8  uses
    19.9    "Tools/Predicate_Compile/predicate_compile_aux.ML"
   19.10    "Tools/Predicate_Compile/predicate_compile_compilations.ML"
    20.1 --- a/src/HOL/Product_Type.thy	Thu Mar 15 20:07:00 2012 +0100
    20.2 +++ b/src/HOL/Product_Type.thy	Thu Mar 15 22:08:53 2012 +0100
    20.3 @@ -7,6 +7,7 @@
    20.4  
    20.5  theory Product_Type
    20.6  imports Typedef Inductive Fun
    20.7 +keywords "inductive_set" "coinductive_set" :: thy_decl
    20.8  uses
    20.9    ("Tools/split_rule.ML")
   20.10    ("Tools/inductive_set.ML")
    21.1 --- a/src/HOL/Quickcheck_Exhaustive.thy	Thu Mar 15 20:07:00 2012 +0100
    21.2 +++ b/src/HOL/Quickcheck_Exhaustive.thy	Thu Mar 15 22:08:53 2012 +0100
    21.3 @@ -4,6 +4,7 @@
    21.4  
    21.5  theory Quickcheck_Exhaustive
    21.6  imports Quickcheck
    21.7 +keywords "quickcheck_generator" :: thy_decl
    21.8  uses
    21.9    ("Tools/Quickcheck/exhaustive_generators.ML")
   21.10    ("Tools/Quickcheck/abstract_generators.ML")
    22.1 --- a/src/HOL/Quickcheck_Narrowing.thy	Thu Mar 15 20:07:00 2012 +0100
    22.2 +++ b/src/HOL/Quickcheck_Narrowing.thy	Thu Mar 15 22:08:53 2012 +0100
    22.3 @@ -4,6 +4,7 @@
    22.4  
    22.5  theory Quickcheck_Narrowing
    22.6  imports Quickcheck_Exhaustive
    22.7 +keywords "find_unused_assms" :: diag
    22.8  uses
    22.9    ("Tools/Quickcheck/PNF_Narrowing_Engine.hs")
   22.10    ("Tools/Quickcheck/Narrowing_Engine.hs")
    23.1 --- a/src/HOL/Quotient.thy	Thu Mar 15 20:07:00 2012 +0100
    23.2 +++ b/src/HOL/Quotient.thy	Thu Mar 15 22:08:53 2012 +0100
    23.3 @@ -6,7 +6,10 @@
    23.4  
    23.5  theory Quotient
    23.6  imports Plain Hilbert_Choice Equiv_Relations
    23.7 -keywords "/"
    23.8 +keywords
    23.9 +  "print_quotmaps" "print_quotients" "print_quotconsts" :: diag and
   23.10 +  "quotient_type" :: thy_goal and "/" and
   23.11 +  "quotient_definition" :: thy_decl
   23.12  uses
   23.13    ("Tools/Quotient/quotient_info.ML")
   23.14    ("Tools/Quotient/quotient_type.ML")
    24.1 --- a/src/HOL/Record.thy	Thu Mar 15 20:07:00 2012 +0100
    24.2 +++ b/src/HOL/Record.thy	Thu Mar 15 22:08:53 2012 +0100
    24.3 @@ -10,6 +10,7 @@
    24.4  
    24.5  theory Record
    24.6  imports Plain Quickcheck_Narrowing
    24.7 +keywords "record" :: thy_decl
    24.8  uses ("Tools/record.ML")
    24.9  begin
   24.10  
    25.1 --- a/src/HOL/Refute.thy	Thu Mar 15 20:07:00 2012 +0100
    25.2 +++ b/src/HOL/Refute.thy	Thu Mar 15 22:08:53 2012 +0100
    25.3 @@ -9,6 +9,7 @@
    25.4  
    25.5  theory Refute
    25.6  imports Hilbert_Choice List Sledgehammer
    25.7 +keywords "refute" :: diag and "refute_params" :: thy_decl
    25.8  uses "Tools/refute.ML"
    25.9  begin
   25.10  
    26.1 --- a/src/HOL/SMT.thy	Thu Mar 15 20:07:00 2012 +0100
    26.2 +++ b/src/HOL/SMT.thy	Thu Mar 15 22:08:53 2012 +0100
    26.3 @@ -6,6 +6,7 @@
    26.4  
    26.5  theory SMT
    26.6  imports Record
    26.7 +keywords "smt_status" :: diag
    26.8  uses
    26.9    "Tools/SMT/smt_utils.ML"
   26.10    "Tools/SMT/smt_failure.ML"
    27.1 --- a/src/HOL/SPARK/SPARK_Setup.thy	Thu Mar 15 20:07:00 2012 +0100
    27.2 +++ b/src/HOL/SPARK/SPARK_Setup.thy	Thu Mar 15 22:08:53 2012 +0100
    27.3 @@ -7,6 +7,9 @@
    27.4  
    27.5  theory SPARK_Setup
    27.6  imports Word
    27.7 +keywords
    27.8 +  "spark_open" "spark_proof_functions" "spark_types" "spark_end" :: thy_decl and
    27.9 +  "spark_vc" :: thy_goal and "spark_status" :: diag
   27.10  uses
   27.11    "Tools/fdl_lexer.ML"
   27.12    "Tools/fdl_parser.ML"
    28.1 --- a/src/HOL/Sledgehammer.thy	Thu Mar 15 20:07:00 2012 +0100
    28.2 +++ b/src/HOL/Sledgehammer.thy	Thu Mar 15 22:08:53 2012 +0100
    28.3 @@ -8,6 +8,7 @@
    28.4  
    28.5  theory Sledgehammer
    28.6  imports ATP SMT
    28.7 +keywords "sledgehammer" :: diag and "sledgehammer_params" :: thy_decl
    28.8  uses "Tools/Sledgehammer/async_manager.ML"
    28.9       "Tools/Sledgehammer/sledgehammer_util.ML"
   28.10       "Tools/Sledgehammer/sledgehammer_filter.ML"
    29.1 --- a/src/HOL/Statespace/StateSpaceLocale.thy	Thu Mar 15 20:07:00 2012 +0100
    29.2 +++ b/src/HOL/Statespace/StateSpaceLocale.thy	Thu Mar 15 22:08:53 2012 +0100
    29.3 @@ -5,6 +5,7 @@
    29.4  header {* Setup for State Space Locales \label{sec:StateSpaceLocale}*}
    29.5  
    29.6  theory StateSpaceLocale imports StateFun 
    29.7 +keywords "statespace" :: thy_decl
    29.8  uses "state_space.ML" "state_fun.ML"
    29.9  begin
   29.10  
    30.1 --- a/src/HOL/TPTP/TPTP_Parser.thy	Thu Mar 15 20:07:00 2012 +0100
    30.2 +++ b/src/HOL/TPTP/TPTP_Parser.thy	Thu Mar 15 22:08:53 2012 +0100
    30.3 @@ -9,6 +9,7 @@
    30.4  
    30.5  theory TPTP_Parser
    30.6  imports Main
    30.7 +keywords "import_tptp" :: diag (* FIXME !? *) 
    30.8  uses
    30.9    "TPTP_Parser/ml_yacc_lib.ML" (*generated from ML-Yacc's lib*)
   30.10  
    31.1 --- a/src/HOL/Typedef.thy	Thu Mar 15 20:07:00 2012 +0100
    31.2 +++ b/src/HOL/Typedef.thy	Thu Mar 15 22:08:53 2012 +0100
    31.3 @@ -6,7 +6,7 @@
    31.4  
    31.5  theory Typedef
    31.6  imports Set
    31.7 -keywords "morphisms"
    31.8 +keywords "typedef" :: thy_goal and "morphisms"
    31.9  uses ("Tools/typedef.ML")
   31.10  begin
   31.11  
    32.1 --- a/src/HOL/ex/Interpretation_with_Defs.thy	Thu Mar 15 20:07:00 2012 +0100
    32.2 +++ b/src/HOL/ex/Interpretation_with_Defs.thy	Thu Mar 15 22:08:53 2012 +0100
    32.3 @@ -6,6 +6,7 @@
    32.4  
    32.5  theory Interpretation_with_Defs
    32.6  imports Pure
    32.7 +keywords "interpretation" :: thy_goal
    32.8  uses "~~/src/Tools/interpretation_with_defs.ML"
    32.9  begin
   32.10  
    33.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Mar 15 20:07:00 2012 +0100
    33.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Mar 15 22:08:53 2012 +0100
    33.3 @@ -21,7 +21,7 @@
    33.4      "constrains", "defines", "fixes", "for", "identifier", "if",
    33.5      "imports", "in", "infix", "infixl", "infixr", "is", "keywords",
    33.6      "notes", "obtains", "open", "output", "overloaded", "pervasive",
    33.7 -    "shows", "structure", "unchecked", "uses", "where", "|", "by"]));
    33.8 +    "shows", "structure", "unchecked", "uses", "where", "|"]));
    33.9  
   33.10  
   33.11  
    34.1 --- a/src/Pure/Isar/keyword.ML	Thu Mar 15 20:07:00 2012 +0100
    34.2 +++ b/src/Pure/Isar/keyword.ML	Thu Mar 15 22:08:53 2012 +0100
    34.3 @@ -48,7 +48,7 @@
    34.4    val status: unit -> unit
    34.5    val keyword: string -> unit
    34.6    val command: string -> T -> unit
    34.7 -  val declare: string * (string * string list) option -> unit
    34.8 +  val declare: string -> T option -> unit
    34.9    val is_diag: string -> bool
   34.10    val is_control: string -> bool
   34.11    val is_regular: string -> bool
   34.12 @@ -215,8 +215,8 @@
   34.13    change_commands (Symtab.update (name, kind));
   34.14    command_status (name, kind));
   34.15  
   34.16 -fun declare (name, NONE) = keyword name
   34.17 -  | declare (name, SOME kind) = command name (make kind);
   34.18 +fun declare name NONE = keyword name
   34.19 +  | declare name (SOME kind) = command name kind;
   34.20  
   34.21  
   34.22  (* command categories *)
    35.1 --- a/src/Pure/Isar/outer_syntax.ML	Thu Mar 15 20:07:00 2012 +0100
    35.2 +++ b/src/Pure/Isar/outer_syntax.ML	Thu Mar 15 22:08:53 2012 +0100
    35.3 @@ -123,11 +123,23 @@
    35.4  val global_outer_syntax = Unsynchronized.ref empty_outer_syntax;
    35.5  
    35.6  fun add_command name kind cmd = CRITICAL (fn () =>
    35.7 - (Keyword.command name kind;
    35.8 -  Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
    35.9 -   (if not (Symtab.defined commands name) then ()
   35.10 -    else warning ("Redefining outer syntax command " ^ quote name);
   35.11 -    Symtab.update (name, cmd) commands)))));
   35.12 +  let
   35.13 +    val thy = ML_Context.the_global_context ();
   35.14 +    val _ =
   35.15 +      (case try (Thy_Header.the_keyword thy) name of
   35.16 +        SOME k =>
   35.17 +          if k = SOME kind then ()
   35.18 +          else error ("Inconsistent outer syntax keyword declaration " ^ quote name)
   35.19 +      | NONE =>
   35.20 +          (Keyword.command name kind;
   35.21 +           if Context.theory_name thy = Context.PureN then ()
   35.22 +           else error ("Undeclared outer syntax command " ^ quote name)));
   35.23 +  in
   35.24 +    Unsynchronized.change global_outer_syntax (map_commands (fn commands =>
   35.25 +     (if not (Symtab.defined commands name) then ()
   35.26 +      else warning ("Redefining outer syntax command " ^ quote name);
   35.27 +      Symtab.update (name, cmd) commands)))
   35.28 +  end);
   35.29  
   35.30  in
   35.31  
    36.1 --- a/src/Pure/PIDE/document.ML	Thu Mar 15 20:07:00 2012 +0100
    36.2 +++ b/src/Pure/PIDE/document.ML	Thu Mar 15 22:08:53 2012 +0100
    36.3 @@ -215,7 +215,8 @@
    36.4            val imports = (case header of Exn.Res (_, {imports, ...}) => imports | _ => []);
    36.5            val keywords = (case header of Exn.Res (_, {keywords, ...}) => keywords | _ => []);
    36.6            val header' =
    36.7 -            (List.app Keyword.declare keywords; header)
    36.8 +            (List.app (fn (name, decl) =>
    36.9 +                Keyword.declare name (Option.map Keyword.make decl)) keywords; header)
   36.10                handle exn as ERROR _ => Exn.Exn exn;
   36.11            val nodes1 = nodes
   36.12              |> default_node name
    37.1 --- a/src/Pure/Thy/thy_header.ML	Thu Mar 15 20:07:00 2012 +0100
    37.2 +++ b/src/Pure/Thy/thy_header.ML	Thu Mar 15 22:08:53 2012 +0100
    37.3 @@ -43,15 +43,15 @@
    37.4    fun merge data : T = Symtab.merge (op =) data handle Symtab.DUP name => err_dup name;
    37.5  );
    37.6  
    37.7 -fun declare_keyword (name, kind) =
    37.8 -  Data.map (fn data =>
    37.9 -   (if is_none kind then Keyword.keyword name else ();
   37.10 -    Symtab.update_new (name, Option.map Keyword.make kind) data
   37.11 -      handle Symtab.DUP name => err_dup name));
   37.12 +fun declare_keyword (name, decl) = Data.map (fn data =>
   37.13 +  let
   37.14 +    val kind = Option.map Keyword.make decl;
   37.15 +    val _ = Keyword.declare name kind;
   37.16 +  in Symtab.update_new (name, kind) data handle Symtab.DUP name => err_dup name end);
   37.17  
   37.18  fun the_keyword thy name =
   37.19    (case Symtab.lookup (Data.get thy) name of
   37.20 -    SOME decl => decl
   37.21 +    SOME kind => kind
   37.22    | NONE => error ("Unknown outer syntax keyword " ^ quote name));
   37.23  
   37.24  
    38.1 --- a/src/Pure/Thy/thy_output.ML	Thu Mar 15 20:07:00 2012 +0100
    38.2 +++ b/src/Pure/Thy/thy_output.ML	Thu Mar 15 22:08:53 2012 +0100
    38.3 @@ -626,6 +626,8 @@
    38.4  
    38.5  (* embedded lemma *)
    38.6  
    38.7 +val _ = Keyword.keyword "by";
    38.8 +
    38.9  val _ =
   38.10    Context.>> (Context.map_theory
   38.11     (antiquotation (Binding.name "lemma")
    39.1 --- a/src/Tools/Code_Generator.thy	Thu Mar 15 20:07:00 2012 +0100
    39.2 +++ b/src/Tools/Code_Generator.thy	Thu Mar 15 22:08:53 2012 +0100
    39.3 @@ -6,7 +6,13 @@
    39.4  
    39.5  theory Code_Generator
    39.6  imports Pure
    39.7 -keywords "datatypes" "functions" "module_name" "file" "checking"
    39.8 +keywords
    39.9 +  "try" "solve_direct" "quickcheck" "value" "print_codeproc"
   39.10 +    "code_thms" "code_deps" "export_code" :: diag and
   39.11 +  "quickcheck_params" "code_class" "code_instance" "code_type"
   39.12 +    "code_const" "code_reserved" "code_include" "code_modulename"
   39.13 +    "code_abort" "code_monad" "code_reflect" :: thy_decl and
   39.14 +  "datatypes" "functions" "module_name" "file" "checking"
   39.15  uses
   39.16    "~~/src/Tools/misc_legacy.ML"
   39.17    "~~/src/Tools/cache_io.ML"
    40.1 --- a/src/ZF/Datatype_ZF.thy	Thu Mar 15 20:07:00 2012 +0100
    40.2 +++ b/src/ZF/Datatype_ZF.thy	Thu Mar 15 22:08:53 2012 +0100
    40.3 @@ -7,6 +7,7 @@
    40.4  
    40.5  theory Datatype_ZF
    40.6  imports Inductive_ZF Univ QUniv
    40.7 +keywords "datatype" "codatatype" :: thy_decl
    40.8  uses "Tools/datatype_package.ML"
    40.9  begin
   40.10  
    41.1 --- a/src/ZF/Inductive_ZF.thy	Thu Mar 15 20:07:00 2012 +0100
    41.2 +++ b/src/ZF/Inductive_ZF.thy	Thu Mar 15 22:08:53 2012 +0100
    41.3 @@ -14,8 +14,10 @@
    41.4  theory Inductive_ZF
    41.5  imports Fixedpt QPair Nat_ZF
    41.6  keywords
    41.7 +  "inductive" "coinductive" "rep_datatype" "primrec" :: thy_decl and
    41.8 +  "inductive_cases" :: thy_script and
    41.9 +  "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
   41.10    "elimination" "induction" "case_eqns" "recursor_eqns"
   41.11 -  "domains" "intros" "monos" "con_defs" "type_intros" "type_elims"
   41.12  uses
   41.13    ("ind_syntax.ML")
   41.14    ("Tools/cartprod.ML")
    42.1 --- a/src/ZF/upair.thy	Thu Mar 15 20:07:00 2012 +0100
    42.2 +++ b/src/ZF/upair.thy	Thu Mar 15 22:08:53 2012 +0100
    42.3 @@ -11,8 +11,11 @@
    42.4  
    42.5  header{*Unordered Pairs*}
    42.6  
    42.7 -theory upair imports ZF
    42.8 -uses "Tools/typechk.ML" begin
    42.9 +theory upair
   42.10 +imports ZF
   42.11 +keywords "print_tcset" :: diag
   42.12 +uses "Tools/typechk.ML"
   42.13 +begin
   42.14  
   42.15  setup TypeCheck.setup
   42.16