casl-mode.el revision b66e97d7d836d878bbaf31abc81c3b88bd3397f6
55cf6e01272ec475edea32aa9b7923de2d36cb42Christian Maeder;;;###autoload
ab419eb9bb19c32515fb35793f1192a86c74712eTill Mossakowski(autoload 'turn-on-casl-indent "casl-indent" "Turn on CASL indentation." t)
e071fb22ea9923a2a4ff41184d80ca46b55ee932Till Mossakowski;; Version number
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu "Version of CASL-Mode")
ab419eb9bb19c32515fb35793f1192a86c74712eTill Mossakowski "Major mode for editing (heterogeneous) CASL programs."
ab419eb9bb19c32515fb35793f1192a86c74712eTill Mossakowski(defvar casl-mode-map (let ((keymap (make-keymap)))
ab419eb9bb19c32515fb35793f1192a86c74712eTill Mossakowski (define-key keymap "\C-c\C-c" 'comment-region)
ab419eb9bb19c32515fb35793f1192a86c74712eTill Mossakowski (define-key keymap "\C-c\C-r" 'casl-run-hets-r)
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder (define-key keymap "\C-c\C-g" 'casl-run-hets-g)
ab419eb9bb19c32515fb35793f1192a86c74712eTill Mossakowski (define-key keymap "\C-c\C-n" 'casl-compile-goto-next-error)
ab419eb9bb19c32515fb35793f1192a86c74712eTill Mossakowski "Keymap for CASL major mode")
71bf376677866b4735ae3c13ee08a863d25c1188Christian Maeder;; Are we running FSF Emacs or XEmacs?
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder (string-match "Lucid\\|XEmacs" emacs-version)
ab419eb9bb19c32515fb35793f1192a86c74712eTill Mossakowski "non-nil if we are running XEmacs, nil otherwise.")
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder;; ====================== S Y N T A X T A B L E ==================
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder;; Syntax table for CASL major mode
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder "Syntax table for CASL mode.")
71bf376677866b4735ae3c13ee08a863d25c1188Christian Maeder ;; Indicate that underscore may be part of a word
86b1d0c80abdd4ca36491cf7025b718a5fea5080Christian Maeder ;; commenting-out plus including other kinds of comment
ab419eb9bb19c32515fb35793f1192a86c74712eTill Mossakowski ;; Some of these are actually OK by default.
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder "!#$&*+.,/\\\\:<=>?@^|~()[]{}")
179581802dda2f071129f542a2c10e28b35c45b9Christian Maeder;; Various mode variables.
ab419eb9bb19c32515fb35793f1192a86c74712eTill Mossakowski (make-local-variable 'comment-indent-function)
ab419eb9bb19c32515fb35793f1192a86c74712eTill Mossakowski (setq comment-indent-function 'casl-comment-indent)
179581802dda2f071129f542a2c10e28b35c45b9Christian Maeder;; Find the indentation level for a comment.
3d3889e0cefcdce9b3f43c53aaa201943ac2e895Jonathan von Schroeder ;; if the line is blank, put the comment at the beginning,
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder ;; else at comment-column
d6c6b2543c509ec7f6213e4cba675d96304a7fd6Christian Maeder (if (bolp) 0 (max (1+ (current-column)) comment-column)))
ab419eb9bb19c32515fb35793f1192a86c74712eTill Mossakowski;; ============= K E Y W O R D H I G H L I G H T I N G ============
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian Maeder(defvar casl-black-komma-face 'casl-black-komma-face
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian Maeder "Face name to use for black komma.")
0e2ae85e2453466d03c1fc5884a3d693235bb9d9Christian Maeder(defvar casl-annotation-face 'casl-annotation-face
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder "CASL mode face for Annotations")
a7be28e157e9ceeec73a8fd0e642c36ea29d4218Christian Maeder(setq casl-annotation-face 'font-lock-constant-face)
fbf1cdad9a9775bd7332e85f01b6a307d7dbb1cfChristian Maeder(setq casl-name-face 'font-lock-variable-name-face)
9eb39c7a0e7a1ddad1eec1d23c6d4e3a99c54023Christian Maeder(defvar casl-keyword-face 'casl-keyword-face)
ab419eb9bb19c32515fb35793f1192a86c74712eTill Mossakowski(setq casl-keyword-face 'font-lock-keyword-face)
b1f59a4ea7c96f4c03a4d7cfcb9c5e66871cfbbbChristian Maeder(defvar casl-library-name-face 'casl-library-name-face)
b565cd55a13dbccc4e66c344316da525c961e4caTill Mossakowski(setq casl-library-name-face 'font-lock-type-face)
179581802dda2f071129f542a2c10e28b35c45b9Christian Maeder(defvar casl-builtin-face 'casl-builtin-face)
179581802dda2f071129f542a2c10e28b35c45b9Christian Maeder(setq casl-builtin-face 'font-lock-builtin-face)
179581802dda2f071129f542a2c10e28b35c45b9Christian Maeder(defvar casl-comment-face 'casl-comment-face)
179581802dda2f071129f542a2c10e28b35c45b9Christian Maeder(setq casl-comment-face 'font-lock-comment-face)
179581802dda2f071129f542a2c10e28b35c45b9Christian Maeder(defvar casl-other-name-face 'casl-other-name-face)
179581802dda2f071129f542a2c10e28b35c45b9Christian Maeder(setq casl-other-name-face 'font-lock-function-name-face)
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder(defvar casl-string-char-face 'casl-string-char-face)
1dfd1687e9ee6a45e2cb5268a701ead79c1c1f79Christian Maeder(setq casl-string-char-face 'font-lock-string-face)
fbf1cdad9a9775bd7332e85f01b6a307d7dbb1cfChristian Maeder;; Syntax highlighting of CASL
549e39da3e3234118ed35cbe11de91ee3fc62934Christian Maeder ;; Keywords of loading Library
549e39da3e3234118ed35cbe11de91ee3fc62934Christian Maeder '("\\(\\<\\|\\s-+\\)\\(logic\\|from\\|get\\|library\\|version\\)[ :\t\n]+"
549e39da3e3234118ed35cbe11de91ee3fc62934Christian Maeder;; '("\\(\\<\\|\\s-+\\)\\(%authors\\|%date\\|%display\\|%prec\\|%left_assoc\\|%number\\|%floating\\|%LATEX\\|%implies\\)[ :\t\n]+"
b565cd55a13dbccc4e66c344316da525c961e4caTill Mossakowski;; (2 casl-annotation-face keep t))
b565cd55a13dbccc4e66c344316da525c961e4caTill Mossakowski ;; Library and Logic name
ab419eb9bb19c32515fb35793f1192a86c74712eTill Mossakowski '("\\(\\<\\|\\s-+\\)\\(library\\|logic\\)\\s-+\\(\\(\\w\\|/\\)+\\)[ \t\n]*"
ab419eb9bb19c32515fb35793f1192a86c74712eTill Mossakowski ;; name of from, get and given
ab419eb9bb19c32515fb35793f1192a86c74712eTill Mossakowski '("\\(\\<\\|[ \t]+\\)\\(get\\|given\\)[ \t\n]+\\(\\(\\sw+\\s-*\\(,[ \t\n]*\\|$\\)\\)+\\)\\(=\\|:\\|$\\)"
cdcf5d3f1e79d8798d77efa29e6193af94ea0604Till Mossakowski '("\\(\\<\\|\\s-+\\)from[ \t]+\\(.+\\)\\(get\\|$\\)"
71bf376677866b4735ae3c13ee08a863d25c1188Christian Maeder ;; after forall don't highlight
71bf376677866b4735ae3c13ee08a863d25c1188Christian Maeder '("\\bforall\\b\\(.*\\)"
4aa35aadcb28f8a962096efc70d3bdb58ab7d9faChristian Maeder ;; the name of specification and view
71bf376677866b4735ae3c13ee08a863d25c1188Christian Maeder '("\\(\\<\\|\\[\\)\\(spec\\|view\\)\\s-+\\(\\w+\\)[ \t]*\\(\\[\\s-*\\([A-Z]\\w*\\).*\\s-*\\]\\)?\\s-*.*\\([]=:]\\|::=\\)"
71bf376677866b4735ae3c13ee08a863d25c1188Christian Maeder (3 casl-name-face keep t) (5 casl-name-face keep t))
71bf376677866b4735ae3c13ee08a863d25c1188Christian Maeder ;; then, and + name
71bf376677866b4735ae3c13ee08a863d25c1188Christian Maeder '("\\(\\<\\|\\s-+\\)\\(and\\|then\\)[ \t\n]*\\([A-Z]\\w*\\)\\s-*\\(\\[\\([A-Z]\\sw*\\).*\\]\\)?"
71bf376677866b4735ae3c13ee08a863d25c1188Christian Maeder (3 casl-name-face keep t) (5 casl-name-face keep t))
'("[ \t\n]*\\(\\sw+\\)[ \t\n]+to[ \t\n]+\\(\\(\\sw+\\)\\s-*\\(\\[\\([A-Z]\\sw*\\).*\\]\\)?[, \t]*\\)?"
'("\\<spec.+=\\s-*\\(%\\sw+\\s-*\\)?[ \t\n]*\\([A-Z]\\w*\\)\\s-*\\(\\[\\s-*\\([A-Z]\\w*\\).*\\s-*\\]\\)?"
'("\\(\\<\\|\\s-+\\)sorts?[ \t\n]+\\(\\(\\sw+\\s-*\\(\\[\\s-*\\(\\sw\\|,\\)+\\s-*\\]\\s-*\\)?\\(,\\(\\s-\\)*\\|$\\|<\\|;\\|=\\)\\(=\\|<\\|;\\|,\\)*[ \t\n]*\\)+\\)"
'("\\(\\(^[^.{%]\\)\\s-*\\|\\bops?\\b\\|\\bpreds?\\b\\|\\bvars?\\b\\)\\([^:{()]*\\)\\(\(.*\)\\)?:\\??[^?.:=%].*;?[ \t]*$"
'("[ \t\n]*\\(__[^|_]+__\\|[^[ \t\n]+\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?[ \t\n]*|->[ \t\n]*\\(__[^|_]+__\\|[^[ \t\n]+\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?[, \t]*"
'("\\(\\btype\\|\\bfree type\\)?\\s-+\\(\\sw+\\)\\s-+\\(\\sw*\\|\\[\\(\\s-*\\sw+\\s-*\\)\\]\\)[ \t\n]*::?=[ \t\n]*\\(\\(\_\_[^_]+\_\_\\|[^|][^(|]+\\)\\s-*\\(\(.*\)\\)?\\)"
'("\\(\\<\\|\\s-+\\)\\(/\\\\\\|\\\\/\\|=>\\|<=>\\|and\\|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?\\)\\)[,;]?[ \t\n]"
(list '("\\(\\(\"\\|^>[ \t]*\\\\\\)\\([^\"\\\\\n]\\|\\\\.\\)*\\(\"\\|\\\\[ \t]*$\\)\\|'\\([^'\\\\\n]\\|\\\\.[^'\n]*\\)'\\)" (0 casl-string-char-face t t))
(list
(defvar hets-program nil)
(defvar old-buffer nil)
(defvar casl-hets-options '()
(save-buffer nil)
(if hets-program
(if opt
(set-buffer-modified-p nil)
(let* ((process-environment
(window-width))))
hets-command)))
(if opt
(defun casl-run-hets-g ()
msg)
(let ((buffer-read-only nil)
(if (bolp)
(defun casl-parse-error ()
(re-search-forward ":\\([0-9]+\\)\\.\\([0-9]+\\)\\(-[0-9]+\\.[0-9]*\\)?[:,]" (save-excursion (end-of-line) (point)) t 1)
(defun casl-compile-goto-next-error ()
;; (message "DEBUG<Goto Error>: file: %s, line: %s, column: %s" error-file-name error-line error-column)
(defun casl-mode ()
;; Support for compile.el
(lambda()