casl-mode.el revision 79a7f2de0a7e933d26b64d35b2801618ff015954
;;;###autoload
;;;;;;;;;;;;;;;;;;;;;;;;;;
;; $Haeder$
;; Copyright: (c) Heng Jiang, Klaus L�ttich, Uni Bremen 2007
;; License: LGPL, see LICENSE.txt or LIZENZ.txt
;; Contact: hets-users@informatik.uni-bremen.de
;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Version number
"Version of CASL-Mode")
"Major mode for editing (heterogeneous) CASL specifications."
:prefix "casl-")
(defvar casl-mode-hook nil)
"Keymap for CASL major mode")
;; Are we running FSF Emacs or XEmacs?
(defvar casl-running-xemacs
"non-nil if we are running XEmacs, nil otherwise.")
;; ====================== S Y N T A X T A B L E ==================
;; Syntax table for CASL major mode
(defvar casl-mode-syntax-table nil
"Syntax table for CASL mode.")
()
(let ((table (make-syntax-table)))
;; Indicate that underscore may be part of a word
;; Comments
;; commenting-out plus including other kinds of comment
;; Some of these are actually OK by default.
"!#$&*+.,/\\\\:<=>?@^|~")
)
;; Various mode variables.
(defun casl-vars ()
)
;; Find the indentation level for a comment.
(defun casl-comment-indent ()
(skip-chars-backward " \t")
;; if the line is blank, put the comment at the beginning,
;; else at comment-column
;; ============= K E Y W O R D H I G H L I G H T I N G ============
`((t (:foreground "black")))
""
"Face name to use for black komma.")
(defvar casl-annotation-face 'casl-annotation-face
"CASL mode face for Annotations")
(defvar casl-name-face 'casl-name-face)
(defvar casl-keyword-face 'casl-keyword-face)
(defvar casl-library-name-face 'casl-library-name-face)
(defvar casl-builtin-face 'casl-builtin-face)
(defvar casl-comment-face 'casl-comment-face)
(defvar casl-other-name-face 'casl-other-name-face)
(defvar casl-string-char-face 'casl-string-char-face)
;; Syntax highlighting of CASL
;; "Warning: Do not design an element of font-lock-keywords to match
;; text which spans lines; this does not work reliably. While
;; font-lock-fontify-buffer handles multi-line patterns correctly,
;; updating when you edit the buffer does not, since it considers
;; text one line at a time." (from the GNU Emacs Lisp Reference Manual)
;; order of all the following highlighting rules is significant,
;; ony change if really needed
;; Comment
(list
"Special Comment")
;; Alternativ for Annotation
(list
;; always highlight closing )%
;; %words \n
;; %(.....)%
;; %word( ... )%
))
"Annotation")
(list
;; reserved keyword
'("\\(\\<\\|\\s-+\\)\\(/\\\\\\|\\\\/\\|=>\\|<=>\\|and\\|axioms?\\|arch\\|assoc\\|behaviourally\\|closed\\|comm\\|else\\|end\\|exists!?\\|fit\\|forall\\|free\\|generated\\|given\\|hide\\|idem\\|if\\|local\\|not\\|refined\\|refinement\\|reveal\\|spec\\|then\\|to\\|unit\\|via\\|view\\|when\\|within\\|with\\|\\(\\(op\\|pred\\|var\\|type\\|sort\\)s?\\)\\)\\(\\b\\|[ \t\n]\\)"
;; delimiters always in black after this
'("\\([,;.()]\\|::?=\\)\\|[^:]\\(:\\)[^:]"
;; after forall don't highlight
'("\\<\\(forall\\|exists\\)\\>\\(.+\\)"
;; between a descrete : and a descrete ; always in Black
'("[^:]:\\([^:][^;]+?\\);[^;]"
;; Keywords of loading Library
'("\\b\\(logic\\|from\\|get\\|library\\|version\\)\\b"
;; library versions
'("\\b\\(version\\)\\b[ \t]+\\([0-9.]+\\)"
;; = { <up to> : <sort> . always black
;; (var:<sort>) always black
;; Library and Logic name
'("\\b\\(library\\|logic\\)\\s-+\\(\\(\\w\\|/\\)+\\)\\b"
;; name of get
'("\\b\\(get\\)[ \t\n]\\([_A-Za-z�������,\t\n ]+\\)\\(from\\|spec\\|unit\\|arch\\|view\\|logic\\|%[\\[{(\\w]\\|$\\)"
;; library name in from
'("\\bfrom[ \t]+\\(.+?\\)\\(get\\|$\\)"
;; then, and + name
'("\\(\\<\\|\\s-+\\)\\(and\\|then\\)[ \t\n]*\\([A-Z]\\w*\\)\\s-*\\(\\[\\([A-Z]\\sw*\\).*\\]\\)?"
;; names before and after to
'("[ \t\n]*\\(\\sw+\\)[ \t\n]+to[ \t\n]+\\(\\(\\sw+\\)\\s-*\\(\\[\\([A-Z]\\sw*\\).*\\]\\)?[, \t]*\\)?"
;; instance name of specification
'("\\<spec.+=\\s-*\\(%\\sw+\\s-*\\)?[ \t\n]*\\([A-Z]\\w*\\)\\s-*\\(\\[\\s-*\\([A-Z]\\w*\\).*\\s-*\\]\\)?"
;; the name of a specification
'("\\b\\(spec\\)\\([^=\n]+?\\)\\(\\[\\|=\\|$\\)"
;; the name of a view
'("\\b\\(view\\)\\([^:\n]+?\\)\\(\\]\\|\\[\\|:\\|$\\)"
;; Basic signature: sort X, Y, Z
'("\\bsorts?[ \t]+\\(\\(<?[^<]*?\\|\\[[^\\]]+?\\]\\)+\\)\\($\\|=\\|\\]\\||->\\)"
;; Basic signature: op ,pred and var name
'("\\(\\<[0-9]\\|\\w[^()\n]*?[^:]\\|\\w\\):\\??[ \nA-Za-z�������{}]"
'("\\(\\<\\w[^()\n]*?[^(]\\|\\w\\)\([^):]+?:"
;; highlight a line with , at end
'("^\\(\\(\\(__\\s-*[^_\n]+\\s-*__\\|[^.,:>\n]+\\)\\s-*,\\s-*\\)+\\)$"
;; names before and after '|->'
'("[ \t\n]*\\(__[^|_]+__\\|[^[ \t\n]+\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?[ \t\n]*|->[ \t\n]*\\(__[^|_]+__\\|[^[ \t\n]+\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?[, \t]*"
;; type name and first alternative
'("\\btype\\b\\([^:]+\\)::?=\\([^|(]+\\)\\(|\\|(\\|$\\)"
;; from here on everything in parens in black and =
;; name of given
'("\\b\\(given\\)[ \t\n]+\\(.*?\\)\\(=\\|:\\|$\\)"
;; constructor
'("\|\\s-+\\(\_\_[^|_]+\_\_\\|[^|][^(|]+\\)\\s-*\\(\([^|]+\)\\)?[ \t\n]*"
;; in ()1
'("\(\\(\\(\\sw\\|,\\)*\\)\\s-*:\\??[^):]*\)"
;; in ()2+
'("\([^;]*\\(;\\s-*\\(\\sw+\\)\\s-*:\\??.*?\\)+\)"
))
"Reserved keywords highlighting")
;; String and Char
(list '("\\(\\(\"\\|^>[ \t]*\\\\\\)\\([^\"\\\\\n]\\|\\\\.\\)*\\(\"\\|\\\\[ \t]*$\\)\\|'\\([^'\\\\\n]\\|\\\\.[^'\n]*\\)'\\)" (0 casl-string-char-face keep t))
))
"Syntax highlighting of String and Char")
;; Define default highlighting level
;; (defvar casl-font-lock-syntax-highligthing casl-font-lock-keywords
"Default syntax highlighting level in CASL mode")
;; ======================= R U N H E T S =======================
(setq casl-error-list nil)
(defvar hets-program nil)
(defvar old-buffer nil)
(defvar casl-hets-options nil
"*the additional options for running hets.")
"Run hets process to compile the current CASL file."
(save-buffer nil)
(let* ((option " ")
(if hets-program
(if opt
;; Pop up the compilation buffer.
(setq buffer-read-only nil)
(set-buffer-modified-p nil)
;; (display-buffer outbuf nil t)
;; (set-buffer outbuf)
(compilation-mode "hets-compile")
;; Start the compilation.
(if (fboundp 'start-process)
(let* ((process-environment
(if (and (boundp 'system-uses-terminfo)
(list "TERM=dumb" "TERMCAP="
(list "TERM=emacs"
(format "TERMCAP=emacs:co#%d:tc=unknown:"
(window-width))))
;; Set the EMACS variable, but
;; don't override users' setting of $EMACS.
(if (getenv "EMACS")
hets-command)))
(setq buffer-read-only nil)
))
"Run hets process with options (from casl-hets-options) to compile the
current CASL file."
(if opt
)
)
(defun casl-run-hets-g ()
"Run hets process with -g and other options (from variable casl-hets-options)
to compile the current CASL file."
(casl-run-hets-r "-g")
)
;; sentinel and filter of asynchronous process of hets
;; Called when compilation process changes state.
"Sentinel for compilation buffers."
;; buffer killed
(set-process-buffer proc nil)
(let ((obuf (current-buffer)))
;; save-excursion isn't the right thing if
;; process-buffer is current-buffer
;; Write something in the compilation buffer
;; and hack its mode line.
msg)
;; Since the buffer and mode line will show that the
;; process is dead, we can delete it now. Otherwise it
;; will stay around until M-x list-processes.
(set-buffer obuf))))
;; (setq compilation-in-progress (delq proc compilation-in-progress))
))))
;; show the message from hets compile direct on *hets-run* buffer
(pop-to-buffer "*hets-run*")
))
;; Insert the text, advancing the process marker.
"Write msg in the current buffer and hack its mode-line-process."
(let ((buffer-read-only nil)
;; Record where we put the message, so we can ignore it
;; later on.
;; (goto-char omax)
(if (bolp)
(forward-char -1))
;; Force mode line redisplay soon.
;; Automatically parse (and mouse-highlight) error messages:
(if (zerop exit-status)
(setq casl-error-list nil)
(setq casl-error-list nil)
))
;; also functions with old hets-program?
(defun casl-parse-error ()
"Error Parser"
(setq casl-error-list nil)
;;;(pop-to-buffer compiler-buffer)
(pop-to-buffer "*hets-run*")
(skip-chars-forward "a-zA-Z*,/._\\- ")
(re-search-forward ":\\([0-9]+\\)\\.\\([0-9]+\\)\\(-[0-9]+\\.[0-9]*\\)?[:,]" (save-excursion (end-of-line) (point)) t 1)
)
(forward-line 1)))))
(defun casl-compile-goto-next-error ()
"search the next error position from error-list, and move to it."
;; if error-list is empty ...
(if (null casl-error-list)
(if (null casl-error-list)
(message "no error.")
(message "this file have not yet been compiled."))
;; (message "DEBUG<Goto Error>: file: %s, line: %s, column: %s" error-file-name error-line error-column)
;; if the file already opened ...
;; switch to hets-run window to jump to next error message
(pop-to-buffer "*hets-run*")
;; return to current file
)))
;; ================= C A S L M A J O R M O D E ===============
;; casl major mode setup
;; Definition of CASL major mode
(defun casl-mode ()
"Major mode for editing CASL models"
;; Load keymap
;; Load syntax table
;; (casl-create-syntax-table)
;; Highlight CASL keywords
(setq font-lock-keywords-only nil)
;; Support for compile.el
;; We just substitute our own functions to go to the error.
(lambda()
;; FIXME: This has global impact! -stef
)
;; CASL-mode ends here