improvment of phox-x-symbol, supress sym-lock, first support for proof by contextual menu

6 files changed, 324 insertions, 443 deletions

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)
-    ("\\<or\\>" 0 3 218) 
-    ("\\<in\\>" 0 3 206) 
-    ("\\<notin\\>" 0 4 207) 
-    ("\\<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)))
-;  "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 <wg@cs.tu-berlin.de> 5-96
-;; tweaked by Steve Dunham <dunham@gdl.msu.edu> 5-96
-;; rewritten and enhanced by Albert Cohen <Albert.Cohen@prism.uvsq.fr> 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