Finish support for proof-query-identifier

[David Aspinall]

Some time ago, David Aspinall gave me some code that would display the theorem whose identifier was currently pointed out in Proof General. This command was bound to the key combination C-c C-a C-t. It did not work if the identifier contained a qualified name (.) however. The attached version contains a small hack (noslashes) to fix that problem. I am not sure whether anybody else has seen this code, but I certainly find it useful. (Larry Paulson)

;; GNU Emacs doesn't have symbol-near-point apparently
;; stolen from browse-cltl2.el, and in turn:
;; stolen from XEmacs 19.15 syntax.el
(if (not (fboundp (function symbol-near-point)))
    (defun symbol-near-point ()
      "Return the first textual item to the nearest point."
      (interactive)
      ;;alg stolen from etag.el
      (save-excursion
    (if (not (memq (char-syntax (preceding-char)) '(?w ?_)))
        (while (not (looking-at "\\sw\\|\\s_\\|\\'"))
          (forward-char 1)))
    (while (looking-at "\\sw\\|\\s_")
      (forward-char 1))
    (if (re-search-backward "\\sw\\|\\s_" nil t)
        (regexp-quote
         (progn (forward-char 1)
            (buffer-substring (point)
                      (progn (forward-sexp -1)
                         (while (looking-at "\\s'")
                           (forward-char 1))
                         (point)))))
      nil))))

(eval-after-load "isar"
   '(proof-definvisible isar-theorem
            '(format "thm %s" (read-string "theorem: "))))

(eval-after-load "isar"
  '(global-set-key '[f5] 'isar-theorem))

(defun noslashes (s) (replace-in-string s "[\\]" ""))

(eval-after-load "isar"   ; bound to  C-c C-a C-t
   '(proof-definvisible isar-theorem-at-point
            '(format "thm %s" (noslashes (symbol-near-point)))
            [(control t)]))

[David Aspinall]

This feature was actually already implemented at a generic level under a different name.

It is now reworked slightly, and made available in two ways:

• use the new toolbar "info" button or M-x proof-query-identifier (bound to C-c C-i)
• use the awkward mouse binding C-M-mouse-1 which runs pg-identifier-under-mouse-query

The second command adds a span to the buffer which will work as a hover thereafter (experimental).

Still to do: update documentation for this.

[David Aspinall]

Documentation added now, and a few cleanups.