;;;###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
(defconst hpf-mode-version "0.1"
  "Version of HPF-Mode")

(defgroup hpf nil
  "Major mode for editing (heterogeneous) HPF specifications."
  :group 'languages
  :prefix "hpf-")

(defvar hpf-mode-hook nil)
(defvar hpf-mode-map (let ((keymap (make-keymap)))
			(define-key keymap "\C-c\C-c" 'comment-region)
			keymap) 
  "Keymap for HPF major mode")

;; Are we running FSF Emacs or XEmacs?
(defvar hpf-running-xemacs
  (string-match "Lucid\\|XEmacs" emacs-version)
  "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.")

(if hpf-mode-syntax-table
    ()
  (let ((table (make-syntax-table)))
    ;; Indicate that underscore may be part of a word
    (modify-syntax-entry ?_ "w" table)
    (modify-syntax-entry ?\t " " table)
    (modify-syntax-entry ?\" "\"" table)
    (modify-syntax-entry ?\' "\'" table)

    (mapcar (lambda (x)
	      (modify-syntax-entry x "_" table))
	    ;; Some of these are actually OK by default.
	    "!#$&*+.,/\\\\:<=>?@^|~")
    ;; commenting-out plus including other kinds of comment
    (setq hpf-mode-syntax-table table))
  )

;; Various mode variables.
(defun hpf-vars ()
  (kill-all-local-variables)
  (make-local-variable 'comment-start)
  (setq comment-start "#")
  (make-local-variable 'comment-padding)
  (setq comment-padding 0)
  (make-local-variable 'comment-start-skip)
  (setq comment-start-skip "#")      ;; %[%{[]() *")
  (make-local-variable 'comment-column)
  (setq comment-column 40)
  (make-local-variable 'comment-indent-function)
)

;; ============= K E Y W O R D   H I G H L I G H T I N G ============
(defface hpf-black-komma-face
  `((t (:foreground "black")))
  ""
  :group 'basic-faces)

(defface hpf-blue-komma-face
  `((t (:foreground "blue")))
  ""
  :group 'basic-faces)

(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")
(setq hpf-annotation-face 'font-lock-constant-face)

(defvar hpf-name-face 'hpf-name-face)
(setq hpf-name-face 'font-lock-variable-name-face)

(defvar hpf-keyword-face 'hpf-keyword-face)
(setq hpf-keyword-face 'font-lock-keyword-face)

(defvar hpf-library-name-face 'hpf-library-name-face)
(setq hpf-library-name-face 'font-lock-type-face)

(defvar hpf-builtin-face 'hpf-builtin-face)
(setq hpf-builtin-face 'font-lock-builtin-face)

(defvar hpf-comment-face 'hpf-comment-face)
(setq hpf-comment-face 'font-lock-comment-face)

(defvar hpf-other-name-face 'hpf-other-name-face)
(if (featurep 'xemacs)
    (setq hpf-other-name-face 'hpf-blue-komma-face)
  (setq hpf-other-name-face 'font-lock-function-name-face)
)

(defvar hpf-string-char-face 'hpf-string-char-face)
(setq hpf-string-char-face 'font-lock-string-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
(defconst hpf-font-lock-specialcomment
	 (list    
	  '("#.*$" (0 (symbol-value 'hpf-comment-face) keep t)))
	 "Special Comment")

(defconst hpf-font-lock-keywords
  (append hpf-font-lock-specialcomment
   (list
   '("[,;.]" (0 (symbol-value 'casl-black-komma-face) t t))
   ;; 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]"
       (2 (symbol-value 'hpf-keyword-face) keep t))
   ;; axiom-selection
   '("\\(\\<\\|\\s-+\\)\\(with\\|excluding\\)\\s-+\\(.*\\)[ \t\n]"  
     (2 (symbol-value 'hpf-keyword-face) keep t))
   ;; 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]"  
     (2 (symbol-value 'hpf-keyword-face) keep t)
     (3 (symbol-value 'hpf-other-name-face) keep t)
     (5 (symbol-value 'hpf-other-name-face) keep t)
     (7 (symbol-value 'hpf-other-name-face) keep t))
   ))	
   "Reserved keywords highlighting")

(defconst hpf-font-lock-idname
  (append hpf-font-lock-keywords
   (list
   ;; use PATH
   '("\\(\\<\\|\\s-+\\)use\\s-+\\(.*\\)$"  
     (2 (symbol-value 'hpf-library-name-face) keep t))
   ;; goal
   ;; See dg-commands
   ;; COMORPHISM
   '("\\(\\<\\|\\s-+\\)translate\\s-+\\(.*\\)$"  
     (2 (symbol-value 'hpf-other-name-face) keep t))
   ;; PROVER
   '("\\(\\<\\|\\s-+\\)\\(prover\\|cons-check\\)\\s-+\\(.*\\)$"  
     (3 (symbol-value 'hpf-builtin-face) keep t))
   ;; Formula
   '("\\(\\<\\|\\s-+\\)\\(prove\\|prove-all\\)\\s-+\\(\\(\\w\\|\\s-\\)*\\)\\s-+\\(with\\|exlcuding\\|$\\)"  
     (3 (symbol-value 'hpf-other-name-face) keep t))
   ))) 

;; String and Char
(defconst hpf-font-lock-string
  (append hpf-font-lock-idname
	  (list '("\\(\\(\"\\|^>[ \t]*\\\\\\)\\([^\"\\\\\n]\\|\\\\.\\)*\\(\"\\|\\\\[ \t]*$\\)\\|'\\([^'\\\\\n]\\|\\\\.[^'\n]*\\)'\\)" 
		  (0 (symbol-value 'hpf-string-char-face) keep t))
	  ))
  "Syntax highlighting of String and Char") 

;; Define default highlighting level
;; (defvar hpf-font-lock-syntax-highligthing hpf-font-lock-keywords
(defvar hpf-font-lock-syntax-highligthing (symbol-value 'hpf-font-lock-string)
  "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"
  (interactive)
  (hpf-vars)
  (setq major-mode 'hpf-mode)
  (setq mode-name "HPF")
  ;; Load keymap
  (use-local-map hpf-mode-map)
  ;; Load syntax table
  (set-syntax-table hpf-mode-syntax-table)
  ;; (hpf-create-syntax-table)
  ;; Highlight HPF keywords
  (make-local-variable 'font-lock-defaults)
  (setq font-lock-defaults
	'(hpf-font-lock-syntax-highligthing))
  (make-local-variable 'font-lock-keywords-only)
  (setq font-lock-keywords-only nil)
  ;; Support for compile.el
  ;; We just substitute our own functions to go to the error.
  (run-hooks 'hpf-mode-hook)
  )
(provide 'hpf-mode)

;; HPF-mode ends here