dol-mode.el revision 453058446f4b25ac85504960f6aaf8d9e4bc1a9b
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina;;;###autoload
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina(autoload 'turn-on-dol-indent "dol-indent" "Turn on DOL indentation." t)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina;;;;;;;;;;;;;;;;;;;;;;;;;;
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina;; $Haeder$
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina;; Copyright: (c) University of Magdeburg, 2007-2016
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina;; License: LGPL, see LICENSE.txt or LIZENZ.txt
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina;; Contact: hets-users@informatik.uni-bremen.de
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina;;;;;;;;;;;;;;;;;;;;;;;;;;
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina;; Version number
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina(defconst dol-mode-version "0.4"
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina "Version of DOL-Mode")
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina(defgroup dol nil
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina "Major mode for editing (heterogeneous) DOL specifications."
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina :group 'languages
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina :prefix "dol-")
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina(defvar dol-mode-hook nil)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina(defvar dol-mode-map (let ((keymap (make-keymap)))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (define-key keymap "\C-c\C-r" 'dol-run-hets-r)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (if (featurep 'xemacs)
d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina (define-key keymap "\C-c\C-u" 'dol-run-hets-g)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (define-key keymap "\C-c\C-c" 'dol-run-hets-g))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (define-key keymap "\C-c\C-n" 'dol-compile-goto-next-error)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina keymap)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina "Keymap for DOL major mode")
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina;; Are we running FSF Emacs or XEmacs?
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(defvar dol-running-xemacs
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (string-match "Lucid\\|XEmacs" emacs-version)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina "non-nil if we are running XEmacs, nil otherwise.")
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina;; ====================== S Y N T A X T A B L E ==================
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina;; Syntax table for DOL major mode
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina(defvar dol-mode-syntax-table nil
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina "Syntax table for DOL mode.")
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina(if dol-mode-syntax-table
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov ()
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (let ((table (make-syntax-table)))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ;; Indicate that underscore may be part of a word
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (modify-syntax-entry ?_ "w" table)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (modify-syntax-entry ?\t " " table)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (modify-syntax-entry ?\" "\"" table)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (modify-syntax-entry ?\' "\'" table)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (mapcar (lambda (x)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (modify-syntax-entry x "_" table))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ;; Some of these are actually OK by default.
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina "!#$&*+.,/\\\\:<=>?@^|~")
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina ;; commenting-out plus including other kinds of comment
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina ;; Comments
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (cond ((featurep 'xemacs)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (modify-syntax-entry ?( "()" table)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (modify-syntax-entry ?) ")(" table)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (modify-syntax-entry ?{ "(}2" table)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (modify-syntax-entry ?} "){3" table)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (modify-syntax-entry ?[ "(]2" table)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (modify-syntax-entry ?] ")[3" table)
1b3144586978c47506eaa39db505e6231e3b0c0aJakub Hrozek (modify-syntax-entry ?% "_ 14" table))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (t
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (modify-syntax-entry ?\( "()" table)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (modify-syntax-entry ?\) ")(" table)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (modify-syntax-entry ?{ "(} 2n" table)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (modify-syntax-entry ?} "){ 3n" table)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (modify-syntax-entry ?% ". 14nb" table)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (modify-syntax-entry ?\[ "(] 2n" table)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (modify-syntax-entry ?\] ")[ 3n" table))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina )
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (setq dol-mode-syntax-table table))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina )
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina;; Various mode variables.
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(defun dol-vars ()
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (kill-all-local-variables)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (make-local-variable 'comment-start)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (setq comment-start "%[")
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (make-local-variable 'comment-padding)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (setq comment-padding 0)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (make-local-variable 'comment-start-skip)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (setq comment-start-skip "%[{[]") ;; %[%{[]() *")
573e86dc3156e481ce53d39ac901da2e99cfa0caJakub Hrozek (make-local-variable 'comment-column)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (setq comment-column 40)
573e86dc3156e481ce53d39ac901da2e99cfa0caJakub Hrozek (make-local-variable 'comment-indent-function)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (setq comment-indent-function 'dol-comment-indent)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (make-local-variable 'comment-end)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (setq comment-end "]%")
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov (set (make-local-variable 'comment-end-skip) "[\]}]%")
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina;; Find the indentation level for a comment.
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(defun dol-comment-indent ()
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (skip-chars-backward " \t")
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina ;; if the line is blank, put the comment at the beginning,
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina ;; else at comment-column
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (if (bolp) 0 (max (1+ (current-column)) comment-column)))
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina;; ============= K E Y W O R D H I G H L I G H T I N G ============
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(defface dol-black-komma-face
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina `((t (:foreground "black")))
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina ""
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina :group 'basic-faces)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(defface dol-blue-komma-face
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina `((t (:foreground "blue")))
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina ""
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina :group 'basic-faces)
573e86dc3156e481ce53d39ac901da2e99cfa0caJakub Hrozek
573e86dc3156e481ce53d39ac901da2e99cfa0caJakub Hrozek(defvar dol-black-komma-face 'dol-black-komma-face
573e86dc3156e481ce53d39ac901da2e99cfa0caJakub Hrozek "Face name to use for black komma.")
87f8bee53ee1b4ca87b602ff8536bc5fd5b5b595Lukas Slebodnik
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(defvar dol-annotation-face 'dol-annotation-face
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina "DOL mode face for Annotations")
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(setq dol-annotation-face 'font-lock-constant-face)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(defvar dol-name-face 'dol-name-face)
573e86dc3156e481ce53d39ac901da2e99cfa0caJakub Hrozek(setq dol-name-face 'font-lock-variable-name-face)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(defvar dol-keyword-face 'dol-keyword-face)
573e86dc3156e481ce53d39ac901da2e99cfa0caJakub Hrozek(setq dol-keyword-face 'font-lock-keyword-face)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(defvar dol-library-name-face 'dol-library-name-face)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(setq dol-library-name-face 'font-lock-type-face)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(defvar dol-builtin-face 'dol-builtin-face)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(setq dol-builtin-face 'font-lock-builtin-face)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(defvar dol-comment-face 'dol-comment-face)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(setq dol-comment-face 'font-lock-comment-face)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(defvar dol-other-name-face 'dol-other-name-face)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(if (featurep 'xemacs)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (setq dol-other-name-face 'dol-blue-komma-face)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (setq dol-other-name-face 'font-lock-function-name-face)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(defvar dol-string-char-face 'dol-string-char-face)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(setq dol-string-char-face 'font-lock-string-face)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina;; Syntax highlighting of DOL
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina;; "Warning: Do not design an element of font-lock-keywords to match
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina;; text which spans lines; this does not work reliably. While
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina;; font-lock-fontify-buffer handles multi-line patterns correctly,
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina;; updating when you edit the buffer does not, since it considers
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina;; text one line at a time." (from the GNU Emacs Lisp Reference Manual)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina;; order of all the following highlighting rules is significant,
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina;; ony change if really needed
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov ;; Comment
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina(defconst dol-font-lock-specialcomment
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (list
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina '("%%.*$" (0 (symbol-value 'dol-comment-face) keep t)))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina "Special Comment")
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina;; Alternativ for Annotation
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina(defconst dol-font-lock-annotations
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (append dol-font-lock-specialcomment
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (list
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ;; always highlight closing )%
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina '("\\(\)%\\)[^%]"
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (1 (symbol-value 'dol-annotation-face) keep t))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ;; %words \n
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina '("%\\w+\\b[^\n]*$"
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (0 (symbol-value 'dol-annotation-face) keep t))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ;; %(.....)%
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina '("[^%]\\(%\([^)]*?\)%\\)[^%]"
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (1 (symbol-value 'dol-annotation-face) keep t))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ;; %word( ... )%
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina '("\\(%\\sw+\([^)]*?\)%\\)[^%]"
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (1 (symbol-value 'dol-annotation-face) keep t))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina "Annotation")
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina(defconst dol-font-lock-keywords
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (append dol-font-lock-annotations
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (list
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ;; reserved keyword
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina '("\\(\\<\\|\\s-+\\)\\(/\\\\\\|\\\\/\\|=>\\|<=>\\|and\\|arch\\|assoc\\|behaviourally\\|closed\\|comm\\|else\\|end\\|exists\\|fit\\|flexible\\|forall\\|free\\|generated\\|given\\|idem\\|if\\|local\\|modality\\|not\\|orElse\\|unit\\|when\\|alignment\\|along\\|assuming\\|and\\|closed-world\\|cofree\\|combine\\|cons-ext\\|end\\|entails\\|entailment\\|equivalence\\|excluding\\|extract\\|free\\|hide\\|import\\|in\\|for\\|forget\\|interpretation\\|keep\\|language\\|library\\|logic\\|maximize\\|model\\|minimize\\|network\\|ni\\|of\\|oms\\|onto\\|ontology\\|refined\\|refinement\\|reject\\|relation\\|remove\\|result\\|reveal\\|select\\|separators\\|serialization\\|spec\\|specification\\|substitution\\|syntax\\|then\\|to\\|translation\\|using\\|vars\\|via\\|view\\|where\\|with\\|cons\\|ccons\\|complete\\|consistent\\|def\\|implied\\|inconsistent\\|mcons\\|mono\\|notccons\\|notmcons\\|prefix\\|wdef\\|within\\|\\(\\(op\\|pred\\|var\\|type\\|sort\\)s?\\)\\)[,;]?[ \t\n]"
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (2 (symbol-value 'dol-keyword-face) keep t))
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina '("[,;.]" (0 (symbol-value 'dol-black-komma-face) t t))
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina ;; after forall don't highlight
46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina '("\\bforall\\b\\(.*\\)"
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (1 (symbol-value 'dol-black-komma-face) keep t))
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina ;; Keywords of loading Library
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina '("\\(\\<\\|\\s-+\\)\\(logic\\|from\\|get\\|library\\|version\\)[ :\t\n]+"
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (2 (symbol-value 'dol-builtin-face) keep t))
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina ;; Library and Logic name
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina '("\\b\\(library\\|logic\\)\\s-+\\(\\(\\w\\|/\\)+\\)\\(\\s-*->\\s-*\\(\\(\\w\\|/\\)+\\)\\)?[ \t\n]"
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (2 (symbol-value 'dol-library-name-face) keep t)
5ff1c3c5a12930692cb6284d14f7fda3a974af8ePavel Březina (5 (symbol-value 'dol-library-name-face) keep t))
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina ;; name of from, get and given
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina '("\\b\\(get\\|given\\)[ \t\n]+\\(\\(\\sw+\\s-*\\(,[ \t\n]*\\|$\\)\\)+\\)\\(=\\|:\\|$\\)"
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (2 (symbol-value 'dol-name-face) t t))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina '("\\bfrom[ \t]+\\(.+\\)\\(get\\|$\\)"
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (1 (symbol-value 'dol-library-name-face) keep t))
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina ;; the name of specification and view
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina '("\\(\\<\\|\\[\\)\\(spec\\|view\\)\\s-+\\(\\w+\\)[ \t]*\\(\\[\\s-*\\([A-Z]\\w*\\).*\\s-*\\]\\)?\\s-*.*\\([]=:]\\|::=\\)"
5ff1c3c5a12930692cb6284d14f7fda3a974af8ePavel Březina (3 (symbol-value 'dol-name-face) keep t)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (5 (symbol-value 'dol-name-face) keep t))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ;; then, and + name
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina '("\\b\\(and\\|then\\)[ \t\n]*\\([A-Z]\\w*\\)\\s-*\\(\\[\\([A-Z]\\sw*\\).*\\]\\)?"
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (2 (symbol-value 'dol-name-face) keep t)
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov (4 (symbol-value 'dol-name-face) keep t))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ;; names before and after to
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina '("[ \t\n]*\\(\\sw+\\)[ \t\n]+to[ \t\n]+\\(\\(\\sw+\\)\\s-*\\(\\[\\([A-Z]\\sw*\\).*\\]\\)?[, \t]*\\)?"
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (1 (symbol-value 'dol-name-face) keep t)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (3 (symbol-value 'dol-name-face) keep t)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (5 (symbol-value 'dol-name-face) keep t))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ;; instance name of specification
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina '("\\<spec.+=\\s-*\\(%\\sw+\\s-*\\)?[ \t\n]*\\([A-Z]\\w*\\)\\s-*\\(\\[\\s-*\\([A-Z]\\w*\\).*\\s-*\\]\\)?"
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (2 (symbol-value 'dol-name-face) keep t)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (4 (symbol-value 'dol-name-face) keep t))
573e86dc3156e481ce53d39ac901da2e99cfa0caJakub Hrozek ;; Basic signature: sort X, Y, Z
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina '("\\(\\<\\|\\s-+\\)sorts?[ \t\n]+\\(\\(\\sw+\\s-*\\(\\[\\s-*\\(\\sw\\|,\\)+\\s-*\\]\\s-*\\)?\\(,\\(\\s-\\)*\\|$\\|<\\|;\\|=\\)\\(=\\|<\\|;\\|,\\)*[ \t\n]*\\)+\\)"
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (2 (symbol-value 'dol-other-name-face) keep t))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ;; Basic signature: op ,pred and var name
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina '("\\(\\(^[^.{%]\\)\\s-*\\|\\bops?\\b\\|\\bpreds?\\b\\|\\bvars?\\b\\)\\([^:{()\n]*\\)\\(\(.*\)\\)?:\\??[^?.:=%].*;?[ \t]*$"
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (2 (symbol-value 'dol-other-name-face) keep t)
7379170a0860790f2739e07fffe3d6ec85264566Pavel Březina (3 (symbol-value 'dol-other-name-face) keep t))
7379170a0860790f2739e07fffe3d6ec85264566Pavel Březina ;; highlight a line with , an end
7379170a0860790f2739e07fffe3d6ec85264566Pavel Březina '("^\\(\\(\\(__\\s-*[^_\n]+\\s-*__\\|[^.,:>\n]+\\)\\s-*,\\s-*\\)+\\)$"
46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina (0 (symbol-value 'dol-other-name-face) keep t))
46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina ;; names before and after '|->'
46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina '("[ \t\n]*\\(__[^|_]+__\\|[^[ \t\n]+\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?[ \t\n]*|->[ \t\n]*\\(__[^|_]+__\\|[^[ \t\n]+\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?[, \t]*"
46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina (1 (symbol-value 'dol-other-name-face) keep t)
46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina (3 (symbol-value 'dol-other-name-face) keep t)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (4 (symbol-value 'dol-other-name-face) keep t)
5ff1c3c5a12930692cb6284d14f7fda3a974af8ePavel Březina (6 (symbol-value 'dol-other-name-face) keep t))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ;; type name
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina '("\\(\\btype\\|\\bfree type\\)?\\s-+\\(\\sw+\\)\\s-+\\(\\sw*\\|\\[\\(\\s-*\\sw+\\s-*\\)\\]\\)[ \t\n]*::?=[ \t\n]*\\(\\(\_\_[^_]+\_\_\\|[^|][^(|]+\\)\\s-*\\(\(.*\)\\)?\\)"
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (2 (symbol-value 'dol-other-name-face) keep t)
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (4 (symbol-value 'dol-other-name-face) keep t)
573e86dc3156e481ce53d39ac901da2e99cfa0caJakub Hrozek (6 (symbol-value 'dol-other-name-face) keep t))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ;; constructor
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina '("\|\\s-+\\(\_\_[^|_]+\_\_\\|[^|][^(|]+\\)\\s-*\\(\([^|]+\)\\)?[ \t\n]*"
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (1 (symbol-value 'dol-other-name-face) keep t))
573e86dc3156e481ce53d39ac901da2e99cfa0caJakub Hrozek ;; in ()1
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina '("\(\\(\\(\\sw\\|,\\)*\\)\\s-*:\\??[^)]*\)"
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (1 (symbol-value 'dol-other-name-face) keep t))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ;; in ()2
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina '("\([^;]*;\\s-*\\(\\sw+\\)\\s-*:\\??.*\)"
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (1 (symbol-value 'dol-other-name-face) keep t))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina ))
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina "Reserved keywords highlighting")
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina;; String and Char
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina(defconst dol-font-lock-string
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (append dol-font-lock-keywords
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (list '("\\(\\(\"\\|^>[ \t]*\\\\\\)\\([^\"\\\\\n]\\|\\\\.\\)*\\(\"\\|\\\\[ \t]*$\\)\\|'\\([^'\\\\\n]\\|\\\\.[^'\n]*\\)'\\)"
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (0 (symbol-value 'dol-string-char-face) keep t))
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina ))
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina "Syntax highlighting of String and Char")
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina;; Define default highlighting level
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina;; (defvar dol-font-lock-syntax-highligthing dol-font-lock-keywords
15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina(defvar dol-font-lock-syntax-highligthing (symbol-value 'dol-font-lock-string)
15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina "Default syntax highlighting level in DOL mode")
15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina
15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina;; ======================= R U N H E T S =======================
15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina(require 'compile)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina(setq dol-error-list nil)
15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina(defvar hets-program nil)
15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina(defvar old-buffer nil)
15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina(defvar dol-hets-options nil
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina "*the additional options for running hets.")
46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina
46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina(defun dol-run-hets (&rest opt)
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov "Run hets process to compile the current DOL file."
15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina (interactive)
46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina (save-buffer nil)
15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina (setq old-buffer (current-buffer))
46d3d2c731e8c7e138462e5b60a39a279dc77d81Pavel Březina (let* ((run-option " ")
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (dol-hets-file-name (buffer-file-name))
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (outbuf (get-buffer-create "*hets-run*")))
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (if hets-program
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (setq dol-hets-program hets-program)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (setq dol-hets-program "hets"))
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov (if opt
15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina (dolist (current opt run-option)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (setq run-option (concat run-option current " "))))
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (setq hets-command (concat dol-hets-program run-option "\"" dol-hets-file-name "\""))
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov ;; Pop up the compilation buffer.
15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina (set-buffer outbuf)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (setq buffer-read-only nil)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (buffer-disable-undo (current-buffer))
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (erase-buffer)
a3c8390d19593b1e5277d95bfb4ab206d4785150Nikolai Kondrashov (buffer-enable-undo (current-buffer))
15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina (set-buffer-modified-p nil)
d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina (insert hets-command "\n")
d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina (pop-to-buffer outbuf)
15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina (goto-char (point-max))
15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina ;; (display-buffer outbuf nil t)
15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina (save-excursion
d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina ;; (set-buffer outbuf)
d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina (compilation-mode "hets-compile")
15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina ;; Start the compilation.
15d41c8f28259061e39715acdbbbaea778b6ecc8Pavel Březina (if (fboundp 'start-process)
710472d946f6c337a095699dfd79134fa8b9eab9Pavel Březina (let* ((process-environment
d38ffc9c92daeb62de7d28c409bdaeff98f82775Pavel Březina (append
2827b0d03f7b6bafa504d22a5d7ca39cbda048b3Pavel Březina (if (and (boundp 'system-uses-terminfo)
system-uses-terminfo)
(list "TERM=dumb" "TERMCAP="
(format "COLUMNS=%d" (window-width)))
(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")
process-environment
(cons "EMACS=t" process-environment))))
(proc (start-process-shell-command "hets-compile" outbuf
hets-command)))
(setq buffer-read-only nil)
(set-process-sentinel proc 'dol-compilation-sentinel)
(set-process-filter proc 'dol-compilation-filter)
(set-marker (process-mark proc) (point) outbuf))
))
(pop-to-buffer old-buffer)))
(defun dol-run-hets-r (&rest opt)
"Run hets process with options (from dol-hets-options) to compile the
current DOL file."
(interactive)
(setq option1 nil)
(setq option2 nil)
(setq run-option-r nil)
(if dol-hets-options
(setq run-option-r dol-hets-options))
(if opt
(dolist (current opt option2)
(setq option2 (concat option2 current " ")))
)
(setq run-option-r (concat run-option-r " " option2))
(dol-run-hets run-option-r)
)
(defun dol-run-hets-g ()
"Run hets process with -g and other options (from variable dol-hets-options)
to compile the current DOL file."
(interactive)
(dol-run-hets-r "-g")
)
;; sentinel and filter of asynchronous process of hets
;; Called when compilation process changes state.
(defun dol-compilation-sentinel (proc msg)
"Sentinel for compilation buffers."
(let ((buffer (process-buffer proc)))
(if (memq (process-status proc) '(signal exit))
(progn
(if (null (buffer-name buffer))
;; buffer killed
(set-process-buffer proc nil)
(let ((obuf (current-buffer)))
;; save-excursion isn't the right thing if
;; process-buffer is current-buffer
(unwind-protect
(progn
;; Write something in the compilation buffer
;; and hack its mode line.
(set-buffer buffer)
(dol-compilation-handle-exit (process-status proc)
(process-exit-status proc)
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.
(delete-process proc))
(set-buffer obuf))))
;; (setq compilation-in-progress (delq proc compilation-in-progress))
))))
;; show the message from hets compile direct on *hets-run* buffer
(defun dol-compilation-filter (proc string)
(display-buffer (process-buffer proc))
(unless (equal (buffer-name) "*hets-run*")
(progn
(pop-to-buffer "*hets-run*")
(goto-char (point-max))
))
(with-current-buffer (process-buffer proc)
(let ((moving (= (point) (process-mark proc))))
(save-excursion
;; Insert the text, advancing the process marker.
(goto-char (process-mark proc))
(insert string)
(set-marker (process-mark proc) (point)))
(if moving (goto-char (process-mark proc)))))
(pop-to-buffer old-buffer))
(defun dol-compilation-handle-exit (process-status exit-status msg)
"Write msg in the current buffer and hack its mode-line-process."
(let ((buffer-read-only nil)
(status (cons msg exit-status))
(omax (point-max))
(opoint (point)))
;; Record where we put the message, so we can ignore it
;; later on.
;; (goto-char omax)
(goto-char (point-max))
(insert ?\n mode-name " " (car status))
(if (bolp)
(forward-char -1))
(insert " at " (substring (current-time-string) 0 19))
(goto-char (point-max))
(setq mode-line-process (format ":%s [%s]" process-status (cdr status)))
;; Force mode line redisplay soon.
(force-mode-line-update)
(if (and opoint (< opoint omax))
(goto-char opoint))
;; Automatically parse (and mouse-highlight) error messages:
(if (zerop exit-status)
(setq dol-error-list nil)
(setq dol-error-list nil)
(dol-parse-error)
(message "%s errors have been found." (length dol-error-list)))
(pop-to-buffer old-buffer)
))
;; also functions with old hets-program?
(defun dol-parse-error ()
"Error Parser"
(interactive)
(setq dol-error-list nil)
;;;(pop-to-buffer compiler-buffer)
(pop-to-buffer "*hets-run*")
(goto-char (point-min))
(while (not (eobp))
(if (not (or (looking-at "Fail") (and (looking-at "\\*\\*\\*") (looking-at "[0-9]+\\.[0-9]+-[0-9]+\\.[0-9]*"))))
(forward-line 1)
(skip-chars-forward "a-zA-Z*,/._\\- ")
(if (not (search-forward ":" (save-excursion (end-of-line) (point)) t 1))
(forward-line 1)
(re-search-backward "\\(\(\\|\\s-+\\)\\([^.]+\\.\\(dol\\|het\\)\\)" nil t 1)
(setq file-name (match-string-no-properties 2))
(re-search-forward ":\\([0-9]+\\)\\.\\([0-9]+\\)\\(-[0-9]+\\.[0-9]*\\)?[:,]" (save-excursion (end-of-line) (point)) t 1)
(when (not (string= (match-string-no-properties 0) ""))
(setq error-line (match-string-no-properties 1))
(setq error-colnum (match-string-no-properties 2))
(setq error-window-point (point))
(setq dol-error-list
(nconc dol-error-list (list (list file-name error-line error-colnum error-window-point))))
)
(forward-line 1)))))
(defun dol-compile-goto-next-error ()
"search the next error position from error-list, and move to it."
(interactive)
;; if error-list is empty ...
(if (null dol-error-list)
(dol-parse-error))
(if (null dol-error-list)
(if (member (get-buffer "*hets-run*") (buffer-list))
(message "no error.")
(message "this file have not yet been compiled."))
(let* ((this-error (pop dol-error-list))
(error-file-name (nth 0 this-error))
(error-line (nth 1 this-error))
(error-column (nth 2 this-error))
(error-window-point (nth 3 this-error)))
;; (message "DEBUG<Goto Error>: file: %s, line: %s, column: %s" error-file-name error-line error-column)
;; if the file already opened ...
(if (get-file-buffer error-file-name)
(pop-to-buffer (get-file-buffer error-file-name))
(generate-new-buffer error-file-name)
(pop-to-buffer error-file-name)
(insert-file-contents error-file-name))
;; switch to hets-run window to jump to next error message
(setq file-buffer (current-buffer))
(pop-to-buffer "*hets-run*")
(goto-char error-window-point)
;; return to current file
(pop-to-buffer file-buffer)
(goto-line (string-to-number error-line))
(move-to-column (- (string-to-number error-column) 1))
(message "goto next error... line: %s column: %s" error-line error-column)
(setq dol-error-list (nconc dol-error-list (list this-error)))
)))
;; ================= D O L M A J O R M O D E ===============
;; dol major mode setup
;; Definition of DOL major mode
(defun dol-mode ()
"Major mode for editing DOL models"
(interactive)
(dol-vars)
(setq major-mode 'dol-mode)
(setq mode-name "DOL")
;; Load keymap
(use-local-map dol-mode-map)
;; Load syntax table
(set-syntax-table dol-mode-syntax-table)
;; (dol-create-syntax-table)
;; Highlight DOL keywords
(make-local-variable 'font-lock-defaults)
(setq font-lock-defaults
'(dol-font-lock-syntax-highligthing))
(make-local-variable 'font-lock-keywords-only)
(setq font-lock-keywords-only nil)
;; Support for compile.el
;; We just substitute our own functions to go to the error.
(add-hook 'compilation-mode-hook
(lambda()
(set (make-local-variable 'compile-auto-highlight) 40)
;; FIXME: This has global impact! -stef
(define-key compilation-minor-mode-map [mouse-2]
'dol-compile-mouse-goto-error)
(define-key compilation-minor-mode-map "\C-m"
'dol-compile-goto-next-error)))
(run-hooks 'dol-mode-hook)
)
(provide 'dol-mode)
;; DOL-mode ends here