diff options
author | 2003-06-08 21:39:38 +0000 | |
---|---|---|
committer | 2003-06-08 21:39:38 +0000 | |
commit | d9cd3030cc2b1c0f074f9fc5efd7d63fc4369710 (patch) | |
tree | 58f8b7e84358e178b582fc0b03ebdebac84feaea /generic | |
parent | 2c6e3b95b7d9669885129c06112ef608e5cb616a (diff) |
Extend proof-shell-identifier-under-mouse to allow regions, and also depend on buffer context.
Diffstat (limited to 'generic')
-rw-r--r-- | generic/pg-user.el | 36 | ||||
-rw-r--r-- | generic/proof-config.el | 6 |
2 files changed, 30 insertions, 12 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 |