history commands;

--- a/src/Pure/Isar/isar_cmd.ML	Fri May 21 11:40:15 1999 +0200
+++ b/src/Pure/Isar/isar_cmd.ML	Fri May 21 11:40:34 1999 +0200
@@ -11,6 +11,10 @@
   val exit: Toplevel.transition -> Toplevel.transition
   val restart: Toplevel.transition -> Toplevel.transition
   val quit: Toplevel.transition -> Toplevel.transition
+  val clear_undo: Toplevel.transition -> Toplevel.transition
+  val undo: Toplevel.transition -> Toplevel.transition
+  val redo: Toplevel.transition -> Toplevel.transition
+  val undos: int -> 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
@@ -49,6 +53,23 @@
 val quit = Toplevel.imperative quit;
 
 
+(* history commands *)
+
+val clear_undo = Toplevel.history History.clear o Toplevel.proof ProofHistory.clear;
+val redo = Toplevel.history History.redo o Toplevel.proof ProofHistory.redo;
+
+fun undo_proof prf =
+  if ProofHistory.is_initial prf then raise Toplevel.UNDEF else ProofHistory.undo prf;
+
+fun undo_node hist =
+  if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist;
+
+val undo = Toplevel.kill o Toplevel.history undo_node o Toplevel.proof undo_proof;
+
+(* FIXME fix *)
+fun undos n = Toplevel.history (funpow n History.undo) o Toplevel.proof (funpow n undo_proof);
+
+
 (* use ML text *)
 
 fun use name = Toplevel.keep (fn state =>