explicit Keyword.control markup for various control commands -- to prevent them from occurring in proof documents;

--- a/etc/isar-keywords-ZF.el	Wed Jul 28 00:03:22 2010 +0200
+++ b/etc/isar-keywords-ZF.el	Wed Jul 28 00:13:26 2010 +0200
@@ -269,13 +269,18 @@
     "ProofGeneral\\.restart"
     "ProofGeneral\\.undo"
     "cannot_undo"
+    "disable_pr"
+    "enable_pr"
     "exit"
     "init_toplevel"
     "kill"
+    "kill_thy"
     "linear_undo"
     "quit"
+    "remove_thy"
     "undo"
-    "undos_proof"))
+    "undos_proof"
+    "use_thy"))
 
 (defconst isar-keywords-diag
   '("ML_command"
@@ -284,15 +289,12 @@
     "cd"
     "class_deps"
     "commit"
-    "disable_pr"
     "display_drafts"
-    "enable_pr"
     "find_consts"
     "find_theorems"
     "full_prf"
     "header"
     "help"
-    "kill_thy"
     "pr"
     "pretty_setmargin"
     "prf"
@@ -324,14 +326,12 @@
     "print_trans_rules"
     "prop"
     "pwd"
-    "remove_thy"
     "term"
     "thm"
     "thm_deps"
     "thy_deps"
     "typ"
     "unused_thms"
-    "use_thy"
     "welcome"))
 
 (defconst isar-keywords-theory-begin

--- a/etc/isar-keywords.el	Wed Jul 28 00:03:22 2010 +0200
+++ b/etc/isar-keywords.el	Wed Jul 28 00:13:26 2010 +0200
@@ -333,13 +333,18 @@
     "ProofGeneral\\.restart"
     "ProofGeneral\\.undo"
     "cannot_undo"
+    "disable_pr"
+    "enable_pr"
     "exit"
     "init_toplevel"
     "kill"
+    "kill_thy"
     "linear_undo"
     "quit"
+    "remove_thy"
     "undo"
-    "undos_proof"))
+    "undos_proof"
+    "use_thy"))
 
 (defconst isar-keywords-diag
   '("ML_command"
@@ -351,16 +356,13 @@
     "code_deps"
     "code_thms"
     "commit"
-    "disable_pr"
     "display_drafts"
-    "enable_pr"
     "export_code"
     "find_consts"
     "find_theorems"
     "full_prf"
     "header"
     "help"
-    "kill_thy"
     "nitpick"
     "normal_form"
     "pr"
@@ -400,7 +402,6 @@
     "pwd"
     "quickcheck"
     "refute"
-    "remove_thy"
     "sledgehammer"
     "smt_status"
     "term"
@@ -409,7 +410,6 @@
     "thy_deps"
     "typ"
     "unused_thms"
-    "use_thy"
     "value"
     "values"
     "welcome"))

--- a/src/Pure/Isar/isar_syn.ML	Wed Jul 28 00:03:22 2010 +0200
+++ b/src/Pure/Isar/isar_syn.ML	Wed Jul 28 00:13:26 2010 +0200
@@ -947,18 +947,18 @@
     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.pwd));
 
 val _ =
-  Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.diag
+  Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.control
     (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.diag
+  Outer_Syntax.improper_command "remove_thy" "remove theory from loader database" Keyword.control
     (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.diag (Parse.name >> (fn name =>
+    Keyword.control (Parse.name >> (fn name =>
       Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
 
 val _ =
@@ -977,11 +977,11 @@
     (opt_modes -- opt_limits >> (Toplevel.no_timing oo Isar_Cmd.pr));
 
 val _ =
-  Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.diag
+  Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.control
     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.disable_pr));
 
 val _ =
-  Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.diag
+  Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.control
     (Scan.succeed (Toplevel.no_timing o Isar_Cmd.enable_pr));
 
 val _ =