Re-enabled and renamed proof-send-span: becomes proof-copy-span bound to C-button1

1 files changed, 3 insertions, 4 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 3b2125da..7b78b855 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1773,12 +1773,11 @@ Otherwise just do proof-restart-buffers to delete some spans from memory."
 (define-key map [(control c) ?u]	  'proof-retract-until-point-interactive)
 ;;;; (define-key map [(control c) (control u)] 'proof-undo-last-successful-command-interactive)
 (define-key map [(control c) ?\']	  'proof-goto-end-of-locked-interactive)
-;; FIXME da: I don't understand what this function is supposed to do.
-;; It will copy a proof command from within the locked region
-;; to the end of it at the moment (contrary to the name "send", nothing to
+;; FIXME da: this command copies a proof command from within the locked region
+;; to the end of it at the moment (contrary to the old name "send", nothing to
 ;; do with shell).  Perhaps we could define a
 ;; collection of useful copying functions which do this kind of thing.
-;; (define-key map [(control button1)]	  'proof-send-span)
+(define-key map [(control button1)]	  'proof-copy-span)
 ;;; (define-key map [(control c) (control b)] 'proof-process-buffer)
 
 (define-key map [(control c) (control z)] 'proof-frob-locked-end)