verif/md/promela-mode.el

   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