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
|
;; coq-font-lock.el --- Coq syntax highlighting for Emacs - compatibilty code
;; Pierre Courtieu, may 2009
;;
;; Authors: Pierre Courtieu
;; License: GPL (GNU GENERAL PUBLIC LICENSE)
;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr>
;; This is copy paste from ProofGeneral by David Aspinall
;; <David.Aspinall@ed.ac.uk>. ProofGeneral is under GPL and Copyright
;; (C) LFCS Edinburgh.
;;; Commentary:
;; This file contains the code necessary to coq-syntax.el and
;; coq-db.el from ProofGeneral. It is also pocked from ProofGeneral.
;;; History:
;; First created from ProofGeneral may 28th 2009
;;; Code:
(setq coq-version-is-V8-1 t)
(defun coq-build-regexp-list-from-db (db &optional filter)
"Take a keyword database DB and return the list of regexps for font-lock.
If non-nil Optional argument FILTER is a function applying to each line of DB.
For each line if FILTER returns nil, then the keyword is not added to the
regexp. See `coq-syntax-db' for DB structure."
(let ((l db) (res ()))
(while l
(let* ((hd (car l)) (tl (cdr l)) ; hd is the first infos list
(e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry
(e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation
(e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion
(e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing
(e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string
)
;; TODO delete doublons
(when (and e5 (or (not filter) (funcall filter hd)))
(setq res (nconc res (list e5)))) ; careful: nconc destructive!
(setq l tl)))
res
))
(defun filter-state-preserving (l)
; checkdoc-params: (l)
"Not documented."
(not (nth 3 l))) ; fourth argument is nil --> state preserving command
(defun filter-state-changing (l)
; checkdoc-params: (l)
"Not documented."
(nth 3 l)) ; fourth argument is nil --> state preserving command
;; Generic font-lock
(defvar proof-id "\\(\\w\\(\\w\\|\\s_\\)*\\)"
"A regular expression for parsing identifiers.")
;; For font-lock, we treat ,-separated identifiers as one identifier
;; and refontify commata using \{proof-zap-commas}.
(defun proof-anchor-regexp (e)
"Anchor (\\`) and group the regexp E."
(concat "\\`\\(" e "\\)"))
(defun proof-ids (proof-id &optional sepregexp)
"Generate a regular expression for separated lists of identifiers PROOF-ID.
Default is comma separated, or SEPREGEXP if set."
(concat proof-id "\\(\\s-*" (or sepregexp ",") "\\s-*"
proof-id "\\)*"))
(defun proof-ids-to-regexp (l)
"Maps a non-empty list of tokens `L' to a regexp matching any element."
(if (featurep 'xemacs)
(mapconcat (lambda (s) (concat "\\_<" s "\\_>")) l "\\|") ;; old version
(concat "\\_<\\(?:" (mapconcat 'identity l "\\|") "\\)\\_>")))
;; TODO: get rid of this list. Does 'default work widely enough
;; by now?
(defconst pg-defface-window-systems
'(x ;; bog standard
mswindows ;; Windows
w32 ;; Windows
gtk ;; gtk emacs (obsolete?)
mac ;; used by Aquamacs
carbon ;; used by Carbon XEmacs
ns ;; NeXTstep Emacs (Emacs.app)
x-toolkit) ;; possible catch all (but probably not)
"A list of possible values for variable `window-system'.
If you are on a window system and your value of variable
`window-system' is not listed here, you may not get the correct
syntax colouring behaviour.")
(defmacro proof-face-specs (bl bd ow)
"Return a spec for `defface' with BL for light bg, BD for dark, OW o/w."
`(append
(apply 'append
(mapcar
(lambda (ty) (list
(list (list (list 'type ty) '(class color)
(list 'background 'light))
(quote ,bl))
(list (list (list 'type ty) '(class color)
(list 'background 'dark))
(quote ,bd))))
pg-defface-window-systems))
(list (list t (quote ,ow)))))
;;A new face for tactics
(defface coq-solve-tactics-face
(proof-face-specs
(:foreground "forestgreen" t) ; pour les fonds clairs
(:foreground "forestgreen" t) ; pour les fond foncs
()) ; pour le noir et blanc
"Face for names of closing tactics in proof scripts."
:group 'proof-faces)
;;A new face for tactics which fail when they don't kill the current goal
(defface coq-solve-tactics-face
(proof-face-specs
(:foreground "red" t) ; pour les fonds clairs
(:foreground "red" t) ; pour les fond foncs
()) ; pour le noir et blanc
"Face for names of closing tactics in proof scripts."
:group 'proof-faces)
(defconst coq-solve-tactics-face 'coq-solve-tactics-face
"Expression that evaluates to a face.
Required so that 'proof-solve-tactics-face is a proper facename")
(defconst proof-tactics-name-face 'coq-solve-tactics-face)
(defconst proof-tacticals-name-face 'coq-solve-tactics-face)
(provide 'coq-font-lock)
;;; coq-font-lock.el ends here
|
