diff options
author | David Aspinall <da@inf.ed.ac.uk> | 2007-12-12 00:37:06 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 2007-12-12 00:37:06 +0000 |
commit | 8f467626040080c276c1b0a67c4eae7cbd1787af (patch) | |
tree | 2954449ee0553bf7d25c37ef003f459f477999b7 /generic | |
parent | 25c4827afce71f907ece0d5264765dbdc262b9ff (diff) |
Add undo command to context menu
Diffstat (limited to 'generic')
-rw-r--r-- | generic/pg-user.el | 9 |
1 files changed, 8 insertions, 1 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index 5339f2ed..6b7de5a8 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -963,6 +963,9 @@ If NUM is negative, move upwards. Return new span." (not (not idiom)))) (list (vector "Copy" (list 'pg-copy-span-contents span) t)) + (list (vector + "Undo" + (list 'pg-span-undo span) t)) (if proof-experimental-features (list (vector "Move up" (list 'pg-move-span-contents span -1) @@ -977,7 +980,11 @@ If NUM is negative, move upwards. Return new span." proof-shell-theorem-dependency-list-regexp) (proof-dependency-in-span-context-menu span)))) - +(defun pg-span-undo (span) + "Undo to the start of the given SPAN." + (interactive) + (goto-char (span-start span)) + (proof-retract-until-point)) |