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

3 files changed, 8 insertions, 7 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)
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 9f8d2458..60fdeb0f 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -463,9 +463,10 @@ Proof General with the proof assistant."
       (incf a))
     (apply 'concat (nreverse ls))))
 
-;; FIXME da: this is an oddity.  Was bound by default to
-;; control - button1, I've turned it off.
-(defun proof-send-span (event)
+;; FIXME da: this is an oddity.  It copies the span, but does not
+;; send it, contrary to it's old name ("proof-send-span").   
+;; Maybe belongs elsewhere.
+(defun proof-copy-span (event)
   (interactive "e")
   (let* ((span (span-at (mouse-set-point event) 'type))
 	 (str  (if span (span-property span 'cmd))))
diff --git a/todo b/todo
index 6a413d98..cd501c6d 100644
--- a/todo
+++ b/todo
@@ -49,6 +49,7 @@ A Pending work, in progress [da]:
     - investigate toolbar refresh problems
     - investigate of excessive processing for large proofs
     - investigate bug fix for vacuous locked regions
+    - document proof-copy-span (new name for proof-send-span, re-enabled).
 
 A Usability enhancement:
    Enable toolbar in other buffers.  Should switch to active