diff options
| -rw-r--r-- | Makefile.devel | 1 | ||||
| -rw-r--r-- | generic/proof-config.el | 6 | ||||
| -rw-r--r-- | generic/proof-utils.el | 3 | ||||
| -rw-r--r-- | phox/phox-font.el | 5 | ||||
| -rw-r--r-- | phox/phox.el | 2 | ||||
| -rw-r--r-- | phox/x-symbol-phox.el | 7 |
6 files changed, 22 insertions, 2 deletions
diff --git a/Makefile.devel b/Makefile.devel index 722585fa..fb8ffec6 100644 --- a/Makefile.devel +++ b/Makefile.devel @@ -107,6 +107,7 @@ FULLVERSION=$(VERSION) # NB: CVS tags can't have points in them. # Substitute points for hyphens. CVS_VERSION=$(shell echo $(FULLVERSION) | sed 's/\./-/g') +NOCVS=yes # Name of tar file and RPM file. RELEASENAME = $(NAME)-$(VERSION) diff --git a/generic/proof-config.el b/generic/proof-config.el index bdee9eac..df76244c 100644 --- a/generic/proof-config.el +++ b/generic/proof-config.el @@ -2055,6 +2055,12 @@ toolbar." :type '(repeat function) :group 'proof-shell) +(defcustom proof-before-fontify-output-hook nil + "This hook is called before fonfitying a region in an output buffer. +This hook is mainly used by phox-sym-lock." + :type '(repeat function) + :group 'proof-shell) + (defcustom proof-shell-font-lock-keywords nil "Value of font-lock-keywords used to fontify the proof shell. This is currently used only by proof-easy-config mechanism, diff --git a/generic/proof-utils.el b/generic/proof-utils.el index 44604fe9..4b825adf 100644 --- a/generic/proof-utils.el +++ b/generic/proof-utils.el @@ -392,7 +392,8 @@ Returns new END value." (set-marker font-lock-cache-position 0))) ;; ================================================ - (font-lock-default-fontify-region start end nil) + (run-hooks 'proof-before-fontify-output-hook) + (font-lock-default-fontify-region start end) (proof-zap-commas-region start end)))) (if proof-shell-leave-annotations-in-output ;; Remove special characters that were used for font lock, diff --git a/phox/phox-font.el b/phox/phox-font.el index 49e9d0ed..da677764 100644 --- a/phox/phox-font.el +++ b/phox/phox-font.el @@ -68,9 +68,14 @@ ("\\\\/" 0 1 36) ("/\\\\" 0 1 34) ("\\<or\\>" 0 3 218) + ("\\<in\\>" 0 3 206) + ("\\<inter\\>" 0 3 199) + ("\\<union\\>" 0 3 200) + ("\\<minus\\>" 0 3 45) ("&" 0 1 217) ("<->" 0 1 171) ("=>" 0 1 222) + ("\\<subset\\>" 0 4 204) ("->" 0 1 174) ("~" 0 1 216) ("\\\\" 0 1 108))) diff --git a/phox/phox.el b/phox/phox.el index eb5295d8..88396b5b 100644 --- a/phox/phox.el +++ b/phox/phox.el @@ -206,6 +206,7 @@ font-lock-keywords phox-font-lock-keywords proof-output-fontify-enable t) (phox-sym-lock-start) + (add-hook 'proof-shell-handle-delayed-output-hook 'phox-sym-lock-font-lock-hook) (proof-response-config-done)) (define-derived-mode phox-goals-mode proof-goals-mode @@ -214,6 +215,7 @@ font-lock-keywords phox-font-lock-keywords proof-output-fontify-enable t) (phox-sym-lock-start) + (add-hook 'proof-before-fontify-output-hook 'phox-sym-lock-font-lock-hook) (proof-goals-config-done)) ;; The response buffer and goals buffer modes defined above are diff --git a/phox/x-symbol-phox.el b/phox/x-symbol-phox.el index 26e2f1f6..e67d8774 100644 --- a/phox/x-symbol-phox.el +++ b/phox/x-symbol-phox.el @@ -59,7 +59,12 @@ '((greaterequal () ">=") (lessequal () "<=") (notequal () "!=") - (element () ":") + (element () "in") + (notelement () "notin") + (propersubset () "<<") + (intersection () "inter") + (union () "union") + (backslash3 () "minus") (universal1 () "/\\") (existential1 () "\\/") (logicalor () "or") |