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
|
;; proof-fontlock.el Generic font lock expressions
;; Copyright (C) 1997 LFCS Edinburgh.
;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequiera
;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>
;; $Log$
;; Revision 1.8 1998/06/10 11:45:12 hhg
;; Changed "\\s " to "\\s-" in proof-id as whitespace pattern.
;;
;; Revision 1.7 1998/05/29 09:49:53 tms
;; o outsourced indentation to proof-indent
;; o support indentation of commands
;; o replaced test of Emacs version with availability test of specific
;; features
;; o C-c C-c, C-c C-v and M-tab is now available in all buffers
;;
;; Revision 1.6 1998/05/06 15:56:14 hhg
;; Fixed problem introduced by working on emacs19 in
;; proof-zap-commas-region.
;;
;; Revision 1.5 1998/05/05 14:25:45 hhg
;; Simple white-space changes.
;;
;; Revision 1.4 1998/01/16 15:40:28 djs
;; Commented the code of proof.el and lego.el a bit. Made a minor change
;; to the way errors are handled, so that any delayed output is inserted
;; in the buffer before the error message is printed.
;;
;; Revision 1.3 1997/11/17 17:11:19 djs
;; Added some magic commands: proof-frob-locked-end, proof-try-command,
;; proof-interrupt-process. Added moving nested lemmas above goal for coq.
;; Changed the key mapping for assert-until-point to C-c RET.
;;
;; Revision 1.2 1997/10/13 17:13:50 tms
;; *** empty log message ***
;;
;; Revision 1.1.2.1 1997/10/07 13:34:27 hhg
;; New structure to share as much as possible between LEGO and Coq.
;;
;;
(require 'font-lock)
(defun ids-to-regexp (l)
"transforms a non-empty list of identifiers `l' into a regular
expression matching any of its elements"
(mapconcat (lambda (s) (concat "\\<" s "\\>")) l "\\|"))
;; Generic font-lock
;; proof-commands-regexp is used for indentation
(defvar proof-commands-regexp ""
"Subset of keywords and tacticals which are terminated by the
`proof-terminal-char'")
(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-unfontify-separator}.
(defun proof-ids (proof-id)
"Function to generate a regular expression for separated lists of
identifiers."
(concat proof-id "\\(\\s-*,\\s-*" proof-id "\\)*"))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; font lock faces: declarations, errors, tacticals ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
(defun proof-have-color ()
())
(defvar font-lock-declaration-name-face
(progn
(cond
((proof-have-color)
(copy-face 'bold 'font-lock-declaration-name-face)
;; Emacs 19.28 compiles this down to
;; internal-set-face-1. This is not compatible with XEmacs
(set-face-foreground
'font-lock-declaration-name-face "chocolate"))
(t (copy-face 'bold-italic 'font-lock-declaration-name-face)))))
;; (if running-emacs19
;; (setq font-lock-declaration-name-face
;; (face-name 'font-lock-declaration-name-face))
(defvar font-lock-tacticals-name-face
(if (proof-have-color)
(let ((face (make-face 'font-lock-tacticals-name-face)))
(dont-compile
(set-face-foreground face "MediumOrchid3"))
face)
(copy-face 'bold 'font-lock-tacticals-name-face)))
(defvar font-lock-error-face
(if (proof-have-color)
(let ((face (make-face 'font-lock-error-face)))
(dont-compile
(set-face-foreground face "red"))
face)
(copy-face 'bold 'font-lock-error-face)))
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; A big hack to unfontify commas in declarations and definitions. ;;
;; All that can be said for it is that the previous way of doing ;;
;; this was even more bogus. ;;
;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Refontify the whole line, 'cos that's what font-lock-after-change
;; does.
(defun proof-zap-commas-region (start end length)
(save-excursion
(let
((start (progn (goto-char start) (beginning-of-line) (point)))
(end (progn (goto-char end) (end-of-line) (point))))
(goto-char start)
(while (search-forward "," end t)
(if (memq (get-char-property (- (point) 1) 'face)
'(font-lock-declaration-name-face
font-lock-function-name-face))
(font-lock-remove-face (- (point) 1) (point))
)))))
(defun proof-zap-commas-buffer ()
(proof-zap-commas-region (point-min) (point-max) 0))
(defun proof-unfontify-separator ()
(make-local-variable 'after-change-functions)
(setq after-change-functions
(append (delq 'proof-zap-commas-region after-change-functions)
'(proof-zap-commas-region))))
(provide 'proof-fontlock)
|
