1.1 --- a/etc/isar-keywords-ZF.el	Wed Jul 28 00:03:22 2010 +0200
     1.2 +++ b/etc/isar-keywords-ZF.el	Wed Jul 28 00:13:26 2010 +0200
     1.3 @@ -269,13 +269,18 @@
     1.4      "ProofGeneral\\.restart"
     1.5      "ProofGeneral\\.undo"
     1.6      "cannot_undo"
     1.7 +    "disable_pr"
     1.8 +    "enable_pr"
     1.9      "exit"
    1.10      "init_toplevel"
    1.11      "kill"
    1.12 +    "kill_thy"
    1.13      "linear_undo"
    1.14      "quit"
    1.15 +    "remove_thy"
    1.16      "undo"
    1.17 -    "undos_proof"))
    1.18 +    "undos_proof"
    1.19 +    "use_thy"))
    1.20  
    1.21  (defconst isar-keywords-diag
    1.22    '("ML_command"
    1.23 @@ -284,15 +289,12 @@
    1.24      "cd"
    1.25      "class_deps"
    1.26      "commit"
    1.27 -    "disable_pr"
    1.28      "display_drafts"
    1.29 -    "enable_pr"
    1.30      "find_consts"
    1.31      "find_theorems"
    1.32      "full_prf"
    1.33      "header"
    1.34      "help"
    1.35 -    "kill_thy"
    1.36      "pr"
    1.37      "pretty_setmargin"
    1.38      "prf"
    1.39 @@ -324,14 +326,12 @@
    1.40      "print_trans_rules"
    1.41      "prop"
    1.42      "pwd"
    1.43 -    "remove_thy"
    1.44      "term"
    1.45      "thm"
    1.46      "thm_deps"
    1.47      "thy_deps"
    1.48      "typ"
    1.49      "unused_thms"
    1.50 -    "use_thy"
    1.51      "welcome"))
    1.52  
    1.53  (defconst isar-keywords-theory-begin

     2.1 --- a/etc/isar-keywords.el	Wed Jul 28 00:03:22 2010 +0200
     2.2 +++ b/etc/isar-keywords.el	Wed Jul 28 00:13:26 2010 +0200
     2.3 @@ -333,13 +333,18 @@
     2.4      "ProofGeneral\\.restart"
     2.5      "ProofGeneral\\.undo"
     2.6      "cannot_undo"
     2.7 +    "disable_pr"
     2.8 +    "enable_pr"
     2.9      "exit"
    2.10      "init_toplevel"
    2.11      "kill"
    2.12 +    "kill_thy"
    2.13      "linear_undo"
    2.14      "quit"
    2.15 +    "remove_thy"
    2.16      "undo"
    2.17 -    "undos_proof"))
    2.18 +    "undos_proof"
    2.19 +    "use_thy"))
    2.20  
    2.21  (defconst isar-keywords-diag
    2.22    '("ML_command"
    2.23 @@ -351,16 +356,13 @@
    2.24      "code_deps"
    2.25      "code_thms"
    2.26      "commit"
    2.27 -    "disable_pr"
    2.28      "display_drafts"
    2.29 -    "enable_pr"
    2.30      "export_code"
    2.31      "find_consts"
    2.32      "find_theorems"
    2.33      "full_prf"
    2.34      "header"
    2.35      "help"
    2.36 -    "kill_thy"
    2.37      "nitpick"
    2.38      "normal_form"
    2.39      "pr"
    2.40 @@ -400,7 +402,6 @@
    2.41      "pwd"
    2.42      "quickcheck"
    2.43      "refute"
    2.44 -    "remove_thy"
    2.45      "sledgehammer"
    2.46      "smt_status"
    2.47      "term"
    2.48 @@ -409,7 +410,6 @@
    2.49      "thy_deps"
    2.50      "typ"
    2.51      "unused_thms"
    2.52 -    "use_thy"
    2.53      "value"
    2.54      "values"
    2.55      "welcome"))

     3.1 --- a/src/Pure/Isar/isar_syn.ML	Wed Jul 28 00:03:22 2010 +0200
     3.2 +++ b/src/Pure/Isar/isar_syn.ML	Wed Jul 28 00:13:26 2010 +0200
     3.3 @@ -947,18 +947,18 @@
     3.4      (Scan.succeed (Toplevel.no_timing o Isar_Cmd.pwd));
     3.5  
     3.6  val _ =
     3.7 -  Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.diag
     3.8 +  Outer_Syntax.improper_command "use_thy" "use theory file" Keyword.control
     3.9      (Parse.name >> (fn name =>
    3.10        Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.use_thy name)));
    3.11  
    3.12  val _ =
    3.13 -  Outer_Syntax.improper_command "remove_thy" "remove theory from loader database" Keyword.diag
    3.14 +  Outer_Syntax.improper_command "remove_thy" "remove theory from loader database" Keyword.control
    3.15      (Parse.name >> (fn name =>
    3.16        Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.remove_thy name)));
    3.17  
    3.18  val _ =
    3.19    Outer_Syntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
    3.20 -    Keyword.diag (Parse.name >> (fn name =>
    3.21 +    Keyword.control (Parse.name >> (fn name =>
    3.22        Toplevel.no_timing o Toplevel.imperative (fn () => Thy_Info.kill_thy name)));
    3.23  
    3.24  val _ =
    3.25 @@ -977,11 +977,11 @@
    3.26      (opt_modes -- opt_limits >> (Toplevel.no_timing oo Isar_Cmd.pr));
    3.27  
    3.28  val _ =
    3.29 -  Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.diag
    3.30 +  Outer_Syntax.improper_command "disable_pr" "disable printing of toplevel state" Keyword.control
    3.31      (Scan.succeed (Toplevel.no_timing o Isar_Cmd.disable_pr));
    3.32  
    3.33  val _ =
    3.34 -  Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.diag
    3.35 +  Outer_Syntax.improper_command "enable_pr" "enable printing of toplevel state" Keyword.control
    3.36      (Scan.succeed (Toplevel.no_timing o Isar_Cmd.enable_pr));
    3.37  
    3.38  val _ =