casl-mode.el revision 67d5e49547d78aa56a8f9ba5e64a950b730eba66
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik;;;###autoload
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik(autoload 'turn-on-casl-indent "casl-indent" "Turn on CASL indentation." t)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik;; Version number
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik "Version of CASL-Mode")
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik "Major mode for editing Haskell programs."
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik;; casl major mode setup
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik(defvar casl-mode-map (let ((keymap (make-keymap)))
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik (define-key keymap "\C-c\C-c" 'comment-region)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik (define-key keymap "\C-c\C-r" 'casl-run-hets)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik (define-key keymap "\C-c\C-g" 'casl-run-hetsg)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik (define-key keymap "\C-c\C-n" 'casl-compile-goto-next-error)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik "Keymap for CASL major mode")
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik;; Are we running FSF Emacs or XEmacs?
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik (string-match "Lucid\\|XEmacs" emacs-version)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik "non-nil if we are running XEmacs, nil otherwise.")
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik;; ============= K E Y W O R D H I G H L I G H T I N G ============
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik(defvar casl-black-komma-face 'casl-black-komma-face
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik "Face name to use for black komma.")
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik(defvar casl-annotation-face 'casl-annotation-face
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik "CASL mode face for Annotations")
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik(setq casl-annotation-face 'font-lock-constant-face)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik(defvar casl-keyword-face 'casl-keyword-face)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik(setq casl-keyword-face 'font-lock-keyword-face)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik(defvar casl-library-name-face 'casl-library-name-face)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik(setq casl-library-name-face 'font-lock-type-face)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik(setq casl-name-face 'font-lock-variable-name-face)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik(defvar casl-builtin-face 'casl-builtin-face)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik(setq casl-builtin-face 'font-lock-builtin-face)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik(defvar casl-comment-face 'casl-comment-face)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik(setq casl-comment-face 'font-lock-comment-face)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik(defvar casl-other-name-face 'casl-other-name-face)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik(setq casl-other-name-face 'font-lock-function-name-face)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik(defvar casl-string-char-face 'casl-string-char-face)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik(setq casl-string-char-face 'font-lock-string-face)
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik;; Syntax highlighting of CASL
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik ;; Keywords of loading Library
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik '("\\(\\<\\|\\s-+\\)\\(logic\\|from\\|get\\|library\\|version\\)[ :\t\n]+"
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik;; '("\\(\\<\\|\\s-+\\)\\(%authors\\|%date\\|%display\\|%prec\\|%left_assoc\\|%number\\|%floating\\|%LATEX\\|%implies\\)[ :\t\n]+"
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik;; (2 casl-annotation-face keep t))
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik ;; Library and Logic name
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik '("\\(\\<\\|\\s-+\\)\\(library\\|logic\\)\\s-+\\(\\(\\w\\|/\\)+\\)[ \t\n]*"
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik ;; name of from get and given
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik '("\\(\\<\\|[ \t]+\\)\\(get\\|given\\)[ \t\n]+\\(\\(\\sw+\\s-*\\(,\\|$\\)[ \t\n]*\\)+\\)"
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik '("\\(\\<\\|\\s-+\\)from\\([ \t]+\\)\\(.+\\)\\(get\\|\\s-*\\)"
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik ;; the name of specification and view
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik '("\\(\\<\\|\\[\\)\\(spec\\|view\\)\\s-+\\(\\w+\\)[ \t]*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?\\s-*.*\\([]=:]\\|::=\\)"
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik (3 casl-name-face keep t) (5 casl-name-face keep t))
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik ;; then, and + name
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik '("\\(\\<\\|\\s-+\\)\\(and\\|then\\)[ \t\n]*\\([A-Z]\\w*\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?"
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik (3 casl-name-face keep t) (5 casl-name-face keep t))
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik ;; names before and after to
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik '("[ \t\n]*\\(\\w+\\)[ \t\n]+to[ \t\n]+\\(\\(\\w+\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?[, \t]*\\)?"
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik (1 casl-name-face keep t) (3 casl-name-face keep t) (5 casl-name-face keep t))
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik ;; instance name of specification
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik '("\\<spec.+=\\s-*\\(%\\sw+\\s-*\\)?[ \t\n]*\\([A-Z]\\sw*\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?"
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik (2 casl-name-face keep t) (4 casl-name-face keep t))
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik ;; Basic signature: sort X, Y, Z
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik '("\\(\\<\\|\\s-+\\)sorts?[ \t]+\\(\\(\\sw+\\s-*\\(\\[\\(\\sw\\|,\\)+\\]\\s-*\\)?\\(,\\|$\\|<\\|;\\|=\\)\\(\\sw\\|=\\|<\\|;\\|,\\)*[ \t\n]*\\)+\\)"
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik ;; Basic signature: op ,pred and var name
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik '("\\(^\\|\\bops?\\|\\bpreds?\\|\\bvars?\\)\\s-+\\([^.]\\(\\w\\|\\s_\\)*\\)\\s-*\\(\(.*\)\\s-*\\)?\\(:\\??\\|<=>\\)[^:]*"
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik '("\\s-+\\(\\sw+\\)[ \t\n]*::=.*"
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik ;; constructor
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik '("|\\s-*\\(\\sw+\\)[ \t\n|(]*"
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik '("\(\\(\\(\\sw\\|,\\)*\\)\\s-*:\\??[^)]*\)"
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik '("\([^;]*;\\s-*\\(\\sw+\\)\\s-*:\\??.*\)"
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik ;; names before and after '|->'
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik '("[ \t\n]*\\([^[ \t\n]+\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?[ \t\n]+|->[ \t\n]+\\([^[ \t\n]+\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?[, \t]*"
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik (1 casl-other-name-face keep t) (3 casl-other-name-face keep t)
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik (4 casl-other-name-face keep t) (6 casl-other-name-face keep t))
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik ;; reserved keyword
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik '("\\(\\<\\|\\s-+\\)\\(/\\\\\\|\\\\/\\|=>\\|<=>\\|and\\|arch\\|assoc\\|closed\\|comm\\|else\\|end\\|exists\\|fit\\|forall\\|free\\|generated\\|given\\|hide\\|if\\|local\\|not\\|reveal\\|spec\\|then\\|to\\|unit\\|view\\|when\\|within\\|with\\|\\(\\(op\\|pred\\|var\\|type\\|sort\\)s?\\)\\)[,;]?[ \t\n]"
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik "Reserved keywords highlighting")
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik;; String and Char
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik (list '("\\(\\(\"\\|^>[ \t]*\\\\\\)\\([^\"\\\\\n]\\|\\\\.\\)*\\(\"\\|\\\\[ \t]*$\\)\\|'\\([^'\\\\\n]\\|\\\\.[^'\n]*\\)'\\)" (0 casl-string-char-face t t))
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik "Syntax highlighting of String and Char")
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik (list '("\\(%%.*$\\)" (0 casl-comment-face t t))
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik '("%{[^}]*}%[ \t\n]*" (0 casl-comment-face t t))
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik "Special Comment")
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik;; Alternativ for Annotation
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik ;; %word(...)\n
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik '("%\\sw+\([^%\n]+\)$" (0 casl-annotation-face t t))
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik '("%\\w+[^\n]*$" (0 casl-annotation-face t t))
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik '("%\([^)%]*\)%[ \t\n]*" (0 casl-annotation-face t t))
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik ;; %word( ... )%
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik '("%\\sw+\([^)%]*\)%[ \t\n]*" (0 casl-annotation-face t t))
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik "Annotation")
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik;; Define default highlighting level
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik;; (defvar casl-font-lock-syntax-highligthing casl-font-lock-keywords
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik(defvar casl-font-lock-syntax-highligthing casl-font-lock-annotations
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik "Default syntax highlighting level in CASL mode")
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik;; ====================== S Y N T A X T A B L E ==================
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik;; Syntax table for CASL major mode
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik "Syntax table for CASL mode.")
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik ;; Indicate that underscore may be part of a word
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik ;; commenting-out plus including other kinds of comment
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik ;; Some of these are actually OK by default.
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik "!#$&*+.,/:<=>?@^|~")
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik;; Various mode variables.
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik (make-local-variable 'comment-indent-function)
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik (setq comment-indent-function 'casl-comment-indent)
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik;; Find the indentation level for a comment.
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik ;; if the line is blank, put the comment at the beginning,
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik ;; else at comment-column
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik (if (bolp) 0 (max (1+ (current-column)) comment-column)))
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik;; ======================= R U N H E T S =======================
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik "Run hets process to compile the current CASL file."
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik (let* ((casl-hets-file-name (buffer-file-name))
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik (insert casl-hets-program " " casl-hets-file-name "\n")
c596fc4d75304ff224cbad0aa2aecd3cbe82d2ffLukas Slebodnik (call-process shell-file-name nil t nil "-c"
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik (concat casl-hets-program " " casl-hets-file-name))))
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik (format "exited abnormally with code %d\n" status))))
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik (compilation-handle-exit 'bizarre status status)))
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik (message "%s errors have been found." (length casl-error-list)))
b4633e73067d7bf3b0dbaf212569c123de88f306Lukas Slebodnik "Run hets -g process to compile the current CASL file."
(defun casl-parse-error ()
(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()