src/Pure/Isar/isar_cmd.ML
changeset 6686 08b06cd19f8d
parent 6662 e53968c1df53
child 6694 335833a8b10a
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri May 21 11:40:15 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Fri May 21 11:40:34 1999 +0200
     1.3 @@ -11,6 +11,10 @@
     1.4    val exit: Toplevel.transition -> Toplevel.transition
     1.5    val restart: Toplevel.transition -> Toplevel.transition
     1.6    val quit: Toplevel.transition -> Toplevel.transition
     1.7 +  val clear_undo: Toplevel.transition -> Toplevel.transition
     1.8 +  val undo: Toplevel.transition -> Toplevel.transition
     1.9 +  val redo: Toplevel.transition -> Toplevel.transition
    1.10 +  val undos: int -> Toplevel.transition -> Toplevel.transition
    1.11    val use: string -> Toplevel.transition -> Toplevel.transition
    1.12    val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
    1.13    val use_mltext: string -> Toplevel.transition -> Toplevel.transition
    1.14 @@ -49,6 +53,23 @@
    1.15  val quit = Toplevel.imperative quit;
    1.16  
    1.17  
    1.18 +(* history commands *)
    1.19 +
    1.20 +val clear_undo = Toplevel.history History.clear o Toplevel.proof ProofHistory.clear;
    1.21 +val redo = Toplevel.history History.redo o Toplevel.proof ProofHistory.redo;
    1.22 +
    1.23 +fun undo_proof prf =
    1.24 +  if ProofHistory.is_initial prf then raise Toplevel.UNDEF else ProofHistory.undo prf;
    1.25 +
    1.26 +fun undo_node hist =
    1.27 +  if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist;
    1.28 +
    1.29 +val undo = Toplevel.kill o Toplevel.history undo_node o Toplevel.proof undo_proof;
    1.30 +
    1.31 +(* FIXME fix *)
    1.32 +fun undos n = Toplevel.history (funpow n History.undo) o Toplevel.proof (funpow n undo_proof);
    1.33 +
    1.34 +
    1.35  (* use ML text *)
    1.36  
    1.37  fun use name = Toplevel.keep (fn state =>