Add simple but effective identifier-under-mouse-query command.

1 files changed, 27 insertions, 1 deletions

diff --git a/generic/pg-user.el b/generic/pg-user.el
index 28fd12ec..b30b2a03 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -990,7 +990,7 @@ If NUM is negative, move upwards.  Return new span."
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;
-;; Message buffer hints
+;; Message buffer hints  (added in PG 3.5)
 ;;
 
 (defun pg-goals-buffers-hint ()
@@ -1026,5 +1026,31 @@ If NUM is negative, move upwards.  Return new span."
 The function `substitute-command-keys' is called on the argument."
   (if pg-show-hints (message (substitute-command-keys hintmsg))))
 
+
+;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
+;;
+;; Identifier under mouse query  (added in PG 3.5)
+;;
+
+;; FIXME: next setting perhaps a bit obnoxious, but this modifier
+;; combination is currently unused.
+(global-set-key '(control meta button1) 'pg-identifier-under-mouse-query)
+
+(defun pg-identifier-under-mouse-query (event)
+  (interactive "e")
+  (if proof-shell-identifier-under-mouse-cmd
+      (let ((identifier (save-selected-window
+			  (save-selected-frame
+			    (save-excursion
+			      (mouse-set-point event)
+			      (current-word))))))
+	(proof-shell-invisible-command 
+	 (format proof-shell-identifier-under-mouse-cmd
+		 identifier)))))
+				    
+
+
+
+
 (provide 'pg-user)
 ;; pg-user.el ends here.