Revive sendback behaviour (using button1)

3 files changed, 46 insertions, 17 deletions

diff --git a/generic/pg-goals.el b/generic/pg-goals.el
index 18f87577..35ea669c 100644
--- a/generic/pg-goals.el
+++ b/generic/pg-goals.el
@@ -1,6 +1,6 @@
 ;; pg-goals.el ---  Proof General goals buffer mode.
 ;;
-;; Copyright (C) 1994-2008 LFCS Edinburgh.
+;; Copyright (C) 1994-2009 LFCS, University of Edinburgh.
 ;; Authors:   David Aspinall, Yves Bertot, Healfdene Goguen,
 ;;            Thomas Kleymann and Dilip Sequeira
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
@@ -52,20 +52,14 @@ May enable proof-by-pointing or similar features.
       "Menu for Proof General goals buffer."
       (proof-aux-menu)))
 
-
 ;;
 ;; Keys for goals buffer
 ;;
 (define-key proof-goals-mode-map [q] 'bury-buffer)
-
-(define-key proof-goals-mode-map [mouse-2] 'pg-goals-button-action)
-(define-key proof-goals-mode-map [C-mouse-2] 'proof-undo-and-delete-last-successful-command)
-;; (define-key proof-goals-mode-map [mouse-1] 'pg-goals-button-action)
-;; (define-key proof-goals-mode-map [C-mouse-1] 'proof-undo-and-delete-last-successful-command)
-;; C Raffalli: The next key on button3 will be remapped to proof by contextual
-;; menu by pg-pbrpm.el.  In this case, control button3 is mapped to
-;; 'pg-goals-yank-subterm
-(define-key proof-goals-mode-map [mouse-3] 'pg-goals-yank-subterm)
+;; TODO: use standard Emacs button behaviour here (cf Info mode)
+(define-key proof-goals-mode-map [mouse-1] 'pg-goals-button-action)
+(define-key proof-goals-mode-map [C-mouse-3] 
+  'proof-undo-and-delete-last-successful-command)
 
 
 
@@ -119,6 +113,32 @@ Converts term substructure markup into mouse-highlighted extents."
       (proof-display-and-keep-buffer
        proof-goals-buffer (point-min)))))
 
+;;
+;; Actions in the goals buffer
+;;
+
+(defun pg-goals-button-action (event)
+  "Construct a command based on the mouse-click EVENT."
+  (interactive "e")
+  (let* ((posn     (event-start event))
+	 (pos      (posn-point posn))
+	 (buf      (window-buffer (posn-window posn)))
+	 (props    (text-properties-at pos buf))
+	 (sendback (plist-get props 'sendback)))
+    (cond
+     (sendback
+      (with-current-buffer buf
+	(let* ((cmdstart (previous-single-property-change pos 'sendback 
+							  nil (point-min)))
+	       (cmdend   (next-single-property-change pos 'sendback 
+						      nil (point-max)))
+	       (cmd      (buffer-substring-no-properties cmdstart cmdend)))
+	  (proof-insert-sendback-command cmd)))))))
+
+	
+
+
+
 (provide 'pg-goals)
 
 ;;; pg-goals.el ends here
diff --git a/generic/pg-response.el b/generic/pg-response.el
index bb43250a..7176fae3 100644
--- a/generic/pg-response.el
+++ b/generic/pg-response.el
@@ -1,6 +1,6 @@
 ;; pg-response.el --- Proof General response buffer mode.
 ;;
-;; Copyright (C) 1994-2008 LFCS Edinburgh.
+;; Copyright (C) 1994-2009 LFCS Edinburgh.
 ;; Authors:   David Aspinall, Healfdene Goguen,
 ;;		Thomas Kleymann and Dilip Sequeira
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
@@ -41,9 +41,6 @@
 (define-derived-mode proof-response-mode proof-universal-keys-only-mode
   "PGResp" "Responses from Proof Assistant"
   (setq proof-buffer-type 'response)
-  (define-key proof-response-mode-map [(button2)] 'pg-goals-button-action)
-  (define-key proof-response-mode-map [q] 'bury-buffer)
-  (define-key proof-response-mode-map [c] 'pg-response-clear-displays)
   (add-hook 'kill-buffer-hook 'pg-save-from-death nil t)
   (easy-menu-add proof-response-mode-menu proof-response-mode-map)
   (easy-menu-add proof-assistant-menu proof-response-mode-map)
@@ -55,12 +52,24 @@
   (set-buffer-modified-p nil)
   (setq cursor-type 'bar))
 
+;;
+;; Menu for response buffer
+;;
 (proof-eval-when-ready-for-assistant ; proof-aux-menu depends on <PA>
     (easy-menu-define proof-response-mode-menu
       proof-response-mode-map
       "Menu for Proof General response buffer."
       (proof-aux-menu)))
 
+;;
+;; Keys for response buffer
+;;
+;; TODO: use standard Emacs button behaviour here (cf Info mode)
+(define-key proof-response-mode-map [mouse-1] 'pg-goals-button-action)
+(define-key proof-response-mode-map [q] 'bury-buffer)
+(define-key proof-response-mode-map [c] 'pg-response-clear-displays)
+
+
 ;;;###autoload
 (defun proof-response-config-done ()
   "Complete initialisation of a response-mode derived buffer."
diff --git a/generic/proof-script.el b/generic/proof-script.el
index b7be033e..d9ef6d44 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -1,6 +1,6 @@
 ;;; proof-script.el --- Major mode for proof assistant script files.
 ;;
-;; Copyright (C) 1994-2008 LFCS Edinburgh.
+;; Copyright (C) 1994-2009 LFCS Edinburgh.
 ;; Authors:   David Aspinall, Yves Bertot, Healfdene Goguen,
 ;;            Thomas Kleymann and Dilip Sequeira
 ;; License:   GPL (GNU GENERAL PUBLIC LICENSE)
@@ -2227,7 +2227,7 @@ appropriate."
 ;;;###autoload
 (defun proof-insert-sendback-command (cmd)
   "Insert CMD into the proof script, execute assert-until-point."
-  (let (span)
+  (proof-with-script-buffer
     (proof-goto-end-of-locked)
     (insert "\n") ;; could be user opt 
     (insert cmd)