equal
deleted
inserted
replaced
129 |
129 |
130 (* history commands *) |
130 (* history commands *) |
131 |
131 |
132 fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt)); |
132 fun cannot_undo txt = Toplevel.imperative (fn () => error ("Cannot undo " ^ quote txt)); |
133 val clear_undos_theory = Toplevel.history o History.clear; |
133 val clear_undos_theory = Toplevel.history o History.clear; |
134 val redo = Toplevel.history History.redo o Toplevel.proof'' ProofHistory.redo o |
134 |
|
135 val redo = |
|
136 Toplevel.history History.redo o |
|
137 Toplevel.actual_proof ProofHistory.redo o |
135 Toplevel.skip_proof History.redo; |
138 Toplevel.skip_proof History.redo; |
136 |
139 |
137 fun undos_proof n = Toplevel.proof'' (fn prf => |
140 fun undos_proof n = |
|
141 Toplevel.actual_proof (fn prf => |
138 if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf) o |
142 if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf) o |
139 Toplevel.skip_proof (fn h => |
143 Toplevel.skip_proof (fn h => |
140 if History.is_initial h then raise Toplevel.UNDEF else funpow n History.undo h); |
144 if History.is_initial h then raise Toplevel.UNDEF else funpow n History.undo h); |
141 |
145 |
142 fun kill_proof_notify (f: unit -> unit) = Toplevel.history (fn hist => |
146 fun kill_proof_notify (f: unit -> unit) = Toplevel.history (fn hist => |