Extend proof-shell-identifier-under-mouse to allow regions, and also depend on buffer context.

3 files changed, 34 insertions, 13 deletions

diff --git a/generic/pg-user.el b/generic/pg-user.el
index 4351a8b3..7e8aa173 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -1043,18 +1043,36 @@ The function `substitute-command-keys' is called on the argument."
 (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))))))
+      (let (identifier ctxt oldend) 
+	(save-selected-window
+	  (save-selected-frame
+	    (save-excursion
+	      (if (event-window event)
+		  (progn
+		    (select-window (event-window event))
+		    (setq oldend (if (region-exists-p)
+				     (region-end)))))
+	      (mouse-set-point event)
+	      (setq identifier
+		    ;; If there's an active region in this buffer, use that
+		    ;; instead of the identifier under point.  Since
+		    ;; region-end moves immediately to new point with 
+		    ;; zmacs-regions we use oldend instead of current.
+		    (if (region-exists-p)
+			(buffer-substring (region-beginning) 
+					  (or oldend (region-end)))
+		     (setq identifier (current-word))))
+	      (setq ctxt (proof-buffer-syntactic-context)))))
 	(unless (or (null identifier)
 		    (string-equal identifier ""))
 	  (proof-shell-invisible-command 
-	   (format proof-shell-identifier-under-mouse-cmd
-		   identifier))))))
-				    
-
+	   (if (stringp proof-shell-identifier-under-mouse-cmd)
+	       ;; simple customization
+	       (format proof-shell-identifier-under-mouse-cmd identifier)
+	     ;; buffer-syntactic context dependent, as an alist
+	     ;; (handy for Isabelle: not a true replacement for parsing)
+	     (format (nth 1 (assq ctxt proof-shell-identifier-under-mouse-cmd))
+		     identifier)))))))
 
 
 
diff --git a/generic/proof-config.el b/generic/proof-config.el
index 5935df1f..f3aea42c 100644
--- a/generic/proof-config.el
+++ b/generic/proof-config.el
@@ -2006,11 +2006,11 @@ A string with %s replaced by the dependency name."
 (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
+A string with %s replaced by the identifier, or maybe an association
+list between values for `proof-buffer-syntactic-context' and strings."
+  :type '(or string (list (cons (choice 'nil 'string 'comment)  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
diff --git a/isar/isar.el b/isar/isar.el
index 615d40e2..b7b87a43 100644
--- a/isar/isar.el
+++ b/isar/isar.el
@@ -247,7 +247,10 @@ See -k option for Isabelle interface script."
    proof-shell-theorem-dependency-list-regexp "Proof General, theorem dependencies of \\(.*\\) are \"\\(.*\\)\"\361"
    proof-shell-theorem-dependency-list-split "\" \""
    proof-shell-show-dependency-cmd "thm %s;"
-   proof-shell-identifier-under-mouse-cmd "thm %s;"
+   proof-shell-identifier-under-mouse-cmd 
+   '((nil     "thm %s;")
+     (string  "term \"%s\";")
+     (comment "term \"%s\";"))
 
    ;; Allow font-locking for output based on hidden annotations, see
    ;; isar-output-font-lock-keywords-1