diff options
author | David Aspinall <da@inf.ed.ac.uk> | 1998-09-03 13:51:41 +0000 |
---|---|---|
committer | David Aspinall <da@inf.ed.ac.uk> | 1998-09-03 13:51:41 +0000 |
commit | 8b836f84d70fcea59ffa186f6809ebc6765b8a5f (patch) | |
tree | 8dc74b560cadf3b6e847e547776ccd0015dfa7f1 /generic/proof-syntax.el | |
parent | abbe57d8b69d79e9eb6899f182379d9c6c4fdc7f (diff) |
Renamed for new subdirectory structure
Diffstat (limited to 'generic/proof-syntax.el')
-rw-r--r-- | generic/proof-syntax.el | 104 |
1 files changed, 104 insertions, 0 deletions
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el new file mode 100644 index 00000000..5caa8fe3 --- /dev/null +++ b/generic/proof-syntax.el @@ -0,0 +1,104 @@ +;; proof-syntax.el Generic font lock expressions +;; Copyright (C) 1997-1998 LFCS Edinburgh. +;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequiera +;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> + +(require 'font-lock) + +;;; FIXME: change this to proof- +(defun ids-to-regexp (l) + "transforms a non-empty list of identifiers `l' into a regular + expression matching any of its elements" + (mapconcat (lambda (s) (concat "\\<" s "\\>")) l "\\|")) + +;; Generic font-lock + +;; proof-commands-regexp is used for indentation +(defvar proof-commands-regexp "" + "Subset of keywords and tacticals which are terminated by the + `proof-terminal-char'") + + +(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-unfontify-separator}. + +(defun proof-ids (proof-id) + "Function to generate a regular expression for separated lists of + identifiers." + (concat proof-id "\\(\\s-*,\\s-*" proof-id "\\)*")) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; font lock faces: declarations, errors, tacticals ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +(defun proof-have-color () + ()) + +(defvar font-lock-declaration-name-face +(progn + (cond + ((proof-have-color) + (copy-face 'bold 'font-lock-declaration-name-face) + + ;; Emacs 19.28 compiles this down to + ;; internal-set-face-1. This is not compatible with XEmacs + (set-face-foreground + 'font-lock-declaration-name-face "chocolate")) + (t (copy-face 'bold-italic 'font-lock-declaration-name-face))))) + +;; (if running-emacs19 +;; (setq font-lock-declaration-name-face +;; (face-name 'font-lock-declaration-name-face)) + +(defvar font-lock-tacticals-name-face +(if (proof-have-color) + (let ((face (make-face 'font-lock-tacticals-name-face))) + (dont-compile + (set-face-foreground face "MediumOrchid3")) + face) + (copy-face 'bold 'font-lock-tacticals-name-face))) + +(defvar font-lock-error-face +(if (proof-have-color) + (let ((face (make-face 'font-lock-error-face))) + (dont-compile + (set-face-foreground face "red")) + face) + (copy-face 'bold 'font-lock-error-face))) + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; A big hack to unfontify commas in declarations and definitions. ;; +;; All that can be said for it is that the previous way of doing ;; +;; this was even more bogus. ;; +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; + +;; Refontify the whole line, 'cos that's what font-lock-after-change +;; does. + +(defun proof-zap-commas-region (start end length) + (save-excursion + (let + ((start (progn (goto-char start) (beginning-of-line) (point))) + (end (progn (goto-char end) (end-of-line) (point)))) + (goto-char start) + (while (search-forward "," end t) + (if (memq (get-char-property (- (point) 1) 'face) + '(font-lock-declaration-name-face + font-lock-function-name-face)) + (font-lock-remove-face (- (point) 1) (point)) + ))))) + +(defun proof-zap-commas-buffer () + (proof-zap-commas-region (point-min) (point-max) 0)) + +(defun proof-unfontify-separator () + (make-local-variable 'after-change-functions) + (setq after-change-functions + (append (delq 'proof-zap-commas-region after-change-functions) + '(proof-zap-commas-region)))) + + +(provide 'proof-syntax) |