;; lego-fontlock.el Font lock expressions for LEGO
;; Copyright (C) 1994, 1995, 1996, 1997 LFCS Edinburgh. 
;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequeira
;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk>

;; $Log$
;; Revision 1.3  1997/11/26 14:11:29  tms
;; simplified code:
;;   lego-goal-with-hole-regexp and lego-save-with-hole-regexp is now
;;   used for lego-font-lock-keywords-1 as well
;;
;; Revision 1.2  1997/10/13 17:13:14  tms
;; *** empty log message ***
;;
;; Revision 1.1.2.2  1997/10/08 08:22:31  hhg
;; Updated undo, fixed bugs, more modularization
;;
;; Revision 1.1.2.1  1997/10/07 13:34:23  hhg
;; New structure to share as much as possible between LEGO and Coq.
;;
;;


(require 'proof-fontlock)

;; ----- keywords for font-lock.

(defvar lego-keywords-goal '("$?Goal"))

(defvar lego-keywords-save '("$?Save" "SaveFrozen" "SaveUnfrozen"))

(defvar lego-keywords
  (append lego-keywords-goal lego-keywords-save
	  '("allE" "allI" "andE" "andI" "Assumption" "Claim"
  "Constructors" "Cut" "Discharge" "DischargeKeep"
    "Double" "echo" "ElimOver" "exE" "exI" "Expand" "ExpAll"
    "ExportState" "Equiv" "Fields" "Freeze" "From" "Hnf" "Immed"
    "impE" "impI" "Import" "Induction" "Inductive" "Inversion" "Init"
    "intros" "Intros" "Module" "Next" "NoReductions" "Normal" "notE"
    "notI" "orE" "orIL" "orIR" "Parameters" "Qnify" "Qrepl" "Record"
    "Refine" "Relation" "Theorems" "Unfreeze")))

(defvar lego-tacticals '("Then" "Else" "Try" "Repeat" "For"))

;; ----- regular expressions for font-lock
(defvar lego-error-regexp "^\\(Error\\|Lego parser\\)"
  "A regular expression indicating that the LEGO process has
  identified an error.") 

(defvar lego-id proof-id)

(defvar lego-ids (concat lego-id "\\(\\s *,\\s *" lego-id "\\)*")
  "*For font-lock, we treat \",\" separated identifiers as one identifier
  and refontify commata using \\{lego-fixup-change}.")

(defun lego-decl-defn-regexp (char)
    (concat "\\[\\s *\\(" lego-ids
 "\\)\\s *\\(\\[[^]]+\\]\\s *\\)*" char))
; Examples
;              ^        ^^^^        ^^^^^^^^^^^^^^^^^^^^^^^  ^^^^
;              [        sort                                 =
;              [        sort        [n:nat]                  =
;              [        sort        [abbrev=...][n:nat]      =

(defvar lego-font-lock-terms
  (list

   ; lambda binders
     (list (lego-decl-defn-regexp "[:|]") 1
	   'font-lock-declaration-name-face)

     ; let binders
     (list (lego-decl-defn-regexp "=") 1 'font-lock-function-name-face)

     ; Pi and Sigma binders
     (list (concat "[{<]\\s *\\(" lego-ids "\\)") 1
	   'font-lock-declaration-name-face)
   
     ;; Kinds
     (cons (concat "\\<Prop\\>\\|\\<Type\\s *\\(("
		   lego-id ")\\)?") 'font-lock-type-face))
  "*Font-lock table for LEGO terms.")

;; Instead of "[^:]+", it may be better to use "lego-id". Furthermore,
;; it might be safer to append "\\s-*:".
(defconst lego-goal-with-hole-regexp
  (concat "\\(" (ids-to-regexp lego-keywords-goal) "\\)\\s-+\\([^:]+\\)")
  "Regular expression which matches an entry in `lego-keywords-goal'
  and the name of the goal.") 

(defconst lego-save-with-hole-regexp
  (concat "\\(" (ids-to-regexp lego-keywords-save) "\\)\\s-+\\([^;]+\\)")
  "Regular expression which matches an entry in
  `lego-keywords-save' and the name of the goal.")

(defvar lego-font-lock-keywords-1
   (append
    lego-font-lock-terms
    (list
     (cons (ids-to-regexp lego-keywords) 'font-lock-keyword-face)
     (cons (ids-to-regexp lego-tacticals) 'font-lock-tacticals-name-face)
     (list lego-goal-with-hole-regexp 2 'font-lock-function-name-face)
     (list lego-save-with-hole-regexp 2 'font-lock-function-name-face))))
     
(provide 'lego-fontlock)