equal
deleted
inserted
replaced
18 val kill_thy: string -> Toplevel.transition -> Toplevel.transition |
18 val kill_thy: string -> Toplevel.transition -> Toplevel.transition |
19 val cannot_undo: string -> Toplevel.transition -> Toplevel.transition |
19 val cannot_undo: string -> Toplevel.transition -> Toplevel.transition |
20 val clear_undos_theory: int -> Toplevel.transition -> Toplevel.transition |
20 val clear_undos_theory: int -> Toplevel.transition -> Toplevel.transition |
21 val redo: Toplevel.transition -> Toplevel.transition |
21 val redo: Toplevel.transition -> Toplevel.transition |
22 val undos_proof: int -> Toplevel.transition -> Toplevel.transition |
22 val undos_proof: int -> Toplevel.transition -> Toplevel.transition |
|
23 val kill_proof_notify: (unit -> unit) -> Toplevel.transition -> Toplevel.transition |
23 val kill_proof: Toplevel.transition -> Toplevel.transition |
24 val kill_proof: Toplevel.transition -> Toplevel.transition |
24 val undo_theory: Toplevel.transition -> Toplevel.transition |
25 val undo_theory: Toplevel.transition -> Toplevel.transition |
25 val undo: Toplevel.transition -> Toplevel.transition |
26 val undo: Toplevel.transition -> Toplevel.transition |
26 val use: string -> Toplevel.transition -> Toplevel.transition |
27 val use: string -> Toplevel.transition -> Toplevel.transition |
27 val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition |
28 val use_mltext_theory: string -> Toplevel.transition -> Toplevel.transition |
82 val redo = Toplevel.history History.redo o Toplevel.proof ProofHistory.redo; |
83 val redo = Toplevel.history History.redo o Toplevel.proof ProofHistory.redo; |
83 |
84 |
84 fun undos_proof n = Toplevel.proof (fn prf => |
85 fun undos_proof n = Toplevel.proof (fn prf => |
85 if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf); |
86 if ProofHistory.is_initial prf then raise Toplevel.UNDEF else funpow n ProofHistory.undo prf); |
86 |
87 |
87 val kill_proof = Toplevel.history (fn hist => |
88 fun kill_proof_notify (f: unit -> unit) = Toplevel.history (fn hist => |
88 (case History.current hist of |
89 (case History.current hist of |
89 Toplevel.Theory _ => raise Toplevel.UNDEF |
90 Toplevel.Theory _ => raise Toplevel.UNDEF |
90 | Toplevel.Proof _ => History.undo hist)); |
91 | Toplevel.Proof _ => (f (); History.undo hist))); |
|
92 |
|
93 val kill_proof = kill_proof_notify (K ()); |
91 |
94 |
92 val undo_theory = Toplevel.history (fn hist => |
95 val undo_theory = Toplevel.history (fn hist => |
93 if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist); |
96 if History.is_initial hist then raise Toplevel.UNDEF else History.undo hist); |
94 |
97 |
95 val undo = Toplevel.kill o undo_theory o undos_proof 1; |
98 val undo = Toplevel.kill o undo_theory o undos_proof 1; |