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
;; 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)]))