;; promela-mode.el --- major mode for editing PROMELA program files
;; $Revision: 1.11 $ $Date: 2001/07/09 18:36:45 $ $Author: engstrom $
;; Author: Eric Engstrom <eric.engstrom@honeywell.com>
;; Maintainer: Eric Engstrom
;; Keywords: spin, promela, tools
;; Copyright (C) 1998-2003 Eric Engstrom / Honeywell Laboratories
;; ... Possibly insert GPL here someday ...
;;; Commentary:
;; This file contains code for a GNU Emacs major mode for editing
;; PROMELA (SPIN) program files.
;; Type "C-h m" in Emacs (while in a buffer in promela-mode) for
;; information on how to configure indentation and fontification,
;; or look at the configuration variables below.
;; To use, place promela-mode.el in a directory in your load-path.
;; Then, put the following lines into your .emacs and promela-mode
;; will be automatically loaded when editing a PROMELA program.
;; (autoload 'promela-mode "promela-mode" "PROMELA mode" nil t)
;; (setq auto-mode-alist
;; (append
;; (list (cons "\\.promela$" 'promela-mode)
;; (cons "\\.spin$" 'promela-mode)
;; (cons "\\.pml$" 'promela-mode)
;; ;; (cons "\\.other-extensions$" 'promela-mode)
;; )
;; auto-mode-alist))
;; If you wish for promela-mode to be used for files with other
;; extensions you add your own patterned after the code above.
;; Note that promela-mode adhears to the font-lock "standards" and
;; defines several "levels" of fontification or colorization. The
;; default is fairly gaudy, so I can imagine that some folks would
;; like a bit less. FMI: see `font-lock-maximum-decoration'
;; This mode is known to work under the following versions of emacs:
;; - XEmacs: 19.16, 20.x, 21.x
;; - FSF/GNU Emacs: 19.34
;; - NTEmacs (FSF): 20.[67]
;; That is not to say there are no bugs specific to one of those versions :-)
;; Please send any comments, bugs, patches or other requests to
;; Eric Engstrom at engstrom@htc.honeywell.com
;; To-Do:
;; - compile/syntax-check/verify? (suggested by R.Goldman)
;; - indentation - splitting lines at logical operators (M. Rangarajan)
;; [ This might "devolve" to indentation after "->" or ";"
;; being as is, but anything else indent even more? ]
;; :: SomeReallyLongArrayRef[this].typedefField != SomeReallyLongConstant -> /* some-comment */
;; [ Suggestion would be to break the first line after the !=, therefore: ]
;; :: SomeReallyLongArrayRef[this].typedefField
;; != SomeReallyLongConstant -> /* some-comment */
;; [ at this point I'm not so sure about this change... EE: 2001/05/19 ]
;;; -------------------------------------------------------------------------
;;; Code:
;; NOTE: same as CVS revision:
(defconst promela-mode-version "$Revision: 1.11 $"
"Promela-mode version number.")
;; -------------------------------------------------------------------------
;; The following constant values can be modified by the user in a .emacs file
(defconst promela-block-indent 2
"*Controls indentation of lines within a block (`{') construct")
(defconst promela-selection-indent 2
"*Controls indentation of options within a selection (`if')
or iteration (`do') construct")
(defconst promela-selection-option-indent 3
"*Controls indentation of lines after options within selection or
iteration construct (`::')")
(defconst promela-comment-col 32
"*Defines the desired comment column for comments to the right of text.")
(defconst promela-tab-always-indent t
"*Non-nil means TAB in Promela mode should always reindent the current line,
regardless of where in the line point is when the TAB command is used.")
(defconst promela-auto-match-delimiter t
"*Non-nil means typing an open-delimiter (i.e. parentheses, brace, quote, etc)
should also insert the matching closing delmiter character.")
;; That should be about it for most users...
;; unless you wanna hack elisp, the rest of this is probably uninteresting
;; -------------------------------------------------------------------------
;; help determine what emacs we have here...
(defconst promela-xemacsp (string-match "XEmacs" (emacs-version))
"Non-nil if we are running in the XEmacs environment.")
;;;(defconst promela-xemacs20p (and promela-xemacsp (>= emacs-major-version 20))
;; "Non-nil if we are running in an XEmacs environment version 20 or greater.")
;; -------------------------------------------------------------------------
;; promela-mode font faces/definitions
;; make use of font-lock stuff, so say that explicitly
(require 'font-lock)
;; BLECH! YUCK! I just wish these guys could agree to something....
;; Faces available in: ntemacs emacs xemacs xemacs xemacs
;; font-lock- xxx -face 20.6 19.34 19.16 20.x 21.x
;; -builtin- X
;; -constant- X
;; -comment- X X X X X
;; -doc-string- X X X
;; -function-name- X X X X X
;; -keyword- X X X X X
;; -preprocessor- X X X
;; -reference- X X X X
;; -signal-name- X X!20.0
;; -string- X X X X X
;; -type- X X X X X
;; -variable-name- X X X X X
;; -warning- X X
;;; Compatibility on faces between versions of emacs-en
(unless promela-xemacsp
(defvar font-lock-preprocessor-face 'font-lock-preprocessor-face
"Face name to use for preprocessor statements.")
;; For consistency try to define the preprocessor face == builtin face
(condition-case nil
(copy-face 'font-lock-builtin-face 'font-lock-preprocessor-face)
(error
(defface font-lock-preprocessor-face
'((t (:foreground "blue" :italic nil :underline t)))
"Face Lock mode face used to highlight preprocessor statements."
:group 'font-lock-highlighting-faces)))
(defvar font-lock-reference-face 'font-lock-reference-face
"Face name to use for constants and reference and label names.")
;; For consistency try to define the reference face == constant face
(condition-case nil
(copy-face 'font-lock-constant-face 'font-lock-reference-face)
(error
(defface font-lock-reference-face
'((((class grayscale) (background light))
(:foreground "LightGray" :bold t :underline t))
(((class grayscale) (background dark))
(:foreground "Gray50" :bold t :underline t))
(((class color) (background light)) (:foreground "CadetBlue"))
(((class color) (background dark)) (:foreground "Aquamarine"))
(t (:bold t :underline t)))
"Font Lock mode face used to highlight constancs, references and labels."
:group 'font-lock-highlighting-faces)))
)
;; send-poll "symbol" face is custom to promela-mode
;; but check for existence to allow someone to override it
(defvar promela-fl-send-poll-face 'promela-fl-send-poll-face
"Face name to use for Promela Send or Poll symbols: `!' or `?'")
(copy-face (if promela-xemacsp 'modeline 'region)
'promela-fl-send-poll-face)
;; some emacs-en don't define or have regexp-opt available.
(unless (functionp 'regexp-opt)
(defmacro regexp-opt (strings)
"Cheap imitation of `regexp-opt' since it's not availble in this emacs"
`(mapconcat 'identity ,strings "\\|")))
;; -------------------------------------------------------------------------
;; promela-mode font lock specifications/regular-expressions
;; - for help, look at definition of variable 'font-lock-keywords
;; - some fontification ideas from -- [engstrom:20010309.1435CST]
;; Pat Tullman (tullmann@cs.utah.edu) and
;; Ny Aina Razermera Mamy (ainarazr@cs.uoregon.edu)
;; both had promela-mode's that I discovered after starting this one...
;; (but neither did any sort of indentation ;-)
(defconst promela-font-lock-keywords-1 nil
"Subdued level highlighting for Promela mode.")
(defconst promela-font-lock-keywords-2 nil
"Medium level highlighting for Promela mode.")
(defconst promela-font-lock-keywords-3 nil
"Gaudy level highlighting for Promela mode.")
;; set each of those three variables now..
(let ((promela-keywords
(eval-when-compile
(regexp-opt
'("active" "assert" "atomic" "break" "d_step"
"do" "dproctype" "else" "empty" "enabled"
"eval" "fi" "full" "goto" "hidden" "if" "init"
"inline" "len" "local" "mtype" "nempty" "never"
"nfull" "od" "of" "pcvalue" "printf" "priority"
"proctype" "provided" "run" "show" "skip"
"timeout" "trace" "typedef" "unless" "xr" "xs"))))
(promela-types
(eval-when-compile
(regexp-opt '("bit" "bool" "byte" "short"
"int" "unsigned" "chan")))))
;; really simple fontification (strings and comments come for "free")
(setq promela-font-lock-keywords-1
(list
;; Keywords:
(cons (concat "\\<\\(" promela-keywords "\\)\\>")
'font-lock-keyword-face)
;; Types:
(cons (concat "\\<\\(" promela-types "\\)\\>")
'font-lock-type-face)
;; Special constants:
'("\\<_\\(np\\|pid\\|last\\)\\>" . font-lock-reference-face)))
;; more complex fontification
;; add function (proctype) names, lables and goto statements
;; also add send/receive/poll fontification
(setq promela-font-lock-keywords-2
(append promela-font-lock-keywords-1
(list
;; ANY Pre-Processor directive (lazy method: any line beginning with "#[a-z]+")
'("^\\(#[ \t]*[a-z]+\\)" 1 'font-lock-preprocessor-face t)
;; "Functions" (proctype-s and inline-s)
(list (concat "\\<\\("
(eval-when-compile
(regexp-opt '("run" "dproctype" "proctype" "inline")))
"\\)\\>[ \t]*\\(\\sw+\\)?")
;;'(1 'font-lock-keyword-face nil)
'(2 'font-lock-function-name-face nil t))
;; Labels and GOTO labels
'("^\\(\\sw+\\):" 1 'font-lock-reference-face)
'("\\<\\(goto\\)\\>[ \t]+\\(\\sw+\\)"
;;(1 'font-lock-keyword-face nil)
(2 'font-lock-reference-face nil t))
;; Send, Receive and Poll
'("\\(\\sw+\\)\\(\\[[^\\?!]+\\]\\)?\\(\\??\\?\\|!?!\\)\\(\\sw+\\)"
(1 'font-lock-variable-name-face nil t)
(3 'promela-fl-send-poll-face nil t)
(4 'font-lock-reference-face nil t)
)
)))
;; most complex fontification
;; add pre-processor directives, typed variables and hidden/typedef decls.
(setq promela-font-lock-keywords-3
(append promela-font-lock-keywords-2
(list
;; ANY Pre-Processor directive (lazy method: any line beginning with "#[a-z]+")
;;'("^\\(#[ \t]*[a-z]+\\)" 1 'font-lock-preprocessor-face t)
;; "defined" in an #if or #elif and associated macro names
'("^#[ \t]*\\(el\\)?if\\>"
("\\<\\(defined\\)\\>[ \t]*(?\\(\\sw+\\)" nil nil
(1 'font-lock-preprocessor-face nil t)
(2 'font-lock-reference-face nil t)))
'("^#[ \t]*ifn?def\\>"
("[ \t]*\\(\\sw+\\)" nil nil
(1 'font-lock-reference-face nil t)))
;; Filenames in #include <...> directives
'("^#[ \t]*include[ \t]+<\\([^>\"\n]+\\)>" 1 'font-lock-string-face nil t)
;; Defined functions and constants/types (non-functions)
'("^#[ \t]*define[ \t]+"
("\\(\\sw+\\)(" nil nil (1 'font-lock-function-name-face nil t))
("\\(\\sw+\\)[ \t]+\\(\\sw+\\)" nil nil (1 'font-lock-variable-name-face)
(2 'font-lock-reference-face nil t))
("\\(\\sw+\\)[^(]?" nil nil (1 'font-lock-reference-face nil t)))
;; Types AND variables
;; - room for improvement: (i.e. don't currently):
;; highlight user-defined types and asociated variable declarations
(list (concat "\\<\\(" promela-types "\\)\\>")
;;'(1 'font-lock-type-face)
;; now match the variables after the type definition, if any
'(promela-match-variable-or-declaration
nil nil
(1 'font-lock-variable-name-face) ;; nil t)
(2 font-lock-reference-face nil t)))
;; Typedef/hidden types and declarations
'("\\<\\(typedef\\|hidden\\)\\>[ \t]*\\(\\sw+\\)?"
;;(1 'font-lock-keyword-face nil)
(2 'font-lock-type-face nil t)
;; now match the variables after the type definition, if any
(promela-match-variable-or-declaration
nil nil
(1 'font-lock-variable-name-face nil t)
(2 'font-lock-reference-face nil t)))
)))
)
(defvar promela-font-lock-keywords promela-font-lock-keywords-1
"Default expressions to highlight in Promela mode.")
;; Font-lock matcher functions:
(defun promela-match-variable-or-declaration (limit)
"Match, and move over, any declaration/definition item after point.
Matches after point, but ignores leading whitespace characters.
Does not move further than LIMIT.
The expected syntax of a declaration/definition item is `word' (preceded
by optional whitespace) optionally followed by a `= value' (preceded and
followed by more optional whitespace)
Thus the regexp matches after point: word [ = value ]
^^^^ ^^^^^
Where the match subexpressions are: 1 2
The item is delimited by (match-beginning 1) and (match-end 1).
If (match-beginning 2) is non-nil, the item is followed by a `value'."
(when (looking-at "[ \t]*\\(\\sw+\\)[ \t]*=?[ \t]*\\(\\sw+\\)?[ \t]*,?")
(goto-char (min limit (match-end 0)))))
;; -------------------------------------------------------------------------
;; "install" promela-mode font lock specifications
;; FMI: look up 'font-lock-defaults
(defconst promela-font-lock-defaults
'(
(promela-font-lock-keywords
promela-font-lock-keywords-1
promela-font-lock-keywords-2
promela-font-lock-keywords-3) ;; font-lock stuff (keywords)
nil ;; keywords-only flag
nil ;; case-fold keyword searching
;;((?_ . "w") (?$ . ".")) ;; mods to syntax table
nil ;; mods to syntax table (see below)
nil ;; syntax-begin
(font-lock-mark-block-function . mark-defun))
)
;; "install" the font-lock-defaults based upon version of emacs we have
(cond (promela-xemacsp
(put 'promela-mode 'font-lock-defaults promela-font-lock-defaults))
((not (assq 'promela-mode font-lock-defaults-alist))
(setq font-lock-defaults-alist
(cons
(cons 'promela-mode promela-font-lock-defaults)
font-lock-defaults-alist))))
;; -------------------------------------------------------------------------
;; other promela-mode specific definitions
(defconst promela-defun-prompt-regexp
"^[ \t]*\\(\\(active \\)?d?proctype\\|init\\|inline\\|never\\|trace\\|typedef\\|mtype\\s-+=\\)[ \t][^{]*"
"Regexp describing the beginning of a Promela top-level definition.")
(defvar promela-mode-syntax-table nil
"Syntax table in use in PROMELA-mode buffers.")
(if promela-mode-syntax-table
()
(setq promela-mode-syntax-table (make-syntax-table))
(modify-syntax-entry ?\\ "\\" promela-mode-syntax-table)
(modify-syntax-entry ?/ ". 14" promela-mode-syntax-table)
(modify-syntax-entry ?* ". 23" promela-mode-syntax-table)
(modify-syntax-entry ?+ "." promela-mode-syntax-table)
(modify-syntax-entry ?- "." promela-mode-syntax-table)
(modify-syntax-entry ?= "." promela-mode-syntax-table)
(modify-syntax-entry ?% "." promela-mode-syntax-table)
(modify-syntax-entry ?< "." promela-mode-syntax-table)
(modify-syntax-entry ?> "." promela-mode-syntax-table)
(modify-syntax-entry ?& "." promela-mode-syntax-table)
(modify-syntax-entry ?| "." promela-mode-syntax-table)
(modify-syntax-entry ?. "_" promela-mode-syntax-table)
(modify-syntax-entry ?_ "w" promela-mode-syntax-table)
(modify-syntax-entry ?\' "\"" promela-mode-syntax-table)
)
(defvar promela-mode-abbrev-table nil
"*Abbrev table in use in promela-mode buffers.")
(if promela-mode-abbrev-table
nil
(define-abbrev-table 'promela-mode-abbrev-table
'(
;; Commented out for now - need to think about what abbrevs make sense
;; ("assert" "ASSERT" promela-check-expansion 0)
;; ("d_step" "D_STEP" promela-check-expansion 0)
;; ("break" "BREAK" promela-check-expansion 0)
;; ("do" "DO" promela-check-expansion 0)
;; ("proctype" "PROCTYPE" promela-check-expansion 0)
)))
(defvar promela-mode-map nil
"Keymap for promela-mode.")
(if promela-mode-map
nil
(setq promela-mode-map (make-sparse-keymap))
(define-key promela-mode-map "\t" 'promela-indent-command)
(define-key promela-mode-map "\C-m" 'promela-newline-and-indent)
;(define-key promela-mode-map 'backspace 'backward-delete-char-untabify)
(define-key promela-mode-map "\C-c\C-p" 'promela-beginning-of-block)
;(define-key promela-mode-map "\C-c\C-n" 'promela-end-of-block)
(define-key promela-mode-map "\M-\C-a" 'promela-beginning-of-defun)
;(define-key promela-mode-map "\M-\C-e" 'promela-end-of-defun)
(define-key promela-mode-map "\C-c(" 'promela-toggle-auto-match-delimiter)
(define-key promela-mode-map "{" 'promela-open-delimiter)
(define-key promela-mode-map "}" 'promela-close-delimiter)
(define-key promela-mode-map "(" 'promela-open-delimiter)
(define-key promela-mode-map ")" 'promela-close-delimiter)
(define-key promela-mode-map "[" 'promela-open-delimiter)
(define-key promela-mode-map "]" 'promela-close-delimiter)
(define-key promela-mode-map ";" 'promela-insert-and-indent)
(define-key promela-mode-map ":" 'promela-insert-and-indent)
;;
;; this is preliminary at best - use at your own risk:
(define-key promela-mode-map "\C-c\C-s" 'promela-syntax-check)
;;
;;(define-key promela-mode-map "\C-c\C-d" 'promela-mode-toggle-debug)
;;(define-key promela-mode-map "\C-c\C-r" 'promela-mode-revert-buffer)
)
(defvar promela-matching-delimiter-alist
'( (?( . ?))
(?[ . ?])
(?{ . "\n}")
;(?< . ?>)
(?\' . ?\')
(?\` . ?\`)
(?\" . ?\") )
"List of pairs of matching open/close delimiters - for auto-insert")
;; -------------------------------------------------------------------------
;; Promela-mode itself
(defun promela-mode ()
"Major mode for editing PROMELA code.
\\{promela-mode-map}
Variables controlling indentation style:
promela-block-indent
Relative offset of lines within a block (`{') construct.
promela-selection-indent
Relative offset of option lines within a selection (`if')
or iteration (`do') construct.
promela-selection-option-indent
Relative offset of lines after/within options (`::') within
selection or iteration constructs.
promela-comment-col
Defines the desired comment column for comments to the right of text.
promela-tab-always-indent
Non-nil means TAB in PROMELA mode should always reindent the current
line, regardless of where in the line the point is when the TAB
command is used.
promela-auto-match-delimiter
Non-nil means typing an open-delimiter (i.e. parentheses, brace,
quote, etc) should also insert the matching closing delmiter
character.
Turning on PROMELA mode calls the value of the variable promela-mode-hook with
no args, if that value is non-nil.
For example: '
(setq promela-mode-hook '(lambda ()
(setq promela-block-indent 2)
(setq promela-selection-indent 0)
(setq promela-selection-option-indent 2)
(local-set-key \"\\C-m\" 'promela-indent-newline-indent)
))'
will indent block two steps, will make selection options aligned with DO/IF
and sub-option lines indent to a column after the `::'. Also, lines will
be reindented when you hit RETURN.
Note that promela-mode adhears to the font-lock \"standards\" and
defines several \"levels\" of fontification or colorization. The
default is fairly gaudy, so if you would prefer a bit less, please see
the documentation for the variable: `font-lock-maximum-decoration'.
"
(interactive)
(kill-all-local-variables)
(setq mode-name "Promela")
(setq major-mode 'promela-mode)
(use-local-map promela-mode-map)
(set-syntax-table promela-mode-syntax-table)
(setq local-abbrev-table promela-mode-abbrev-table)
;; Make local variables
(make-local-variable 'case-fold-search)
(make-local-variable 'paragraph-start)
(make-local-variable 'paragraph-separate)
(make-local-variable 'paragraph-ignore-fill-prefix)
(make-local-variable 'indent-line-function)
(make-local-variable 'indent-region-function)
(make-local-variable 'parse-sexp-ignore-comments)
(make-local-variable 'comment-start)
(make-local-variable 'comment-end)
(make-local-variable 'comment-column)
(make-local-variable 'comment-start-skip)
(make-local-variable 'comment-indent-hook)
(make-local-variable 'defun-prompt-regexp)
(make-local-variable 'compile-command)
;; Now set their values
(setq case-fold-search t
paragraph-start (concat "^$\\|" page-delimiter)
paragraph-separate paragraph-start
paragraph-ignore-fill-prefix t
indent-line-function 'promela-indent-command
;;indent-region-function 'promela-indent-region
parse-sexp-ignore-comments t
comment-start "/* "
comment-end " */"
comment-column 32
comment-start-skip "/\\*+ *"
;;comment-start-skip "/\\*+ *\\|// *"
;;comment-indent-hook 'promela-comment-indent
defun-prompt-regexp promela-defun-prompt-regexp
)
;; Turn on font-lock mode
;; (and promela-font-lock-mode (font-lock-mode))
(font-lock-mode)
;; Finally, run the hooks and be done.
(run-hooks 'promela-mode-hook))
;; -------------------------------------------------------------------------
;; Interactive functions
;;
(defun promela-mode-version ()
"Print the current version of promela-mode in the minibuffer"
(interactive)
(message (concat "Promela-Mode: " promela-mode-version)))
(defun promela-beginning-of-block ()
"Move backward to start of containing block.
Containing block may be `{', `do' or `if' construct, or comment."
(interactive)
(goto-char (promela-find-start-of-containing-block-or-comment)))
(defun promela-beginning-of-defun (&optional arg)
"Move backward to the beginning of a defun.
With argument, do it that many times.
Negative arg -N means move forward to Nth following beginning of defun.
Returns t unless search stops due to beginning or end of buffer.
See also 'beginning-of-defun.
This is a Promela-mode specific version since default (in xemacs 19.16 and
NT-Emacs 20) don't seem to skip comments - they will stop inside them.
Also, this makes sure that the beginning of the defun is actually the
line which starts the proctype/init/etc., not just the open-brace."
(interactive "p")
(beginning-of-defun arg)
(if (not (looking-at promela-defun-prompt-regexp))
(re-search-backward promela-defun-prompt-regexp nil t))
(if (promela-inside-comment-p)
(goto-char (promela-find-start-of-containing-comment))))
(defun promela-indent-command ()
"Indent the current line as PROMELA code."
(interactive)
(if (and (not promela-tab-always-indent)
(save-excursion
(skip-chars-backward " \t")
(not (bolp))))
(tab-to-tab-stop)
(promela-indent-line)))
(defun promela-newline-and-indent ()
"Promela-mode specific newline-and-indent which expands abbrevs before
running a regular newline-and-indent."
(interactive)
(if abbrev-mode
(expand-abbrev))
(newline-and-indent))
(defun promela-indent-newline-indent ()
"Promela-mode specific newline-and-indent which expands abbrevs and
indents the current line before running a regular newline-and-indent."
(interactive)
(save-excursion (promela-indent-command))
(if abbrev-mode
(expand-abbrev))
(newline-and-indent))
(defun promela-insert-and-indent ()
"Insert the last character typed and re-indent the current line"
(interactive)
(insert last-command-char)
(save-excursion (promela-indent-command)))
(defun promela-open-delimiter ()
"Inserts the open and matching close delimiters, indenting as appropriate."
(interactive)
(insert last-command-char)
(if (and promela-auto-match-delimiter (not (promela-inside-comment-p)))
(save-excursion
(insert (cdr (assq last-command-char promela-matching-delimiter-alist)))
(promela-indent-command))))
(defun promela-close-delimiter ()
"Inserts and indents a close delimiter."
(interactive)
(insert last-command-char)
(if (not (promela-inside-comment-p))
(save-excursion (promela-indent-command))))
(defun promela-toggle-auto-match-delimiter ()
"Toggle auto-insertion of parens and other delimiters.
See variable `promela-auto-insert-matching-delimiter'"
(interactive)
(setq promela-auto-match-delimiter
(not promela-auto-match-delimiter))
(message (concat "Promela auto-insert matching delimiters "
(if promela-auto-match-delimiter
"enabled" "disabled"))))
;; -------------------------------------------------------------------------
;; Compilation/Verification functions
;; all of this is in serious "beta" mode - don't trust it ;-)
(setq
promela-compile-command "spin "
promela-syntax-check-args "-a -v "
)
;;(setq compilation-error-regexp-alist
;; (append compilation-error-regexp-alist
;; '(("spin: +line +\\([0-9]+\\) +\"\\([^\"]+\\)\"" 2 1))))
(defun promela-syntax-check ()
(interactive)
(compile (concat promela-compile-command
promela-syntax-check-args
(buffer-name))))
;; -------------------------------------------------------------------------
;; Indentation support functions
(defun promela-indent-around-label ()
"Indent the current line as PROMELA code,
but make sure to consider the label at the beginning of the line."
(beginning-of-line)
(delete-horizontal-space) ; delete any leading whitespace
(if (not (looking-at "\\sw+:\\([ \t]*\\)"))
(error "promela-indent-around-label: no label on this line")
(goto-char (match-beginning 1))
(let* ((space (length (match-string 1)))
(indent (promela-calc-indent))
(wanted (max 0 (- indent (current-column)))))
(if (>= space wanted)
(delete-region (point) (+ (point) (- space wanted)))
(goto-char (+ (point) space))
(indent-to-column indent)))))
;; Note that indentation is based ENTIRELY upon the indentation of the
;; previous line(s), esp. the previous non-blank line and the line
;; starting the current containgng block...
(defun promela-indent-line ()
"Indent the current line as PROMELA code.
Return the amount the by which the indentation changed."
(beginning-of-line)
(if (looking-at "[ \t]*\\sw+:")
(promela-indent-around-label)
(let ((indent (promela-calc-indent))
beg
shift-amt
(pos (- (point-max) (point))))
(setq beg (point))
(skip-chars-forward " \t")
(setq shift-amt (- indent (current-column)))
(if (zerop shift-amt)
(if (> (- (point-max) pos) (point))
(goto-char (- (point-max) pos)))
(delete-region beg (point))
(indent-to indent)
(if (> (- (point-max) pos) (point))
(goto-char (- (point-max) pos))))
shift-amt)))
(defun promela-calc-indent ()
"Return the appropriate indentation for this line as an int."
(save-excursion
(beginning-of-line)
(let* ((orig-point (point))
(state (promela-parse-partial-sexp))
(paren-depth (nth 0 state))
(paren-point (or (nth 1 state) 1))
(paren-char (char-after paren-point)))
;;(what-cursor-position)
(cond
;; Indent not-at-all - inside a string
((nth 3 state)
(current-indentation))
;; Indent inside a comment
((nth 4 state)
(promela-calc-indent-within-comment))
;; looking at a pre-processor directive - indent=0
((looking-at "[ \t]*#\\(define\\|if\\(n?def\\)?\\|else\\|endif\\)")
0)
;; If we're not inside a "true" block (i.e. "{}"), then indent=0
;; I think this is fair, since no (indentable) code in promela
;; exists outside of a proctype or similar "{ .. }" structure.
((zerop paren-depth)
0)
;; Indent relative to non curly-brace "paren"
;; [ NOTE: I'm saving this, but don't use it any more.
;; Now, we let parens be indented like curly braces
;;((and (>= paren-depth 1) (not (char-equal ?\{ paren-char)))
;; (goto-char paren-point)
;; (1+ (current-column)))
;;
;; Last option: indent relative to contaning block(s)
(t
(goto-char orig-point)
(promela-calc-indent-within-block paren-point))))))
(defun promela-calc-indent-within-block (&optional limit)
"Return the appropriate indentation for this line, assume within block.
with optional arg, limit search back to `limit'"
(save-excursion
(let* ((stop (or limit 1))
(block-point (promela-find-start-of-containing-block stop))
(block-type (promela-block-type-after block-point))
(indent-point (point))
(indent-type (promela-block-type-after indent-point)))
(if (not block-type) 0
;;(message "paren: %d (%d); block: %s (%d); indent: %s (%d); stop: %d"
;; paren-depth paren-point block-type block-point
;; indent-type indent-point stop)
(goto-char block-point)
(cond
;; Indent (options) inside "if" or "do"
((memq block-type '(selection iteration))
(if (re-search-forward "\\(do\\|if\\)[ \t]*::" indent-point t)
(- (current-column) 2)
(+ (current-column) promela-selection-indent)))
;; indent (generic code) inside "::" option
((eq 'option block-type)
(if (and (not indent-type)
(re-search-forward "::.*->[ \t]*\\sw"
(save-excursion (end-of-line) (point))
t))
(1- (current-column))
(+ (current-column) promela-selection-option-indent))
)
;; indent code inside "{"
((eq 'block block-type)
(cond
;; if we are indenting the end of a block,
;; use indentation of start-of-block
((equal 'block-end indent-type)
(current-indentation))
;; if the start of the code inside the block is not at eol
;; then indent to the same column as the block start +some
;; [ but ignore comments after "{" ]
((and (not (promela-effective-eolp (1+ (point))))
(not (looking-at "{[ \t]*/\\*")))
(forward-char) ; skip block-start
(skip-chars-forward "{ \t") ; skip whitespace, if any
(current-column))
;; anything else we indent +promela-block-indent from
;; the indentation of the start of block (where we are now)
(t
(+ (current-indentation)
promela-block-indent))))
;; dunno what kind of block this is - sound an error
(t
(error "promela-calc-indent-within-block: unknown block type: %s" block-type)
(current-indentation)))))))
(defun promela-calc-indent-within-comment ()
"Return the indentation amount for line, assuming that the
current line is to be regarded as part of a block comment."
(save-excursion
(beginning-of-line)
(skip-chars-forward " \t")
(let ((indenting-end-of-comment (looking-at "\\*/"))
(indenting-blank-line (eolp)))
;; if line is NOT blank and next char is NOT a "*'
(if (not (or indenting-blank-line (= (following-char) ?\*)))
;; leave indent alone
(current-column)
;; otherwise look back for _PREVIOUS_ possible nested comment start
(let ((comment-start (save-excursion
(re-search-backward comment-start-skip))))
;; and see if there is an appropriate middle-comment "*"
(if (re-search-backward "^[ \t]+\\*" comment-start t)
(current-indentation)
;; guess not, so indent relative to comment start
(goto-char comment-start)
(if indenting-end-of-comment
(current-column)
(1+ (current-column)))))))))
;; -------------------------------------------------------------------------
;; Misc other support functions
(defun promela-parse-partial-sexp (&optional start limit)
"Return the partial parse state of current defun or from optional start
to end limit"
(save-excursion
(let ((end (or limit (point))))
(if start
(goto-char start)
(promela-beginning-of-defun))
(parse-partial-sexp (point) end))))
;;(defun promela-at-end-of-block-p ()
;; "Return t if cursor is at the end of a promela block"
;; (save-excursion
;; (let ((eol (progn (end-of-line) (point))))
;; (beginning-of-line)
;; (skip-chars-forward " \t")
;; ;;(re-search-forward "\\(}\\|\\b\\(od\\|fi\\)\\b\\)" eol t))))
;; (looking-at "[ \t]*\\(od\\|fi\\)\\b"))))
(defun promela-inside-comment-p ()
"Check if the point is inside a comment block."
(save-excursion
(let ((origpoint (point))
state)
(goto-char 1)
(while (> origpoint (point))
(setq state (parse-partial-sexp (point) origpoint 0)))
(nth 4 state))))
(defun promela-inside-comment-or-string-p ()
"Check if the point is inside a comment or a string."
(save-excursion
(let ((origpoint (point))
state)
(goto-char 1)
(while (> origpoint (point))
(setq state (parse-partial-sexp (point) origpoint 0)))
(or (nth 3 state) (nth 4 state)))))
(defun promela-effective-eolp (&optional point)
"Check if we are at the effective end-of-line, ignoring whitespace"
(save-excursion
(if point (goto-char point))
(skip-chars-forward " \t")
(eolp)))
(defun promela-check-expansion ()
"If abbrev was made within a comment or a string, de-abbrev!"
(if promela-inside-comment-or-string-p
(unexpand-abbrev)))
(defun promela-block-type-after (&optional point)
"Return the type of block after current point or parameter as a symbol.
Return one of 'iteration `do', 'selection `if', 'option `::',
'block `{' or `}' or nil if none of the above match."
(save-excursion
(goto-char (or point (point)))
(skip-chars-forward " \t")
(cond
((looking-at "do\\b") 'iteration)
;;((looking-at "od\\b") 'iteration-end)
((looking-at "if\\b") 'selection)
;;((looking-at "fi\\b") 'selection-end)
((looking-at "::") 'option)
((looking-at "[{(]") 'block)
((looking-at "[})]") 'block-end)
(t nil))))
(defun promela-find-start-of-containing-comment (&optional limit)
"Return the start point of the containing comment block.
Stop at `limit' or beginning of buffer."
(let ((stop (or limit 1)))
(save-excursion
(while (and (>= (point) stop)
(nth 4 (promela-parse-partial-sexp)))
(re-search-backward comment-start-skip stop t))
(point))))
(defun promela-find-start-of-containing-block (&optional limit)
"Return the start point of the containing `do', `if', `::' or
`{' block or containing comment.
Stop at `limit' or beginning of buffer."
(save-excursion
(skip-chars-forward " \t")
(let* ((type (promela-block-type-after))
(stop (or limit
(save-excursion (promela-beginning-of-defun) (point))))
(state (promela-parse-partial-sexp stop))
(level (if (looking-at "\\(od\\|fi\\)\\b")
2
(if (zerop (nth 0 state)) 0 1))))
;;(message "find-start-of-containing-block: type: %s; level %d; stop %d"
;; type level stop)
(while (and (> (point) stop) (not (zerop level)))
(re-search-backward
"\\({\\|}\\|::\\|\\b\\(do\\|od\\|if\\|fi\\)\\b\\)"
stop 'move)
;;(message "looking from %d back-to %d" (point) stop)
(setq state (promela-parse-partial-sexp stop))
(setq level (+ level
(cond ((or (nth 3 state) (nth 4 state)) 0)
((and (= 1 level) (looking-at "::")
(not (equal type 'option))) -1)
((looking-at "\\({\\|\\(do\\|if\\)\\b\\)") -1)
((looking-at "\\(}\\|\\(od\\|fi\\)\\b\\)") +1)
(t 0)))))
(point))))
(defun promela-find-start-of-containing-block-or-comment (&optional limit)
"Return the start point of the containing comment or
the start of the containing `do', `if', `::' or `{' block.
Stop at limit or beginning of buffer."
(if (promela-inside-comment-p)
(promela-find-start-of-containing-comment limit)
(promela-find-start-of-containing-block limit)))
;; -------------------------------------------------------------------------
;; Debugging/testing
;; (defun promela-mode-toggle-debug ()
;; (interactive)
;; (make-local-variable 'debug-on-error)
;; (setq debug-on-error (not debug-on-error)))
;;(defun promela-mode-revert-buffer ()
;; (interactive)
;; (revert-buffer t t))
;; -------------------------------------------------------------------------
;;###autoload
(provide 'promela-mode)
;;----------------------------------------------------------------------
;; Change History:
;;
;; $Log: promela-mode.el,v $
;; Revision 1.11 2001/07/09 18:36:45 engstrom
;; - added comments on use of font-lock-maximum-decoration
;; - moved basic preprocess directive fontification to "level 2"
;;
;; Revision 1.10 2001/05/22 16:29:59 engstrom
;; - fixed error introduced in fontification levels stuff (xemacs only)
;;
;; Revision 1.9 2001/05/22 16:21:29 engstrom
;; - commented out the compilation / syntax check stuff for now
;;
;; Revision 1.8 2001/05/22 16:18:49 engstrom
;; - Munched history in preparation for first non-Honeywell release
;; - Added "levels" of fontification to be controlled by the std. variable:
;; 'font-lock-maximum-decoration'
;;
;; Revision 1.7 2001/04/20 01:41:46 engstrom
;; Revision 1.6 2001/04/06 23:57:18 engstrom
;; Revision 1.5 2001/04/04 20:04:15 engstrom
;; Revision 1.4 2001/03/15 02:22:18 engstrom
;; Revision 1.3 2001/03/09 19:39:51 engstrom
;; Revision 1.2 2001/03/01 18:07:47 engstrom
;; Revision 1.1 2001/02/01 xx:xx:xx engstrom
;; migrated to CVS versioning...
;; Pre-CVS-History:
;; 99-10-04 V0.4 EDE Fixed bug in end-of-block indentation
;; Simplified indentation code significantly
;; 99-09-2x V0.3 EDE Hacked on indentation more while at FM'99
;; 99-09-16 V0.2 EDE Hacked, hacked, hacked on indentation
;; 99-04-01 V0.1 EDE Introduced (less-than) half-baked indentation
;; 98-11-05 V0.0 EDE Created - much code stolen from rexx-mode.el
;; Mostly just a fontification mode -
;; (indentation is HARD ;-)
;;
;; EOF promela-mode.el
