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