Merge changes from Version4Branch.

3 files changed, 29 insertions, 314 deletions

diff --git a/phox/phox-tags.el b/phox/phox-tags.el
index c62fe331..4851eb8c 100644
--- a/phox/phox-tags.el
+++ b/phox/phox-tags.el
@@ -21,29 +21,15 @@
 (defun phox-tags-add-table(table)
   "add tags table"
   (interactive "D directory, location of a file named TAGS to add : ")
-  (if (featurep 'xemacs)
-      (let ((association (cons buffer-file-name table)))
-	(if (member association tag-table-alist)
-	    (message "%s already loaded." table)
-	  (setq tag-table-alist (cons association tag-table-alist))))
-					; gnu emacs
-    (if (member table tags-table-list)
-	(message "%s already loaded." table)
-;    (make-local-variable 'tags-table-list) ; ne fonctionne pas
-      (setq tags-table-list (cons table tags-table-list))
-      )
-    )
-  )
+  (if (member table tags-table-list)
+      (message "%s already loaded." table)
+    ;; (make-local-variable 'tags-table-list) ; ne fonctionne pas
+    (setq tags-table-list (cons table tags-table-list))))
 
 (defun phox-tags-reset-table()
   "Set tags-table-list to nil."
   (interactive)
-;  (make-local-variable 'tags-table-list)
-  (if (featurep 'xemacs)
-      (progn
-	(setq tag-table-alist (remassoc buffer-file-name tag-table-alist)))
-    (setq tags-table-list nil))
-  )
+  (setq tags-table-list nil))
 
 (defun phox-tags-add-doc-table()
   "Add tags in text documentation."
@@ -75,37 +61,25 @@
 
 
 (defun phox-complete-tag()
-"Complete symbol using tags table. Works with FSF emacs.
- Problems with xemacs."
-;; xemacs build a table for completion, tag-completion-table this table
-;; donnot contains key words that use ".". There is a problem with
-;; syntax-table. In xemacs you need to redefine
-;; add-to-tag-completion-table, in order to add your file-type and
-;; syntax-table. The modification is very simple, there should be an
-;; hook for that.
-;; 
-(interactive)
-(if (featurep 'xemacs)
-     (tag-complete-symbol)
-  (complete-tag)
-  )
-)
+  "Complete symbol using tags table."
+  (interactive)
+  (complete-tag))
 
 ;; menu
 
 (defvar phox-tags-menu
-     '("Tags"
-       ["create a tags table for local buffer" phox-tags-create-local-table t]
-       ["------------------" nil nil]
-       ["add table"               phox-tags-add-table       t]
-       ["add local table"         phox-tags-add-local-table t]
-       ["add table for libraries" phox-tags-add-lib-table   t]
-       ["add table for text doc"  phox-tags-add-doc-table   t]
-       ["reset tags table list"   phox-tags-reset-table     t]
-       ["------------------" nil nil]
-       ["Find theorem, definition ..." find-tag t]
-       ["complete theorem, definition ..." phox-complete-tag t]
-      )
+  '("Tags"
+    ["create a tags table for local buffer" phox-tags-create-local-table t]
+    ["------------------" nil nil]
+    ["add table"               phox-tags-add-table       t]
+    ["add local table"         phox-tags-add-local-table t]
+    ["add table for libraries" phox-tags-add-lib-table   t]
+    ["add table for text doc"  phox-tags-add-doc-table   t]
+    ["reset tags table list"   phox-tags-reset-table     t]
+    ["------------------" nil nil]
+    ["Find theorem, definition ..." find-tag t]
+    ["complete theorem, definition ..." phox-complete-tag t]
+    )
 "Phox menu for dealing with tags"
 )
 
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)
 
 
diff --git a/phox/x-symbol-phox.el b/phox/x-symbol-phox.el
deleted file mode 100644
index 8590dd23..00000000
--- a/phox/x-symbol-phox.el
+++ /dev/null
@@ -1,230 +0,0 @@
-;; x-symbol-phox.el   
-;;	Token language "PhoX Symbols" for package x-symbol
-;;
-;;  ID:         $Id$
-;;  Author:     C. Raffalli
-;;              Updates by Markus Wenzel, Christoph Wedler, David Aspinall.
-;;  Copyright   1998 Technische Universitaet Muenchen
-;;  License     GPL (GNU GENERAL PUBLIC LICENSE)
-;;
-;;  Adapted from x-symbol-isabelle.el
-;; NB: Part of Proof General distribution.
-;;
-
-(require 'proof-utils)
-
-(defvar x-symbol-phox-required-fonts nil)
-
-;;;===========================================================================
-;;;  General language accesses, see `x-symbol-language-access-alist'
-;;;===========================================================================
-
-;; NB da: these next two are also set in proof-x-symbol.el, but
-;; 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.
-(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.
-See `x-symbol-header-groups-alist'."
-  :group 'x-symbol-phox
-  :group 'x-symbol-input-init
-  :type 'x-symbol-headers)
-
-(defcustom x-symbol-phox-electric-ignore 
-  "/\\\\\\|\\\\/"
-  "*Additional Phox version of `x-symbol-electric-ignore'."
-  :group 'x-symbol-phox
-  :group 'x-symbol-input-control
-  :type 'x-symbol-function-or-regexp)
-
-(defvar x-symbol-phox-required-fonts nil
-  "List of features providing fonts for language `phox'.")
-
-(defvar x-symbol-phox-extra-menu-items nil
-  "Extra menu entries for language `phox'.")
-
-(defvar x-symbol-phox-token-grammar
-  ;; CW: for X-Symbol-4.4.3:
-  ;; '(x-symbol-make-grammar ...)
-  (if (fboundp 'x-symbol-make-grammar) ;; x-symbol >=4.3 versions
-      (x-symbol-make-grammar
-       :encode-spec '(((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]")) .
-                    ((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]")))
-       :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 '(((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]")) .
-                    ((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]"))))))
-
-(defvar x-symbol-phox-input-token-grammar
-  '("\\([_'a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)"
-     ((id . "[A-Za-z_0-9]") (op . "[<>!+-*/|&]"))
-     (id . "[A-Za-z_0-9]") (op . "[<>!+-*/|&]"))
-  "Grammar of input method Token for language `phox'.")
-
-(defun x-symbol-phox-default-token-list (tokens)
-  (mapcar 
-   (lambda (x)
-     (cons x 
-	   (cond
-	    ;; the shapes `id' and `op' are used by x-symbol-phox-token-grammar
-	    ((string-match "\\`[A-Za-z_][A-Za-z_0-9]+\\'" x)
-	     'id)
-	    ((string-match "\\`[]><=\\/~&+-*%!{}:-]+\\'" x) 
-	     'op))))
-   tokens))
-
-(defvar x-symbol-phox-user-table nil
-  "User table defining Phox commands, used in `x-symbol-phox-table'.")
-
-(defvar x-symbol-phox-generated-data nil
-  "Internal.")
-
-
-;;;===========================================================================
-;;;  No image support
-;;;===========================================================================
-
-(defvar x-symbol-phox-master-directory  'ignore)
-(defvar x-symbol-phox-image-searchpath '("./"))
-(defvar x-symbol-phox-image-cached-dirs '("images/" "pictures/"))
-(defvar x-symbol-phox-image-file-truename-alist nil)
-(defvar x-symbol-phox-image-keywords nil)
-
-
-;;;===========================================================================
-;;;  Charsym Info
-;;;===========================================================================
-
-(defcustom x-symbol-phox-class-alist
-  '((VALID "Phox Symbol" (x-symbol-info-face))
-    (INVALID "no Phox Symbol" (red x-symbol-info-face)))
-  "Alist for Phox's token classes displayed by info in echo area.
-See `x-symbol-language-access-alist' for details."
-  :group 'x-symbol-texi
-  :group 'x-symbol-info-strings
-  :set 'x-symbol-set-cache-variable
-  :type 'x-symbol-class-info)
-
-
-(defcustom x-symbol-phox-class-face-alist nil
-  "Alist for Phox's color scheme in TeXinfo's grid and info.
-See `x-symbol-language-access-alist' for details."
-  :group 'x-symbol-phox
-  :group 'x-symbol-input-init
-  :group 'x-symbol-info-general
-  :set 'x-symbol-set-cache-variable
-  :type 'x-symbol-class-faces)
-
-
-(defvar x-symbol-phox-font-lock-keywords nil)
-
-(defvar x-symbol-phox-font-lock-allowed-faces t)
-
-;;;===========================================================================
-;;;  The tables
-;;;===========================================================================
-
-(defvar x-symbol-phox-case-insensitive nil)
-(defvar x-symbol-phox-token-shape nil)
-(defvar x-symbol-phox-input-token-ignore nil)
-
-;; FIXME: next one not needed in X-Symbol 4, kept for back compat.
-;;(defvar x-symbol-phox-exec-specs 
-;;  '(nil ("\\`\\\\<[A-Za-z][A-Za-z0-9_']*>\\'" .
-;;	 "\\\\<[A-Za-z][A-Za-z0-9_']*>")))
-
-(defvar x-symbol-phox-token-list 'identity)
-
-(defvar x-symbol-phox-xsymb0-table      ; symbols 
-  '((greaterequal ">=")
-    (lessequal "<=")
-    (notequal "!=")
-    (element "in")
-    (notelement "notin")
-    (propersubset "subset")
-    (intersection "inter")
-    (union "union")
-    (backslash3 "minus")
-    (universal1 "/\\")
-    (existential1 "\\/")
-    (logicalor "or")
-    (logicaland "&")
-    (arrowboth "<->")
-    (arrowright "->")
-    (arrowdblright "=>")
-    (notsign "~")
-    (lambda "\\")
-))
-
-(defun x-symbol-phox-prepare-table (table)
-  "Prepar the table."
-    (mapcar (lambda (entry)
-	      (progn
-		(list (car entry) nil
-		      (cadr entry))))
-            table))
-
-(defvar x-symbol-phox-table
-  (x-symbol-phox-prepare-table
-    (append x-symbol-phox-user-table x-symbol-phox-xsymb0-table)))
-
-(provide 'x-symbol-phox)
-
-;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
-;;
-;; User-level settings for X-Symbol 
-;;
-;; this is MODE-ON CODING 8BITS UNIQUE SUBSCRIPTS IMAGE
-(defcustom x-symbol-phox-auto-style
-  '(phox-x-symbol-enable	 ; MODE-ON: whether to turn on interactively
-    nil   ;; x-symbol-coding
-    'null ;; x-symbol-8bits	   [NEVER want it; null disables search]
-    nil   ;; x-symbol-unique
-    nil   ;; x-symbol-subscripts
-    nil)  ;; x-symbol-image
-  "Variable used to document a language access.
-See documentation of `x-symbol-auto-style'."
-  :group 'x-symbol-phox
-  :group 'x-symbol-mode
-  :type 'x-symbol-auto-style)
-
-;; CW: this sexpr can be deleted with X-Symbol 4.4.3
-(eval-when-compile
-  ;; Next lines should allow this file to work standalone 
-  ;; without proof-x-symbol.el.  See comments further below too.
-  (require 'cl)
-  (ignore-errors (require 'x-symbol-vars)))
-
-
-;;;===========================================================================
-;;;  Internal
-;;;===========================================================================
-;; CW: all are not needed in X-Symbol >= v4.3
-
-(defvar x-symbol-phox-menu-alist nil
-  "Internal.  Alist used for Isasym specific menu.")
-(defvar x-symbol-phox-grid-alist nil
-  "Internal.  Alist used for Isasym specific grid.")
-
-(defvar x-symbol-phox-decode-atree nil
-  "Internal.  Atree used by `x-symbol-token-input'.")
-(defvar x-symbol-phox-decode-alist nil
-  "Internal.  Alist used for decoding of Isasym macros.")
-(defvar x-symbol-phox-encode-alist nil
-  "Internal.  Alist used for encoding to Isasym macros.")
-
-;; FIXME: next two not needed for newer X-Symbol versions.
-(defvar x-symbol-phox-nomule-decode-exec nil
-  "Internal.  File name of Isasym decode executable.")
-(defvar x-symbol-phox-nomule-encode-exec nil
-  "Internal.  File name of Isasym encode executable.")
-
-(provide 'x-symbol-phox)
-