removed obsolete clear_undos_theory;
authorwenzelm
Sat Dec 30 12:33:25 2006 +0100 (2006-12-30)
changeset 21955c1a6fad248ca
parent 21954 ffeb00290397
child 21956 2cbee05b18a1
removed obsolete clear_undos_theory;
undo/cannot_undo: proper undo of 'end';
src/Pure/Isar/isar_cmd.ML
     1.1 --- a/src/Pure/Isar/isar_cmd.ML	Fri Dec 29 20:35:03 2006 +0100
     1.2 +++ b/src/Pure/Isar/isar_cmd.ML	Sat Dec 30 12:33:25 2006 +0100
     1.3 @@ -43,14 +43,13 @@
     1.4    val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition
     1.5    val disable_pr: Toplevel.transition -> Toplevel.transition
     1.6    val enable_pr: Toplevel.transition -> Toplevel.transition
     1.7 -  val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
     1.8 -  val clear_undos_theory: int -> Toplevel.transition -> Toplevel.transition
     1.9    val redo: Toplevel.transition -> Toplevel.transition
    1.10    val undos_proof: int -> Toplevel.transition -> Toplevel.transition
    1.11    val kill_proof_notify: (unit -> unit) -> Toplevel.transition -> Toplevel.transition
    1.12    val kill_proof: Toplevel.transition -> Toplevel.transition
    1.13    val undo_theory: Toplevel.transition -> Toplevel.transition
    1.14    val undo: Toplevel.transition -> Toplevel.transition
    1.15 +  val cannot_undo: string -> Toplevel.transition -> Toplevel.transition
    1.16    val kill: Toplevel.transition -> Toplevel.transition
    1.17    val back: Toplevel.transition -> Toplevel.transition
    1.18    val use: Path.T -> Toplevel.transition -> Toplevel.transition
    1.19 @@ -240,10 +239,6 @@
    1.20  
    1.21  (* history commands *)
    1.22  
    1.23 -fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
    1.24 -
    1.25 -val clear_undos_theory = Toplevel.history o History.clear;
    1.26 -
    1.27  val redo =
    1.28    Toplevel.history History.redo o
    1.29    Toplevel.actual_proof ProofHistory.redo o
    1.30 @@ -264,7 +259,11 @@
    1.31  val undo_theory = Toplevel.history (fn hist =>
    1.32    if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist);
    1.33  
    1.34 -val undo = Toplevel.kill o undo_theory o undos_proof 1;
    1.35 +val undo = Toplevel.kill o undos_proof 1 o undo_theory o Toplevel.undo_exit;
    1.36 +
    1.37 +fun cannot_undo "end" = undo   (*ProofGeneral legacy*)
    1.38 +  | cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt));
    1.39 +
    1.40  val kill = Toplevel.kill o kill_proof;
    1.41  
    1.42  val back =