dol-mode.el revision f93990c928a2b0b8f970b86d0fbd18d604147af6
;;;###autoload
;;;;;;;;;;;;;;;;;;;;;;;;;;
;; $Haeder$
;; Copyright: (c) University of Magdeburg, 2007-2016
;; License: LGPL, see LICENSE.txt or LIZENZ.txt
;; Contact: hets-users@informatik.uni-bremen.de
;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Version number
"Version of DOL-Mode")
"Major mode for editing (heterogeneous) DOL specifications."
:prefix "dol-")
(defvar dol-mode-hook nil)
"Keymap for DOL major mode")
;; Are we running FSF Emacs or XEmacs?
(defvar dol-running-xemacs
"non-nil if we are running XEmacs, nil otherwise.")
;; ====================== S Y N T A X T A B L E ==================
;; Syntax table for DOL major mode
(defvar dol-mode-syntax-table nil
"Syntax table for DOL mode.")
()
(let ((table (make-syntax-table)))
;; Indicate that underscore may be part of a word
;; Some of these are actually OK by default.
"!#$&*+.,/\\\\:<=>?@^|~")
;; commenting-out plus including other kinds of comment
;; Comments
(t
)
)
;; Various mode variables.
(defun dol-vars ()
)
;; Find the indentation level for a comment.
(defun dol-comment-indent ()
(skip-chars-backward " \t")
;; if the line is blank, put the comment at the beginning,
;; else at comment-column
;; ============= K E Y W O R D H I G H L I G H T I N G ============
`((t (:foreground "black")))
""
`((t (:foreground "blue")))
""
(defvar dol-black-komma-face 'dol-black-komma-face
"Face name to use for black komma.")
(defvar dol-annotation-face 'dol-annotation-face
"DOL mode face for Annotations")
(defvar dol-name-face 'dol-name-face)
(defvar dol-keyword-face 'dol-keyword-face)
(defvar dol-library-name-face 'dol-library-name-face)
(defvar dol-builtin-face 'dol-builtin-face)
(defvar dol-comment-face 'dol-comment-face)
(defvar dol-other-name-face 'dol-other-name-face)
)
(defvar dol-string-char-face 'dol-string-char-face)
;; Syntax highlighting of DOL
;; "Warning: Do not design an element of font-lock-keywords to match
;; text which spans lines; this does not work reliably. While
;; font-lock-fontify-buffer handles multi-line patterns correctly,
;; updating when you edit the buffer does not, since it considers
;; text one line at a time." (from the GNU Emacs Lisp Reference Manual)
;; order of all the following highlighting rules is significant,
;; ony change if really needed
;; Comment
(list
"Special Comment")
;; Alternativ for Annotation
(list
;; always highlight closing )%
'("\\(\)%\\)[^%]"
;; %words \n
'("%\\w+\\b[^\n]*$"
;; %(.....)%
'("[^%]\\(%\([^)]*?\)%\\)[^%]"
;; %word( ... )%
'("\\(%\\sw+\([^)]*?\)%\\)[^%]"
))
"Annotation")
(list
;; reserved keyword
'("\\(\\<\\|\\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]"
;; after forall don't highlight
'("\\bforall\\b\\(.*\\)"
;; Keywords of loading Library
'("\\(\\<\\|\\s-+\\)\\(logic\\|from\\|get\\|library\\|version\\)[ :\t\n]+"
;; Library and Logic name
'("\\b\\(library\\|logic\\)\\s-+\\(\\(\\w\\|/\\)+\\)\\(\\s-*->\\s-*\\(\\(\\w\\|/\\)+\\)\\)?[ \t\n]"
;; name of from, get and given
'("\\b\\(get\\|given\\)[ \t\n]+\\(\\(\\sw+\\s-*\\(,[ \t\n]*\\|$\\)\\)+\\)\\(=\\|:\\|$\\)"
'("\\bfrom[ \t]+\\(.+\\)\\(get\\|$\\)"
;; the name of specification and view
'("\\(\\<\\|\\[\\)\\(spec\\|view\\)\\s-+\\(\\w+\\)[ \t]*\\(\\[\\s-*\\([A-Z]\\w*\\).*\\s-*\\]\\)?\\s-*.*\\([]=:]\\|::=\\)"
;; then, and + name
'("\\b\\(and\\|then\\)[ \t\n]*\\([A-Z]\\w*\\)\\s-*\\(\\[\\([A-Z]\\sw*\\).*\\]\\)?"
;; names before and after to
'("[ \t\n]*\\(\\sw+\\)[ \t\n]+to[ \t\n]+\\(\\(\\sw+\\)\\s-*\\(\\[\\([A-Z]\\sw*\\).*\\]\\)?[, \t]*\\)?"
;; instance name of specification
'("\\<spec.+=\\s-*\\(%\\sw+\\s-*\\)?[ \t\n]*\\([A-Z]\\w*\\)\\s-*\\(\\[\\s-*\\([A-Z]\\w*\\).*\\s-*\\]\\)?"
;; Basic signature: sort X, Y, Z
'("\\(\\<\\|\\s-+\\)sorts?[ \t\n]+\\(\\(\\sw+\\s-*\\(\\[\\s-*\\(\\sw\\|,\\)+\\s-*\\]\\s-*\\)?\\(,\\(\\s-\\)*\\|$\\|<\\|;\\|=\\)\\(=\\|<\\|;\\|,\\)*[ \t\n]*\\)+\\)"
;; Basic signature: op ,pred and var name
'("\\(\\(^[^.{%]\\)\\s-*\\|\\bops?\\b\\|\\bpreds?\\b\\|\\bvars?\\b\\)\\([^:{()\n]*\\)\\(\(.*\)\\)?:\\??[^?.:=%].*;?[ \t]*$"
;; highlight a line with , an end
'("^\\(\\(\\(__\\s-*[^_\n]+\\s-*__\\|[^.,:>\n]+\\)\\s-*,\\s-*\\)+\\)$"
;; names before and after '|->'
'("[ \t\n]*\\(__[^|_]+__\\|[^[ \t\n]+\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?[ \t\n]*|->[ \t\n]*\\(__[^|_]+__\\|[^[ \t\n]+\\)\\s-*\\(\\[\\([A-Z]\\w*\\).*\\]\\)?[, \t]*"
;; type name
'("\\(\\btype\\|\\bfree type\\)?\\s-+\\(\\sw+\\)\\s-+\\(\\sw*\\|\\[\\(\\s-*\\sw+\\s-*\\)\\]\\)[ \t\n]*::?=[ \t\n]*\\(\\(\_\_[^_]+\_\_\\|[^|][^(|]+\\)\\s-*\\(\(.*\)\\)?\\)"
;; constructor
'("\|\\s-+\\(\_\_[^|_]+\_\_\\|[^|][^(|]+\\)\\s-*\\(\([^|]+\)\\)?[ \t\n]*"
;; in ()1
'("\(\\(\\(\\sw\\|,\\)*\\)\\s-*:\\??[^)]*\)"
;; in ()2
'("\([^;]*;\\s-*\\(\\sw+\\)\\s-*:\\??.*\)"
))
"Reserved keywords highlighting")
;; String and Char
(list '("\\(\\(\"\\|^>[ \t]*\\\\\\)\\([^\"\\\\\n]\\|\\\\.\\)*\\(\"\\|\\\\[ \t]*$\\)\\|'\\([^'\\\\\n]\\|\\\\.[^'\n]*\\)'\\)"
))
"Syntax highlighting of String and Char")
;; Define default highlighting level
;; (defvar dol-font-lock-syntax-highligthing dol-font-lock-keywords
"Default syntax highlighting level in DOL mode")
;; ======================= R U N H E T S =======================
(setq dol-error-list nil)
(defvar hets-program nil)
(defvar old-buffer nil)
(defvar dol-hets-options nil
"*the additional options for running hets.")
"Run hets process to compile the current DOL file."
(save-buffer nil)
(let* ((run-option " ")
(if hets-program
(if opt
;; Pop up the compilation buffer.
(setq buffer-read-only nil)
(set-buffer-modified-p nil)
;; (display-buffer outbuf nil t)
;; (set-buffer outbuf)
(compilation-mode "hets-compile")
;; Start the compilation.
(if (fboundp 'start-process)
(let* ((process-environment
(if (and (boundp 'system-uses-terminfo)
(list "TERM=dumb" "TERMCAP="
(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")
hets-command)))
(setq buffer-read-only nil)
))
"Run hets process with options (from dol-hets-options) to compile the
current DOL file."
(setq run-option-r nil)
(if dol-hets-options
(if opt
)
)
(defun dol-run-hets-g ()
"Run hets process with -g and other options (from variable dol-hets-options)
to compile the current DOL file."
(dol-run-hets-r "-g")
)
;; sentinel and filter of asynchronous process of hets
;; Called when compilation process changes state.
"Sentinel for compilation buffers."
;; buffer killed
(set-process-buffer proc nil)
(let ((obuf (current-buffer)))
;; save-excursion isn't the right thing if
;; process-buffer is current-buffer
;; Write something in the compilation buffer
;; and hack its mode line.
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.
(set-buffer obuf))))
;; (setq compilation-in-progress (delq proc compilation-in-progress))
))))
;; show the message from hets compile direct on *hets-run* buffer
(pop-to-buffer "*hets-run*")
))
;; Insert the text, advancing the process marker.
"Write msg in the current buffer and hack its mode-line-process."
(let ((buffer-read-only nil)
;; Record where we put the message, so we can ignore it
;; later on.
;; (goto-char omax)
(if (bolp)
(forward-char -1))
;; Force mode line redisplay soon.
;; Automatically parse (and mouse-highlight) error messages:
(if (zerop exit-status)
(setq dol-error-list nil)
(setq dol-error-list nil)
))
;; also functions with old hets-program?
(defun dol-parse-error ()
"Error Parser"
(setq dol-error-list nil)
;;;(pop-to-buffer compiler-buffer)
(pop-to-buffer "*hets-run*")
(if (not (or (looking-at "Fail") (and (looking-at "\\*\\*\\*") (looking-at "[0-9]+\\.[0-9]+-[0-9]+\\.[0-9]*"))))
(skip-chars-forward "a-zA-Z*,/._\\- ")
(re-search-forward ":\\([0-9]+\\)\\.\\([0-9]+\\)\\(-[0-9]+\\.[0-9]*\\)?[:,]" (save-excursion (end-of-line) (point)) t 1)
)
(forward-line 1)))))
(defun dol-compile-goto-next-error ()
"search the next error position from error-list, and move to it."
;; if error-list is empty ...
(if (null dol-error-list)
(if (null dol-error-list)
(message "no error.")
(message "this file have not yet been compiled."))
;; (message "DEBUG<Goto Error>: file: %s, line: %s, column: %s" error-file-name error-line error-column)
;; if the file already opened ...
;; switch to hets-run window to jump to next error message
(pop-to-buffer "*hets-run*")
;; return to current file
)))
;; ================= 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"
(dol-vars)
;; Load keymap
;; Load syntax table
;; (dol-create-syntax-table)
;; Highlight DOL keywords
(setq font-lock-keywords-only nil)
;; Support for compile.el
;; We just substitute our own functions to go to the error.
(lambda()
;; FIXME: This has global impact! -stef
)
;; DOL-mode ends here