diff options
| author |  David Aspinall <da@inf.ed.ac.uk> | 2011-01-19 19:25:28 +0000 |
|---|---|---|
| committer | David Aspinall <da@inf.ed.ac.uk> | 2011-01-19 19:25:28 +0000 |
| commit | 70140e80a12f3081cfc3fdf2c77ca759cc02dddc (patch) | |
| tree | 948deed644d444baf819f5cf8a49d6b3ee16e7b7 /generic/pg-user.el | |
| parent | b75b6a895171a7746ae3ff8fe5023ea32f018f6d (diff) | |
pg-create-in-span-context-menu: remove "Move up" and "Move down".
These don't seem to be very useful or reliable.
Diffstat (limited to 'generic/pg-user.el')
| -rw-r--r-- | generic/pg-user.el | 13 |
1 files changed, 7 insertions, 6 deletions
diff --git a/generic/pg-user.el b/generic/pg-user.el index e49dcba5..dcbaffba 100644 --- a/generic/pg-user.el +++ b/generic/pg-user.el @@ -743,12 +743,13 @@ If NUM is negative, move upwards. Return new span." (list (vector "Undo" (list 'pg-span-undo span) t)) - (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))) + ;; PG 4.1: these commands are neither very useful nor reliable + ;; (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 |