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

2 files changed, 36 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.
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 4792c022..5935df1f 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -137,6 +137,7 @@ buffer modes)."
   :type 'boolean
   :group 'proof-user-options)
 
+;; FIXME: next one could be integer value for catchup delay
 (defcustom proof-trace-output-slow-catchup t 
   "*If non-nil, try to redisplay less often during frequent trace output.
 Proof General will try to configure itself to update the display
@@ -2002,6 +2003,14 @@ A string with %s replaced by the dependency name."
   :type 'string
   :group 'proof-shell)
 
+(defcustom proof-shell-identifier-under-mouse-cmd nil
+  "Command sent to the prover to query about an identifier under the mouse.
+This is typically a command used to print a theorem, constant, or whatever.
+A string with %s replaced by the identifier."
+  :type 'string
+  :group 'proof-shell)
+
+
 (defcustom proof-shell-trace-output-regexp nil
   "Matches tracing output which should be displayed in trace buffer.
 Each line which matches this regexp but would otherwise be treated