diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2010-09-22 00:32:57 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2010-09-22 00:32:57 +0000 |
| commit | 3d711cf80edd759f2a6def0c8a65d51e1909bc3f (patch) | |
| tree | cef41e8d035859597601160002de2b796dd90b48 /generic/pg-user.el | |
| parent | fbb9e24a8ff503ad6f5ddd44fa435c5bc095d165 (diff) | |
proof-undo-and-delete-last-successful-command: repair (after
proof-retract-until-point changed type).
Diffstat (limited to 'generic/pg-user.el')
| -rw-r--r-- | generic/pg-user.el | 11 |
1 files changed, 5 insertions, 6 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index cfc1e1fc..8021b45c 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -220,13 +220,12 @@ Notice that the deleted command is put into the Emacs kill ring, so you can use the usual `yank' and similar commands to retrieve the deleted text." (interactive) - (proof-undo-last-successful-command-1 'delete)) - ; (proof-script-new-command-advance)) + (proof-undo-last-successful-command-1 'delete-region)) -(defun proof-undo-last-successful-command-1 (&optional delete) +(defun proof-undo-last-successful-command-1 (&optional undo-action) "Undo last successful command at end of locked region. -If optional DELETE is non-nil, the text is also deleted from -the proof script." +If optional UNDO-ACTION is non-nil, that function is called on +the text region in the proof script after undoing." (interactive "P") (proof-with-script-buffer (let (lastspan) @@ -235,7 +234,7 @@ the proof script." (if (setq lastspan (span-at-before (proof-unprocessed-begin) 'type)) (progn (goto-char (span-start lastspan)) - (proof-retract-until-point delete)) + (proof-retract-until-point undo-action)) (error "Nothing to undo!")))) (if lastspan (proof-maybe-follow-locked-end (span-start lastspan)))))) |