diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2009-08-07 14:40:00 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2009-08-07 14:40:00 +0000 |
| commit | fcd935b7a2713230349e70f1a13dc6ca0a29fe7c (patch) | |
| tree | b2e88b0b49f6b0ecbde86b470dc3aa720f073f3f /generic | |
| parent | fa8a8cf284c1ccde49fdadaacc861d5505c94f80 (diff) | |
Fix pareno
Diffstat (limited to 'generic')
| -rw-r--r-- | generic/pg-user.el | 23 |
1 files changed, 10 insertions, 13 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index dde8c81f..32f554e1 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -847,19 +847,16 @@ If NUM is negative, move upwards. Return new span." (list (vector "Undo" (list 'pg-span-undo span) t)) - (if proof-experimental-features - (list (vector - "Move up" (list 'pg-move-span-contents span -1) - (pg-numth-span-higher-or-lower (pg-control-span-of span) -1 'noerr)))) - (if proof-experimental-features - (list (vector - "Move down" (list 'pg-move-span-contents span 1) - (pg-numth-span-higher-or-lower (pg-control-span-of span) 1 'noerr)))) - (if proof-script-span-context-menu-extensions - (funcall proof-script-span-context-menu-extensions span idiom name)) - (if (and proof-experimental-features - proof-shell-theorem-dependency-list-regexp) - (proof-dependency-in-span-context-menu span)))) + (list (vector + "Move up" (list 'pg-move-span-contents span -1) + (pg-numth-span-higher-or-lower (pg-control-span-of span) -1 'noerr)))) + (list (vector + "Move down" (list 'pg-move-span-contents span 1) + (pg-numth-span-higher-or-lower (pg-control-span-of span) 1 'noerr))) + (if proof-script-span-context-menu-extensions + (funcall proof-script-span-context-menu-extensions span idiom name)) + (if 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." |