src/Pure/Isar/isar_cmd.ML
changeset 6742 6b5cb872d997
parent 6734 151c07f5b70a
child 7012 ae9dac5af9d1
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Thu May 27 11:39:44 1999 +0200
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Thu May 27 20:45:20 1999 +0200
     1.3 @@ -13,9 +13,12 @@
     1.4    val quit: Toplevel.transition -> Toplevel.transition
     1.5    val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
     1.6    val clear_undo: Toplevel.transition -> Toplevel.transition
     1.7 +  val redo: Toplevel.transition -> Toplevel.transition
     1.8 +  val undos_proof: int -> Toplevel.transition -> Toplevel.transition
     1.9 +  val kill_proof: Toplevel.transition -> Toplevel.transition
    1.10 +  val undo_theory: Toplevel.transition -> Toplevel.transition
    1.11 +  val kill_theory: Toplevel.transition -> Toplevel.transition
    1.12    val undo: Toplevel.transition -> Toplevel.transition
    1.13 -  val redo: Toplevel.transition -> Toplevel.transition
    1.14 -  val undos: int -> Toplevel.transition -> Toplevel.transition
    1.15    val use: string -> Toplevel.transition -> Toplevel.transition
    1.16    val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition
    1.17    val use_mltext: string -> Toplevel.transition -> Toplevel.transition
    1.18 @@ -58,20 +61,22 @@
    1.19  (* history commands *)
    1.20  
    1.21  fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
    1.22 -
    1.23  val clear_undo = Toplevel.history History.clear o Toplevel.proof ProofHistory.clear;
    1.24  val redo = Toplevel.history History.redo o Toplevel.proof ProofHistory.redo;
    1.25  
    1.26 -fun undo_proof prf =
    1.27 -  if ProofHistory.is_initial prf then raise Toplevel.UNDEF else ProofHistory.undo prf;
    1.28 +fun undos_proof n = Toplevel.proof (fn prf =>
    1.29 +  if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf);
    1.30  
    1.31 -fun undo_node hist =
    1.32 -  if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist;
    1.33 +val kill_proof = Toplevel.history (fn hist =>
    1.34 +  (case History.current hist of
    1.35 +    Toplevel.Theory _ => raise Toplevel.UNDEF
    1.36 +  | Toplevel.Proof _ => History.undo hist));
    1.37  
    1.38 -val undo = Toplevel.kill o Toplevel.history undo_node o Toplevel.proof undo_proof;
    1.39 +val undo_theory = Toplevel.history (fn hist =>
    1.40 +  if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist);
    1.41  
    1.42 -(* FIXME fix *)
    1.43 -fun undos n = Toplevel.history (funpow n History.undo) o Toplevel.proof (funpow n undo_proof);
    1.44 +val kill_theory = Toplevel.imperative (fn () => warning "Nothing to kill.") o Toplevel.kill;
    1.45 +val undo = kill_theory o undo_theory o undos_proof 1;
    1.46  
    1.47  
    1.48  (* use ML text *)