added kill_thy;
authorwenzelm
Tue Oct 26 14:35:10 1999 +0200 (1999-10-26 ago)
changeset 7931fa6fec415492
parent 7930 220892918bd1
child 7932 92df50fb89ca
added kill_thy;
src/Pure/Isar/isar_cmd.ML
src/Pure/Isar/isar_syn.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Oct 26 14:34:50 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Oct 26 14:35:10 1999 +0200
     1.3 @@ -15,6 +15,7 @@
     1.4    val touch_all_thys: Toplevel.transition -> Toplevel.transition
     1.5    val touch_thy: string -> Toplevel.transition -> Toplevel.transition
     1.6    val remove_thy: string -> Toplevel.transition -> Toplevel.transition
     1.7 +  val kill_thy: string -> Toplevel.transition -> Toplevel.transition
     1.8    val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
     1.9    val clear_undos_theory: int -> Toplevel.transition -> Toplevel.transition
    1.10    val redo: Toplevel.transition -> Toplevel.transition
    1.11 @@ -71,6 +72,7 @@
    1.12  val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys;
    1.13  fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name);
    1.14  fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name);
    1.15 +fun kill_thy name = Toplevel.imperative (fn () => IsarThy.kill_theory name);
    1.16  
    1.17  
    1.18  (* history commands *)
     2.1 --- a/src/Pure/Isar/isar_syn.ML	Tue Oct 26 14:34:50 1999 +0200
     2.2 +++ b/src/Pure/Isar/isar_syn.ML	Tue Oct 26 14:35:10 1999 +0200
     2.3 @@ -562,6 +562,10 @@
     2.4    OuterSyntax.improper_command "remove_thy" "remove theory from loader database" K.diag
     2.5      (P.name >> IsarCmd.remove_thy);
     2.6  
     2.7 +val kill_thyP =
     2.8 +  OuterSyntax.improper_command "kill_thy" "kill theory -- try to remove from loader database"
     2.9 +    K.diag (P.name >> IsarCmd.kill_thy);
    2.10 +
    2.11  val prP =
    2.12    OuterSyntax.improper_command "pr" "print current toplevel state" K.diag
    2.13      (Scan.succeed (Toplevel.print o Toplevel.imperative (fn () => Toplevel.quiet := false)));
    2.14 @@ -574,16 +578,13 @@
    2.15    OuterSyntax.improper_command "enable_pr" "enable printing of toplevel state" K.diag
    2.16      (Scan.succeed (Toplevel.imperative (fn () => Toplevel.quiet := false)));
    2.17  
    2.18 -
    2.19 -val opt_unit = Scan.optional (P.$$$ "(" -- P.$$$ ")" >> (K ())) ();
    2.20 -
    2.21  val commitP =
    2.22    OuterSyntax.improper_command "commit" "commit current session to ML database" K.diag
    2.23 -    (opt_unit >> (K IsarCmd.use_commit));
    2.24 +    (P.opt_unit >> (K IsarCmd.use_commit));
    2.25  
    2.26  val quitP =
    2.27    OuterSyntax.improper_command "quit" "quit Isabelle" K.control
    2.28 -    (opt_unit >> (K IsarCmd.quit));
    2.29 +    (P.opt_unit >> (K IsarCmd.quit));
    2.30  
    2.31  val exitP =
    2.32    OuterSyntax.improper_command "exit" "exit Isar loop" K.control
    2.33 @@ -636,9 +637,9 @@
    2.34    print_propP, print_termP, print_typeP,
    2.35    (*system commands*)
    2.36    cdP, pwdP, use_thyP, use_thy_onlyP, update_thyP, update_thy_onlyP,
    2.37 -  touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP, prP,
    2.38 -  disable_prP, enable_prP, commitP, quitP, exitP, init_toplevelP,
    2.39 -  welcomeP];
    2.40 +  touch_thyP, touch_all_thysP, touch_child_thysP, remove_thyP,
    2.41 +  kill_thyP, prP, disable_prP, enable_prP, commitP, quitP, exitP,
    2.42 +  init_toplevelP, welcomeP];
    2.43  
    2.44  
    2.45  end;