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
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
|
;;; pg-dev.el --- Developer settings for Proof General
;; This file is part of Proof General.
;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc.
;; Portions © Copyright 2001-2017 Pierre Courtieu
;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
;; Portions © Copyright 2015-2017 Clément Pit-Claudel
;; Author: David Aspinall <David.Aspinall@ed.ac.uk> and others
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;;; Commentary:
;;
;; Some configuration of Emacs Lisp mode for developing PG, not needed
;; for ordinary users.
;;
;;; Code:
(require 'whitespace)
(eval-when-compile
(require 'cl))
(eval-when-compile
(require 'proof-site))
(with-no-warnings
(setq proof-general-debug t))
;; Use checkdoc, eldoc, Flyspell, whitespace, copyright update
;; and byte compilation on save:
(add-hook 'emacs-lisp-mode-hook
(lambda ()
(checkdoc-minor-mode 1)
(eldoc-mode 1)
(flyspell-prog-mode)
(customize-set-variable 'whitespace-action '(cleanup))
(define-key emacs-lisp-mode-map [(control c)(control c)]
'emacs-lisp-byte-compile)
(add-hook 'write-file-functions
'whitespace-write-file-hook nil t)
(add-hook 'before-save-hook
'copyright-update nil t)))
;; Fill in template for new files
(add-hook 'find-file-hook 'auto-insert)
;; 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
(concat "(\\(def" ;; also proof-def
;; Function like things:
;; Variable like things
"\\(pgcustom\\|pacustom\\)\\)"
;; Any whitespace and declared object.
"[ \t'\(]*"
"\\(\\sw+\\)?")
'(1 font-lock-keyword-face)
'(3 (cond ((match-beginning 2) 'font-lock-variable-name-face)
(t 'font-lock-function-name-face))
nil t)))
;; Not working, see font-lock.el for usual emacs lisp settings.
;;(add-hook 'emacs-lisp-mode-hook
;; (lambda ()
;; (font-lock-add-keywords nil
;; 'pg-dev-lisp-font-lock-keywords)))
;;
;; Path set for a clean environment to byte-compile within Emacs
;; without loading.
;;
(defun pg-loadpath ()
(interactive)
(proof-add-to-load-path "../generic/")
(proof-add-to-load-path "../lib/"))
;;;
;;; 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
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-keywords
;;
coq-abbrev coq-db coq-unicode-tokens coq-local-vars coq coq-syntax
coq-indent coq-autotest)))
;;
;; Proling interesting packages
;;
(require 'elp)
;;;###autoload
(defun profile-pg ()
"Configure Proof General for profiling. Use \\[elp-results] to see results."
(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")
(elp-instrument-package "span")
(elp-instrument-package "replace-") ; for replace-regexp etc
(elp-instrument-package "re-search-") ; for re-search-forwad etc
(elp-instrument-package "skip-chars-") ; for skip chars etc
(elp-instrument-list
'(string-match match-string re-search-forward re-search-backward
skip-chars-forward skip-chars-backward
goto-char insert
set-marker marker-position
nreverse nconc mapc
member
redisplay
sit-for
overlay-put overlay-start overlay-end make-overlay
buffer-live-p kill-buffer
process-status get-buffer-process
delete-overlay move-overlay
accept-process-output))
(elp-instrument-package "font-lock"))
;; improve readability of profile results, give milliseconds
(defun elp-pack-number (number width)
(format (concat "%" (number-to-string (- width 3)) ".2f")
(* 100 (string-to-number number))))
;;
;; Make references to bugs clickable; [e.g., trac #1]
;;
(defun pg-bug-references ()
(interactive)
(if (fboundp 'bug-reference-mode)
(with-no-warnings
(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
|
