Some org-bable config

1 files changed, 985 insertions, 0 deletions

diff --git a/lisp/promela-mode.el b/lisp/promela-mode.el
new file mode 100644
index 0000000..3ab4da7
--- /dev/null
+++ b/lisp/promela-mode.el
@@ -0,0 +1,985 @@
+;; 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