dc45444e |
1 | ;; promela-mode.el --- major mode for editing PROMELA program files |
2 | ;; $Revision: 1.11 $ $Date: 2001/07/09 18:36:45 $ $Author: engstrom $ |
3 | |
4 | ;; Author: Eric Engstrom <eric.engstrom@honeywell.com> |
5 | ;; Maintainer: Eric Engstrom |
6 | ;; Keywords: spin, promela, tools |
7 | |
8 | ;; Copyright (C) 1998-2003 Eric Engstrom / Honeywell Laboratories |
9 | |
10 | ;; ... Possibly insert GPL here someday ... |
11 | |
12 | ;;; Commentary: |
13 | |
14 | ;; This file contains code for a GNU Emacs major mode for editing |
15 | ;; PROMELA (SPIN) program files. |
16 | |
17 | ;; Type "C-h m" in Emacs (while in a buffer in promela-mode) for |
18 | ;; information on how to configure indentation and fontification, |
19 | ;; or look at the configuration variables below. |
20 | |
21 | ;; To use, place promela-mode.el in a directory in your load-path. |
22 | ;; Then, put the following lines into your .emacs and promela-mode |
23 | ;; will be automatically loaded when editing a PROMELA program. |
24 | |
25 | ;; (autoload 'promela-mode "promela-mode" "PROMELA mode" nil t) |
26 | ;; (setq auto-mode-alist |
27 | ;; (append |
28 | ;; (list (cons "\\.promela$" 'promela-mode) |
29 | ;; (cons "\\.spin$" 'promela-mode) |
30 | ;; (cons "\\.pml$" 'promela-mode) |
31 | ;; ;; (cons "\\.other-extensions$" 'promela-mode) |
32 | ;; ) |
33 | ;; auto-mode-alist)) |
34 | |
35 | ;; If you wish for promela-mode to be used for files with other |
36 | ;; extensions you add your own patterned after the code above. |
37 | |
38 | ;; Note that promela-mode adhears to the font-lock "standards" and |
39 | ;; defines several "levels" of fontification or colorization. The |
40 | ;; default is fairly gaudy, so I can imagine that some folks would |
41 | ;; like a bit less. FMI: see `font-lock-maximum-decoration' |
42 | |
43 | ;; This mode is known to work under the following versions of emacs: |
44 | ;; - XEmacs: 19.16, 20.x, 21.x |
45 | ;; - FSF/GNU Emacs: 19.34 |
46 | ;; - NTEmacs (FSF): 20.[67] |
47 | ;; That is not to say there are no bugs specific to one of those versions :-) |
48 | |
49 | ;; Please send any comments, bugs, patches or other requests to |
50 | ;; Eric Engstrom at engstrom@htc.honeywell.com |
51 | |
52 | ;; To-Do: |
53 | ;; - compile/syntax-check/verify? (suggested by R.Goldman) |
54 | ;; - indentation - splitting lines at logical operators (M. Rangarajan) |
55 | ;; [ This might "devolve" to indentation after "->" or ";" |
56 | ;; being as is, but anything else indent even more? ] |
57 | ;; :: SomeReallyLongArrayRef[this].typedefField != SomeReallyLongConstant -> /* some-comment */ |
58 | ;; [ Suggestion would be to break the first line after the !=, therefore: ] |
59 | ;; :: SomeReallyLongArrayRef[this].typedefField |
60 | ;; != SomeReallyLongConstant -> /* some-comment */ |
61 | ;; [ at this point I'm not so sure about this change... EE: 2001/05/19 ] |
62 | \f |
63 | ;;; ------------------------------------------------------------------------- |
64 | ;;; Code: |
65 | |
66 | ;; NOTE: same as CVS revision: |
67 | (defconst promela-mode-version "$Revision: 1.11 $" |
68 | "Promela-mode version number.") |
69 | |
70 | ;; ------------------------------------------------------------------------- |
71 | ;; The following constant values can be modified by the user in a .emacs file |
72 | |
73 | (defconst promela-block-indent 2 |
74 | "*Controls indentation of lines within a block (`{') construct") |
75 | |
76 | (defconst promela-selection-indent 2 |
77 | "*Controls indentation of options within a selection (`if') |
78 | or iteration (`do') construct") |
79 | |
80 | (defconst promela-selection-option-indent 3 |
81 | "*Controls indentation of lines after options within selection or |
82 | iteration construct (`::')") |
83 | |
84 | (defconst promela-comment-col 32 |
85 | "*Defines the desired comment column for comments to the right of text.") |
86 | |
87 | (defconst promela-tab-always-indent t |
88 | "*Non-nil means TAB in Promela mode should always reindent the current line, |
89 | regardless of where in the line point is when the TAB command is used.") |
90 | |
91 | (defconst promela-auto-match-delimiter t |
92 | "*Non-nil means typing an open-delimiter (i.e. parentheses, brace, quote, etc) |
93 | should also insert the matching closing delmiter character.") |
94 | |
95 | ;; That should be about it for most users... |
96 | ;; unless you wanna hack elisp, the rest of this is probably uninteresting |
97 | |
98 | \f |
99 | ;; ------------------------------------------------------------------------- |
100 | ;; help determine what emacs we have here... |
101 | |
102 | (defconst promela-xemacsp (string-match "XEmacs" (emacs-version)) |
103 | "Non-nil if we are running in the XEmacs environment.") |
104 | |
105 | ;;;(defconst promela-xemacs20p (and promela-xemacsp (>= emacs-major-version 20)) |
106 | ;; "Non-nil if we are running in an XEmacs environment version 20 or greater.") |
107 | |
108 | ;; ------------------------------------------------------------------------- |
109 | ;; promela-mode font faces/definitions |
110 | |
111 | ;; make use of font-lock stuff, so say that explicitly |
112 | (require 'font-lock) |
113 | |
114 | ;; BLECH! YUCK! I just wish these guys could agree to something.... |
115 | ;; Faces available in: ntemacs emacs xemacs xemacs xemacs |
116 | ;; font-lock- xxx -face 20.6 19.34 19.16 20.x 21.x |
117 | ;; -builtin- X |
118 | ;; -constant- X |
119 | ;; -comment- X X X X X |
120 | ;; -doc-string- X X X |
121 | ;; -function-name- X X X X X |
122 | ;; -keyword- X X X X X |
123 | ;; -preprocessor- X X X |
124 | ;; -reference- X X X X |
125 | ;; -signal-name- X X!20.0 |
126 | ;; -string- X X X X X |
127 | ;; -type- X X X X X |
128 | ;; -variable-name- X X X X X |
129 | ;; -warning- X X |
130 | |
131 | ;;; Compatibility on faces between versions of emacs-en |
132 | (unless promela-xemacsp |
133 | |
134 | (defvar font-lock-preprocessor-face 'font-lock-preprocessor-face |
135 | "Face name to use for preprocessor statements.") |
136 | ;; For consistency try to define the preprocessor face == builtin face |
137 | (condition-case nil |
138 | (copy-face 'font-lock-builtin-face 'font-lock-preprocessor-face) |
139 | (error |
140 | (defface font-lock-preprocessor-face |
141 | '((t (:foreground "blue" :italic nil :underline t))) |
142 | "Face Lock mode face used to highlight preprocessor statements." |
143 | :group 'font-lock-highlighting-faces))) |
144 | |
145 | (defvar font-lock-reference-face 'font-lock-reference-face |
146 | "Face name to use for constants and reference and label names.") |
147 | ;; For consistency try to define the reference face == constant face |
148 | (condition-case nil |
149 | (copy-face 'font-lock-constant-face 'font-lock-reference-face) |
150 | (error |
151 | (defface font-lock-reference-face |
152 | '((((class grayscale) (background light)) |
153 | (:foreground "LightGray" :bold t :underline t)) |
154 | (((class grayscale) (background dark)) |
155 | (:foreground "Gray50" :bold t :underline t)) |
156 | (((class color) (background light)) (:foreground "CadetBlue")) |
157 | (((class color) (background dark)) (:foreground "Aquamarine")) |
158 | (t (:bold t :underline t))) |
159 | "Font Lock mode face used to highlight constancs, references and labels." |
160 | :group 'font-lock-highlighting-faces))) |
161 | |
162 | ) |
163 | |
164 | ;; send-poll "symbol" face is custom to promela-mode |
165 | ;; but check for existence to allow someone to override it |
166 | (defvar promela-fl-send-poll-face 'promela-fl-send-poll-face |
167 | "Face name to use for Promela Send or Poll symbols: `!' or `?'") |
168 | (copy-face (if promela-xemacsp 'modeline 'region) |
169 | 'promela-fl-send-poll-face) |
170 | |
171 | ;; some emacs-en don't define or have regexp-opt available. |
172 | (unless (functionp 'regexp-opt) |
173 | (defmacro regexp-opt (strings) |
174 | "Cheap imitation of `regexp-opt' since it's not availble in this emacs" |
175 | `(mapconcat 'identity ,strings "\\|"))) |
176 | |
177 | \f |
178 | ;; ------------------------------------------------------------------------- |
179 | ;; promela-mode font lock specifications/regular-expressions |
180 | ;; - for help, look at definition of variable 'font-lock-keywords |
181 | ;; - some fontification ideas from -- [engstrom:20010309.1435CST] |
182 | ;; Pat Tullman (tullmann@cs.utah.edu) and |
183 | ;; Ny Aina Razermera Mamy (ainarazr@cs.uoregon.edu) |
184 | ;; both had promela-mode's that I discovered after starting this one... |
185 | ;; (but neither did any sort of indentation ;-) |
186 | |
187 | (defconst promela-font-lock-keywords-1 nil |
188 | "Subdued level highlighting for Promela mode.") |
189 | |
190 | (defconst promela-font-lock-keywords-2 nil |
191 | "Medium level highlighting for Promela mode.") |
192 | |
193 | (defconst promela-font-lock-keywords-3 nil |
194 | "Gaudy level highlighting for Promela mode.") |
195 | |
196 | ;; set each of those three variables now.. |
197 | (let ((promela-keywords |
198 | (eval-when-compile |
199 | (regexp-opt |
200 | '("active" "assert" "atomic" "break" "d_step" |
201 | "do" "dproctype" "else" "empty" "enabled" |
202 | "eval" "fi" "full" "goto" "hidden" "if" "init" |
203 | "inline" "len" "local" "mtype" "nempty" "never" |
204 | "nfull" "od" "of" "pcvalue" "printf" "priority" |
205 | "proctype" "provided" "run" "show" "skip" |
206 | "timeout" "trace" "typedef" "unless" "xr" "xs")))) |
207 | (promela-types |
208 | (eval-when-compile |
209 | (regexp-opt '("bit" "bool" "byte" "short" |
210 | "int" "unsigned" "chan"))))) |
211 | |
212 | ;; really simple fontification (strings and comments come for "free") |
213 | (setq promela-font-lock-keywords-1 |
214 | (list |
215 | ;; Keywords: |
216 | (cons (concat "\\<\\(" promela-keywords "\\)\\>") |
217 | 'font-lock-keyword-face) |
218 | ;; Types: |
219 | (cons (concat "\\<\\(" promela-types "\\)\\>") |
220 | 'font-lock-type-face) |
221 | ;; Special constants: |
222 | '("\\<_\\(np\\|pid\\|last\\)\\>" . font-lock-reference-face))) |
223 | |
224 | ;; more complex fontification |
225 | ;; add function (proctype) names, lables and goto statements |
226 | ;; also add send/receive/poll fontification |
227 | (setq promela-font-lock-keywords-2 |
228 | (append promela-font-lock-keywords-1 |
229 | (list |
230 | ;; ANY Pre-Processor directive (lazy method: any line beginning with "#[a-z]+") |
231 | '("^\\(#[ \t]*[a-z]+\\)" 1 'font-lock-preprocessor-face t) |
232 | |
233 | ;; "Functions" (proctype-s and inline-s) |
234 | (list (concat "\\<\\(" |
235 | (eval-when-compile |
236 | (regexp-opt '("run" "dproctype" "proctype" "inline"))) |
237 | "\\)\\>[ \t]*\\(\\sw+\\)?") |
238 | ;;'(1 'font-lock-keyword-face nil) |
239 | '(2 'font-lock-function-name-face nil t)) |
240 | |
241 | ;; Labels and GOTO labels |
242 | '("^\\(\\sw+\\):" 1 'font-lock-reference-face) |
243 | '("\\<\\(goto\\)\\>[ \t]+\\(\\sw+\\)" |
244 | ;;(1 'font-lock-keyword-face nil) |
245 | (2 'font-lock-reference-face nil t)) |
246 | |
247 | ;; Send, Receive and Poll |
248 | '("\\(\\sw+\\)\\(\\[[^\\?!]+\\]\\)?\\(\\??\\?\\|!?!\\)\\(\\sw+\\)" |
249 | (1 'font-lock-variable-name-face nil t) |
250 | (3 'promela-fl-send-poll-face nil t) |
251 | (4 'font-lock-reference-face nil t) |
252 | ) |
253 | ))) |
254 | |
255 | ;; most complex fontification |
256 | ;; add pre-processor directives, typed variables and hidden/typedef decls. |
257 | (setq promela-font-lock-keywords-3 |
258 | (append promela-font-lock-keywords-2 |
259 | (list |
260 | ;; ANY Pre-Processor directive (lazy method: any line beginning with "#[a-z]+") |
261 | ;;'("^\\(#[ \t]*[a-z]+\\)" 1 'font-lock-preprocessor-face t) |
262 | ;; "defined" in an #if or #elif and associated macro names |
263 | '("^#[ \t]*\\(el\\)?if\\>" |
264 | ("\\<\\(defined\\)\\>[ \t]*(?\\(\\sw+\\)" nil nil |
265 | (1 'font-lock-preprocessor-face nil t) |
266 | (2 'font-lock-reference-face nil t))) |
267 | '("^#[ \t]*ifn?def\\>" |
268 | ("[ \t]*\\(\\sw+\\)" nil nil |
269 | (1 'font-lock-reference-face nil t))) |
270 | ;; Filenames in #include <...> directives |
271 | '("^#[ \t]*include[ \t]+<\\([^>\"\n]+\\)>" 1 'font-lock-string-face nil t) |
272 | ;; Defined functions and constants/types (non-functions) |
273 | '("^#[ \t]*define[ \t]+" |
274 | ("\\(\\sw+\\)(" nil nil (1 'font-lock-function-name-face nil t)) |
275 | ("\\(\\sw+\\)[ \t]+\\(\\sw+\\)" nil nil (1 'font-lock-variable-name-face) |
276 | (2 'font-lock-reference-face nil t)) |
277 | ("\\(\\sw+\\)[^(]?" nil nil (1 'font-lock-reference-face nil t))) |
278 | |
279 | ;; Types AND variables |
280 | ;; - room for improvement: (i.e. don't currently): |
281 | ;; highlight user-defined types and asociated variable declarations |
282 | (list (concat "\\<\\(" promela-types "\\)\\>") |
283 | ;;'(1 'font-lock-type-face) |
284 | ;; now match the variables after the type definition, if any |
285 | '(promela-match-variable-or-declaration |
286 | nil nil |
287 | (1 'font-lock-variable-name-face) ;; nil t) |
288 | (2 font-lock-reference-face nil t))) |
289 | |
290 | ;; Typedef/hidden types and declarations |
291 | '("\\<\\(typedef\\|hidden\\)\\>[ \t]*\\(\\sw+\\)?" |
292 | ;;(1 'font-lock-keyword-face nil) |
293 | (2 'font-lock-type-face nil t) |
294 | ;; now match the variables after the type definition, if any |
295 | (promela-match-variable-or-declaration |
296 | nil nil |
297 | (1 'font-lock-variable-name-face nil t) |
298 | (2 'font-lock-reference-face nil t))) |
299 | ))) |
300 | ) |
301 | |
302 | (defvar promela-font-lock-keywords promela-font-lock-keywords-1 |
303 | "Default expressions to highlight in Promela mode.") |
304 | |
305 | ;; Font-lock matcher functions: |
306 | (defun promela-match-variable-or-declaration (limit) |
307 | "Match, and move over, any declaration/definition item after point. |
308 | Matches after point, but ignores leading whitespace characters. |
309 | Does not move further than LIMIT. |
310 | |
311 | The expected syntax of a declaration/definition item is `word' (preceded |
312 | by optional whitespace) optionally followed by a `= value' (preceded and |
313 | followed by more optional whitespace) |
314 | |
315 | Thus the regexp matches after point: word [ = value ] |
316 | ^^^^ ^^^^^ |
317 | Where the match subexpressions are: 1 2 |
318 | |
319 | The item is delimited by (match-beginning 1) and (match-end 1). |
320 | If (match-beginning 2) is non-nil, the item is followed by a `value'." |
321 | (when (looking-at "[ \t]*\\(\\sw+\\)[ \t]*=?[ \t]*\\(\\sw+\\)?[ \t]*,?") |
322 | (goto-char (min limit (match-end 0))))) |
323 | |
324 | \f |
325 | ;; ------------------------------------------------------------------------- |
326 | ;; "install" promela-mode font lock specifications |
327 | |
328 | ;; FMI: look up 'font-lock-defaults |
329 | (defconst promela-font-lock-defaults |
330 | '( |
331 | (promela-font-lock-keywords |
332 | promela-font-lock-keywords-1 |
333 | promela-font-lock-keywords-2 |
334 | promela-font-lock-keywords-3) ;; font-lock stuff (keywords) |
335 | nil ;; keywords-only flag |
336 | nil ;; case-fold keyword searching |
337 | ;;((?_ . "w") (?$ . ".")) ;; mods to syntax table |
338 | nil ;; mods to syntax table (see below) |
339 | nil ;; syntax-begin |
340 | (font-lock-mark-block-function . mark-defun)) |
341 | ) |
342 | |
343 | ;; "install" the font-lock-defaults based upon version of emacs we have |
344 | (cond (promela-xemacsp |
345 | (put 'promela-mode 'font-lock-defaults promela-font-lock-defaults)) |
346 | ((not (assq 'promela-mode font-lock-defaults-alist)) |
347 | (setq font-lock-defaults-alist |
348 | (cons |
349 | (cons 'promela-mode promela-font-lock-defaults) |
350 | font-lock-defaults-alist)))) |
351 | |
352 | \f |
353 | ;; ------------------------------------------------------------------------- |
354 | ;; other promela-mode specific definitions |
355 | |
356 | (defconst promela-defun-prompt-regexp |
357 | "^[ \t]*\\(d?proctype\\|init\\|inline\\|never\\|trace\\|typedef\\|mtype\\s-+=\\)[^{]*" |
358 | "Regexp describing the beginning of a Promela top-level definition.") |
359 | |
360 | (defvar promela-mode-syntax-table nil |
361 | "Syntax table in use in PROMELA-mode buffers.") |
362 | (if promela-mode-syntax-table |
363 | () |
364 | (setq promela-mode-syntax-table (make-syntax-table)) |
365 | (modify-syntax-entry ?\\ "\\" promela-mode-syntax-table) |
366 | (modify-syntax-entry ?/ ". 14" promela-mode-syntax-table) |
367 | (modify-syntax-entry ?* ". 23" promela-mode-syntax-table) |
368 | (modify-syntax-entry ?+ "." promela-mode-syntax-table) |
369 | (modify-syntax-entry ?- "." promela-mode-syntax-table) |
370 | (modify-syntax-entry ?= "." promela-mode-syntax-table) |
371 | (modify-syntax-entry ?% "." promela-mode-syntax-table) |
372 | (modify-syntax-entry ?< "." promela-mode-syntax-table) |
373 | (modify-syntax-entry ?> "." promela-mode-syntax-table) |
374 | (modify-syntax-entry ?& "." promela-mode-syntax-table) |
375 | (modify-syntax-entry ?| "." promela-mode-syntax-table) |
376 | (modify-syntax-entry ?. "_" promela-mode-syntax-table) |
377 | (modify-syntax-entry ?_ "w" promela-mode-syntax-table) |
378 | (modify-syntax-entry ?\' "\"" promela-mode-syntax-table) |
379 | ) |
380 | |
381 | (defvar promela-mode-abbrev-table nil |
382 | "*Abbrev table in use in promela-mode buffers.") |
383 | (if promela-mode-abbrev-table |
384 | nil |
385 | (define-abbrev-table 'promela-mode-abbrev-table |
386 | '( |
387 | ;; Commented out for now - need to think about what abbrevs make sense |
388 | ;; ("assert" "ASSERT" promela-check-expansion 0) |
389 | ;; ("d_step" "D_STEP" promela-check-expansion 0) |
390 | ;; ("break" "BREAK" promela-check-expansion 0) |
391 | ;; ("do" "DO" promela-check-expansion 0) |
392 | ;; ("proctype" "PROCTYPE" promela-check-expansion 0) |
393 | ))) |
394 | |
395 | (defvar promela-mode-map nil |
396 | "Keymap for promela-mode.") |
397 | (if promela-mode-map |
398 | nil |
399 | (setq promela-mode-map (make-sparse-keymap)) |
400 | (define-key promela-mode-map "\t" 'promela-indent-command) |
401 | (define-key promela-mode-map "\C-m" 'promela-newline-and-indent) |
402 | ;(define-key promela-mode-map 'backspace 'backward-delete-char-untabify) |
403 | (define-key promela-mode-map "\C-c\C-p" 'promela-beginning-of-block) |
404 | ;(define-key promela-mode-map "\C-c\C-n" 'promela-end-of-block) |
405 | (define-key promela-mode-map "\M-\C-a" 'promela-beginning-of-defun) |
406 | ;(define-key promela-mode-map "\M-\C-e" 'promela-end-of-defun) |
407 | (define-key promela-mode-map "\C-c(" 'promela-toggle-auto-match-delimiter) |
408 | (define-key promela-mode-map "{" 'promela-open-delimiter) |
409 | (define-key promela-mode-map "}" 'promela-close-delimiter) |
410 | (define-key promela-mode-map "(" 'promela-open-delimiter) |
411 | (define-key promela-mode-map ")" 'promela-close-delimiter) |
412 | (define-key promela-mode-map "[" 'promela-open-delimiter) |
413 | (define-key promela-mode-map "]" 'promela-close-delimiter) |
414 | (define-key promela-mode-map ";" 'promela-insert-and-indent) |
415 | (define-key promela-mode-map ":" 'promela-insert-and-indent) |
416 | ;; |
417 | ;; this is preliminary at best - use at your own risk: |
418 | (define-key promela-mode-map "\C-c\C-s" 'promela-syntax-check) |
419 | ;; |
420 | ;;(define-key promela-mode-map "\C-c\C-d" 'promela-mode-toggle-debug) |
421 | ;;(define-key promela-mode-map "\C-c\C-r" 'promela-mode-revert-buffer) |
422 | ) |
423 | |
424 | (defvar promela-matching-delimiter-alist |
425 | '( (?( . ?)) |
426 | (?[ . ?]) |
427 | (?{ . "\n}") |
428 | ;(?< . ?>) |
429 | (?\' . ?\') |
430 | (?\` . ?\`) |
431 | (?\" . ?\") ) |
432 | "List of pairs of matching open/close delimiters - for auto-insert") |
433 | |
434 | \f |
435 | ;; ------------------------------------------------------------------------- |
436 | ;; Promela-mode itself |
437 | |
438 | (defun promela-mode () |
439 | "Major mode for editing PROMELA code. |
440 | \\{promela-mode-map} |
441 | |
442 | Variables controlling indentation style: |
443 | promela-block-indent |
444 | Relative offset of lines within a block (`{') construct. |
445 | |
446 | promela-selection-indent |
447 | Relative offset of option lines within a selection (`if') |
448 | or iteration (`do') construct. |
449 | |
450 | promela-selection-option-indent |
451 | Relative offset of lines after/within options (`::') within |
452 | selection or iteration constructs. |
453 | |
454 | promela-comment-col |
455 | Defines the desired comment column for comments to the right of text. |
456 | |
457 | promela-tab-always-indent |
458 | Non-nil means TAB in PROMELA mode should always reindent the current |
459 | line, regardless of where in the line the point is when the TAB |
460 | command is used. |
461 | |
462 | promela-auto-match-delimiter |
463 | Non-nil means typing an open-delimiter (i.e. parentheses, brace, |
464 | quote, etc) should also insert the matching closing delmiter |
465 | character. |
466 | |
467 | Turning on PROMELA mode calls the value of the variable promela-mode-hook with |
468 | no args, if that value is non-nil. |
469 | |
470 | For example: ' |
471 | (setq promela-mode-hook '(lambda () |
472 | (setq promela-block-indent 2) |
473 | (setq promela-selection-indent 0) |
474 | (setq promela-selection-option-indent 2) |
475 | (local-set-key \"\\C-m\" 'promela-indent-newline-indent) |
476 | ))' |
477 | |
478 | will indent block two steps, will make selection options aligned with DO/IF |
479 | and sub-option lines indent to a column after the `::'. Also, lines will |
480 | be reindented when you hit RETURN. |
481 | |
482 | Note that promela-mode adhears to the font-lock \"standards\" and |
483 | defines several \"levels\" of fontification or colorization. The |
484 | default is fairly gaudy, so if you would prefer a bit less, please see |
485 | the documentation for the variable: `font-lock-maximum-decoration'. |
486 | " |
487 | (interactive) |
488 | (kill-all-local-variables) |
489 | (setq mode-name "Promela") |
490 | (setq major-mode 'promela-mode) |
491 | (use-local-map promela-mode-map) |
492 | (set-syntax-table promela-mode-syntax-table) |
493 | (setq local-abbrev-table promela-mode-abbrev-table) |
494 | |
495 | ;; Make local variables |
496 | (make-local-variable 'case-fold-search) |
497 | (make-local-variable 'paragraph-start) |
498 | (make-local-variable 'paragraph-separate) |
499 | (make-local-variable 'paragraph-ignore-fill-prefix) |
500 | (make-local-variable 'indent-line-function) |
501 | (make-local-variable 'indent-region-function) |
502 | (make-local-variable 'parse-sexp-ignore-comments) |
503 | (make-local-variable 'comment-start) |
504 | (make-local-variable 'comment-end) |
505 | (make-local-variable 'comment-column) |
506 | (make-local-variable 'comment-start-skip) |
507 | (make-local-variable 'comment-indent-hook) |
508 | (make-local-variable 'defun-prompt-regexp) |
509 | (make-local-variable 'compile-command) |
510 | ;; Now set their values |
511 | (setq case-fold-search t |
512 | paragraph-start (concat "^$\\|" page-delimiter) |
513 | paragraph-separate paragraph-start |
514 | paragraph-ignore-fill-prefix t |
515 | indent-line-function 'promela-indent-command |
516 | ;;indent-region-function 'promela-indent-region |
517 | parse-sexp-ignore-comments t |
518 | comment-start "/* " |
519 | comment-end " */" |
520 | comment-column 32 |
521 | comment-start-skip "/\\*+ *" |
522 | ;;comment-start-skip "/\\*+ *\\|// *" |
523 | ;;comment-indent-hook 'promela-comment-indent |
524 | defun-prompt-regexp promela-defun-prompt-regexp |
525 | ) |
526 | |
527 | ;; Turn on font-lock mode |
528 | ;; (and promela-font-lock-mode (font-lock-mode)) |
529 | (font-lock-mode) |
530 | |
531 | ;; Finally, run the hooks and be done. |
532 | (run-hooks 'promela-mode-hook)) |
533 | |
534 | \f |
535 | ;; ------------------------------------------------------------------------- |
536 | ;; Interactive functions |
537 | ;; |
538 | |
539 | (defun promela-mode-version () |
540 | "Print the current version of promela-mode in the minibuffer" |
541 | (interactive) |
542 | (message (concat "Promela-Mode: " promela-mode-version))) |
543 | |
544 | (defun promela-beginning-of-block () |
545 | "Move backward to start of containing block. |
546 | Containing block may be `{', `do' or `if' construct, or comment." |
547 | (interactive) |
548 | (goto-char (promela-find-start-of-containing-block-or-comment))) |
549 | |
550 | (defun promela-beginning-of-defun (&optional arg) |
551 | "Move backward to the beginning of a defun. |
552 | With argument, do it that many times. |
553 | Negative arg -N means move forward to Nth following beginning of defun. |
554 | Returns t unless search stops due to beginning or end of buffer. |
555 | |
556 | See also 'beginning-of-defun. |
557 | |
558 | This is a Promela-mode specific version since default (in xemacs 19.16 and |
559 | NT-Emacs 20) don't seem to skip comments - they will stop inside them. |
560 | |
561 | Also, this makes sure that the beginning of the defun is actually the |
562 | line which starts the proctype/init/etc., not just the open-brace." |
563 | (interactive "p") |
564 | (beginning-of-defun arg) |
565 | (if (not (looking-at promela-defun-prompt-regexp)) |
566 | (re-search-backward promela-defun-prompt-regexp nil t)) |
567 | (if (promela-inside-comment-p) |
568 | (goto-char (promela-find-start-of-containing-comment)))) |
569 | |
570 | (defun promela-indent-command () |
571 | "Indent the current line as PROMELA code." |
572 | (interactive) |
573 | (if (and (not promela-tab-always-indent) |
574 | (save-excursion |
575 | (skip-chars-backward " \t") |
576 | (not (bolp)))) |
577 | (tab-to-tab-stop) |
578 | (promela-indent-line))) |
579 | |
580 | (defun promela-newline-and-indent () |
581 | "Promela-mode specific newline-and-indent which expands abbrevs before |
582 | running a regular newline-and-indent." |
583 | (interactive) |
584 | (if abbrev-mode |
585 | (expand-abbrev)) |
586 | (newline-and-indent)) |
587 | |
588 | (defun promela-indent-newline-indent () |
589 | "Promela-mode specific newline-and-indent which expands abbrevs and |
590 | indents the current line before running a regular newline-and-indent." |
591 | (interactive) |
592 | (save-excursion (promela-indent-command)) |
593 | (if abbrev-mode |
594 | (expand-abbrev)) |
595 | (newline-and-indent)) |
596 | |
597 | (defun promela-insert-and-indent () |
598 | "Insert the last character typed and re-indent the current line" |
599 | (interactive) |
600 | (insert last-command-char) |
601 | (save-excursion (promela-indent-command))) |
602 | |
603 | (defun promela-open-delimiter () |
604 | "Inserts the open and matching close delimiters, indenting as appropriate." |
605 | (interactive) |
606 | (insert last-command-char) |
607 | (if (and promela-auto-match-delimiter (not (promela-inside-comment-p))) |
608 | (save-excursion |
609 | (insert (cdr (assq last-command-char promela-matching-delimiter-alist))) |
610 | (promela-indent-command)))) |
611 | |
612 | (defun promela-close-delimiter () |
613 | "Inserts and indents a close delimiter." |
614 | (interactive) |
615 | (insert last-command-char) |
616 | (if (not (promela-inside-comment-p)) |
617 | (save-excursion (promela-indent-command)))) |
618 | |
619 | (defun promela-toggle-auto-match-delimiter () |
620 | "Toggle auto-insertion of parens and other delimiters. |
621 | See variable `promela-auto-insert-matching-delimiter'" |
622 | (interactive) |
623 | (setq promela-auto-match-delimiter |
624 | (not promela-auto-match-delimiter)) |
625 | (message (concat "Promela auto-insert matching delimiters " |
626 | (if promela-auto-match-delimiter |
627 | "enabled" "disabled")))) |
628 | |
629 | \f |
630 | ;; ------------------------------------------------------------------------- |
631 | ;; Compilation/Verification functions |
632 | |
633 | ;; all of this is in serious "beta" mode - don't trust it ;-) |
634 | (setq |
635 | promela-compile-command "spin " |
636 | promela-syntax-check-args "-a -v " |
637 | ) |
638 | |
639 | ;;(setq compilation-error-regexp-alist |
640 | ;; (append compilation-error-regexp-alist |
641 | ;; '(("spin: +line +\\([0-9]+\\) +\"\\([^\"]+\\)\"" 2 1)))) |
642 | |
643 | (defun promela-syntax-check () |
644 | (interactive) |
645 | (compile (concat promela-compile-command |
646 | promela-syntax-check-args |
647 | (buffer-name)))) |
648 | |
649 | \f |
650 | ;; ------------------------------------------------------------------------- |
651 | ;; Indentation support functions |
652 | |
653 | (defun promela-indent-around-label () |
654 | "Indent the current line as PROMELA code, |
655 | but make sure to consider the label at the beginning of the line." |
656 | (beginning-of-line) |
657 | (delete-horizontal-space) ; delete any leading whitespace |
658 | (if (not (looking-at "\\sw+:\\([ \t]*\\)")) |
659 | (error "promela-indent-around-label: no label on this line") |
660 | (goto-char (match-beginning 1)) |
661 | (let* ((space (length (match-string 1))) |
662 | (indent (promela-calc-indent)) |
663 | (wanted (max 0 (- indent (current-column))))) |
664 | (if (>= space wanted) |
665 | (delete-region (point) (+ (point) (- space wanted))) |
666 | (goto-char (+ (point) space)) |
667 | (indent-to-column indent))))) |
668 | |
669 | ;; Note that indentation is based ENTIRELY upon the indentation of the |
670 | ;; previous line(s), esp. the previous non-blank line and the line |
671 | ;; starting the current containgng block... |
672 | (defun promela-indent-line () |
673 | "Indent the current line as PROMELA code. |
674 | Return the amount the by which the indentation changed." |
675 | (beginning-of-line) |
676 | (if (looking-at "[ \t]*\\sw+:") |
677 | (promela-indent-around-label) |
678 | (let ((indent (promela-calc-indent)) |
679 | beg |
680 | shift-amt |
681 | (pos (- (point-max) (point)))) |
682 | (setq beg (point)) |
683 | (skip-chars-forward " \t") |
684 | (setq shift-amt (- indent (current-column))) |
685 | (if (zerop shift-amt) |
686 | (if (> (- (point-max) pos) (point)) |
687 | (goto-char (- (point-max) pos))) |
688 | (delete-region beg (point)) |
689 | (indent-to indent) |
690 | (if (> (- (point-max) pos) (point)) |
691 | (goto-char (- (point-max) pos)))) |
692 | shift-amt))) |
693 | |
694 | (defun promela-calc-indent () |
695 | "Return the appropriate indentation for this line as an int." |
696 | (save-excursion |
697 | (beginning-of-line) |
698 | (let* ((orig-point (point)) |
699 | (state (promela-parse-partial-sexp)) |
700 | (paren-depth (nth 0 state)) |
701 | (paren-point (or (nth 1 state) 1)) |
702 | (paren-char (char-after paren-point))) |
703 | ;;(what-cursor-position) |
704 | (cond |
705 | ;; Indent not-at-all - inside a string |
706 | ((nth 3 state) |
707 | (current-indentation)) |
708 | ;; Indent inside a comment |
709 | ((nth 4 state) |
710 | (promela-calc-indent-within-comment)) |
711 | ;; looking at a pre-processor directive - indent=0 |
712 | ((looking-at "[ \t]*#\\(define\\|if\\(n?def\\)?\\|else\\|endif\\)") |
713 | 0) |
714 | ;; If we're not inside a "true" block (i.e. "{}"), then indent=0 |
715 | ;; I think this is fair, since no (indentable) code in promela |
716 | ;; exists outside of a proctype or similar "{ .. }" structure. |
717 | ((zerop paren-depth) |
718 | 0) |
719 | ;; Indent relative to non curly-brace "paren" |
720 | ;; [ NOTE: I'm saving this, but don't use it any more. |
721 | ;; Now, we let parens be indented like curly braces |
722 | ;;((and (>= paren-depth 1) (not (char-equal ?\{ paren-char))) |
723 | ;; (goto-char paren-point) |
724 | ;; (1+ (current-column))) |
725 | ;; |
726 | ;; Last option: indent relative to contaning block(s) |
727 | (t |
728 | (goto-char orig-point) |
729 | (promela-calc-indent-within-block paren-point)))))) |
730 | |
731 | (defun promela-calc-indent-within-block (&optional limit) |
732 | "Return the appropriate indentation for this line, assume within block. |
733 | with optional arg, limit search back to `limit'" |
734 | (save-excursion |
735 | (let* ((stop (or limit 1)) |
736 | (block-point (promela-find-start-of-containing-block stop)) |
737 | (block-type (promela-block-type-after block-point)) |
738 | (indent-point (point)) |
739 | (indent-type (promela-block-type-after indent-point))) |
740 | (if (not block-type) 0 |
741 | ;;(message "paren: %d (%d); block: %s (%d); indent: %s (%d); stop: %d" |
742 | ;; paren-depth paren-point block-type block-point |
743 | ;; indent-type indent-point stop) |
744 | (goto-char block-point) |
745 | (cond |
746 | ;; Indent (options) inside "if" or "do" |
747 | ((memq block-type '(selection iteration)) |
748 | (if (re-search-forward "\\(do\\|if\\)[ \t]*::" indent-point t) |
749 | (- (current-column) 2) |
750 | (+ (current-column) promela-selection-indent))) |
751 | ;; indent (generic code) inside "::" option |
752 | ((eq 'option block-type) |
753 | (if (and (not indent-type) |
754 | (re-search-forward "::.*->[ \t]*\\sw" |
755 | (save-excursion (end-of-line) (point)) |
756 | t)) |
757 | (1- (current-column)) |
758 | (+ (current-column) promela-selection-option-indent)) |
759 | ) |
760 | ;; indent code inside "{" |
761 | ((eq 'block block-type) |
762 | (cond |
763 | ;; if we are indenting the end of a block, |
764 | ;; use indentation of start-of-block |
765 | ((equal 'block-end indent-type) |
766 | (current-indentation)) |
767 | ;; if the start of the code inside the block is not at eol |
768 | ;; then indent to the same column as the block start +some |
769 | ;; [ but ignore comments after "{" ] |
770 | ((and (not (promela-effective-eolp (1+ (point)))) |
771 | (not (looking-at "{[ \t]*/\\*"))) |
772 | (forward-char) ; skip block-start |
773 | (skip-chars-forward "{ \t") ; skip whitespace, if any |
774 | (current-column)) |
775 | ;; anything else we indent +promela-block-indent from |
776 | ;; the indentation of the start of block (where we are now) |
777 | (t |
778 | (+ (current-indentation) |
779 | promela-block-indent)))) |
780 | ;; dunno what kind of block this is - sound an error |
781 | (t |
782 | (error "promela-calc-indent-within-block: unknown block type: %s" block-type) |
783 | (current-indentation))))))) |
784 | |
785 | (defun promela-calc-indent-within-comment () |
786 | "Return the indentation amount for line, assuming that the |
787 | current line is to be regarded as part of a block comment." |
788 | (save-excursion |
789 | (beginning-of-line) |
790 | (skip-chars-forward " \t") |
791 | (let ((indenting-end-of-comment (looking-at "\\*/")) |
792 | (indenting-blank-line (eolp))) |
793 | ;; if line is NOT blank and next char is NOT a "*' |
794 | (if (not (or indenting-blank-line (= (following-char) ?\*))) |
795 | ;; leave indent alone |
796 | (current-column) |
797 | ;; otherwise look back for _PREVIOUS_ possible nested comment start |
798 | (let ((comment-start (save-excursion |
799 | (re-search-backward comment-start-skip)))) |
800 | ;; and see if there is an appropriate middle-comment "*" |
801 | (if (re-search-backward "^[ \t]+\\*" comment-start t) |
802 | (current-indentation) |
803 | ;; guess not, so indent relative to comment start |
804 | (goto-char comment-start) |
805 | (if indenting-end-of-comment |
806 | (current-column) |
807 | (1+ (current-column))))))))) |
808 | |
809 | \f |
810 | ;; ------------------------------------------------------------------------- |
811 | ;; Misc other support functions |
812 | |
813 | (defun promela-parse-partial-sexp (&optional start limit) |
814 | "Return the partial parse state of current defun or from optional start |
815 | to end limit" |
816 | (save-excursion |
817 | (let ((end (or limit (point)))) |
818 | (if start |
819 | (goto-char start) |
820 | (promela-beginning-of-defun)) |
821 | (parse-partial-sexp (point) end)))) |
822 | |
823 | ;;(defun promela-at-end-of-block-p () |
824 | ;; "Return t if cursor is at the end of a promela block" |
825 | ;; (save-excursion |
826 | ;; (let ((eol (progn (end-of-line) (point)))) |
827 | ;; (beginning-of-line) |
828 | ;; (skip-chars-forward " \t") |
829 | ;; ;;(re-search-forward "\\(}\\|\\b\\(od\\|fi\\)\\b\\)" eol t)))) |
830 | ;; (looking-at "[ \t]*\\(od\\|fi\\)\\b")))) |
831 | |
832 | (defun promela-inside-comment-p () |
833 | "Check if the point is inside a comment block." |
834 | (save-excursion |
835 | (let ((origpoint (point)) |
836 | state) |
837 | (goto-char 1) |
838 | (while (> origpoint (point)) |
839 | (setq state (parse-partial-sexp (point) origpoint 0))) |
840 | (nth 4 state)))) |
841 | |
842 | (defun promela-inside-comment-or-string-p () |
843 | "Check if the point is inside a comment or a string." |
844 | (save-excursion |
845 | (let ((origpoint (point)) |
846 | state) |
847 | (goto-char 1) |
848 | (while (> origpoint (point)) |
849 | (setq state (parse-partial-sexp (point) origpoint 0))) |
850 | (or (nth 3 state) (nth 4 state))))) |
851 | |
852 | |
853 | (defun promela-effective-eolp (&optional point) |
854 | "Check if we are at the effective end-of-line, ignoring whitespace" |
855 | (save-excursion |
856 | (if point (goto-char point)) |
857 | (skip-chars-forward " \t") |
858 | (eolp))) |
859 | |
860 | (defun promela-check-expansion () |
861 | "If abbrev was made within a comment or a string, de-abbrev!" |
862 | (if promela-inside-comment-or-string-p |
863 | (unexpand-abbrev))) |
864 | |
865 | (defun promela-block-type-after (&optional point) |
866 | "Return the type of block after current point or parameter as a symbol. |
867 | Return one of 'iteration `do', 'selection `if', 'option `::', |
868 | 'block `{' or `}' or nil if none of the above match." |
869 | (save-excursion |
870 | (goto-char (or point (point))) |
871 | (skip-chars-forward " \t") |
872 | (cond |
873 | ((looking-at "do\\b") 'iteration) |
874 | ;;((looking-at "od\\b") 'iteration-end) |
875 | ((looking-at "if\\b") 'selection) |
876 | ;;((looking-at "fi\\b") 'selection-end) |
877 | ((looking-at "::") 'option) |
878 | ((looking-at "[{(]") 'block) |
879 | ((looking-at "[})]") 'block-end) |
880 | (t nil)))) |
881 | |
882 | (defun promela-find-start-of-containing-comment (&optional limit) |
883 | "Return the start point of the containing comment block. |
884 | Stop at `limit' or beginning of buffer." |
885 | (let ((stop (or limit 1))) |
886 | (save-excursion |
887 | (while (and (>= (point) stop) |
888 | (nth 4 (promela-parse-partial-sexp))) |
889 | (re-search-backward comment-start-skip stop t)) |
890 | (point)))) |
891 | |
892 | (defun promela-find-start-of-containing-block (&optional limit) |
893 | "Return the start point of the containing `do', `if', `::' or |
894 | `{' block or containing comment. |
895 | Stop at `limit' or beginning of buffer." |
896 | (save-excursion |
897 | (skip-chars-forward " \t") |
898 | (let* ((type (promela-block-type-after)) |
899 | (stop (or limit |
900 | (save-excursion (promela-beginning-of-defun) (point)))) |
901 | (state (promela-parse-partial-sexp stop)) |
902 | (level (if (looking-at "\\(od\\|fi\\)\\b") |
903 | 2 |
904 | (if (zerop (nth 0 state)) 0 1)))) |
905 | ;;(message "find-start-of-containing-block: type: %s; level %d; stop %d" |
906 | ;; type level stop) |
907 | (while (and (> (point) stop) (not (zerop level))) |
908 | (re-search-backward |
909 | "\\({\\|}\\|::\\|\\b\\(do\\|od\\|if\\|fi\\)\\b\\)" |
910 | stop 'move) |
911 | ;;(message "looking from %d back-to %d" (point) stop) |
912 | (setq state (promela-parse-partial-sexp stop)) |
913 | (setq level (+ level |
914 | (cond ((or (nth 3 state) (nth 4 state)) 0) |
915 | ((and (= 1 level) (looking-at "::") |
916 | (not (equal type 'option))) -1) |
917 | ((looking-at "\\({\\|\\(do\\|if\\)\\b\\)") -1) |
918 | ((looking-at "\\(}\\|\\(od\\|fi\\)\\b\\)") +1) |
919 | (t 0))))) |
920 | (point)))) |
921 | |
922 | (defun promela-find-start-of-containing-block-or-comment (&optional limit) |
923 | "Return the start point of the containing comment or |
924 | the start of the containing `do', `if', `::' or `{' block. |
925 | Stop at limit or beginning of buffer." |
926 | (if (promela-inside-comment-p) |
927 | (promela-find-start-of-containing-comment limit) |
928 | (promela-find-start-of-containing-block limit))) |
929 | |
930 | ;; ------------------------------------------------------------------------- |
931 | ;; Debugging/testing |
932 | |
933 | ;; (defun promela-mode-toggle-debug () |
934 | ;; (interactive) |
935 | ;; (make-local-variable 'debug-on-error) |
936 | ;; (setq debug-on-error (not debug-on-error))) |
937 | |
938 | ;;(defun promela-mode-revert-buffer () |
939 | ;; (interactive) |
940 | ;; (revert-buffer t t)) |
941 | |
942 | ;; ------------------------------------------------------------------------- |
943 | ;;###autoload |
944 | |
945 | (provide 'promela-mode) |
946 | |
947 | \f |
948 | ;;---------------------------------------------------------------------- |
949 | ;; Change History: |
950 | ;; |
951 | ;; $Log: promela-mode.el,v $ |
952 | ;; Revision 1.11 2001/07/09 18:36:45 engstrom |
953 | ;; - added comments on use of font-lock-maximum-decoration |
954 | ;; - moved basic preprocess directive fontification to "level 2" |
955 | ;; |
956 | ;; Revision 1.10 2001/05/22 16:29:59 engstrom |
957 | ;; - fixed error introduced in fontification levels stuff (xemacs only) |
958 | ;; |
959 | ;; Revision 1.9 2001/05/22 16:21:29 engstrom |
960 | ;; - commented out the compilation / syntax check stuff for now |
961 | ;; |
962 | ;; Revision 1.8 2001/05/22 16:18:49 engstrom |
963 | ;; - Munched history in preparation for first non-Honeywell release |
964 | ;; - Added "levels" of fontification to be controlled by the std. variable: |
965 | ;; 'font-lock-maximum-decoration' |
966 | ;; |
967 | ;; Revision 1.7 2001/04/20 01:41:46 engstrom |
968 | ;; Revision 1.6 2001/04/06 23:57:18 engstrom |
969 | ;; Revision 1.5 2001/04/04 20:04:15 engstrom |
970 | ;; Revision 1.4 2001/03/15 02:22:18 engstrom |
971 | ;; Revision 1.3 2001/03/09 19:39:51 engstrom |
972 | ;; Revision 1.2 2001/03/01 18:07:47 engstrom |
973 | ;; Revision 1.1 2001/02/01 xx:xx:xx engstrom |
974 | ;; migrated to CVS versioning... |
975 | ;; Pre-CVS-History: |
976 | ;; 99-10-04 V0.4 EDE Fixed bug in end-of-block indentation |
977 | ;; Simplified indentation code significantly |
978 | ;; 99-09-2x V0.3 EDE Hacked on indentation more while at FM'99 |
979 | ;; 99-09-16 V0.2 EDE Hacked, hacked, hacked on indentation |
980 | ;; 99-04-01 V0.1 EDE Introduced (less-than) half-baked indentation |
981 | ;; 98-11-05 V0.0 EDE Created - much code stolen from rexx-mode.el |
982 | ;; Mostly just a fontification mode - |
983 | ;; (indentation is HARD ;-) |
984 | ;; |
985 | ;; EOF promela-mode.el |