diff options
| -rw-r--r-- | generic/proof-syntax.el | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el index 5caa8fe3..1d454523 100644 --- a/generic/proof-syntax.el +++ b/generic/proof-syntax.el @@ -2,6 +2,9 @@ ;; Copyright (C) 1997-1998 LFCS Edinburgh. ;; Author: Healfdene Goguen, Thomas Kleymann and Dilip Sequiera ;; Maintainer: LEGO Team <lego@dcs.ed.ac.uk> +;; +;; $Id$ +;; (require 'font-lock) @@ -34,6 +37,9 @@ ;; font lock faces: declarations, errors, tacticals ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; FIXME 1: these names are bad, should be proof-<blah>-face. +;; FIXME 2: use defface here + (defun proof-have-color () ()) @@ -71,6 +77,7 @@ ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; ;; A big hack to unfontify commas in declarations and definitions. ;; +;; Useful for provers which have declarations of the form x,y,z:Ty ;; ;; All that can be said for it is that the previous way of doing ;; ;; this was even more bogus. ;; ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; |