removed restart;
authorwenzelm
Tue Jul 27 21:56:32 1999 +0200 (1999-07-27 ago)
changeset 7101ee79bf6feee2
parent 7100 4f777a0e1c8b
child 7102 ead5c234b28c
removed restart;
added touch_all_thys, touch_thy, remove_thy, update_thy_only;
src/Pure/Isar/isar_cmd.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Tue Jul 27 21:55:39 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Tue Jul 27 21:56:32 1999 +0200
     1.3 @@ -8,15 +8,18 @@
     1.4  signature ISAR_CMD =
     1.5  sig
     1.6    val exit: Toplevel.transition -> Toplevel.transition
     1.7 -  val restart: Toplevel.transition -> Toplevel.transition
     1.8    val quit: Toplevel.transition -> Toplevel.transition
     1.9 +  val init_toplevel: Toplevel.transition -> Toplevel.transition
    1.10 +  val touch_all_thys: Toplevel.transition -> Toplevel.transition
    1.11 +  val touch_thy: string -> Toplevel.transition -> Toplevel.transition
    1.12 +  val remove_thy: string -> Toplevel.transition -> Toplevel.transition
    1.13 +  val kill_theory: Toplevel.transition -> Toplevel.transition
    1.14    val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
    1.15    val clear_undo: Toplevel.transition -> Toplevel.transition
    1.16    val redo: Toplevel.transition -> Toplevel.transition
    1.17    val undos_proof: int -> Toplevel.transition -> Toplevel.transition
    1.18    val kill_proof: Toplevel.transition -> Toplevel.transition
    1.19    val undo_theory: Toplevel.transition -> Toplevel.transition
    1.20 -  val kill_theory: Toplevel.transition -> Toplevel.transition
    1.21    val undo: Toplevel.transition -> Toplevel.transition
    1.22    val use: string -> Toplevel.transition -> Toplevel.transition
    1.23    val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
    1.24 @@ -27,6 +30,7 @@
    1.25    val use_thy: string -> Toplevel.transition -> Toplevel.transition
    1.26    val use_thy_only: string -> Toplevel.transition -> Toplevel.transition
    1.27    val update_thy: string -> Toplevel.transition -> Toplevel.transition
    1.28 +  val update_thy_only: string -> Toplevel.transition -> Toplevel.transition
    1.29    val print_theory: Toplevel.transition -> Toplevel.transition
    1.30    val print_syntax: Toplevel.transition -> Toplevel.transition
    1.31    val print_theorems: Toplevel.transition -> Toplevel.transition
    1.32 @@ -51,9 +55,18 @@
    1.33      writeln "Leaving the Isar loop.  Invoke 'loop();' to restart.";
    1.34      raise Toplevel.TERMINATE));
    1.35  
    1.36 -val restart = Toplevel.imperative (fn () => raise Toplevel.RESTART);
    1.37  val quit = Toplevel.imperative quit;
    1.38  
    1.39 +val init_toplevel = Toplevel.imperative (fn () => raise Toplevel.RESTART);
    1.40 +
    1.41 +
    1.42 +(* touch theories *)
    1.43 +
    1.44 +val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys;
    1.45 +fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name);
    1.46 +fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name);
    1.47 +val kill_theory = Toplevel.imperative (fn () => warning "Nothing to kill.") o Toplevel.kill;
    1.48 +
    1.49  
    1.50  (* history commands *)
    1.51  
    1.52 @@ -72,7 +85,6 @@
    1.53  val undo_theory = Toplevel.history (fn hist =>
    1.54    if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist);
    1.55  
    1.56 -val kill_theory = Toplevel.imperative (fn () => warning "Nothing to kill.") o Toplevel.kill;
    1.57  val undo = kill_theory o undo_theory o undos_proof 1;
    1.58  
    1.59  
    1.60 @@ -105,6 +117,7 @@
    1.61  fun use_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy name);
    1.62  fun use_thy_only name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy_only name);
    1.63  fun update_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy name);
    1.64 +fun update_thy_only name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy_only name);
    1.65  
    1.66  
    1.67  (* print theory contents *)