+++ /dev/null
-;; 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 ]
-\f
-;;; -------------------------------------------------------------------------
-;;; 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
-
-\f
-;; -------------------------------------------------------------------------
-;; 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 "\\|")))
-
-\f
-;; -------------------------------------------------------------------------
-;; 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)))))
-
-\f
-;; -------------------------------------------------------------------------
-;; "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))))
-
-\f
-;; -------------------------------------------------------------------------
-;; other promela-mode specific definitions
-
-(defconst promela-defun-prompt-regexp
- "^[ \t]*\\(d?proctype\\|init\\|inline\\|never\\|trace\\|typedef\\|mtype\\s-+=\\)[^{]*"
- "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")
-
-\f
-;; -------------------------------------------------------------------------
-;; 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))
-
-\f
-;; -------------------------------------------------------------------------
-;; 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"))))
-
-\f
-;; -------------------------------------------------------------------------
-;; 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))))
-
-\f
-;; -------------------------------------------------------------------------
-;; 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)))))))))
-
-\f
-;; -------------------------------------------------------------------------
-;; 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)
-
-\f
-;;----------------------------------------------------------------------
-;; 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
projects / lttv.git / blobdiff