1 files changed, 9 insertions, 38 deletions
diff --git a/phox/phox.el b/phox/phox.el
index 7f54c5a8..1f8c2ef1 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -7,7 +7,7 @@
 
 (eval-after-load "pg-custom"
   '(setq phox-toolbar-entries
-    (remassoc 'context phox-toolbar-entries)))
+    (assq-delete-all 'context phox-toolbar-entries)))
 
 
 ;; ======== User settings for PhoX ========
@@ -34,7 +34,7 @@
   :group 'phox)
 
 (defcustom phox-sym-lock-enabled t
-  "*Whether to use x-symbol or not."
+  "*Whether to use yum symbol or not."
   :type 'boolean
   :group 'phox)
 
@@ -107,9 +107,7 @@
 (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)))
+      (phox-sym-lock-start))
   (setq
    proof-terminal-char		?\.	; ends every command
    proof-script-command-end-regexp "[.]\\([ \t\n\r]\\)"
@@ -145,10 +143,7 @@
    )
   (phox-init-syntax-table)
   (setq pbp-goal-command "intro %s;")
-  (setq pbp-hyp-command "elim %s;")
-;; the following is only useful for xemacs
-  (define-key phox-mode-map [(meta ?.)] 'phox-complete-tag)
-)
+  (setq pbp-hyp-command "elim %s;"))
 
 (defun phox-shell-config ()
   "Configure Proof General shell for PhoX."
@@ -189,14 +184,7 @@
     ;; 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))
 
 (define-derived-mode phox-shell-mode proof-shell-mode
    "PhoX shell" nil
@@ -206,7 +194,8 @@
 (define-derived-mode phox-response-mode proof-response-mode
   "PhoX response" nil
   (setq 
-   font-lock-keywords (append phox-font-lock-keywords proof-xsym-font-lock-keywords)
+   proof-resp-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)
@@ -218,7 +207,8 @@
 (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)
+   proof-goals-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)
@@ -244,25 +234,6 @@
   (append phox-top-keywords phox-proof-keywords)
 )
 
-;;;
-;;; X-Symbol
-;;;
-
-(defpgdefault x-symbol-language 'phox)
-
-(eval-after-load "x-symbol-phox"
- ;; Add x-symbol tokens to phox-completion-table and rebuild
- ;; internal completion table if completion is already active
-'(progn
-   (defpgdefault completion-table
-     (append phox-completion-table
-	     (mapcar (lambda (xsym) (nth 2 xsym))
-		     x-symbol-phox-table)))
-   (setq proof-xsym-font-lock-keywords
-	 x-symbol-phox-font-lock-keywords)
-   (if (featurep 'completion)
-       (proof-add-completions))))
-
 (provide 'phox)