hpf-mode.el revision b9b8f261fe6ee3907ec15372993cbfec33448c52
;;;###autoload
;;;;;;;;;;;;;;;;;;;;;;;;;;
;; $Haeder$
;; Copyright: (c) Heng Jiang, Uni Bremen 2007
;; License: LGPL, see LICENSE.txt or LIZENZ.txt
;; Contact: hets-users@informatik.uni-bremen.de
;;;;;;;;;;;;;;;;;;;;;;;;;;
;; Version number
"Version of HPF-Mode")
"Major mode for editing (heterogeneous) HPF specifications."
:prefix "hpf-")
(defvar hpf-mode-hook nil)
"Keymap for HPF major mode")
;; Are we running FSF Emacs or XEmacs?
(defvar hpf-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 HPF major mode
(defvar hpf-mode-syntax-table nil
"Syntax table for HPF 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
)
;; Various mode variables.
(defun hpf-vars ()
)
;; ============= 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 hpf-black-komma-face 'hpf-black-komma-face
"Face name to use for black komma.")
(defvar hpf-annotation-face 'hpf-annotation-face
"HPF mode face for Annotations")
(defvar hpf-name-face 'hpf-name-face)
(defvar hpf-keyword-face 'hpf-keyword-face)
(defvar hpf-library-name-face 'hpf-library-name-face)
(defvar hpf-builtin-face 'hpf-builtin-face)
(defvar hpf-comment-face 'hpf-comment-face)
(defvar hpf-other-name-face 'hpf-other-name-face)
)
(defvar hpf-string-char-face 'hpf-string-char-face)
;; Syntax highlighting of HPF
;; "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")
(list
;; commands
'("\\(\\<\\|\\s-+\\)\\(use\\|dg\\|dg-all\\|show-dg-goals\\|show-theory-goals\\|show-theory\\|node-info\\|show-taxonomy\\|show-concepts\\|translate\\|prover\\|proof-script\\|cons-check\\|prove\\|prove-all\\)[ \t\n]"
;; axiom-selection
'("\\(\\<\\|\\s-+\\)\\(with\\|excluding\\)[ \t\n]"
;; dg-commands
'("\\(\\<\\|\\s-+\\)\\(auto\\|glob-subsume\\|glob-decomp\\|loc-infer\\|loc-decomp\\|hide-thm\\|thm-hide\\|basic\\)[ \t\n]"
))
"Reserved keywords highlighting")
;; String and Char
(list '("\\(\\(\"\\|^>[ \t]*\\\\\\)\\([^\"\\\\\n]\\|\\\\.\\)*\\(\"\\|\\\\[ \t]*$\\)\\|'\\([^'\\\\\n]\\|\\\\.[^'\n]*\\)'\\)"
))
"Syntax highlighting of String and Char")
;; Define default highlighting level
;; (defvar hpf-font-lock-syntax-highligthing hpf-font-lock-keywords
"Default syntax highlighting level in HPF mode")
;; ================= C A S L M A J O R M O D E ===============
;; hpf major mode setup
;; Definition of HPF major mode
(defun hpf-mode ()
"Major mode for editing HPF models"
(hpf-vars)
;; Load keymap
;; Load syntax table
;; (hpf-create-syntax-table)
;; Highlight HPF keywords
(setq font-lock-keywords-only nil)
;; Support for compile.el
;; We just substitute our own functions to go to the error.
)
;; HPF-mode ends here