From fc774de804417a399094f61de1880e75b556c851 Mon Sep 17 00:00:00 2001 From: Christophe Raffalli Date: Fri, 24 Feb 2006 17:16:02 +0000 Subject: back to using sym-lock ... x-symbol will not be supported anymore for PhoX + imporvment in proof by contextual menu --- phox/phox-font.el | 40 ++++++ phox/phox-lang.el | 12 +- phox/phox-pbrpm.el | 93 ++++++------- phox/phox-sym-lock.el | 366 ++++++++++++++++++++++++++++++++++++++++++++++++++ phox/phox.el | 42 +++--- 5 files changed, 487 insertions(+), 66 deletions(-) create mode 100644 phox/phox-sym-lock.el (limited to 'phox') diff --git a/phox/phox-font.el b/phox/phox-font.el index c924e3f8..efd44420 100644 --- a/phox/phox-font.el +++ b/phox/phox-font.el @@ -53,5 +53,45 @@ "with" "\\)[ \t.]") '(0 'font-lock-type-face t)))) +;;--------------------------------------------------------------------------;; +;;--------------------------------------------------------------------------;; +;; phox-sym-lock tables +;;--------------------------------------------------------------------------;; + +(if proof-running-on-XEmacs (require 'phox-sym-lock)) + +;; to change this table, xfd -fn '-adobe-symbol-*--12-*' may be +;; used to determine the symbol character codes. +(defconst phox-sym-lock-keywords-table + '((">=" 0 1 179) + ("<=" 0 1 163) + ("!=" 0 1 185) + (":<" 0 1 206) + ("[^:]\\(:\\)[^:= \n\t\r]" 1 7 206) + ("\\\\/" 0 1 36) + ("/\\\\" 0 1 34) + ("\\" 0 3 218) + ("\\" 0 3 206) + ("\\" 0 4 207) + ("\\" 0 3 199) + ("\\" 0 3 200) + ("\\" 0 3 45) + ("&" 0 1 217) + ("<->" 0 1 171) + ("=>" 0 1 222) + ("\\" 0 4 204) + ("->" 0 1 174) + ("~" 0 1 216) + ("\\\\" 0 1 108))) +; "If non nil: Overrides default Phox-Sym-Lock patterns for PhoX.") + +(defun phox-sym-lock-start () + (if (and (featurep 'phox-sym-lock) phox-sym-lock-enabled) + (progn + (setq phox-sym-lock-color + (face-foreground 'font-lock-function-name-face)) + (if (not phox-sym-lock-keywords) + (phox-sym-lock phox-sym-lock-keywords-table))))) + (provide 'phox-font) diff --git a/phox/phox-lang.el b/phox/phox-lang.el index d8456de8..952842e5 100644 --- a/phox/phox-lang.el +++ b/phox/phox-lang.el @@ -44,12 +44,12 @@ (en (concat "Unlock variable" s ".")) (fr (concat "Dévérouille la variable " s ".")))) -(defun phox-lang-prove () +(defun phox-lang-prove (s) (case phox-lang - (en "Let us prove \\[ \\].") - (fr "Prouvons \\[ \\]."))) + (en (concat "Let us prove \\[" s "\\].")) + (fr (concat "Prouvons \\[" s "\\].")))) -(defun phox-lang-let () +(defun phox-lang-let (s) (case phox-lang - (en "Let \\[ \\] = \\[ \\].") - (fr "Définissons \\[ \\] = \\[ \\]."))) + (en (concat "Let \\[ \\] = \\[" s "\\].")) + (fr (concat "Définissons \\[ \\] = \\[" s "\\].")))) diff --git a/phox/phox-pbrpm.el b/phox/phox-pbrpm.el index 80c5f748..9c06d319 100644 --- a/phox/phox-pbrpm.el +++ b/phox/phox-pbrpm.el @@ -82,6 +82,10 @@ (defun phox-pbrpm-get-region-name (region-info) (if (= (nth 0 region-info) 1) (nth 1 region-info) (nth 2 region-info))) +(defun phox-pbrpm-escape-string (str) + "add escape char '\'" + (concat "\"" (replace-regexp-in-string "\\\\" "\\\\\\\\" str) "\"")) + (defun phox-pbrpm-generate-menu (click-infos region-infos) "Use informations to build a list of (name , rule)" ;click-infos = (goal-number, "whole"/hyp-name/"none", expression, depth-tree-list) @@ -124,7 +128,7 @@ (let ((tmp "")) (mapc (lambda (region-info) (setq tmp - (concat tmp " \"" (nth 2 region-info) "\""))) + (concat tmp " " (phox-pbrpm-escape-string (nth 2 region-info))))) region-infos) tmp))) (phox-pbrpm-menu-from-string 1 @@ -133,7 +137,7 @@ (let ((tmp "")) (mapc (lambda (region-info) (setq tmp - (concat tmp " " (phox-pbrpm-get-region-name region-info)))) + (concat tmp " " (phox-pbrpm-escape-string (phox-pbrpm-get-region-name region-info))))) region-infos) tmp)))))) @@ -141,15 +145,15 @@ (if (and (not (or (string= (nth 1 click-infos) "none") (string= (nth 1 click-infos) "whole"))) + (or (string= "" (nth 2 click-infos)) (not (char= (string-to-char (nth 2 click-infos)) ??))) (not region-infos)) (let ((r (proof-shell-invisible-cmd-get-result (concat "is_hypothesis " (int-to-string (nth 0 click-infos)) - " \"" - (nth 1 click-infos) - "\"")))) + " " + (phox-pbrpm-escape-string (nth 1 click-infos)))))) (setq pbrpm-rules-list (append pbrpm-rules-list - (if (char= (string-to-char r) ?t) + (if (char= (string-to-char r) ?t) (list (list 9 (phox-lang-suppress (nth 1 click-infos)) (concat "[" (int-to-string (nth 0 click-infos)) "] " @@ -183,7 +187,7 @@ (let ((tmp "")) (mapc (lambda (region-info) (setq tmp - (concat tmp " \"" (nth 2 region-info) "\""))) + (concat tmp " " (phox-pbrpm-escape-string (nth 2 region-info))))) region-infos) tmp))) (phox-pbrpm-menu-from-string 1 @@ -193,22 +197,35 @@ (let ((tmp "")) (mapc (lambda (region-info) (setq tmp - (concat tmp " " (phox-pbrpm-get-region-name region-info)))) + (concat tmp " " (phox-pbrpm-escape-string (phox-pbrpm-get-region-name region-info))))) region-infos) tmp)))))) + (if (and (not (string= "" (nth 2 click-infos))) (char= (string-to-char (nth 2 click-infos)) ??) + region-infos (not (cdr region-infos))) + (setq pbrpm-rules-list + (append pbrpm-rules-list + (list (list 0 (concat + (phox-lang-instance (nth 2 click-infos)) + (nth 2 (car region-infos))) + (concat + goal-prefix + "instance " + (nth 2 click-infos) + " " + (nth 2 (car region-infos)) + ". ")))))) + ; is clicking on a token with no selection (if (and (not region-infos) (not (string= (nth 2 click-infos) ""))) (let ((r (proof-shell-invisible-cmd-get-result (concat "is_definition " (int-to-string (nth 0 click-infos)) - " \"" - (nth 2 click-infos) - "\""))) + " " + (phox-pbrpm-escape-string (nth 2 click-infos))))) (ri (proof-shell-invisible-cmd-get-result (concat "is_definition " (int-to-string (nth 0 click-infos)) - " \"" - (concat "$" (nth 2 click-infos)) - "\"")))) + " " + (phox-pbrpm-escape-string (concat "$" (nth 2 click-infos))))))) (if (or (char= (string-to-char r) ?t) (char= (string-to-char ri) ?t)) (setq pbrpm-rules-list (append pbrpm-rules-list @@ -219,26 +236,12 @@ goal-prefix (if (or (string= (nth 1 click-infos) "none") (string= (nth 1 click-infos) "whole")) - "unfold " - (concat "unfold_hyp " (nth 1 click-infos) " ")) + "unfold -ortho " + (concat "unfold_hyp " (nth 1 click-infos) " -ortho ")) "$" (nth 2 click-infos) ". "))))) - (if (and (char= (string-to-char (nth 2 click-infos)) ??) - region-infos (not (cdr region-infos))) - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list (list 0 (concat - (phox-lang-instance (nth 2 click-infos)) - (nth 2 (car region-infos))) - (concat - goal-prefix - "instance " - (nth 2 click-infos) - " " - (nth 2 (car region-infos)) - ". ")))))) - (if (char= (string-to-char (nth 2 click-infos)) ??) + (if (and (not (string= "" (nth 2 click-infos))) (char= (string-to-char (nth 2 click-infos)) ??)) (let ((r (proof-shell-invisible-cmd-get-result (concat "is_locked " (nth 2 click-infos))))) (if (char= (string-to-char r) ?t) @@ -259,19 +262,19 @@ (nth 2 click-infos) ". "))))))))))) - - (setq pbrpm-rules-list - (append pbrpm-rules-list - (list - (list 10 "Trivial ?" (concat goal-prefix "trivial")) - (list 10 (phox-lang-prove) (concat goal-prefix "prove") - (lambda (cmd spans) - (let ((span (pop spans))) - (concat cmd " " (span-string span))))) - (list 10 (phox-lang-let) (concat goal-prefix "local") - (lambda (cmd spans) - (let ((span1 (pop spans)) (span2 (pop spans))) - (concat cmd " " (span-string span1) " = "(span-string span2)))))))) + (let ((arg (if (and region-infos (not (cdr region-infos))) (nth 2 (car region-infos)) " "))) + (setq pbrpm-rules-list + (append pbrpm-rules-list + (list + (list 10 "Trivial ?" (concat goal-prefix "trivial")) + (list 10 (phox-lang-prove arg) (concat goal-prefix "prove") + (lambda (cmd spans) + (let ((span (pop spans))) + (concat cmd " " (span-string span))))) + (list 10 (phox-lang-let arg) (concat goal-prefix "local") + (lambda (cmd spans) + (let ((span1 (pop spans)) (span2 (pop spans))) + (concat cmd " " (span-string span1) " = "(span-string span2))))))))) pbrpm-rules-list )) @@ -289,4 +292,4 @@ (require 'pg-pbrpm) (require 'phox-lang) (provide 'phox-pbrpm) -;; phox-pbrpm ends here \ No newline at end of file +;; phox-pbrpm ends here diff --git a/phox/phox-sym-lock.el b/phox/phox-sym-lock.el new file mode 100644 index 00000000..1c4e4cae --- /dev/null +++ b/phox/phox-sym-lock.el @@ -0,0 +1,366 @@ +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; phox-sym-lock.el - Extension of Font-Lock mode for symbol fontification. + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; Copyright © 1997-1998 Albert Cohen, all rights reserved. +;; Copying is covered by the GNU General Public License. +;; +;; This program is free software; you can redistribute it and/or modify +;; it under the terms of the GNU General Public License as published by +;; the Free Software Foundation; either version 2 of the License, or +;; (at your option) any later version. +;; +;; This program is distributed in the hope that it will be useful, +;; but WITHOUT ANY WARRANTY; without even the implied warranty of +;; MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the +;; GNU General Public License for more details. + +;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; +;; History +;; +;; first prototype by wg 5-96 +;; tweaked by Steve Dunham 5-96 +;; rewritten and enhanced by Albert Cohen 3-97 +;; new symbol-face format and ergonomy improvement by Albert Cohen 2-98 +;; major step towards portability and customization by Albert Cohen 5-98 +;; removed bug with multiple appends in hook by Albert Cohen 3-99 +;; removed phox-sym-lock-face&atom which where not working by C Raffalli 4-2000 + +;; more about symbol font ? check out: xfd -fn '-adobe-symbol-*--12-*' + +(require 'font-lock) +(require 'atomic-extents) + +(defvar phox-sym-lock-sym-count 0 + "Counter for internal symbols.") + +(defvar phox-sym-lock-ext-start nil "Temporary for atomicization.") +(make-variable-buffer-local 'phox-sym-lock-ext-start) +(defvar phox-sym-lock-ext-end nil "Temporary for atomicization.") +(make-variable-buffer-local 'phox-sym-lock-ext-end) + +(defvar phox-sym-lock-font-size nil + "Default size for Phox-Sym-Lock symbol font.") +(make-variable-buffer-local 'phox-sym-lock-font-size) +(put 'phox-sym-lock-font-size 'permanent-local t) + +(defvar phox-sym-lock-keywords nil + "Similar to `font-lock-keywords'.") +(make-variable-buffer-local 'phox-sym-lock-keywords) +(put 'phox-sym-lock-keywords 'permanent-local t) + +(defvar phox-sym-lock-enabled nil + "Phox-Sym-Lock switch.") +(make-variable-buffer-local 'phox-sym-lock-enabled) +(put 'phox-sym-lock-enabled 'permanent-local t) + +(defvar phox-sym-lock-color (face-foreground 'default) + "*Phox-Sym-Lock default color in `font-lock-use-colors' mode.") +(make-variable-buffer-local 'phox-sym-lock-color) +(put 'phox-sym-lock-color 'permanent-local t) + +(defvar phox-sym-lock-mouse-face 'default + "*Face for symbols when under mouse.") +(make-variable-buffer-local 'phox-sym-lock-mouse-face) +(put 'phox-sym-lock-mouse-face 'permanent-local t) + +(defvar phox-sym-lock-mouse-face-enabled t + "Mouse face switch.") +(make-variable-buffer-local 'phox-sym-lock-mouse-face-enabled) +(put 'phox-sym-lock-mouse-face-enabled 'permanent-local t) + +(defconst phox-sym-lock-with-mule (featurep 'mule) + "Are we using Mule Xemacs ?") + +(defun phox-sym-lock-gen-symbol (&optional prefix) + "Generate a new internal symbol." + ;; where is the standard function to do this ? + (setq phox-sym-lock-sym-count (+ phox-sym-lock-sym-count 1)) + (intern (concat "phox-sym-lock-gen-" (or prefix "") + (int-to-string phox-sym-lock-sym-count)))) + + +(defun phox-sym-lock-make-symbols-atomic (&optional begin end) + "Function to make symbol faces atomic." + (if phox-sym-lock-enabled + (map-extents + (lambda (extent maparg) + (let ((face (extent-face extent)) (ext)) + (if (and face (setq ext (face-property face 'phox-sym-lock-remap))) + (progn + (if (numberp ext) + (set-extent-endpoints + extent (- (extent-start-position extent) ext) + (extent-end-position extent))) + (if ext + (progn + (if phox-sym-lock-mouse-face-enabled + (set-extent-property extent 'mouse-face + phox-sym-lock-mouse-face)) + (set-extent-property extent 'atomic t) + (set-extent-property extent 'start-open t)))))) + nil) + (current-buffer) + (if begin (save-excursion (goto-char begin) (beginning-of-line) (point)) + (point-min)) + (if end (save-excursion (goto-char end) (end-of-line) (point)) + (point-max)) + nil nil))) + +(defun phox-sym-lock-compute-font-size () + "Computes the size of the \"better\" symbol font." + (let ((font-reg (if proof-running-on-win32 + "[^:]*:[^:]*:\\([^:]*\\):[^:]*:[^:]*" + "-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-[^-]*-\\([^-]*\\)-.*")) + (font-pat (if proof-running-on-win32 + "Symbol:Regular:*::Symbol" + "-adobe-symbol-medium-r-normal--*"))) + (let ( +; face-height is not very good on win32. Why ? + (num (if (and (not proof-running-on-win32) (fboundp 'face-height)) + (face-height 'default) + (let ((str (face-font-name 'default))) + (if + (string-match font-reg str) + (string-to-number (substring str (match-beginning 1) + (match-end 1))))))) + (maxsize 100) (size) (oldsize) + (lf (list-fonts font-pat))) + (while (and lf maxsize) + (if + (string-match font-reg + (car lf)) + (let ((str-size (substring (car lf) (match-beginning 1) + (match-end 1)))) + ; test for variable size fonts. Hope it is generic ? + (if (or (equal str-size "*")(equal str-size "")) + (progn + (setq oldsize num) + (setq lf nil)) + (setq size (string-to-number str-size)) + (if (and (> size num) (< size maxsize)) + (setq lf nil) + (setq oldsize size))))) + (setq lf (cdr lf))) + (number-to-string (if (and oldsize (< oldsize maxsize)) oldsize num))))) + +(defvar phox-sym-lock-font-name + (if window-system + (if proof-running-on-win32 + (concat "Symbol:Regular:" + (if phox-sym-lock-font-size phox-sym-lock-font-size + (phox-sym-lock-compute-font-size)) + "::Symbol") + (concat "-adobe-symbol-medium-r-normal--" + (if phox-sym-lock-font-size phox-sym-lock-font-size + (phox-sym-lock-compute-font-size)) + "-*-*-*-p-*-adobe-fontspecific")) + "") + "Name of the font used by Phox-Sym-Lock.") +(make-variable-buffer-local 'phox-sym-lock-font-name) +(put 'phox-sym-lock-font-name 'permanent-local t) + +(make-face 'phox-sym-lock-adobe-symbol-face) +(if phox-sym-lock-with-mule + (progn + (make-charset 'phox-sym-lock-cset-left "Char set for symbol font" + (list 'registry "adobe-fontspecific" + 'dimension 1 + 'chars 94 + 'final 53 + 'graphic 0)) + (make-charset 'phox-sym-lock-cset-right "Char set for symbol font" + (list 'registry "adobe-fontspecific" + 'dimension 1 + 'chars 94 + 'final 54 + 'graphic 1)) + (set-face-property 'phox-sym-lock-adobe-symbol-face + 'font phox-sym-lock-font-name nil + ;; DA: removed next line, it breaks "make magic" in doc + ;; '(mule-fonts) 'prepend, + )) + (set-face-font 'phox-sym-lock-adobe-symbol-face phox-sym-lock-font-name 'global)) + +(defun phox-sym-lock-set-foreground () + "Set foreground color of Phox-Sym-Lock faces." + (if (and (boundp 'phox-sym-lock-defaults) phox-sym-lock-defaults) + (let ((l (car phox-sym-lock-defaults)) + (color (if (and (boundp 'font-lock-use-fonts) font-lock-use-fonts) + (face-foreground 'default) phox-sym-lock-color))) + (if (and (consp l) (eq (car l) 'quote)) (setq l (eval l))) + (if (symbolp l) (setq l (eval l))) + (dolist (c l) + (setq c (nth 2 c)) + (if (consp c) (setq c (eval c))) + (if (string-match "-adobe-symbol-" (font-name (face-font c))) + (set-face-foreground c color)))))) + +(defun phox-sym-lock-translate-char (char) + (if phox-sym-lock-with-mule + (let ((code (if (integerp char) char (char-int char)))) + (if (< code 128) + (make-char 'phox-sym-lock-cset-left obj) + (make-char 'phox-sym-lock-cset-right (- obj 128)))) + char)) + +(defun phox-sym-lock-translate-char-or-string (obj) + (if (stringp obj) + (if phox-sym-lock-with-mule + (concat (mapcar phox-sym-lock-translate-char obj)) + (obj)) + (make-string 1 (phox-sym-lock-translate-char obj)))) + +(defun phox-sym-lock-remap-face (pat pos obj atomic) + "Make a temporary face which remaps the POS char of PAT to the +given OBJ under `phox-sym-lock-adobe-symbol-face' and all other characters to +the empty string. OBJ may either be a string or a character." + (let* ((name (phox-sym-lock-gen-symbol "face")) + (table (make-display-table)) + (tface (make-face name "phox-sym-lock-remap-face" t))) + (fillarray table "") + (aset table (string-to-char (substring pat (1- pos) pos)) + (phox-sym-lock-translate-char-or-string obj)) + (set-face-foreground tface (if (and (boundp 'font-lock-use-fonts) + font-lock-use-fonts) + (face-foreground 'default) phox-sym-lock-color)) + (set-face-property tface 'display-table table) + (set-face-property tface 'font (face-font 'phox-sym-lock-adobe-symbol-face)) + (set-face-property tface 'phox-sym-lock-remap atomic) ; mark it + tface ; return face value and not face name + ; the temporary face would be otherwise GCed + )) + +(defvar phox-sym-lock-clear-face + (let* ((name (phox-sym-lock-gen-symbol "face")) + (table (make-display-table)) + (tface (make-face name "phox-sym-lock-remap-face" t))) + (fillarray table "") + (set-face-property tface 'display-table table) + (set-face-property tface 'phox-sym-lock-remap 1) ; mark it + tface + ;; return face value and not face name + ;; the temporary face would be otherwise GCed + )) + +(defun phox-sym-lock (fl) + "Create font-lock table entries from a list of (PAT NUM POS OBJ) where +PAT (at NUM) is substituted by OBJ under `phox-sym-lock-adobe-symbol-face'. The +face's extent will become atomic." + (message "Computing Phox-Sym-Lock faces...") + (setq phox-sym-lock-keywords (phox-sym-lock-rec fl)) + (setq phox-sym-lock-enabled t) + (message "Computing Phox-Sym-Lock faces... done.")) + +(defun phox-sym-lock-rec (fl) + (let ((f (car fl))) + (if f + (cons (apply 'phox-sym-lock-atom-face f) + (phox-sym-lock-rec (cdr fl)))))) + +(defun phox-sym-lock-atom-face (pat num pos obj &optional override) + "Define an entry for the font-lock table which substitutes PAT (at NUM) by +OBJ under `phox-sym-lock-adobe-symbol-face'. The face extent will become atomic." + (list pat num (phox-sym-lock-remap-face pat pos obj t) override)) + +(defun phox-sym-lock-pre-idle-hook-first () + (condition-case nil + (if (and phox-sym-lock-enabled font-lock-old-extent) + (setq phox-sym-lock-ext-start (extent-start-position font-lock-old-extent) + phox-sym-lock-ext-end (extent-end-position font-lock-old-extent)) + (setq phox-sym-lock-ext-start nil)) + (error (setq phox-sym-lock-ext-start nil)))) + +(defun phox-sym-lock-pre-idle-hook-last () + (condition-case nil + (if (and phox-sym-lock-enabled phox-sym-lock-ext-start) + (phox-sym-lock-make-symbols-atomic phox-sym-lock-ext-start phox-sym-lock-ext-end)) + (error (warn "Error caught in `phox-sym-lock-pre-idle-hook-last'")))) + +(add-hook 'font-lock-after-fontify-buffer-hook + 'phox-sym-lock-make-symbols-atomic) + +(defun phox-sym-lock-enable () + "Enable Phox-Sym-Lock on this buffer." + (interactive) + (if (not phox-sym-lock-keywords) + (error "No Phox-Sym-Lock keywords defined!") + (setq phox-sym-lock-enabled t) + (if font-lock-mode + (progn +; (setq font-lock-keywords nil) ; Font-Lock explicit-defaults bug! + (font-lock-set-defaults t) + (font-lock-fontify-buffer))) + (message "Phox-Sym-Lock enabled."))) + +(defun phox-sym-lock-disable () + "Disable Phox-Sym-Lock on this buffer." + (interactive) + (if (not phox-sym-lock-keywords) + (error "No Phox-Sym-Lock keywords defined!") + (setq phox-sym-lock-enabled nil) + (if font-lock-mode + (progn +; (setq font-lock-keywords nil) ; Font-Lock explicit-defaults bug! + (font-lock-set-defaults t) + (font-lock-fontify-buffer))) + (message "Phox-Sym-Lock disabled."))) + +(defun phox-sym-lock-mouse-face-enable () + "Enable special face for symbols under mouse." + (interactive) + (setq phox-sym-lock-mouse-face-enabled t) + (if phox-sym-lock-enabled + (font-lock-fontify-buffer))) + +(defun phox-sym-lock-mouse-face-disable () + "Disable special face for symbols under mouse." + (interactive) + (setq phox-sym-lock-mouse-face-enabled nil) + (if phox-sym-lock-enabled + (font-lock-fontify-buffer))) + +(defun phox-sym-lock-font-lock-hook () + "Function called by `font-lock-mode' for initialization purposes." + (add-hook 'pre-idle-hook 'phox-sym-lock-pre-idle-hook-first) + (add-hook 'pre-idle-hook 'phox-sym-lock-pre-idle-hook-last t) + (add-menu-button '("Options" "Syntax Highlighting") + ["Phox-Sym-Lock" + (if phox-sym-lock-enabled (phox-sym-lock-disable) (phox-sym-lock-enable)) + :style toggle :selected phox-sym-lock-enabled + :active phox-sym-lock-keywords] "Automatic") + (if (and (featurep 'phox-sym-lock) phox-sym-lock-enabled + font-lock-defaults (boundp 'phox-sym-lock-keywords)) + (progn + (phox-sym-lock-patch-keywords) + (phox-sym-lock-set-foreground)))) + +(defun font-lock-set-defaults (&optional explicit-defaults) + (when + (and + (featurep 'font-lock) + (if font-lock-auto-fontify + (not (memq major-mode font-lock-mode-disable-list)) + (memq major-mode font-lock-mode-enable-list)) + (font-lock-set-defaults-1 explicit-defaults) + (phox-sym-lock-patch-keywords)) + (turn-on-font-lock))) + +(defun phox-sym-lock-patch-keywords () + (if (and font-lock-keywords phox-sym-lock-enabled + (boundp 'phox-sym-lock-keywords) + (listp (car font-lock-keywords)) + (listp (cdar font-lock-keywords)) + (listp (cddar font-lock-keywords)) + (or (listp (caddar font-lock-keywords)) + (not (string-match + "phox-sym-lock" + (symbol-name + (face-name (cadr (cdar + font-lock-keywords)))))))) + (setq font-lock-keywords (append phox-sym-lock-keywords + font-lock-keywords))) t) + +(add-hook 'font-lock-mode-hook 'phox-sym-lock-font-lock-hook) + +(provide 'phox-sym-lock) diff --git a/phox/phox.el b/phox/phox.el index fa25363a..2c51e434 100644 --- a/phox/phox.el +++ b/phox/phox.el @@ -33,13 +33,10 @@ :type 'file :group 'phox) -; da: I commented this out, it should be defined automatically -; in proof-config.el. If you want to change the default to t, -; then perhaps: (custom-set-default phox-x-symbol-enable t) -;(defcustom phox-x-symbol-enable t -; "*Whether to use x-symbol or not." -; :type 'boolean -; :group 'phox) +(defcustom phox-sym-lock-enabled t + "*Whether to use x-symbol or not." + :type 'boolean + :group 'phox) (defcustom phox-web-page @@ -109,6 +106,10 @@ (defun phox-config () "Configure Proof General scripting for PhoX." + (if phox-sym-lock-enabled + (progn + (phox-sym-lock-start) + (setq phox-x-symbol-enable nil))) (setq proof-terminal-char ?\. ; ends every command proof-script-command-end-regexp "[.]\\([ \t\n\r]\\)" @@ -161,7 +162,7 @@ proof-shell-quit-cmd "quit." proof-shell-restart-cmd "restart." proof-shell-proof-completed-regexp "^.*^proved" -)) + )) ;; @@ -185,12 +186,12 @@ ;; it is nice to do : xmodmap -e "keysym KP_Enter = Linefeed" (define-key phox-mode-map [(control c) (meta d)] - 'phox-delete-symbol-on-cursor) - (if phox-x-symbol-enable - (progn - (setq x-symbol-language 'phox) - (x-symbol-mode t))) ; just to be sure - (font-lock-mode t) ; just to be sure (not always activated on OSX ?? + 'phox-delete-symbol-on-cursor) + ;(if phox-x-symbol-enable +; (progn + ; (setq x-symbol-language 'phox) + ; (x-symbol-mode t))) ; just to be sure +; (font-lock-mode t) ; just to be sure (not always activated on OSX ??) ) @@ -204,15 +205,26 @@ (setq font-lock-keywords (append phox-font-lock-keywords proof-xsym-font-lock-keywords) proof-output-fontify-enable t) + (phox-sym-lock-start) + (if (and (featurep 'phox-sym-lock) phox-sym-lock-enabled) + (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 "PhoX goals" nil (setq - font-lock-keywords (append phox-font-lock-keywords proof-xsym-font-lock-keywords) + font-lock-keywords (append phox-font-lock-keywords proof-xsym-font-lock-keywords) proof-output-fontify-enable t) + (phox-sym-lock-start) + (if (and (featurep 'phox-sym-lock) phox-sym-lock-enabled) + (add-hook 'pg-before-fontify-output-hook + 'phox-sym-lock-font-lock-hook) + ) (proof-goals-config-done)) + ;; The response buffer and goals buffer modes defined above are ;; trivial. In fact, we don't need t²o define them at all -- they ;; would simply default to "proof-response-mode" and "pg-goals-mode". -- cgit v1.2.3