discontinued pointless warnings: commands are only defined inside a theory context;
authorwenzelm
Thu Apr 16 15:22:44 2015 +0200 (2015-04-16)
changeset 60097d20ca79d50e4
parent 60096 7b98dbc1d13e
child 60098 3c66b0a9d7b0
discontinued pointless warnings: commands are only defined inside a theory context;
src/HOL/Orderings.thy
src/HOL/Tools/inductive.ML
src/Provers/classical.ML
src/Pure/Isar/calculation.ML
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
src/Pure/Isar/toplevel.ML
src/Pure/Tools/class_deps.ML
src/Pure/Tools/thm_deps.ML
src/Pure/Tools/thy_deps.ML
src/Tools/Code/code_preproc.ML
src/Tools/Code/code_thingol.ML
src/Tools/induct.ML
src/ZF/Tools/typechk.ML
     1.1 --- a/src/HOL/Orderings.thy	Thu Apr 16 15:11:04 2015 +0200
     1.2 +++ b/src/HOL/Orderings.thy	Thu Apr 16 15:22:44 2015 +0200
     1.3 @@ -441,8 +441,7 @@
     1.4  val _ =
     1.5    Outer_Syntax.command @{command_keyword print_orders}
     1.6      "print order structures available to transitivity reasoner"
     1.7 -    (Scan.succeed (Toplevel.unknown_context o
     1.8 -      Toplevel.keep (print_structures o Toplevel.context_of)));
     1.9 +    (Scan.succeed (Toplevel.keep (print_structures o Toplevel.context_of)));
    1.10  
    1.11  
    1.12  (* tactics *)
     2.1 --- a/src/HOL/Tools/inductive.ML	Thu Apr 16 15:11:04 2015 +0200
     2.2 +++ b/src/HOL/Tools/inductive.ML	Thu Apr 16 15:22:44 2015 +0200
     2.3 @@ -1190,7 +1190,6 @@
     2.4  val _ =
     2.5    Outer_Syntax.command @{command_keyword print_inductives}
     2.6      "print (co)inductive definitions and monotonicity rules"
     2.7 -    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
     2.8 -      Toplevel.keep (print_inductives b o Toplevel.context_of)));
     2.9 +    (Parse.opt_bang >> (fn b => Toplevel.keep (print_inductives b o Toplevel.context_of)));
    2.10  
    2.11  end;
     3.1 --- a/src/Provers/classical.ML	Thu Apr 16 15:11:04 2015 +0200
     3.2 +++ b/src/Provers/classical.ML	Thu Apr 16 15:22:44 2015 +0200
     3.3 @@ -980,6 +980,6 @@
     3.4  
     3.5  val _ =
     3.6    Outer_Syntax.command @{command_keyword print_claset} "print context of Classical Reasoner"
     3.7 -    (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_claset o Toplevel.context_of)));
     3.8 +    (Scan.succeed (Toplevel.keep (print_claset o Toplevel.context_of)));
     3.9  
    3.10  end;
     4.1 --- a/src/Pure/Isar/calculation.ML	Thu Apr 16 15:11:04 2015 +0200
     4.2 +++ b/src/Pure/Isar/calculation.ML	Thu Apr 16 15:22:44 2015 +0200
     4.3 @@ -230,6 +230,6 @@
     4.4  
     4.5  val _ =
     4.6    Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules"
     4.7 -    (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_rules o Toplevel.context_of)));
     4.8 +    (Scan.succeed (Toplevel.keep (print_rules o Toplevel.context_of)));
     4.9  
    4.10  end;
     5.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 15:11:04 2015 +0200
     5.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 15:22:44 2015 +0200
     5.3 @@ -267,7 +267,6 @@
     5.4  (* display dependencies *)
     5.5  
     5.6  val locale_deps =
     5.7 -  Toplevel.unknown_theory o
     5.8    Toplevel.keep (Toplevel.theory_of #> (fn thy =>
     5.9      Locale.pretty_locale_deps thy
    5.10      |> map (fn {name, parents, body} =>
     6.1 --- a/src/Pure/Isar/isar_syn.ML	Thu Apr 16 15:11:04 2015 +0200
     6.2 +++ b/src/Pure/Isar/isar_syn.ML	Thu Apr 16 15:22:44 2015 +0200
     6.3 @@ -350,8 +350,7 @@
     6.4  val _ =
     6.5    Outer_Syntax.command @{command_keyword print_bundles}
     6.6      "print bundles of declarations"
     6.7 -    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
     6.8 -      Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
     6.9 +    (Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
    6.10  
    6.11  
    6.12  (* local theories *)
    6.13 @@ -693,8 +692,7 @@
    6.14  
    6.15  val _ =
    6.16    Outer_Syntax.command @{command_keyword print_options} "print configuration options"
    6.17 -    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
    6.18 -      Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
    6.19 +    (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
    6.20  
    6.21  val _ =
    6.22    Outer_Syntax.command @{command_keyword print_context}
    6.23 @@ -704,99 +702,89 @@
    6.24  val _ =
    6.25    Outer_Syntax.command @{command_keyword print_theory}
    6.26      "print logical theory contents"
    6.27 -    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
    6.28 +    (Parse.opt_bang >> (fn b =>
    6.29        Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of)));
    6.30  
    6.31  val _ =
    6.32    Outer_Syntax.command @{command_keyword print_syntax}
    6.33      "print inner syntax of context"
    6.34 -    (Scan.succeed (Toplevel.unknown_context o
    6.35 -      Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
    6.36 +    (Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
    6.37  
    6.38  val _ =
    6.39    Outer_Syntax.command @{command_keyword print_defn_rules}
    6.40      "print definitional rewrite rules of context"
    6.41 -    (Scan.succeed (Toplevel.unknown_context o
    6.42 -      Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
    6.43 +    (Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
    6.44  
    6.45  val _ =
    6.46    Outer_Syntax.command @{command_keyword print_abbrevs}
    6.47      "print constant abbreviations of context"
    6.48 -    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
    6.49 +    (Parse.opt_bang >> (fn b =>
    6.50        Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of)));
    6.51  
    6.52  val _ =
    6.53    Outer_Syntax.command @{command_keyword print_theorems}
    6.54      "print theorems of local theory or proof context"
    6.55      (Parse.opt_bang >> (fn b =>
    6.56 -      Toplevel.unknown_context o
    6.57        Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
    6.58  
    6.59  val _ =
    6.60    Outer_Syntax.command @{command_keyword print_locales}
    6.61      "print locales of this theory"
    6.62 -    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
    6.63 +    (Parse.opt_bang >> (fn b =>
    6.64        Toplevel.keep (Locale.print_locales b o Toplevel.theory_of)));
    6.65  
    6.66  val _ =
    6.67    Outer_Syntax.command @{command_keyword print_classes}
    6.68      "print classes of this theory"
    6.69 -    (Scan.succeed (Toplevel.unknown_theory o
    6.70 -      Toplevel.keep (Class.print_classes o Toplevel.context_of)));
    6.71 +    (Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of)));
    6.72  
    6.73  val _ =
    6.74    Outer_Syntax.command @{command_keyword print_locale}
    6.75      "print locale of this theory"
    6.76      (Parse.opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
    6.77 -      Toplevel.unknown_theory o
    6.78        Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
    6.79  
    6.80  val _ =
    6.81    Outer_Syntax.command @{command_keyword print_interps}
    6.82      "print interpretations of locale for this theory or proof context"
    6.83      (Parse.position Parse.xname >> (fn name =>
    6.84 -      Toplevel.unknown_context o
    6.85        Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
    6.86  
    6.87  val _ =
    6.88    Outer_Syntax.command @{command_keyword print_dependencies}
    6.89      "print dependencies of locale expression"
    6.90      (Parse.opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) =>
    6.91 -      Toplevel.unknown_context o
    6.92        Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
    6.93  
    6.94  val _ =
    6.95    Outer_Syntax.command @{command_keyword print_attributes}
    6.96      "print attributes of this theory"
    6.97 -    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
    6.98 -      Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
    6.99 +    (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
   6.100  
   6.101  val _ =
   6.102    Outer_Syntax.command @{command_keyword print_simpset}
   6.103      "print context of Simplifier"
   6.104 -    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
   6.105 +    (Parse.opt_bang >> (fn b =>
   6.106        Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of)));
   6.107  
   6.108  val _ =
   6.109    Outer_Syntax.command @{command_keyword print_rules} "print intro/elim rules"
   6.110 -    (Scan.succeed (Toplevel.unknown_context o
   6.111 -      Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
   6.112 +    (Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
   6.113  
   6.114  val _ =
   6.115    Outer_Syntax.command @{command_keyword print_methods} "print methods of this theory"
   6.116 -    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
   6.117 -      Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
   6.118 +    (Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
   6.119  
   6.120  val _ =
   6.121    Outer_Syntax.command @{command_keyword print_antiquotations}
   6.122      "print document antiquotations"
   6.123 -    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
   6.124 +    (Parse.opt_bang >> (fn b =>
   6.125        Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of)));
   6.126  
   6.127  val _ =
   6.128    Outer_Syntax.command @{command_keyword print_ML_antiquotations}
   6.129      "print ML antiquotations"
   6.130 -    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
   6.131 +    (Parse.opt_bang >> (fn b =>
   6.132        Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of)));
   6.133  
   6.134  val _ =
   6.135 @@ -806,19 +794,19 @@
   6.136  val _ =
   6.137    Outer_Syntax.command @{command_keyword print_term_bindings}
   6.138      "print term bindings of proof context"
   6.139 -    (Scan.succeed (Toplevel.unknown_context o
   6.140 -      Toplevel.keep
   6.141 +    (Scan.succeed
   6.142 +      (Toplevel.keep
   6.143          (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
   6.144  
   6.145  val _ =
   6.146    Outer_Syntax.command @{command_keyword print_facts} "print facts of proof context"
   6.147 -    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
   6.148 +    (Parse.opt_bang >> (fn b =>
   6.149        Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of)));
   6.150  
   6.151  val _ =
   6.152    Outer_Syntax.command @{command_keyword print_cases} "print cases of proof context"
   6.153 -    (Scan.succeed (Toplevel.unknown_context o
   6.154 -      Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
   6.155 +    (Scan.succeed
   6.156 +      (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
   6.157  
   6.158  val _ =
   6.159    Outer_Syntax.command @{command_keyword print_statement}
   6.160 @@ -852,8 +840,7 @@
   6.161  
   6.162  val _ =
   6.163    Outer_Syntax.command @{command_keyword print_codesetup} "print code generator setup"
   6.164 -    (Scan.succeed (Toplevel.unknown_theory o
   6.165 -      Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
   6.166 +    (Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
   6.167  
   6.168  val _ =
   6.169    Outer_Syntax.command @{command_keyword print_state}
     7.1 --- a/src/Pure/Isar/toplevel.ML	Thu Apr 16 15:11:04 2015 +0200
     7.2 +++ b/src/Pure/Isar/toplevel.ML	Thu Apr 16 15:22:44 2015 +0200
     7.3 @@ -72,8 +72,6 @@
     7.4    val skip_proof: (int -> int) -> transition -> transition
     7.5    val skip_proof_to_theory: (int -> bool) -> transition -> transition
     7.6    val exec_id: Document_ID.exec -> transition -> transition
     7.7 -  val unknown_theory: transition -> transition
     7.8 -  val unknown_context: transition -> transition
     7.9    val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
    7.10    val add_hook: (transition -> state -> state -> unit) -> unit
    7.11    val get_timing: transition -> Time.time option
    7.12 @@ -355,9 +353,6 @@
    7.13  fun malformed pos msg =
    7.14    empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg);
    7.15  
    7.16 -val unknown_theory = imperative (fn () => warning "Unknown theory context");
    7.17 -val unknown_context = imperative (fn () => warning "Unknown context");
    7.18 -
    7.19  
    7.20  (* theory transitions *)
    7.21  
     8.1 --- a/src/Pure/Tools/class_deps.ML	Thu Apr 16 15:11:04 2015 +0200
     8.2 +++ b/src/Pure/Tools/class_deps.ML	Thu Apr 16 15:22:44 2015 +0200
     8.3 @@ -44,7 +44,6 @@
     8.4  val _ =
     8.5    Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies"
     8.6      (Scan.option class_bounds -- Scan.option class_bounds >> (fn args =>
     8.7 -      (Toplevel.unknown_theory o
     8.8 -       Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) args))));
     8.9 +      Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) args)));
    8.10  
    8.11  end;
     9.1 --- a/src/Pure/Tools/thm_deps.ML	Thu Apr 16 15:11:04 2015 +0200
     9.2 +++ b/src/Pure/Tools/thm_deps.ML	Thu Apr 16 15:22:44 2015 +0200
     9.3 @@ -50,8 +50,8 @@
     9.4  val _ =
     9.5    Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
     9.6      (Parse.xthms1 >> (fn args =>
     9.7 -      Toplevel.unknown_theory o Toplevel.keep (fn state =>
     9.8 -        thm_deps (Toplevel.theory_of state) (Attrib.eval_thms (Toplevel.context_of state) args))));
     9.9 +      Toplevel.keep (fn st =>
    9.10 +        thm_deps (Toplevel.theory_of st) (Attrib.eval_thms (Toplevel.context_of st) args))));
    9.11  
    9.12  
    9.13  (* unused_thms *)
    10.1 --- a/src/Pure/Tools/thy_deps.ML	Thu Apr 16 15:11:04 2015 +0200
    10.2 +++ b/src/Pure/Tools/thy_deps.ML	Thu Apr 16 15:22:44 2015 +0200
    10.3 @@ -43,8 +43,7 @@
    10.4  
    10.5  val _ =
    10.6    Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
    10.7 -    (Scan.option theory_bounds -- Scan.option theory_bounds >> (fn args =>
    10.8 -      (Toplevel.unknown_theory o
    10.9 -       Toplevel.keep (fn st => thy_deps_cmd (Toplevel.theory_of st) args))));
   10.10 +    (Scan.option theory_bounds -- Scan.option theory_bounds >>
   10.11 +      (fn args => Toplevel.keep (fn st => thy_deps_cmd (Toplevel.theory_of st) args)));
   10.12  
   10.13  end;
    11.1 --- a/src/Tools/Code/code_preproc.ML	Thu Apr 16 15:11:04 2015 +0200
    11.2 +++ b/src/Tools/Code/code_preproc.ML	Thu Apr 16 15:22:44 2015 +0200
    11.3 @@ -589,6 +589,6 @@
    11.4  
    11.5  val _ =
    11.6    Outer_Syntax.command @{command_keyword print_codeproc} "print code preprocessor setup"
    11.7 -    (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_codeproc o Toplevel.context_of)));
    11.8 +    (Scan.succeed (Toplevel.keep (print_codeproc o Toplevel.context_of)));
    11.9  
   11.10  end; (*struct*)
    12.1 --- a/src/Tools/Code/code_thingol.ML	Thu Apr 16 15:11:04 2015 +0200
    12.2 +++ b/src/Tools/Code/code_thingol.ML	Thu Apr 16 15:22:44 2015 +0200
    12.3 @@ -960,14 +960,12 @@
    12.4    Outer_Syntax.command @{command_keyword code_thms}
    12.5      "print system of code equations for code"
    12.6      (Scan.repeat1 Parse.term >> (fn cs =>
    12.7 -      Toplevel.unknown_context o
    12.8 -      Toplevel.keep (fn state => code_thms_cmd (Toplevel.context_of state) cs)));
    12.9 +      Toplevel.keep (fn st => code_thms_cmd (Toplevel.context_of st) cs)));
   12.10  
   12.11  val _ =
   12.12    Outer_Syntax.command @{command_keyword code_deps}
   12.13      "visualize dependencies of code equations for code"
   12.14      (Scan.repeat1 Parse.term >> (fn cs =>
   12.15 -      Toplevel.unknown_context o
   12.16        Toplevel.keep (fn st => code_deps_cmd (Toplevel.context_of st) cs)));
   12.17  
   12.18  end;
    13.1 --- a/src/Tools/induct.ML	Thu Apr 16 15:11:04 2015 +0200
    13.2 +++ b/src/Tools/induct.ML	Thu Apr 16 15:22:44 2015 +0200
    13.3 @@ -257,8 +257,7 @@
    13.4  val _ =
    13.5    Outer_Syntax.command @{command_keyword print_induct_rules}
    13.6      "print induction and cases rules"
    13.7 -    (Scan.succeed (Toplevel.unknown_context o
    13.8 -      Toplevel.keep (print_rules o Toplevel.context_of)));
    13.9 +    (Scan.succeed (Toplevel.keep (print_rules o Toplevel.context_of)));
   13.10  
   13.11  
   13.12  (* access rules *)
    14.1 --- a/src/ZF/Tools/typechk.ML	Thu Apr 16 15:11:04 2015 +0200
    14.2 +++ b/src/ZF/Tools/typechk.ML	Thu Apr 16 15:22:44 2015 +0200
    14.3 @@ -127,7 +127,6 @@
    14.4  
    14.5  val _ =
    14.6    Outer_Syntax.command @{command_keyword print_tcset} "print context of ZF typecheck"
    14.7 -    (Scan.succeed (Toplevel.unknown_context o
    14.8 -      Toplevel.keep (print_tcset o Toplevel.context_of)));
    14.9 +    (Scan.succeed (Toplevel.keep (print_tcset o Toplevel.context_of)));
   14.10  
   14.11  end;