blob: 3e86dd28880b8a58671eab8345644809fc3cf8b2 (
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
|
(defvar phox-sym-lock-enabled nil) ; da: for clean compile
(defvar phox-sym-lock-color nil) ; da: for clean compile
(defvar phox-sym-lock-keywords nil) ; da: for clean compile
(declare-function phox-sym-lock "phox-sym-lock")
;;--------------------------------------------------------------------------;;
;;--------------------------------------------------------------------------;;
;; Font lock keywords
;;--------------------------------------------------------------------------;;
(defconst phox-font-lock-keywords
(list
;commands
'("(\\*\\([^*]\\|\\*+[^*)]\\)*\\(\\*+)\\|\\**$\\)"
0 'font-lock-comment-face t)
'("\"\\([^\\\"]\\|\\\\.\\)*\""
0 'font-lock-string-face t)
(cons (concat "\\([ \t]\\|^\\)\\("
"Cst\\|"
"Data\\|"
"I\\(mport\\|nductive\\)\\|"
"Use\\|"
"Sort\\|"
"new_\\(intro\\|e\\(lim\\|quation\\)\\|rewrite\\)\\|"
"a\\(dd_path\\|uthor\\)\\|"
"c\\(l\\(aim\\|ose_def\\)\\|or\\(ollary\\)?\\)\\|"
"d\\(e\\(f\\(\\(_thlist\\|rec\\)\\)?\\|l\\(_proof\\)\\)\\|ocuments\\|epend\\)\\|"
"e\\(lim_after_intro\\|xport\\|del\\|show\\)\\|"
"f\\(act\\|lag\\)\\|"
"goal\\|"
"in\\(clude\\|stitute\\)\\|"
"lem\\(ma\\)?\\|"
"p\\(ath\\|r\\(int\\(_sort\\)?\\|iority\\|op\\(osition\\)?\\|ove_claim\\)\\)\\|"
"quit\\|"
"s\\(ave\\|earch\\)\\|"
"t\\(ex\\(_syntax\\)?\\|heo\\(rem\\)?\\|itle\\|ype\\)"
"\\)[ \t\n\r.]")
'(0 'font-lock-keyword-face t))
;proof command
(cons (concat "\\([ \t]\\|^\\)\\("
"a\\(bort\\|fter\\|nd\\|pply\\|ssume\\|xiom\\)\\|"
"by\\(_absurd\\)?\\|"
"constraints\\|"
"elim\\|"
"deduce\\|"
"evaluate\\(_hyp\\)?\\|"
"from\\|"
"goals\\|"
"in\\(tros?\\|stance\\)\\|"
"l\\(oc\\(al\\|k\\)\\|e\\(t\\|fts?\\)\\)\\|"
"next\\|"
"of\\|"
"prove\\|"
"r\\(e\\(write\\(_hyp\\)?\\|name\\)\\|mh\\)\\|"
"s\\(elect\\|how\\|lh\\)\\|"
"t\\(hen\\|rivial\\)\\|"
"u\\(se\\|n\\(do\\|fold\\(_hyp\\)?\\|lock\\)\\)\\|"
"with"
"\\)[ \t.]")
'(0 'font-lock-type-face t))))
;;--------------------------------------------------------------------------;;
;;--------------------------------------------------------------------------;;
;; phox-sym-lock tables
;;--------------------------------------------------------------------------;;
(if (featurep 'xemacs) (require 'phox-sym-lock))
;; to change this table, xfd -fn '-adobe-symbol-*--12-*' may be
;; used to determine the symbol character codes.
(defconst phox-sym-lock-keywords-table
'((">=" 0 1 179)
("<=" 0 1 163)
("!=" 0 1 185)
(":<" 0 1 206)
("[^:]\\(:\\)[^:= \n\t\r]" 1 7 206)
("\\\\/" 0 1 36)
("/\\\\" 0 1 34)
("\\<or\\>" 0 3 218)
("\\<in\\>" 0 3 206)
("\\<notin\\>" 0 4 207)
("\\<inter\\>" 0 3 199)
("\\<union\\>" 0 3 200)
("\\<minus\\>" 0 3 45)
("&" 0 1 217)
("<->" 0 1 171)
("=>" 0 1 222)
("\\<subset\\>" 0 4 204)
("->" 0 1 174)
("~" 0 1 216)
("\\\\" 0 1 108)))
; "If non nil: Overrides default Phox-Sym-Lock patterns for PhoX.")
(defun phox-sym-lock-start ()
(if (and (featurep 'phox-sym-lock) phox-sym-lock-enabled)
(progn
(setq phox-sym-lock-color
(face-foreground 'font-lock-function-name-face))
(if (not phox-sym-lock-keywords)
(phox-sym-lock phox-sym-lock-keywords-table)))))
(provide 'phox-font)
|
