casl-mode.el revision 3e4305eb6432c65bb0dfe8d9af9707dfc92383ea
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce;;;###autoload
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce(autoload 'turn-on-casl-indent "casl-indent" "Turn on CASL indentation." t)
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce;; Version number
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce "Version of CASL-Mode")
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce "Major mode for editing (heterogeneous) CASL programs."
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce;; casl major mode setup
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce(defvar casl-mode-map (let ((keymap (make-keymap)))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (define-key keymap "\C-c\C-n" 'casl-compile-goto-next-error)
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce "Keymap for CASL major mode")
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce;; Are we running FSF Emacs or XEmacs?
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce "non-nil if we are running XEmacs, nil otherwise.")
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce;; ============= K E Y W O R D H I G H L I G H T I N G ============
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce(defvar casl-black-komma-face 'casl-black-komma-face
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce "Face name to use for black komma.")
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce(defvar casl-annotation-face 'casl-annotation-face
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce "CASL mode face for Annotations")
75e66c388862a4ba05afe0791c5503226395bad0Simo Sorce(setq casl-annotation-face 'font-lock-constant-face)
75e66c388862a4ba05afe0791c5503226395bad0Simo Sorce(defvar casl-library-name-face 'casl-library-name-face)
75e66c388862a4ba05afe0791c5503226395bad0Simo Sorce(setq casl-library-name-face 'font-lock-type-face)
75e66c388862a4ba05afe0791c5503226395bad0Simo Sorce(setq casl-name-face 'font-lock-variable-name-face)
75e66c388862a4ba05afe0791c5503226395bad0Simo Sorce(defvar casl-other-name-face 'casl-other-name-face)
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce(setq casl-other-name-face 'font-lock-function-name-face)
75e66c388862a4ba05afe0791c5503226395bad0Simo Sorce(defvar casl-string-char-face 'casl-string-char-face)
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce(setq casl-string-char-face 'font-lock-string-face)
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce;; Syntax highlighting of CASL
75e66c388862a4ba05afe0791c5503226395bad0Simo Sorce ;; Keywords of loading Library
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce '("\\(\\<\\|\\s-+\\)\\(logic\\|from\\|get\\|library\\|version\\)[ :\t\n]+"
75e66c388862a4ba05afe0791c5503226395bad0Simo Sorce;; '("\\(\\<\\|\\s-+\\)\\(%authors\\|%date\\|%display\\|%prec\\|%left_assoc\\|%number\\|%floating\\|%LATEX\\|%implies\\)[ :\t\n]+"
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce;; (2 casl-annotation-face keep t))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; Library and Logic name
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce '("\\(\\<\\|\\s-+\\)\\(library\\|logic\\)\\s-+\\(\\(\\w\\|/\\)+\\)[ \t\n]*"
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; name of from get and given
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce '("\\(\\<\\|[ \t]+\\)\\(get\\|given\\)[ \t\n]+\\(\\(\\sw+\\s-*\\(,\\|$\\)[ \t\n]*\\)+\\)"
75e66c388862a4ba05afe0791c5503226395bad0Simo Sorce '("\\(\\<\\|\\s-+\\)from\\([ \t]+\\)\\(.+\\)\\(get\\|\\s-*\\)"
75e66c388862a4ba05afe0791c5503226395bad0Simo Sorce ;; the name of specification and view
75e66c388862a4ba05afe0791c5503226395bad0Simo Sorce '("\\(\\<\\|\\[\\)\\(spec\\|view\\)\\s-+\\(\\w+\\)[ \t]*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?\\s-*.*\\([]=:]\\|::=\\)"
75e66c388862a4ba05afe0791c5503226395bad0Simo Sorce (3 casl-name-face keep t) (5 casl-name-face keep t))
75e66c388862a4ba05afe0791c5503226395bad0Simo Sorce ;; then, and + name
75e66c388862a4ba05afe0791c5503226395bad0Simo Sorce '("\\(\\<\\|\\s-+\\)\\(and\\|then\\)[ \t\n]*\\([A-Z]\\w*\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?"
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (3 casl-name-face keep t) (5 casl-name-face keep t))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; names before and after to
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce '("[ \t\n]*\\(\\w+\\)[ \t\n]+to[ \t\n]+\\(\\(\\w+\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?[, \t]*\\)?"
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (1 casl-name-face keep t) (3 casl-name-face keep t) (5 casl-name-face keep t))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; instance name of specification
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce '("\\<spec.+=\\s-*\\(%\\sw+\\s-*\\)?[ \t\n]*\\([A-Z]\\sw*\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?"
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (2 casl-name-face keep t) (4 casl-name-face keep t))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; Basic signature: sort X, Y, Z
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce '("\\(\\<\\|\\s-+\\)sorts?[ \t]+\\(\\(\\sw+\\s-*\\(\\[\\(\\sw\\|,\\)+\\]\\s-*\\)?\\(,\\|$\\|<\\|;\\|=\\)\\(\\sw\\|=\\|<\\|;\\|,\\)*[ \t\n]*\\)+\\)"
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; Basic signature: op ,pred and var name
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce '("\\(^\\|\\bops?\\|\\bpreds?\\|\\bvars?\\)\\s-+\\([^.]\\(\\sw\\|\\s_\\|\\s(\\|\\s)\\)*\\)\\s-*\\(\(.*\)\\)?\\s-*\\(:\\??\\|<=>\\)[^:\n]*;?[ \t]*$"
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; type name
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce '("\\s-+\\(\\sw+\\)[ \t\n]*::?=\\s-*\\(\\sw*\\).*"
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (1 casl-other-name-face keep t) (2 casl-other-name-face keep t) )
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; constructor
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce '("\\(\\sw+\\)?\\s-*|\\s-*\\(\\sw+\\)\\s-*[|(]?\\([ \t]*\\|$\\)"
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (1 casl-other-name-face keep t) (2 casl-other-name-face keep t))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce '("\(\\(\\(\\sw\\|,\\)*\\)\\s-*:\\??[^)]*\)"
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce '("\([^;]*;\\s-*\\(\\sw+\\)\\s-*:\\??.*\)"
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; names before and after '|->'
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce '("[ \t\n]*\\([^[ \t\n]+\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?[ \t\n]+|->[ \t\n]+\\([^[ \t\n]+\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?[, \t]*"
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (1 casl-other-name-face keep t) (3 casl-other-name-face keep t)
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (4 casl-other-name-face keep t) (6 casl-other-name-face keep t))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; reserved keyword
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce '("\\(\\<\\|\\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]"
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce "Reserved keywords highlighting")
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce;; String and Char
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (list '("\\(\\(\"\\|^>[ \t]*\\\\\\)\\([^\"\\\\\n]\\|\\\\.\\)*\\(\"\\|\\\\[ \t]*$\\)\\|'\\([^'\\\\\n]\\|\\\\.[^'\n]*\\)'\\)" (0 casl-string-char-face t t))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce "Syntax highlighting of String and Char")
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce;; Alternativ for Annotation
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; %word(...)\n
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce '("%\\sw+\([^%\n]+\)$" (0 casl-annotation-face t t))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; %words \n
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; %( ... )%
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce '("%\([^)%]*\)%[ \t\n]*" (0 casl-annotation-face t t))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; %word( ... )%
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce '("%\\sw+\([^)%]*\)%[ \t\n]*" (0 casl-annotation-face t t))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce "Annotation")
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce '("\\(%{[^}%]*}%\\)[ \t\n]*" (1 casl-comment-face t t))
bdadcaf271818e88e56e86c2bd90663a08fd9721Lukas Slebodnik "Special Comment")
bdadcaf271818e88e56e86c2bd90663a08fd9721Lukas Slebodnik;; Define default highlighting level
bdadcaf271818e88e56e86c2bd90663a08fd9721Lukas Slebodnik;; (defvar casl-font-lock-syntax-highligthing casl-font-lock-keywords
bdadcaf271818e88e56e86c2bd90663a08fd9721Lukas Slebodnik(defvar casl-font-lock-syntax-highligthing casl-font-lock-specialcomment
bdadcaf271818e88e56e86c2bd90663a08fd9721Lukas Slebodnik "Default syntax highlighting level in CASL mode")
bdadcaf271818e88e56e86c2bd90663a08fd9721Lukas Slebodnik;; ====================== S Y N T A X T A B L E ==================
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce;; Syntax table for CASL major mode
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce "Syntax table for CASL mode.")
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; Indicate that underscore may be part of a word
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; commenting-out plus including other kinds of comment
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; Some of these are actually OK by default.
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce "!#$&*+.,/\\\\:<=>?@^|~")
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce;; Various mode variables.
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (setq comment-indent-function 'casl-comment-indent)
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce;; Find the indentation level for a comment.
e05d3f5872263aadfbc2f6a2a8c9735219922387Simo Sorce ;; if the line is blank, put the comment at the beginning,
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; else at comment-column
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (if (bolp) 0 (max (1+ (current-column)) comment-column)))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce;; ======================= R U N H E T S =======================
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce "Run hets process to compile the current CASL file."
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (insert casl-hets-program " " casl-hets-file-name "\n")
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (concat casl-hets-program " " casl-hets-file-name))))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce "finished\n"
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (format "exited abnormally with code %d\n" status))))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (compilation-handle-exit 'bizarre status status)))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (message "%s errors have been found." (length casl-error-list)))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce "Run hets -g process to compile the current CASL file."
75e66c388862a4ba05afe0791c5503226395bad0Simo Sorce (insert casl-hets-program " " casl-hets-file-name "\n")
75e66c388862a4ba05afe0791c5503226395bad0Simo Sorce (concat casl-hets-program " -g " casl-hets-file-name))))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce "finished\n"
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (format "exited abnormally with code %d\n" status))))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (compilation-handle-exit 'bizarre status status)))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (message "%s errors have been found." (length casl-error-list)))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce;; also functions with old hets-program?
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce "Error Parser"
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;;;(pop-to-buffer compiler-buffer)
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (if (not (or (looking-at "Fail") (looking-at "\\*\\*\\*")))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (if (not (search-forward ":" (save-excursion (end-of-line) (point)) t 1))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (re-search-backward "\\(\(\\|\\s-+\\)\\([^.]+\\.\\(casl\\|het\\)\\)" nil t 1)
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (re-search-forward ":\\([0-9]+\\)\\.\\([0-9]+\\)[:,]" (save-excursion (end-of-line) (point)) t 1)
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (when (not (string= (match-string-no-properties 0) ""))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (setq error-colnum (match-string-no-properties 2))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (nconc casl-error-list (list (list file-name error-line error-colnum))))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce "search the next error position from error-list, and move to it."
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; wenn error-list leer ist...
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (if (member (get-buffer "*hets-run*") (buffer-list))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (message "this file have not yet been compiled.")) ;; wie sagt auf englisch?
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; (message "DEBUG<Goto Error>: file: %s, line: %s, column: %s" error-file-name error-line error-column)
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; wenn die Datei, die fehlerbehaftet ist, schon geoeffnet...
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (pop-to-buffer (get-file-buffer error-file-name))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (move-to-column (- (string-to-number error-column) 1))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (message "goto next error... line: %s column: %s" error-line error-column)
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (setq casl-error-list (nconc casl-error-list (list this-error)))
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce;; ================= C A S L M A J O R M O D E ===============
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce;; Definition of CASL major mode
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce "Major mode for editing CASL models"
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; Load keymap
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; Load syntax table
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; (casl-create-syntax-table)
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; Highlight CASL keywords
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; Support for compile.el
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; We just substitute our own functions to go to the error.
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce (set (make-local-variable 'compile-auto-highlight) 40)
5dbf360f2d6b0281c32f1bba6ebf5cc834c1716eSimo Sorce ;; FIXME: This has global impact! -stef