f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;;;###autoload
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski(autoload 'turn-on-dol-indent "dol-indent" "Turn on DOL indentation." t)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;;;;;;;;;;;;;;;;;;;;;;;;;;
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; Copyright: (c) University of Magdeburg, 2007-2016
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; License: LGPL, see LICENSE.txt or LIZENZ.txt
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; Contact: hets-users@informatik.uni-bremen.de
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;;;;;;;;;;;;;;;;;;;;;;;;;;
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; Version number
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "Version of DOL-Mode")
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "Major mode for editing (heterogeneous) DOL specifications."
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski(defvar dol-mode-map (let ((keymap (make-keymap)))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (define-key keymap "\C-c\C-r" 'dol-run-hets-r)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (define-key keymap "\C-c\C-u" 'dol-run-hets-g)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (define-key keymap "\C-c\C-c" 'dol-run-hets-g))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (define-key keymap "\C-c\C-n" 'dol-compile-goto-next-error)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "Keymap for DOL major mode")
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; Are we running FSF Emacs or XEmacs?
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (string-match "Lucid\\|XEmacs" emacs-version)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "non-nil if we are running XEmacs, nil otherwise.")
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; ====================== S Y N T A X T A B L E ==================
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; Syntax table for DOL major mode
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "Syntax table for DOL mode.")
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; Indicate that underscore may be part of a word
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; Some of these are actually OK by default.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "!#$&*+.,/\\\\:<=>?@^|~")
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; commenting-out plus including other kinds of comment
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; Various mode variables.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (setq comment-start-skip "%[{[]") ;; %[%{[]() *")
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (make-local-variable 'comment-indent-function)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (setq comment-indent-function 'dol-comment-indent)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (set (make-local-variable 'comment-end-skip) "[\]}]%")
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; Find the indentation level for a comment.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; if the line is blank, put the comment at the beginning,
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; else at comment-column
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (if (bolp) 0 (max (1+ (current-column)) comment-column)))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; ============= K E Y W O R D H I G H L I G H T I N G ============
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski(defvar dol-black-komma-face 'dol-black-komma-face
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "Face name to use for black komma.")
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski(defvar dol-annotation-face 'dol-annotation-face
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "DOL mode face for Annotations")
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski(setq dol-annotation-face 'font-lock-constant-face)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski(setq dol-name-face 'font-lock-variable-name-face)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski(setq dol-keyword-face 'font-lock-keyword-face)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski(defvar dol-library-name-face 'dol-library-name-face)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski(setq dol-library-name-face 'font-lock-type-face)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski(setq dol-builtin-face 'font-lock-builtin-face)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski(setq dol-comment-face 'font-lock-comment-face)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski(defvar dol-other-name-face 'dol-other-name-face)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (setq dol-other-name-face 'dol-blue-komma-face)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (setq dol-other-name-face 'font-lock-function-name-face)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski(defvar dol-string-char-face 'dol-string-char-face)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski(setq dol-string-char-face 'font-lock-string-face)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; Syntax highlighting of DOL
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; "Warning: Do not design an element of font-lock-keywords to match
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; text which spans lines; this does not work reliably. While
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; font-lock-fontify-buffer handles multi-line patterns correctly,
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; updating when you edit the buffer does not, since it considers
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; text one line at a time." (from the GNU Emacs Lisp Reference Manual)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; order of all the following highlighting rules is significant,
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; ony change if really needed
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("%%.*$" (0 (symbol-value 'dol-comment-face) keep t)))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "Special Comment")
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; Alternativ for Annotation
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; always highlight closing )%
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("\\(\)%\\)[^%]"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (1 (symbol-value 'dol-annotation-face) keep t))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("%\\w+\\b[^\n]*$"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (0 (symbol-value 'dol-annotation-face) keep t))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("[^%]\\(%\([^)]*?\)%\\)[^%]"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (1 (symbol-value 'dol-annotation-face) keep t))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; %word( ... )%
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("\\(%\\sw+\([^)]*?\)%\\)[^%]"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (1 (symbol-value 'dol-annotation-face) keep t))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "Annotation")
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; reserved keyword
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("\\(\\<\\|\\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]"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (2 (symbol-value 'dol-keyword-face) keep t))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("[,;.]" (0 (symbol-value 'dol-black-komma-face) t t))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; after forall don't highlight
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("\\bforall\\b\\(.*\\)"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (1 (symbol-value 'dol-black-komma-face) keep t))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; Keywords of loading Library
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("\\(\\<\\|\\s-+\\)\\(logic\\|from\\|get\\|library\\|version\\)[ :\t\n]+"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (2 (symbol-value 'dol-builtin-face) keep t))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; Library and Logic name
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("\\b\\(library\\|logic\\)\\s-+\\(\\(\\w\\|/\\)+\\)\\(\\s-*->\\s-*\\(\\(\\w\\|/\\)+\\)\\)?[ \t\n]"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (2 (symbol-value 'dol-library-name-face) keep t)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (5 (symbol-value 'dol-library-name-face) keep t))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; name of from, get and given
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("\\b\\(get\\|given\\)[ \t\n]+\\(\\(\\sw+\\s-*\\(,[ \t\n]*\\|$\\)\\)+\\)\\(=\\|:\\|$\\)"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("\\bfrom[ \t]+\\(.+\\)\\(get\\|$\\)"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (1 (symbol-value 'dol-library-name-face) keep t))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; the name of specification and view
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("\\(\\<\\|\\[\\)\\(spec\\|view\\)\\s-+\\(\\w+\\)[ \t]*\\(\\[\\s-*\\([A-Z]\\w*\\).*\\s-*\\]\\)?\\s-*.*\\([]=:]\\|::=\\)"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; then, and + name
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("\\b\\(and\\|then\\)[ \t\n]*\\([A-Z]\\w*\\)\\s-*\\(\\[\\([A-Z]\\sw*\\).*\\]\\)?"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; names before and after to
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("[ \t\n]*\\(\\sw+\\)[ \t\n]+to[ \t\n]+\\(\\(\\sw+\\)\\s-*\\(\\[\\([A-Z]\\sw*\\).*\\]\\)?[, \t]*\\)?"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; instance name of specification
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("\\<spec.+=\\s-*\\(%\\sw+\\s-*\\)?[ \t\n]*\\([A-Z]\\w*\\)\\s-*\\(\\[\\s-*\\([A-Z]\\w*\\).*\\s-*\\]\\)?"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; Basic signature: sort X, Y, Z
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("\\(\\<\\|\\s-+\\)sorts?[ \t\n]+\\(\\(\\sw+\\s-*\\(\\[\\s-*\\(\\sw\\|,\\)+\\s-*\\]\\s-*\\)?\\(,\\(\\s-\\)*\\|$\\|<\\|;\\|=\\)\\(=\\|<\\|;\\|,\\)*[ \t\n]*\\)+\\)"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (2 (symbol-value 'dol-other-name-face) keep t))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; Basic signature: op ,pred and var name
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("\\(\\(^[^.{%]\\)\\s-*\\|\\bops?\\b\\|\\bpreds?\\b\\|\\bvars?\\b\\)\\([^:{()\n]*\\)\\(\(.*\)\\)?:\\??[^?.:=%].*;?[ \t]*$"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (2 (symbol-value 'dol-other-name-face) keep t)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (3 (symbol-value 'dol-other-name-face) keep t))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; highlight a line with , an end
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("^\\(\\(\\(__\\s-*[^_\n]+\\s-*__\\|[^.,:>\n]+\\)\\s-*,\\s-*\\)+\\)$"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (0 (symbol-value 'dol-other-name-face) keep t))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; names before and after '|->'
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("[ \t\n]*\\(__[^|_]+__\\|[^[ \t\n]+\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?[ \t\n]*|->[ \t\n]*\\(__[^|_]+__\\|[^[ \t\n]+\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?[, \t]*"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (1 (symbol-value 'dol-other-name-face) keep t)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (3 (symbol-value 'dol-other-name-face) keep t)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (4 (symbol-value 'dol-other-name-face) keep t)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (6 (symbol-value 'dol-other-name-face) keep t))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("\\(\\btype\\|\\bfree type\\)?\\s-+\\(\\sw+\\)\\s-+\\(\\sw*\\|\\[\\(\\s-*\\sw+\\s-*\\)\\]\\)[ \t\n]*::?=[ \t\n]*\\(\\(\_\_[^_]+\_\_\\|[^|][^(|]+\\)\\s-*\\(\(.*\)\\)?\\)"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (2 (symbol-value 'dol-other-name-face) keep t)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (4 (symbol-value 'dol-other-name-face) keep t)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (6 (symbol-value 'dol-other-name-face) keep t))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; constructor
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("\|\\s-+\\(\_\_[^|_]+\_\_\\|[^|][^(|]+\\)\\s-*\\(\([^|]+\)\\)?[ \t\n]*"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (1 (symbol-value 'dol-other-name-face) keep t))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("\(\\(\\(\\sw\\|,\\)*\\)\\s-*:\\??[^)]*\)"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (1 (symbol-value 'dol-other-name-face) keep t))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski '("\([^;]*;\\s-*\\(\\sw+\\)\\s-*:\\??.*\)"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (1 (symbol-value 'dol-other-name-face) keep t))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "Reserved keywords highlighting")
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; String and Char
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (list '("\\(\\(\"\\|^>[ \t]*\\\\\\)\\([^\"\\\\\n]\\|\\\\.\\)*\\(\"\\|\\\\[ \t]*$\\)\\|'\\([^'\\\\\n]\\|\\\\.[^'\n]*\\)'\\)"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (0 (symbol-value 'dol-string-char-face) keep t))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "Syntax highlighting of String and Char")
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; Define default highlighting level
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; (defvar dol-font-lock-syntax-highligthing dol-font-lock-keywords
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski(defvar dol-font-lock-syntax-highligthing (symbol-value 'dol-font-lock-string)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "Default syntax highlighting level in DOL mode")
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; ======================= R U N H E T S =======================
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "*the additional options for running hets.")
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "Run hets process to compile the current DOL file."
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (setq run-option (concat run-option current " "))))
453058446f4b25ac85504960f6aaf8d9e4bc1a9bTill Mossakowski (setq hets-command (concat dol-hets-program run-option "\"" dol-hets-file-name "\""))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; Pop up the compilation buffer.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; (display-buffer outbuf nil t)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; (set-buffer outbuf)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; Start the compilation.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; Set the EMACS variable, but
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; don't override users' setting of $EMACS.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (proc (start-process-shell-command "hets-compile" outbuf
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (set-process-sentinel proc 'dol-compilation-sentinel)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (set-process-filter proc 'dol-compilation-filter)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (set-marker (process-mark proc) (point) outbuf))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "Run hets process with options (from dol-hets-options) to compile the
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski current DOL file."
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (setq option2 (concat option2 current " ")))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (setq run-option-r (concat run-option-r " " option2))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "Run hets process with -g and other options (from variable dol-hets-options)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski to compile the current DOL file."
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; sentinel and filter of asynchronous process of hets
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; Called when compilation process changes state.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "Sentinel for compilation buffers."
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (if (memq (process-status proc) '(signal exit))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; buffer killed
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; save-excursion isn't the right thing if
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; process-buffer is current-buffer
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; Write something in the compilation buffer
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; and hack its mode line.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (dol-compilation-handle-exit (process-status proc)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; Since the buffer and mode line will show that the
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; process is dead, we can delete it now. Otherwise it
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; will stay around until M-x list-processes.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; (setq compilation-in-progress (delq proc compilation-in-progress))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; show the message from hets compile direct on *hets-run* buffer
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (let ((moving (= (point) (process-mark proc))))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; Insert the text, advancing the process marker.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (if moving (goto-char (process-mark proc)))))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski(defun dol-compilation-handle-exit (process-status exit-status msg)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "Write msg in the current buffer and hack its mode-line-process."
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; Record where we put the message, so we can ignore it
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; (goto-char omax)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (insert " at " (substring (current-time-string) 0 19))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (setq mode-line-process (format ":%s [%s]" process-status (cdr status)))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; Force mode line redisplay soon.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; Automatically parse (and mouse-highlight) error messages:
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (message "%s errors have been found." (length dol-error-list)))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; also functions with old hets-program?
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "Error Parser"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;;;(pop-to-buffer compiler-buffer)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (if (not (or (looking-at "Fail") (and (looking-at "\\*\\*\\*") (looking-at "[0-9]+\\.[0-9]+-[0-9]+\\.[0-9]*"))))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (if (not (search-forward ":" (save-excursion (end-of-line) (point)) t 1))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (re-search-backward "\\(\(\\|\\s-+\\)\\([^.]+\\.\\(dol\\|het\\)\\)" nil t 1)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (setq file-name (match-string-no-properties 2))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (re-search-forward ":\\([0-9]+\\)\\.\\([0-9]+\\)\\(-[0-9]+\\.[0-9]*\\)?[:,]" (save-excursion (end-of-line) (point)) t 1)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (when (not (string= (match-string-no-properties 0) ""))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (setq error-line (match-string-no-properties 1))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (setq error-colnum (match-string-no-properties 2))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (nconc dol-error-list (list (list file-name error-line error-colnum error-window-point))))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "search the next error position from error-list, and move to it."
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; if error-list is empty ...
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (if (member (get-buffer "*hets-run*") (buffer-list))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (message "this file have not yet been compiled."))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; (message "DEBUG<Goto Error>: file: %s, line: %s, column: %s" error-file-name error-line error-column)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; if the file already opened ...
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (pop-to-buffer (get-file-buffer error-file-name))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; switch to hets-run window to jump to next error message
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; return to current file
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (move-to-column (- (string-to-number error-column) 1))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (message "goto next error... line: %s column: %s" error-line error-column)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (setq dol-error-list (nconc dol-error-list (list this-error)))
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; ================= D O L M A J O R M O D E ===============
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; dol major mode setup
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; Definition of DOL major mode
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski "Major mode for editing DOL models"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; Load keymap
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; Load syntax table
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; (dol-create-syntax-table)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; Highlight DOL keywords
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (make-local-variable 'font-lock-keywords-only)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; We just substitute our own functions to go to the error.
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (set (make-local-variable 'compile-auto-highlight) 40)
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski ;; FIXME: This has global impact! -stef
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (define-key compilation-minor-mode-map [mouse-2]
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski (define-key compilation-minor-mode-map "\C-m"
f93990c928a2b0b8f970b86d0fbd18d604147af6Till Mossakowski;; DOL-mode ends here