src/Pure/Isar/isar_cmd.ML

 *)
 
 signature ISAR_CMD =
 sig
   val exit: Toplevel.transition -> Toplevel.transition
-  val restart: Toplevel.transition -> Toplevel.transition
   val quit: Toplevel.transition -> Toplevel.transition
+  val init_toplevel: Toplevel.transition -> Toplevel.transition
+  val touch_all_thys: Toplevel.transition -> Toplevel.transition
+  val touch_thy: string -> Toplevel.transition -> Toplevel.transition
+  val remove_thy: string -> Toplevel.transition -> Toplevel.transition
+  val kill_theory: Toplevel.transition -> Toplevel.transition
   val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
   val clear_undo: Toplevel.transition -> Toplevel.transition
   val redo: Toplevel.transition -> Toplevel.transition
   val undos_proof: int -> Toplevel.transition -> Toplevel.transition
   val kill_proof: Toplevel.transition -> Toplevel.transition
   val undo_theory: Toplevel.transition -> Toplevel.transition
-  val kill_theory: Toplevel.transition -> Toplevel.transition
   val undo: Toplevel.transition -> Toplevel.transition
   val use: string -> Toplevel.transition -> Toplevel.transition
   val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
   val use_mltext: string -> Toplevel.transition -> Toplevel.transition
   val use_commit: Toplevel.transition -> Toplevel.transition
   val cd: string -> Toplevel.transition -> Toplevel.transition
   val pwd: Toplevel.transition -> Toplevel.transition
   val use_thy: string -> Toplevel.transition -> Toplevel.transition
   val use_thy_only: string -> Toplevel.transition -> Toplevel.transition
   val update_thy: string -> Toplevel.transition -> Toplevel.transition
+  val update_thy_only: string -> Toplevel.transition -> Toplevel.transition
   val print_theory: Toplevel.transition -> Toplevel.transition
   val print_syntax: Toplevel.transition -> Toplevel.transition
   val print_theorems: Toplevel.transition -> Toplevel.transition
   val print_attributes: Toplevel.transition -> Toplevel.transition
   val print_methods: Toplevel.transition -> Toplevel.transition

 val exit = Toplevel.keep (fn state =>
   (Context.set_context (try Toplevel.theory_of state);
     writeln "Leaving the Isar loop.  Invoke 'loop();' to restart.";
     raise Toplevel.TERMINATE));
 
-val restart = Toplevel.imperative (fn () => raise Toplevel.RESTART);
 val quit = Toplevel.imperative quit;
+
+val init_toplevel = Toplevel.imperative (fn () => raise Toplevel.RESTART);
+
+
+(* touch theories *)
+
+val touch_all_thys = Toplevel.imperative ThyInfo.touch_all_thys;
+fun touch_thy name = Toplevel.imperative (fn () => ThyInfo.touch_thy name);
+fun remove_thy name = Toplevel.imperative (fn () => ThyInfo.remove_thy name);
+val kill_theory = Toplevel.imperative (fn () => warning "Nothing to kill.") o Toplevel.kill;
 
 
 (* history commands *)
 
 fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));

   | Toplevel.Proof _ => History.undo hist));
 
 val undo_theory = Toplevel.history (fn hist =>
   if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist);
 
-val kill_theory = Toplevel.imperative (fn () => warning "Nothing to kill.") o Toplevel.kill;
 val undo = kill_theory o undo_theory o undos_proof 1;
 
 
 (* use ML text *)
 

 (* load theory files *)
 
 fun use_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy name);
 fun use_thy_only name = Toplevel.imperative (fn () => Context.save ThyInfo.use_thy_only name);
 fun update_thy name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy name);
+fun update_thy_only name = Toplevel.imperative (fn () => Context.save ThyInfo.update_thy_only name);
 
 
 (* print theory contents *)
 
 val print_theory = Toplevel.keep (PureThy.print_theory o Toplevel.theory_of);