hpf-mode.el revision b9b8f261fe6ee3907ec15372993cbfec33448c52
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder;;;###autoload
6c53458902234dee49b9cc57dfa0047aff7331adChristian Maeder;;;;;;;;;;;;;;;;;;;;;;;;;;
98890889ffb2e8f6f722b00e265a211f13b5a861Corneliu-Claudiu Prodescu;; Copyright: (c) Heng Jiang, Uni Bremen 2007
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder;; License: LGPL, see LICENSE.txt or LIZENZ.txt
3f69b6948966979163bdfe8331c38833d5d90ecdChristian Maeder;; Contact: hets-users@informatik.uni-bremen.de
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder;;;;;;;;;;;;;;;;;;;;;;;;;;
f3a94a197960e548ecd6520bb768cb0d547457bbChristian Maeder;; Version number
6c53458902234dee49b9cc57dfa0047aff7331adChristian Maeder "Version of HPF-Mode")
6c53458902234dee49b9cc57dfa0047aff7331adChristian Maeder "Major mode for editing (heterogeneous) HPF specifications."
6c53458902234dee49b9cc57dfa0047aff7331adChristian Maeder(defvar hpf-mode-map (let ((keymap (make-keymap)))
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder (define-key keymap "\C-c\C-c" 'comment-region)
6c53458902234dee49b9cc57dfa0047aff7331adChristian Maeder "Keymap for HPF major mode")
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder;; Are we running FSF Emacs or XEmacs?
9c07aad044613547d61ab235665c08adcef03a1cChristian Maeder (string-match "Lucid\\|XEmacs" emacs-version)
6c53458902234dee49b9cc57dfa0047aff7331adChristian Maeder "non-nil if we are running XEmacs, nil otherwise.")
6c53458902234dee49b9cc57dfa0047aff7331adChristian Maeder;; ====================== S Y N T A X T A B L E ==================
6c53458902234dee49b9cc57dfa0047aff7331adChristian Maeder;; Syntax table for HPF major mode
6c53458902234dee49b9cc57dfa0047aff7331adChristian Maeder "Syntax table for HPF mode.")
6c53458902234dee49b9cc57dfa0047aff7331adChristian Maeder ;; Indicate that underscore may be part of a word
54f29197f5ccf8ad5057a20d391ed8010c2215efChristian Maeder ;; Some of these are actually OK by default.
6c53458902234dee49b9cc57dfa0047aff7331adChristian Maeder "!#$&*+.,/\\\\:<=>?@^|~")
6c53458902234dee49b9cc57dfa0047aff7331adChristian Maeder ;; commenting-out plus including other kinds of comment
6c53458902234dee49b9cc57dfa0047aff7331adChristian Maeder;; Various mode variables.
92494a941714233bcd640425aa50d3cf4859d7ebChristian Maeder (setq comment-start-skip "#") ;; %[%{[]() *")
674cb6f4b91212b596fe2790bbe344f6a941a32fChristian Maeder (make-local-variable 'comment-indent-function)
6bcdf8fc684a7a2d03f41bba002cfeaa0fbe023cChristian Maeder;; ============= K E Y W O R D H I G H L I G H T I N G ============
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski(defvar hpf-black-komma-face 'hpf-black-komma-face
e935784609f5d43dc57d3000607a8b87d250a9a6Christian Maeder "Face name to use for black komma.")
2bbcdec13d8fd4b862cea292617cba1dca78f513Christian Maeder(defvar hpf-annotation-face 'hpf-annotation-face
67bdb53d077a6a0c9d22aa7b7ccf67dcf9b1a832Christian Maeder "HPF mode face for Annotations")
67bdb53d077a6a0c9d22aa7b7ccf67dcf9b1a832Christian Maeder(setq hpf-annotation-face 'font-lock-constant-face)
8973fbf8b089a81344159a3d003666db34c21a24Christian Maeder(setq hpf-name-face 'font-lock-variable-name-face)
674cb6f4b91212b596fe2790bbe344f6a941a32fChristian Maeder(setq hpf-keyword-face 'font-lock-keyword-face)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski(defvar hpf-library-name-face 'hpf-library-name-face)
2bbcdec13d8fd4b862cea292617cba1dca78f513Christian Maeder(setq hpf-library-name-face 'font-lock-type-face)
674cb6f4b91212b596fe2790bbe344f6a941a32fChristian Maeder(setq hpf-builtin-face 'font-lock-builtin-face)
8a4ac1b3637cc42735d4f85dab1e86d23a6c751bChristian Maeder(setq hpf-comment-face 'font-lock-comment-face)
8a4ac1b3637cc42735d4f85dab1e86d23a6c751bChristian Maeder(defvar hpf-other-name-face 'hpf-other-name-face)
674cb6f4b91212b596fe2790bbe344f6a941a32fChristian Maeder (setq hpf-other-name-face 'hpf-blue-komma-face)
8a4ac1b3637cc42735d4f85dab1e86d23a6c751bChristian Maeder (setq hpf-other-name-face 'font-lock-function-name-face)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski(defvar hpf-string-char-face 'hpf-string-char-face)
2bbcdec13d8fd4b862cea292617cba1dca78f513Christian Maeder(setq hpf-string-char-face 'font-lock-string-face)
8973fbf8b089a81344159a3d003666db34c21a24Christian Maeder;; Syntax highlighting of HPF
52d88f5cd371d33aee53b1f2aa5ad778411bef48Christian Maeder;; "Warning: Do not design an element of font-lock-keywords to match
674cb6f4b91212b596fe2790bbe344f6a941a32fChristian Maeder;; text which spans lines; this does not work reliably. While
52d88f5cd371d33aee53b1f2aa5ad778411bef48Christian Maeder;; font-lock-fontify-buffer handles multi-line patterns correctly,
71de4b92b1ca12890a9e7bc5b0301455da3e052fChristian Maeder;; updating when you edit the buffer does not, since it considers
522b324965f69d3c0c1a2b203a79ff4326dea7b0Christian Maeder;; text one line at a time." (from the GNU Emacs Lisp Reference Manual)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski;; order of all the following highlighting rules is significant,
8973fbf8b089a81344159a3d003666db34c21a24Christian Maeder;; ony change if really needed
52d88f5cd371d33aee53b1f2aa5ad778411bef48Christian Maeder '("#.*$" (0 (symbol-value 'hpf-comment-face) keep t)))
52d88f5cd371d33aee53b1f2aa5ad778411bef48Christian Maeder "Special Comment")
674cb6f4b91212b596fe2790bbe344f6a941a32fChristian Maeder '("\\(\\<\\|\\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]"
52d88f5cd371d33aee53b1f2aa5ad778411bef48Christian Maeder (2 (symbol-value 'hpf-keyword-face) keep t))
674cb6f4b91212b596fe2790bbe344f6a941a32fChristian Maeder ;; axiom-selection
674cb6f4b91212b596fe2790bbe344f6a941a32fChristian Maeder '("\\(\\<\\|\\s-+\\)\\(with\\|excluding\\)[ \t\n]"
674cb6f4b91212b596fe2790bbe344f6a941a32fChristian Maeder (2 (symbol-value 'hpf-keyword-face) keep t))
62198789c7cb57cac13399055515921c0fe3483fChristian Maeder ;; dg-commands
674cb6f4b91212b596fe2790bbe344f6a941a32fChristian Maeder '("\\(\\<\\|\\s-+\\)\\(auto\\|glob-subsume\\|glob-decomp\\|loc-infer\\|loc-decomp\\|hide-thm\\|thm-hide\\|basic\\)[ \t\n]"
62198789c7cb57cac13399055515921c0fe3483fChristian Maeder (2 (symbol-value 'hpf-keyword-face) keep t))
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder "Reserved keywords highlighting")
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder;; String and Char
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder (list '("\\(\\(\"\\|^>[ \t]*\\\\\\)\\([^\"\\\\\n]\\|\\\\.\\)*\\(\"\\|\\\\[ \t]*$\\)\\|'\\([^'\\\\\n]\\|\\\\.[^'\n]*\\)'\\)"
1012fdd997ea1f35eee2ccdd4015199f09f18fe9Christian Maeder (0 (symbol-value 'hpf-string-char-face) keep t))
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder "Syntax highlighting of String and Char")
674cb6f4b91212b596fe2790bbe344f6a941a32fChristian Maeder;; Define default highlighting level
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder;; (defvar hpf-font-lock-syntax-highligthing hpf-font-lock-keywords
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder(defvar hpf-font-lock-syntax-highligthing (symbol-value 'hpf-font-lock-string)
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder "Default syntax highlighting level in HPF mode")
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder;; ================= C A S L M A J O R M O D E ===============
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder;; hpf major mode setup
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder;; Definition of HPF major mode
4561227a776bdf0ab679b19fb92f1eaaed8786f7Christian Maeder "Major mode for editing HPF models"
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder ;; Load keymap
674cb6f4b91212b596fe2790bbe344f6a941a32fChristian Maeder ;; Load syntax table
feb3da029bdab54fe36ff704ca242ab4536b3bc1Christian Maeder ;; (hpf-create-syntax-table)
8973fbf8b089a81344159a3d003666db34c21a24Christian Maeder ;; Highlight HPF keywords
52d88f5cd371d33aee53b1f2aa5ad778411bef48Christian Maeder (make-local-variable 'font-lock-keywords-only)
42c01284bba8d7c8d995c8dfb96ace57d28ed1bcTill Mossakowski ;; We just substitute our own functions to go to the error.
54f29197f5ccf8ad5057a20d391ed8010c2215efChristian Maeder;; HPF-mode ends here