blob: 22aba6e510e80e2e72830758b1b5092423600169 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
|
;;; pg-dev.el --- Developer settings for Proof General
;;
;; Copyright (C) 2008 LFCS Edinburgh.
;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;
;; $Id$
;;
;;; Commentary:
;;
;; Some configuration of Emacs Lisp mode for developing PG, not needed
;; for ordinary users.
;;
;;; Code:
;; Use checkdoc, eldoc, Flyspell, whitespace cleanup:
(add-hook 'emacs-lisp-mode-hook
'(lambda ()
(checkdoc-minor-mode 1)
(turn-on-eldoc-mode)
(flyspell-prog-mode)
(customize-set-variable 'whitespace-action '(cleanup))
(add-hook 'write-file-functions
'whitespace-write-file-hook nil t)))
;; Configure indentation for our macros
(put 'proof-if-setting-configured 'lisp-indent-function 1)
(put 'proof-eval-when-ready-for-assistant 'lisp-indent-function 1)
(put 'proof-define-assistant-command 'lisp-indent-function 'defun)
(put 'proof-define-assistant-command-witharg 'lisp-indent-function 'defun)
(put 'defpgcustom 'lisp-indent-function 'defun)
(put 'proof-map-buffers 'lisp-indent-function 'defun)
(put 'proof-with-current-buffer-if-exists 'lisp-indent-function 'defun)
(defconst pg-dev-lisp-font-lock-keywords
(list
;; FIXME: used to work but now not quite right, see font-lock.el to fix
(concat "(\\(def\\(" ;; also proof-def
;; Function like things
"^(\\(proof-def.*\\|defpg.*\\|defpa.*\\|.*asscustom\\)"
;; Variable like things
"\\([^ \t\n\(\)]*\\)"
;; Any whitespace and declared object.
"[ \t'\(]*"
"\\([^ \t\n\)]+\\)?")
'(1 font-lock-keyword-face)
'(8 (cond ((match-beginning 3) 'font-lock-variable-name-face)
;; ((match-beginning 6) 'font-lock-type-face)
(t 'font-lock-function-name-face))
nil t)))
;(add-hook 'emacs-lisp-mode-hook
; '(lambda ()
; (font-lock-add-keywords 'emacs-lisp-mode
; pg-dev-lisp-font-lock-keywords)))
;;;
;;; Autoloads (as used by "make autoloads")
;;;
(setq autoload-package-name "proof")
(setq generated-autoload-file "proof-autoloads.el")
;;;
;;; Unload utility (not wholly successful)
;;;
(defun unload-pg ()
"Attempt to unload Proof General (for development use only)."
(interactive)
(mapcar
(lambda (feat) (condition-case nil
(unload-feature feat 'force)
(error nil)))
'(proof-splash pg-assoc pg-xml proof-depends proof-indent proof-site
proof-shell proof-menu pg-pbrpm pg-pgip proof-script
proof-autoloads pg-response pg-goals proof-toolbar
proof-easy-config proof-config proof-mmm proof
proof-utils proof-syntax pg-user pg-custom
proof-maths-menu proof-unicode-tokens
pg-thymodes pg-autotest
;;
isar-syntax isar-find-theorems isar-unicode-tokens
isar-autotest interface-setup isabelle-system isar isar-mmm
isar-keywords
;;
coq-abbrev coq-db coq-unicode-tokens coq-local-vars coq coq-syntax
coq-indent coq-autotest)))
;;
;; Proling interesting packages
;;
(defun profile-pg ()
(interactive)
(elp-instrument-package "proof-")
(elp-instrument-package "pg-")
(elp-instrument-package "scomint")
(elp-instrument-package "unicode-tokens")
(elp-instrument-package "coq")
(elp-instrument-package "isar"))
;;
;; Make references to bugs clickable; [e.g., trac #1]
;;
(defun pg-bug-references ()
(interactive)
(bug-reference-mode 1)
(setq bug-reference-bug-regexp
"\\(?:[Tt]rac ?#\\)\\([0-9]+\\)"
bug-reference-url-format
"http://proofgeneral.inf.ed.ac.uk/trac/ticket/%s"))
(add-hook 'emacs-lisp-mode-hook 'pg-bug-references)
(add-hook 'isar-mode-hook 'pg-bug-references)
(add-hook 'coq-mode-hook 'pg-bug-references)
(add-hook 'emacs-lisp-mode-hook 'goto-address-mode)
(provide 'pg-dev)
;;; pg-dev.el ends here
|
