From b7109ce9e307830a271808f04e24d3c4d79b1665 Mon Sep 17 00:00:00 2001 From: Christophe Raffalli Date: Wed, 20 Oct 2004 13:18:30 +0000 Subject: improvment of phox-x-symbol, supress sym-lock, first support for proof by contextual menu --- phox/README.pbrpm | 26 ++++ phox/phox-font.el | 40 ------ phox/phox-pbrpm.el | 279 ++++++++++++++++++++++++++++++++++++++ phox/phox-sym-lock.el | 366 -------------------------------------------------- phox/phox.el | 35 +---- phox/x-symbol-phox.el | 21 +-- 6 files changed, 324 insertions(+), 443 deletions(-) create mode 100644 phox/README.pbrpm create mode 100644 phox/phox-pbrpm.el delete mode 100644 phox/phox-sym-lock.el (limited to 'phox') diff --git a/phox/README.pbrpm b/phox/README.pbrpm new file mode 100644 index 00000000..c0c7bc1b --- /dev/null +++ b/phox/README.pbrpm @@ -0,0 +1,26 @@ +**** +Projet PhoX : Proof By Rules Popup Menu (PBRPM) +***** + +----- +Fichiers concernés : + ProofGeneral/generic/pg-goals.el + ProofGeneral/generic/pg-pbrpm.el + ProofGeneral/phox/phox.el + ProofGeneral/phox/phox-pbrpm.el + + +- Dans pg-goals.el - +(l. 58-59) + inclusion de pg-pbrpm.el + déclaration du 'CTRL + Click Droit' associé à pg-pbrpm-button-action (dans pg-pbrpm.el) + +- Dans pg-pbrpm.el - + Fonctions indépendantes de PhoX implémentant le PBRPM. + +- Dans phox.el - +(l. 86) inclus phox-pbrpm.el +(l. 103-104) ajoute le menu de gestion du buffer de selections dans le menu de PhoX + +- Dans phox-pbrpm.el - + Fonctions spécifiques à PhoX. \ No newline at end of file diff --git a/phox/phox-font.el b/phox/phox-font.el index 3c313990..c924e3f8 100644 --- a/phox/phox-font.el +++ b/phox/phox-font.el @@ -54,44 +54,4 @@ "\\)[ \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) - (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-pbrpm.el b/phox/phox-pbrpm.el new file mode 100644 index 00000000..de9ee603 --- /dev/null +++ b/phox/phox-pbrpm.el @@ -0,0 +1,279 @@ +;; $State$ $Date$ $Revision$ +;;--------------------------------------------------------------------------;; +;;--------------------------------------------------------------------------;; +;; the proof by rules popup menu part +;; +;; Note : program extraction is still experimental This file is very +;; dependant of the actual state of our developments +;;--------------------------------------------------------------------------;; + +;;--------------------------------------------------------------------------;; +;; Syntactic functions +;;--------------------------------------------------------------------------;; +(defun phox-pbrpm-regexps () + (setq + goal-backward-regexp "^goal [0-9]+/[0-9]+$" + goal-number-regexp "[0-9]+" + hyp-backward-regexp "[^A-Za-z0-9_.']\\([A-Za-z0-9_.']+\\) :=" + ccl-backward-regexp "|-") +) + +; TODO : deal with future invisible parentheses (french guillemots) +(defun phox-pbrpm-left-paren-p (char) +"Retrun t if the character is a left parenthesis : '(' or a french guillemot '<<'" + (or + (char-equal char (int-char 40)) + (char-equal char (int-char 171))) +) + +(defun phox-pbrpm-right-paren-p (char) +"Retrun t if the character is a right parenthesis ')' or a french guillemot '>>'" + (or + (char-equal char (int-char 41)) + (char-equal char (int-char 187))) +) + +;;--------------------------------------------------------------------------;; +;; Testing Menu +;;--------------------------------------------------------------------------;; + +(defun phox-pbrpm-generate-menu (click-infos region-infos) +; This FAKE function will be replace by a real 'generate-menu' once the code will be judged stable + +"Use informations to build a list of (name , rule)" + ;click-infos = (goal-number, "whole"/hyp-name/"none", expression, depth-tree-list) + ;region-infos = idem if in the goal buffer, (0, "none", expression, nil ) if in another buffer, do not display if no region available. + + (setq pbrpm-rules-list (list)) + + ; the first goal is the selected one by default, so we prefer not to display it. + + ; if clicking in a conclusion => select.intro + (if (and (string= (nth 1 click-infos) "none") (not region-infos)) + (setq pbrpm-rules-list + (append pbrpm-rules-list + (list + (list "Décompose" + (if (= (nth 0 click-infos) 1) + (identity "intro. ") + (concat "select " (int-to-string (nth 0 click-infos)) ". intro. "))) + (list "Décompose plusieurs" + (if (= (nth 0 click-infos) 1) + (identity "intros. ") + (concat "select " (int-to-string (nth 0 click-infos)) ". intros. "))) + );end list's + ); end append + );end setq + );end if + + ; if clicking in an hypothesis => select.elim + (if (and + (not (or (string= (nth 1 click-infos) "none") + (string= (nth 1 click-infos) "whole"))) + (not region-infos)) + (progn + (setq pbrpm-rules-list + (append pbrpm-rules-list + (list (list "Produit la conclusion" + (if (= (nth 0 click-infos) 1) + (concat "elim " + (nth 1 click-infos) + ". ") + (concat "select " + (int-to-string (nth 0 click-infos)) + ". elim " + (nth 1 click-infos) + ". ")))))) + (setq pbrpm-rules-list + (append pbrpm-rules-list + (list (list "QED" + (if (= (nth 0 click-infos) 1) + (concat "axiom " + (nth 1 click-infos) + ". ") + (concat "select " + (int-to-string (nth 0 click-infos)) + ". axiom " + (nth 1 click-infos) + ". ")))))))) + + ; if clicking in an hypothesis => select.left + (if (and + (not (or (string= (nth 1 click-infos) "none") + (string= (nth 1 click-infos) "whole"))) + (not region-infos)) + (setq pbrpm-rules-list + (append pbrpm-rules-list + (list (list "Décompose" + (if (= (nth 0 click-infos) 1) + (concat "left " + (nth 1 click-infos) + ". ") + (concat "select " + (int-to-string (nth 0 click-infos)) + ". left" + (nth 1 click-infos) + ". ") + )) + (list "Décompose plusieurs" + (if (= (nth 0 click-infos) 1) + (concat "lefts " + (nth 1 click-infos) + ". ") + (concat "select " + (int-to-string (nth 0 click-infos)) + ". lefts" + (nth 1 click-infos) + ". ") + )))))) + + + ; if region is an hypothesis (ie in the goals buffer) and clicking in that hyp's goal => + (if region-infos + (if (and + (not (or (string= (nth 1 region-infos) "none") + (string= (nth 1 region-infos) "whole"))) + (equal (nth 0 click-infos) (nth 0 region-infos)) + ) + (setq pbrpm-rules-list + (append pbrpm-rules-list + (list (list "Réécrit la conclusion" + (if (= (nth 0 click-infos) 1) + (concat "rewrite " + (nth 1 region-infos) + ". ") + (concat "select " + (int-to-string (nth 0 click-infos)) + ". rewrite " + (nth 1 region-infos) + ". "))))))) + ) + + (if (and + (not (or (string= (nth 1 click-infos) "none") + (string= (nth 1 click-infos) "whole"))) + (not (string= (nth 2 region-infos) "")) + ) + (setq pbrpm-rules-list + (append pbrpm-rules-list + (list (list "Applique l'hypothèse à une expression" + (if (= (nth 0 click-infos) 1) + (concat "apply " + (nth 1 click-infos) + " with " + (nth 2 region-infos) + ". ") + (concat "select " + (int-to-string (nth 0 click-infos)) + ". select " + (nth 1 click-infos) + " with " + (nth 2 region-infos) + ". "))))))) + + ; if region is an hypothesis (ie in the goals buffer) and clicking in an (other) hyp', both in the same goal => + (if region-infos + (if (and + (not (or (string= (nth 1 click-infos) "none") + (string= (nth 1 click-infos) "whole"))) + (not (or (string= (nth 1 region-infos) "none") + (string= (nth 1 region-infos) "whole"))) + (equal (nth 0 click-infos) (nth 0 region-infos)) + (not (string= (nth 1 click-infos) (nth 1 region-infos))) + ) + (progn + (setq pbrpm-rules-list + (append pbrpm-rules-list + (list (list "Réécrit l'hypothèse" + (if (= (nth 0 click-infos) 1) + (concat "rewrite_hyp " + (nth 1 click-infos) + " " + (nth 1 region-infos) + ". ") + (concat "select " + (int-to-string (nth 0 click-infos)) + ". rewrite_hyp " + (nth 1 click-infos) + " " + (nth 1 region-infos) + ". ")))))) + (setq pbrpm-rules-list + (append pbrpm-rules-list + (list (list "Applique l'hypothèse à une autre hypothèse" + (if (= (nth 0 click-infos) 1) + (concat "apply " + (nth 1 click-infos) + " with " + (nth 1 region-infos) + ". ") + (concat "select " + (int-to-string (nth 0 click-infos)) + ". select " + (nth 1 click-infos) + " with " + (nth 1 region-infos) + ". ")))))))) + + ) + + (identity pbrpm-rules-list) +) + + +;;--------------------------------------------------------------------------;; +;; Selections Buffer management -- unused for now +;;--------------------------------------------------------------------------;; +;initialize the selections buffer for the PBRPM mode +;1 buffer for every selections +(display-buffer (generate-new-buffer (generate-new-buffer-name "phox-selections"))) + +;copy the current region in the selections buffer +(defun pg-pbrpm-add-selection () +"Append the selection of the current buffer to +the phox-selections buffer used with PBRPM." + (interactive) + ;TODO : check wether the selected region is a well formed expression + ;copy at the end of the selections buffer before switching to it + ; else we'll loose mark & point + (switch-to-buffer (get-buffer "phox-selections")) + (goto-char (point-max)) + (insert-string (get-selection)) + ; if the selected region already ends with a \n, don't insert a second one + (if (not (bolp)) + (insert-string "\n")) + (insert-string "\n") + ;buffer is ready to receive a new selection +) + + +;clean the phox-selections buffer +(defun pg-pbrpm-clean-selections-buffer () +"Clean the phox-selections buffer used with PBRPM." + (interactive) + (erase-buffer (get-buffer "phox-selections")) +) + +;selections management menu +(defvar phox-pbrpm-menu +"Phox menu for dealing with Selections." + '("Selections" + ["Add Selection" pg-pbrpm-add-selection ] + ["Clean Selections buffer" pg-pbrpm-clean-selections-buffer ] + ) +) ;see phox.el > menu-entries + + +;;--------------------------------------------------------------------------;; +;; phox specific functions +;;--------------------------------------------------------------------------;; + +(defalias 'proof-pbrpm-generate-menu 'phox-pbrpm-generate-menu) +(defalias 'proof-pbrpm-left-paren-p 'phox-pbrpm-left-paren-p) +(defalias 'proof-pbrpm-right-paren-p 'phox-pbrpm-right-paren-p) +(defalias 'proof-pbrpm-regexps 'phox-pbrpm-regexps) + +;;--------------------------------------------------------------------------;; +(require 'pg-pbrpm) +(provide 'phox-pbrpm) +;; phox-pbrpm ends here \ No newline at end of file diff --git a/phox/phox-sym-lock.el b/phox/phox-sym-lock.el deleted file mode 100644 index 668f6e8e..00000000 --- a/phox/phox-sym-lock.el +++ /dev/null @@ -1,366 +0,0 @@ -;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; -;; 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) -(proof-try-require 'atomic-extents) ;; da: proof-try-require for Emacs compat - -(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 b0b57f3e..d5e726e3 100644 --- a/phox/phox.el +++ b/phox/phox.el @@ -1,6 +1,7 @@ ;; $State$ $Date$ $Revision$ (require 'proof) ; load generic parts +(require 'proof-config) ;; Adjust toolbar entries. (Must be done ;; before proof-toolbar is loaded). @@ -32,11 +33,6 @@ :type 'file :group 'phox) -(defcustom phox-sym-lock nil - "*Whether to use sym-lock or not (should disappear soon)." - :type 'boolean - :group 'phox) - (defcustom phox-x-symbol-enable t "*Whether to use x-symbol or not." :type 'boolean @@ -83,6 +79,7 @@ (require 'phox-extraction) (require 'phox-tags) (require 'phox-outline) +(require 'phox-pbrpm) ;; default for tags [da: moved here to fix compilation 15/02/03] @@ -99,11 +96,13 @@ phox-tags-menu (cons phox-extraction-menu + (cons + phox-pbrpm-menu ;; not useful ? ; '(["Delete symbol around cursor" phox-delete-symbol-around-point t] ; ["Delete symbol" phox-delete-symbol t]) - nil))) - ) + nil)))) +) ;; ;; ======== Configuration of generic modes ======== @@ -194,7 +193,6 @@ (define-derived-mode phox-mode proof-mode "PhoX script" nil (phox-config) - (phox-sym-lock-start) (proof-config-done) (phox-setup-outline) (define-key phox-mode-map [(control j)] @@ -216,11 +214,6 @@ (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) - (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 @@ -228,10 +221,6 @@ (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) - (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 @@ -271,18 +260,6 @@ ;;; X-Symbol ;;; -(let ((xsymbol (getenv "PROOFGENERAL_XSYMBOL")) - (enable-var (if (equal (getenv "PROOFGENERAL_ASSISTANTS") "phox") - 'phox-x-symbol-enable))) - - ;; avoid confusing warning message - (if (not (boundp 'x-symbol-image-converter)) - (customize-set-variable 'x-symbol-image-converter nil)) - - ;; tell Proof General about -x option - (if (and xsymbol (not (equal xsymbol ""))) - (customize-set-variable enable-var (equal xsymbol "true")))) - (defpgdefault x-symbol-language 'phox) (eval-after-load "x-symbol-phox" diff --git a/phox/x-symbol-phox.el b/phox/x-symbol-phox.el index 38f98a71..84f7d7d1 100644 --- a/phox/x-symbol-phox.el +++ b/phox/x-symbol-phox.el @@ -21,8 +21,10 @@ ;; it would be handy to be able to use this file away from PG. ;; FIXME: In future could fix things so just ;; (require 'proof-x-symbol) would be enough here. -(defvar x-symbol-phox-name "PhoX Symbol") -(defvar x-symbol-phox-modeline-name "phox") +(require 'proof-x-symbol) +;(defvar x-symbol-phox-name "phox") +;(defvar x-symbol-phox-modeline-name "phox") + (defcustom x-symbol-phox-header-groups-alist nil "*If non-nil, used in isasym specific grid/menu. @@ -31,8 +33,8 @@ See `x-symbol-header-groups-alist'." :group 'x-symbol-input-init :type 'x-symbol-headers) -(defcustom x-symbol-phox-electric-ignore nil -;; "[:'][A-Za-z]\\|<=\\|\\[\\[\\|\\]\\]\\|~=" +(defcustom x-symbol-phox-electric-ignore + "/\\\\\\|\\\\/" "*Additional Phox version of `x-symbol-electric-ignore'." :group 'x-symbol-phox :group 'x-symbol-input-control @@ -51,10 +53,12 @@ See `x-symbol-header-groups-alist'." (x-symbol-make-grammar :encode-spec '(((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]")) . ((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]"))) - :decode-spec nil + :decode-spec '(((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]")) . + ((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]"))) :decode-regexp "\\([_'a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)" :token-list #'x-symbol-phox-default-token-list - :input-spec nil))) + :input-spec '(((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]")) . + ((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]")))))) (defvar x-symbol-phox-input-token-grammar '("\\([_'a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)" @@ -160,8 +164,9 @@ See `x-symbol-language-access-alist' for details." (defun x-symbol-phox-prepare-table (table) "Prepar the table." (mapcar (lambda (entry) - (list (car entry) nil - (cadr entry))) + (progn + (list (car entry) nil + (cadr entry)))) table)) (defvar x-symbol-phox-table -- cgit v1.2.3