;;;###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")))
""
"Face name to use for black komma.")
"HPF mode face for Annotations")
)
;; 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\\|begin-script\\|end-script\\)[ \t\n]"
;; axiom-selection
'("\\(\\<\\|\\s-+\\)\\(with\\|excluding\\)\\s-+\\(.*\\)[ \t\n]"
;; dg-commands GOALs
'("\\(\\dg\\|dg-all\\)\\s-+\\(auto\\|glob-subsume\\|glob-decomp\\|loc-infer\\|loc-decomp\\|hide-thm\\|thm-hide\\|basic\\)\\s-+\\(\\w+\\)?\\(->\\([0-9]+\\)\\)?\\(->\\(\\w+\\)\\)?[ \t\n]"
))
"Reserved keywords highlighting")
(list
;; use PATH
'("\\(\\<\\|\\s-+\\)use\\s-+\\(.*\\)$"
;; goal
;; See dg-commands
;; COMORPHISM
'("\\(\\<\\|\\s-+\\)translate\\s-+\\(.*\\)$"
;; PROVER
'("\\(\\<\\|\\s-+\\)\\(prover\\|cons-check\\)\\s-+\\(.*\\)$"
;; Formula
'("\\(\\<\\|\\s-+\\)\\(prove\\|prove-all\\)\\s-+\\(\\(\\w\\|\\s-\\)*\\)\\s-+\\(with\\|exlcuding\\|$\\)"
)))
;; 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