[isabelle-dev] isar-theorem-at-point

Lawrence Paulson lp15 at cam.ac.uk
Tue Feb 10 11:32:32 CET 2009

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.

;; 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."
       ;;alg stolen from etag.el
	(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)
	     (progn (forward-char 1)
		    (buffer-substring (point)
				      (progn (forward-sexp -1)
					     (while (looking-at "\\s'")
					       (forward-char 1))

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

More information about the isabelle-dev mailing list