# HG changeset patch
# User wenzelm
# Date 1429190564 -7200
# Node ID d20ca79d50e4ca7262e0fde89eb79db75f943198
# Parent  7b98dbc1d13efe75e9c9ce8fd3c76f0ecc4f6849
discontinued pointless warnings: commands are only defined inside a theory context;

diff -r 7b98dbc1d13e -r d20ca79d50e4 src/HOL/Orderings.thy
--- a/src/HOL/Orderings.thy	Thu Apr 16 15:11:04 2015 +0200
+++ b/src/HOL/Orderings.thy	Thu Apr 16 15:22:44 2015 +0200
@@ -441,8 +441,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword print_orders}
     "print order structures available to transitivity reasoner"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (print_structures o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (print_structures o Toplevel.context_of)));
 
 
 (* tactics *)
diff -r 7b98dbc1d13e -r d20ca79d50e4 src/HOL/Tools/inductive.ML
--- a/src/HOL/Tools/inductive.ML	Thu Apr 16 15:11:04 2015 +0200
+++ b/src/HOL/Tools/inductive.ML	Thu Apr 16 15:22:44 2015 +0200
@@ -1190,7 +1190,6 @@
 val _ =
   Outer_Syntax.command @{command_keyword print_inductives}
     "print (co)inductive definitions and monotonicity rules"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
-      Toplevel.keep (print_inductives b o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.keep (print_inductives b o Toplevel.context_of)));
 
 end;
diff -r 7b98dbc1d13e -r d20ca79d50e4 src/Provers/classical.ML
--- a/src/Provers/classical.ML	Thu Apr 16 15:11:04 2015 +0200
+++ b/src/Provers/classical.ML	Thu Apr 16 15:22:44 2015 +0200
@@ -980,6 +980,6 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword print_claset} "print context of Classical Reasoner"
-    (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_claset o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (print_claset o Toplevel.context_of)));
 
 end;
diff -r 7b98dbc1d13e -r d20ca79d50e4 src/Pure/Isar/calculation.ML
--- a/src/Pure/Isar/calculation.ML	Thu Apr 16 15:11:04 2015 +0200
+++ b/src/Pure/Isar/calculation.ML	Thu Apr 16 15:22:44 2015 +0200
@@ -230,6 +230,6 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword print_trans_rules} "print transitivity rules"
-    (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_rules o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (print_rules o Toplevel.context_of)));
 
 end;
diff -r 7b98dbc1d13e -r d20ca79d50e4 src/Pure/Isar/isar_cmd.ML
--- a/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 15:11:04 2015 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Thu Apr 16 15:22:44 2015 +0200
@@ -267,7 +267,6 @@
 (* display dependencies *)
 
 val locale_deps =
-  Toplevel.unknown_theory o
   Toplevel.keep (Toplevel.theory_of #> (fn thy =>
     Locale.pretty_locale_deps thy
     |> map (fn {name, parents, body} =>
diff -r 7b98dbc1d13e -r d20ca79d50e4 src/Pure/Isar/isar_syn.ML
--- a/src/Pure/Isar/isar_syn.ML	Thu Apr 16 15:11:04 2015 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Thu Apr 16 15:22:44 2015 +0200
@@ -350,8 +350,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword print_bundles}
     "print bundles of declarations"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
-      Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.keep (Bundle.print_bundles b o Toplevel.context_of)));
 
 
 (* local theories *)
@@ -693,8 +692,7 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword print_options} "print configuration options"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
-      Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_options b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_context}
@@ -704,99 +702,89 @@
 val _ =
   Outer_Syntax.command @{command_keyword print_theory}
     "print logical theory contents"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
+    (Parse.opt_bang >> (fn b =>
       Toplevel.keep (Pretty.writeln o Proof_Display.pretty_full_theory b o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_syntax}
     "print inner syntax of context"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (Proof_Context.print_syntax o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_defn_rules}
     "print definitional rewrite rules of context"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (Local_Defs.print_rules o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_abbrevs}
     "print constant abbreviations of context"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+    (Parse.opt_bang >> (fn b =>
       Toplevel.keep (Proof_Context.print_abbrevs b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_theorems}
     "print theorems of local theory or proof context"
     (Parse.opt_bang >> (fn b =>
-      Toplevel.unknown_context o
       Toplevel.keep (Pretty.writeln o Pretty.chunks o Isar_Cmd.pretty_theorems b)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_locales}
     "print locales of this theory"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
+    (Parse.opt_bang >> (fn b =>
       Toplevel.keep (Locale.print_locales b o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_classes}
     "print classes of this theory"
-    (Scan.succeed (Toplevel.unknown_theory o
-      Toplevel.keep (Class.print_classes o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (Class.print_classes o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_locale}
     "print locale of this theory"
     (Parse.opt_bang -- Parse.position Parse.xname >> (fn (b, name) =>
-      Toplevel.unknown_theory o
       Toplevel.keep (fn state => Locale.print_locale (Toplevel.theory_of state) b name)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_interps}
     "print interpretations of locale for this theory or proof context"
     (Parse.position Parse.xname >> (fn name =>
-      Toplevel.unknown_context o
       Toplevel.keep (fn state => Locale.print_registrations (Toplevel.context_of state) name)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_dependencies}
     "print dependencies of locale expression"
     (Parse.opt_bang -- Parse_Spec.locale_expression true >> (fn (b, expr) =>
-      Toplevel.unknown_context o
       Toplevel.keep (fn state => Expression.print_dependencies (Toplevel.context_of state) b expr)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_attributes}
     "print attributes of this theory"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
-      Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.keep (Attrib.print_attributes b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_simpset}
     "print context of Simplifier"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+    (Parse.opt_bang >> (fn b =>
       Toplevel.keep (Pretty.writeln o Simplifier.pretty_simpset b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_rules} "print intro/elim rules"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (Context_Rules.print_rules o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_methods} "print methods of this theory"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_theory o
-      Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
+    (Parse.opt_bang >> (fn b => Toplevel.keep (Method.print_methods b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_antiquotations}
     "print document antiquotations"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+    (Parse.opt_bang >> (fn b =>
       Toplevel.keep (Thy_Output.print_antiquotations b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_ML_antiquotations}
     "print ML antiquotations"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+    (Parse.opt_bang >> (fn b =>
       Toplevel.keep (ML_Context.print_antiquotations b o Toplevel.context_of)));
 
 val _ =
@@ -806,19 +794,19 @@
 val _ =
   Outer_Syntax.command @{command_keyword print_term_bindings}
     "print term bindings of proof context"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep
+    (Scan.succeed
+      (Toplevel.keep
         (Pretty.writeln_chunks o Proof_Context.pretty_term_bindings o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_facts} "print facts of proof context"
-    (Parse.opt_bang >> (fn b => Toplevel.unknown_context o
+    (Parse.opt_bang >> (fn b =>
       Toplevel.keep (Proof_Context.print_local_facts b o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_cases} "print cases of proof context"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
+    (Scan.succeed
+      (Toplevel.keep (Pretty.writeln_chunks o Proof_Context.pretty_cases o Toplevel.context_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_statement}
@@ -852,8 +840,7 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword print_codesetup} "print code generator setup"
-    (Scan.succeed (Toplevel.unknown_theory o
-      Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
+    (Scan.succeed (Toplevel.keep (Code.print_codesetup o Toplevel.theory_of)));
 
 val _ =
   Outer_Syntax.command @{command_keyword print_state}
diff -r 7b98dbc1d13e -r d20ca79d50e4 src/Pure/Isar/toplevel.ML
--- a/src/Pure/Isar/toplevel.ML	Thu Apr 16 15:11:04 2015 +0200
+++ b/src/Pure/Isar/toplevel.ML	Thu Apr 16 15:22:44 2015 +0200
@@ -72,8 +72,6 @@
   val skip_proof: (int -> int) -> transition -> transition
   val skip_proof_to_theory: (int -> bool) -> transition -> transition
   val exec_id: Document_ID.exec -> transition -> transition
-  val unknown_theory: transition -> transition
-  val unknown_context: transition -> transition
   val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b
   val add_hook: (transition -> state -> state -> unit) -> unit
   val get_timing: transition -> Time.time option
@@ -355,9 +353,6 @@
 fun malformed pos msg =
   empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg);
 
-val unknown_theory = imperative (fn () => warning "Unknown theory context");
-val unknown_context = imperative (fn () => warning "Unknown context");
-
 
 (* theory transitions *)
 
diff -r 7b98dbc1d13e -r d20ca79d50e4 src/Pure/Tools/class_deps.ML
--- a/src/Pure/Tools/class_deps.ML	Thu Apr 16 15:11:04 2015 +0200
+++ b/src/Pure/Tools/class_deps.ML	Thu Apr 16 15:22:44 2015 +0200
@@ -44,7 +44,6 @@
 val _ =
   Outer_Syntax.command @{command_keyword class_deps} "visualize class dependencies"
     (Scan.option class_bounds -- Scan.option class_bounds >> (fn args =>
-      (Toplevel.unknown_theory o
-       Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) args))));
+      Toplevel.keep (fn st => class_deps_cmd (Toplevel.context_of st) args)));
 
 end;
diff -r 7b98dbc1d13e -r d20ca79d50e4 src/Pure/Tools/thm_deps.ML
--- a/src/Pure/Tools/thm_deps.ML	Thu Apr 16 15:11:04 2015 +0200
+++ b/src/Pure/Tools/thm_deps.ML	Thu Apr 16 15:22:44 2015 +0200
@@ -50,8 +50,8 @@
 val _ =
   Outer_Syntax.command @{command_keyword thm_deps} "visualize theorem dependencies"
     (Parse.xthms1 >> (fn args =>
-      Toplevel.unknown_theory o Toplevel.keep (fn state =>
-        thm_deps (Toplevel.theory_of state) (Attrib.eval_thms (Toplevel.context_of state) args))));
+      Toplevel.keep (fn st =>
+        thm_deps (Toplevel.theory_of st) (Attrib.eval_thms (Toplevel.context_of st) args))));
 
 
 (* unused_thms *)
diff -r 7b98dbc1d13e -r d20ca79d50e4 src/Pure/Tools/thy_deps.ML
--- a/src/Pure/Tools/thy_deps.ML	Thu Apr 16 15:11:04 2015 +0200
+++ b/src/Pure/Tools/thy_deps.ML	Thu Apr 16 15:22:44 2015 +0200
@@ -43,8 +43,7 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword thy_deps} "visualize theory dependencies"
-    (Scan.option theory_bounds -- Scan.option theory_bounds >> (fn args =>
-      (Toplevel.unknown_theory o
-       Toplevel.keep (fn st => thy_deps_cmd (Toplevel.theory_of st) args))));
+    (Scan.option theory_bounds -- Scan.option theory_bounds >>
+      (fn args => Toplevel.keep (fn st => thy_deps_cmd (Toplevel.theory_of st) args)));
 
 end;
diff -r 7b98dbc1d13e -r d20ca79d50e4 src/Tools/Code/code_preproc.ML
--- a/src/Tools/Code/code_preproc.ML	Thu Apr 16 15:11:04 2015 +0200
+++ b/src/Tools/Code/code_preproc.ML	Thu Apr 16 15:22:44 2015 +0200
@@ -589,6 +589,6 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword print_codeproc} "print code preprocessor setup"
-    (Scan.succeed (Toplevel.unknown_context o Toplevel.keep (print_codeproc o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (print_codeproc o Toplevel.context_of)));
 
 end; (*struct*)
diff -r 7b98dbc1d13e -r d20ca79d50e4 src/Tools/Code/code_thingol.ML
--- a/src/Tools/Code/code_thingol.ML	Thu Apr 16 15:11:04 2015 +0200
+++ b/src/Tools/Code/code_thingol.ML	Thu Apr 16 15:22:44 2015 +0200
@@ -960,14 +960,12 @@
   Outer_Syntax.command @{command_keyword code_thms}
     "print system of code equations for code"
     (Scan.repeat1 Parse.term >> (fn cs =>
-      Toplevel.unknown_context o
-      Toplevel.keep (fn state => code_thms_cmd (Toplevel.context_of state) cs)));
+      Toplevel.keep (fn st => code_thms_cmd (Toplevel.context_of st) cs)));
 
 val _ =
   Outer_Syntax.command @{command_keyword code_deps}
     "visualize dependencies of code equations for code"
     (Scan.repeat1 Parse.term >> (fn cs =>
-      Toplevel.unknown_context o
       Toplevel.keep (fn st => code_deps_cmd (Toplevel.context_of st) cs)));
 
 end;
diff -r 7b98dbc1d13e -r d20ca79d50e4 src/Tools/induct.ML
--- a/src/Tools/induct.ML	Thu Apr 16 15:11:04 2015 +0200
+++ b/src/Tools/induct.ML	Thu Apr 16 15:22:44 2015 +0200
@@ -257,8 +257,7 @@
 val _ =
   Outer_Syntax.command @{command_keyword print_induct_rules}
     "print induction and cases rules"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (print_rules o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (print_rules o Toplevel.context_of)));
 
 
 (* access rules *)
diff -r 7b98dbc1d13e -r d20ca79d50e4 src/ZF/Tools/typechk.ML
--- a/src/ZF/Tools/typechk.ML	Thu Apr 16 15:11:04 2015 +0200
+++ b/src/ZF/Tools/typechk.ML	Thu Apr 16 15:22:44 2015 +0200
@@ -127,7 +127,6 @@
 
 val _ =
   Outer_Syntax.command @{command_keyword print_tcset} "print context of ZF typecheck"
-    (Scan.succeed (Toplevel.unknown_context o
-      Toplevel.keep (print_tcset o Toplevel.context_of)));
+    (Scan.succeed (Toplevel.keep (print_tcset o Toplevel.context_of)));
 
 end;