diff options
Diffstat (limited to 'tools/coq-font-lock.el')
| -rw-r--r-- | tools/coq-font-lock.el | 137 |
1 files changed, 137 insertions, 0 deletions
diff --git a/tools/coq-font-lock.el b/tools/coq-font-lock.el new file mode 100644 index 00000000..05618a04 --- /dev/null +++ b/tools/coq-font-lock.el @@ -0,0 +1,137 @@ +;; coq-font-lock.el --- Coq syntax highlighting for Emacs - compatibilty code +;; Pierre Courtieu, may 2009 +;; +;; Authors: Pierre Courtieu +;; License: GPL (GNU GENERAL PUBLIC LICENSE) +;; Maintainer: Pierre Courtieu <Pierre.Courtieu@cnam.fr> + +;; This is copy paste from ProofGeneral by David Aspinall +;; <David.Aspinall@ed.ac.uk>. ProofGeneral is under GPL and Copyright +;; (C) LFCS Edinburgh. + + +;;; Commentary: +;; This file contains the code necessary to coq-syntax.el and +;; coq-db.el from ProofGeneral. It is also pocked from ProofGeneral. + + +;;; History: +;; First created from ProofGeneral may 28th 2009 + + +;;; Code: + +(setq coq-version-is-V8-1 t) +(defun coq-build-regexp-list-from-db (db &optional filter) + "Take a keyword database DB and return the list of regexps for font-lock. +If non-nil Optional argument FILTER is a function applying to each line of DB. +For each line if FILTER returns nil, then the keyword is not added to the +regexp. See `coq-syntax-db' for DB structure." + (let ((l db) (res ())) + (while l + (let* ((hd (car l)) (tl (cdr l)) ; hd is the first infos list + (e1 (car hd)) (tl1 (cdr hd)) ; e1 = menu entry + (e2 (car tl1)) (tl2 (cdr tl1)) ; e2 = abbreviation + (e3 (car tl2)) (tl3 (cdr tl2)) ; e3 = completion + (e4 (car-safe tl3)) (tl4 (cdr-safe tl3)) ; e4 = state changing + (e5 (car-safe tl4)) (tl5 (cdr-safe tl4)) ; e5 = colorization string + ) + ;; TODO delete doublons + (when (and e5 (or (not filter) (funcall filter hd))) + (setq res (nconc res (list e5)))) ; careful: nconc destructive! + (setq l tl))) + res + )) +(defun filter-state-preserving (l) + ; checkdoc-params: (l) + "Not documented." + (not (nth 3 l))) ; fourth argument is nil --> state preserving command + +(defun filter-state-changing (l) + ; checkdoc-params: (l) + "Not documented." + (nth 3 l)) ; fourth argument is nil --> state preserving command + +;; Generic font-lock + +(defvar proof-id "\\(\\w\\(\\w\\|\\s_\\)*\\)" + "A regular expression for parsing identifiers.") + +;; For font-lock, we treat ,-separated identifiers as one identifier +;; and refontify commata using \{proof-zap-commas}. + +(defun proof-anchor-regexp (e) + "Anchor (\\`) and group the regexp E." + (concat "\\`\\(" e "\\)")) + +(defun proof-ids (proof-id &optional sepregexp) + "Generate a regular expression for separated lists of identifiers PROOF-ID. +Default is comma separated, or SEPREGEXP if set." + (concat proof-id "\\(\\s-*" (or sepregexp ",") "\\s-*" + proof-id "\\)*")) + +(defun proof-ids-to-regexp (l) + "Maps a non-empty list of tokens `L' to a regexp matching any element." + (if (featurep 'xemacs) + (mapconcat (lambda (s) (concat "\\_<" s "\\_>")) l "\\|") ;; old version + (concat "\\_<\\(?:" (mapconcat 'identity l "\\|") "\\)\\_>"))) + +;; TODO: get rid of this list. Does 'default work widely enough +;; by now? +(defconst pg-defface-window-systems + '(x ;; bog standard + mswindows ;; Windows + w32 ;; Windows + gtk ;; gtk emacs (obsolete?) + mac ;; used by Aquamacs + carbon ;; used by Carbon XEmacs + ns ;; NeXTstep Emacs (Emacs.app) + x-toolkit) ;; possible catch all (but probably not) + "A list of possible values for variable `window-system'. +If you are on a window system and your value of variable +`window-system' is not listed here, you may not get the correct +syntax colouring behaviour.") + +(defmacro proof-face-specs (bl bd ow) + "Return a spec for `defface' with BL for light bg, BD for dark, OW o/w." + `(append + (apply 'append + (mapcar + (lambda (ty) (list + (list (list (list 'type ty) '(class color) + (list 'background 'light)) + (quote ,bl)) + (list (list (list 'type ty) '(class color) + (list 'background 'dark)) + (quote ,bd)))) + pg-defface-window-systems)) + (list (list t (quote ,ow))))) + +;;A new face for tactics +(defface coq-solve-tactics-face + (proof-face-specs + (:foreground "forestgreen" t) ; pour les fonds clairs + (:foreground "forestgreen" t) ; pour les fond foncés + ()) ; pour le noir et blanc + "Face for names of closing tactics in proof scripts." + :group 'proof-faces) + +;;A new face for tactics which fail when they don't kill the current goal +(defface coq-solve-tactics-face + (proof-face-specs + (:foreground "red" t) ; pour les fonds clairs + (:foreground "red" t) ; pour les fond foncés + ()) ; pour le noir et blanc + "Face for names of closing tactics in proof scripts." + :group 'proof-faces) + + +(defconst coq-solve-tactics-face 'coq-solve-tactics-face + "Expression that evaluates to a face. +Required so that 'proof-solve-tactics-face is a proper facename") + +(defconst proof-tactics-name-face 'coq-solve-tactics-face) +(defconst proof-tacticals-name-face 'coq-solve-tactics-face) + +(provide 'coq-font-lock) +;;; coq-font-lock.el ends here |