blob: 49e9d0edfcce2e8d374b66054bc708486978bb04 (
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
|
;;--------------------------------------------------------------------------;;
;;--------------------------------------------------------------------------;;
;; 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\\|elim\\|rewrite\\)\\|"
"a\\(dd_path\\|uthor\\)\\|"
"c\\(l\\(aim\\|ose_def\\)\\|or\\(ollary\\)?\\)\\|"
"d\\(e\\(f\\(_thlist\\)?\\|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\\)"
"\\)[ \t\n\r.]")
'(0 'font-lock-keyword-face t))
;proof command
(cons (concat "\\([ \t]\\|^\\)\\("
"a\\(bort\\|fter\\|pply\\|xiom\\)\\|"
"by_absurd\\|"
"constraints\\|"
"elim\\|"
"from\\|"
"goals\\|"
"in\\(tros?\\|stance\\)\\|"
"l\\(oc\\(al\\|k\\)\\|efts?\\)\\|"
"next\\|"
"prove\\|"
"r\\(e\\(write\\(_hyp\\)?\\|name\\)\\|mh\\)\\|"
"s\\(elect\\|lh\\)\\|"
"trivial\\|"
"u\\(se\\|n\\(do\\|fold\\(_hyp\\)?\\|lock\\)\\)"
"\\)[ \t.]")
'(0 'font-lock-type-face t))))
;;--------------------------------------------------------------------------;;
;;--------------------------------------------------------------------------;;
;; phox-sym-lock tables
;;--------------------------------------------------------------------------;;
(if proof-running-on-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)
("&" 0 1 217)
("<->" 0 1 171)
("=>" 0 1 222)
("->" 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)
(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)
|