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

1 files changed, 3 insertions, 3 deletions

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