;; This file is not part of GNU Emacs.

;; GNU Emacs is free software; you can redistribute it and/or modify
;; it under the terms of the GNU General Public License as published by
;; the Free Software Foundation; either version 2, or (at your option)
;; any later version.

;; GNU Emacs is distributed in the hope that it will be useful,
;; but WITHOUT ANY WARRANTY; without even the implied warranty of
;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
;; GNU General Public License for more details.

;; You should have received a copy of the GNU General Public License
;; along with GNU Emacs; see the file COPYING.  If not, write to the
;; Free Software Foundation, Inc., 59 Temple Place - Suite 330,
;; Boston, MA 02111-1307, USA.
;;

;;; Install:
;;
;;  (require ‘minlog-mode)

;;; Usage:
;;
;;  A new minor mode minlog-mode is defined. You can toggle
;;  it by calling minlog-mode.

;;; Code:

(require ‘easy-mmode)

(defgroup minlog nil
  "Minlog minor mode"
  :group ‘tools)

(defgroup minlog-faces nil
  "Minlog minor mode faces"
  :group ‘minlog)

(defface minlog-all-face
  ‘((((class color)) (:weight bold :foreground "yellow" :height 150)))
  "Face for the all quantifier"
  :group ‘minlog-faces)

(defface minlog-ex-face
  ‘((((class color)) (:weight bold :foreground "yellow")))
  "Face for minlog ex quantifier"
  :group ‘minlog-faces)

(defface minlog-allnc-face
  ‘((((class color)) (:weight bold :foreground "yellow")))
  "Face for the allnc quantifier"
  :group ‘minlog-faces)

(defface minlog-exnc-face
  ‘((((class color)) (:weight bold :foreground "yellow")))
  "Face for minlog exnc quantifier"
  :group ‘minlog-faces)

(defface minlog-type-arrow-face
  ‘((((class color)) (:foreground "orange")))
  "Face for => arrow in types"
  :group ‘minlog-faces)

(defface minlog-implication-arrow-face
  ‘((((class color)) (:foreground "orange")))
  "Face for -> arrow in types"
  :group ‘minlog-faces)

(defface minlog-variable-id-face
  ‘((((class color)) (:foreground "blue")))
  "Face for variable identifiers"
  :group ‘minlog-faces)

(defface minlog-type-id-face
  ‘((((class color)) (:foreground "yellow")))
  "Face for type identifiers"
  :group ‘minlog-faces)

;(makunbound ‘minlog-keywords)
(setq minlog-parse-prefix "\\(?:([\s\t]*p[ytf]\\|parse-\\(?:type\\|formula\\|term\\)\\)[\s\t]+\"[^\"]*")
(setq minlog-parse-postfix ""); [^\"]*\"")
(defun in-parse ( regexp ) (concat minlog-parse-prefix regexp minlog-parse-postfix))
(defvar minlog-keywords
  `(
    (,(in-parse "\\b\\([a-zA-Z]+\\(?:_?[0-9]+\\)?\\)\\b") (1 ‘minlog-variable-id-face t))
    (,(in-parse "\\b\\(nat\\|rat\\|real\\|pos\\|int\\)\\b") (1 ‘minlog-type-id-face t))
    (,(in-parse "\\(=>\\)") (1 ‘minlog-type-arrow-face t))
    (,(in-parse "\\(->\\)") (1 ‘minlog-implication-arrow-face t))
    (,(in-parse "\\b\\(all\\)\\b") (1 ‘minlog-all-face t))
    (,(in-parse "\\b\\(ex\\)\\b") (1 ‘minlog-ex-face t))
    (,(in-parse "\\b\\(allnc\\)\\b") (1 ‘minlog-allnc-face t))
    (,(in-parse "\\b\\(exnc\\)\\b") (1 ‘minlog-exnc-face t))
    )
  "Faces to highlight minlog formulas" )

(easy-mmode-define-minor-mode
 minlog-mode
 "Highlight minlog formulas"
 nil
 " Minlog")

(defun minlog-mode-on ()
  (font-lock-add-keywords nil minlog-keywords)
  (when font-lock-fontified (font-lock-fontify-buffer)))

(defun minlog-mode-off ()
            (font-lock-remove-keywords nil minlog-keywords)
            (when font-lock-fontified (font-lock-fontify-buffer)))

(add-hook ‘minlog-mode-on-hook ‘minlog-mode-on)
(add-hook ‘minlog-mode-off-hook ‘minlog-mode-off)

(provide ‘minlog-mode)