b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;;;###autoload
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;;;;;;;;;;;;;;;;;;;;;;;;;;
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; Copyright: (c) Heng Jiang, Uni Bremen 2007
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; License: LGPL, see LICENSE.txt or LIZENZ.txt
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; Contact: hets-users@informatik.uni-bremen.de
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;;;;;;;;;;;;;;;;;;;;;;;;;;
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; Version number
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang "Version of HPF-Mode")
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang "Major mode for editing (heterogeneous) HPF specifications."
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang(defvar hpf-mode-map (let ((keymap (make-keymap)))
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang "Keymap for HPF major mode")
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; Are we running FSF Emacs or XEmacs?
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang "non-nil if we are running XEmacs, nil otherwise.")
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; ====================== S Y N T A X T A B L E ==================
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; Syntax table for HPF major mode
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang "Syntax table for HPF mode.")
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang ;; Indicate that underscore may be part of a word
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang ;; Some of these are actually OK by default.
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang "!#$&*+.,/\\\\:<=>?@^|~")
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang ;; commenting-out plus including other kinds of comment
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; Various mode variables.
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; ============= K E Y W O R D H I G H L I G H T I N G ============
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang(defvar hpf-black-komma-face 'hpf-black-komma-face
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang "Face name to use for black komma.")
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang "HPF mode face for Annotations")
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang(setq hpf-annotation-face 'font-lock-constant-face)
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang(setq hpf-name-face 'font-lock-variable-name-face)
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang(defvar hpf-library-name-face 'hpf-library-name-face)
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang (setq hpf-other-name-face 'font-lock-function-name-face)
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang(defvar hpf-string-char-face 'hpf-string-char-face)
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang(setq hpf-string-char-face 'font-lock-string-face)
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; Syntax highlighting of HPF
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; "Warning: Do not design an element of font-lock-keywords to match
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; text which spans lines; this does not work reliably. While
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; font-lock-fontify-buffer handles multi-line patterns correctly,
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; updating when you edit the buffer does not, since it considers
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; text one line at a time." (from the GNU Emacs Lisp Reference Manual)
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; order of all the following highlighting rules is significant,
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; ony change if really needed
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang '("#.*$" (0 (symbol-value 'hpf-comment-face) keep t)))
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang "Special Comment")
6cad57c376847a1caa42dbc691dbfa705e410af6Heng Jiang '("[,;.]" (0 (symbol-value 'casl-black-komma-face) t t))
6cad57c376847a1caa42dbc691dbfa705e410af6Heng Jiang '("\\(\\<\\|\\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]"
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang ;; axiom-selection
6cad57c376847a1caa42dbc691dbfa705e410af6Heng Jiang '("\\(\\<\\|\\s-+\\)\\(with\\|excluding\\)\\s-+\\(.*\\)[ \t\n]"
6cad57c376847a1caa42dbc691dbfa705e410af6Heng Jiang ;; dg-commands GOALs
6cad57c376847a1caa42dbc691dbfa705e410af6Heng Jiang '("\\(\\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]"
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang "Reserved keywords highlighting")
6cad57c376847a1caa42dbc691dbfa705e410af6Heng Jiang '("\\(\\<\\|\\s-+\\)use\\s-+\\(.*\\)$"
6cad57c376847a1caa42dbc691dbfa705e410af6Heng Jiang (2 (symbol-value 'hpf-library-name-face) keep t))
6cad57c376847a1caa42dbc691dbfa705e410af6Heng Jiang ;; See dg-commands
6cad57c376847a1caa42dbc691dbfa705e410af6Heng Jiang ;; COMORPHISM
6cad57c376847a1caa42dbc691dbfa705e410af6Heng Jiang '("\\(\\<\\|\\s-+\\)translate\\s-+\\(.*\\)$"
6cad57c376847a1caa42dbc691dbfa705e410af6Heng Jiang '("\\(\\<\\|\\s-+\\)\\(prover\\|cons-check\\)\\s-+\\(.*\\)$"
6cad57c376847a1caa42dbc691dbfa705e410af6Heng Jiang '("\\(\\<\\|\\s-+\\)\\(prove\\|prove-all\\)\\s-+\\(\\(\\w\\|\\s-\\)*\\)\\s-+\\(with\\|exlcuding\\|$\\)"
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; String and Char
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang (list '("\\(\\(\"\\|^>[ \t]*\\\\\\)\\([^\"\\\\\n]\\|\\\\.\\)*\\(\"\\|\\\\[ \t]*$\\)\\|'\\([^'\\\\\n]\\|\\\\.[^'\n]*\\)'\\)"
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang "Syntax highlighting of String and Char")
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; Define default highlighting level
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; (defvar hpf-font-lock-syntax-highligthing hpf-font-lock-keywords
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang(defvar hpf-font-lock-syntax-highligthing (symbol-value 'hpf-font-lock-string)
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang "Default syntax highlighting level in HPF mode")
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; ================= C A S L M A J O R M O D E ===============
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; hpf major mode setup
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; Definition of HPF major mode
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang "Major mode for editing HPF models"
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang ;; Load keymap
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang ;; Load syntax table
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang ;; (hpf-create-syntax-table)
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang ;; Highlight HPF keywords
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang ;; Support for compile.el
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang ;; We just substitute our own functions to go to the error.
b9b8f261fe6ee3907ec15372993cbfec33448c52Heng Jiang;; HPF-mode ends here