# HG changeset patch # User wenzelm # Date 1167478405 -3600 # Node ID c1a6fad248ca4ff7e0724e38a6efdea78c76c3ce # Parent ffeb00290397651e4308fd75a8b3d7d0e9739dd9 removed obsolete clear_undos_theory; undo/cannot_undo: proper undo of 'end'; diff -r ffeb00290397 -r c1a6fad248ca src/Pure/Isar/isar_cmd.ML --- a/src/Pure/Isar/isar_cmd.ML Fri Dec 29 20:35:03 2006 +0100 +++ b/src/Pure/Isar/isar_cmd.ML Sat Dec 30 12:33:25 2006 +0100 @@ -43,14 +43,13 @@ val pr: string list * (int option * int option) -> Toplevel.transition -> Toplevel.transition val disable_pr: Toplevel.transition -> Toplevel.transition val enable_pr: Toplevel.transition -> Toplevel.transition - val cannot_undo: string -> Toplevel.transition -> Toplevel.transition - val clear_undos_theory: int -> Toplevel.transition -> Toplevel.transition val redo: Toplevel.transition -> Toplevel.transition val undos_proof: int -> Toplevel.transition -> Toplevel.transition val kill_proof_notify: (unit -> unit) -> Toplevel.transition -> Toplevel.transition val kill_proof: Toplevel.transition -> Toplevel.transition val undo_theory: Toplevel.transition -> Toplevel.transition val undo: Toplevel.transition -> Toplevel.transition + val cannot_undo: string -> Toplevel.transition -> Toplevel.transition val kill: Toplevel.transition -> Toplevel.transition val back: Toplevel.transition -> Toplevel.transition val use: Path.T -> Toplevel.transition -> Toplevel.transition @@ -240,10 +239,6 @@ (* history commands *) -fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt)); - -val clear_undos_theory = Toplevel.history o History.clear; - val redo = Toplevel.history History.redo o Toplevel.actual_proof ProofHistory.redo o @@ -264,7 +259,11 @@ val undo_theory = Toplevel.history (fn hist => if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist); -val undo = Toplevel.kill o undo_theory o undos_proof 1; +val undo = Toplevel.kill o undos_proof 1 o undo_theory o Toplevel.undo_exit; + +fun cannot_undo "end" = undo (*ProofGeneral legacy*) + | cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt)); + val kill = Toplevel.kill o kill_proof; val back =