change to support version 4.4 of x-symbol

3 files changed, 195 insertions, 64 deletions

diff --git a/phox/phox-font.el b/phox/phox-font.el
index 020417ac..f34b051a 100644
--- a/phox/phox-font.el
+++ b/phox/phox-font.el
@@ -3,10 +3,8 @@
 ;;                       Font lock keywords
 ;;--------------------------------------------------------------------------;;
 
-(require 'proof-x-symbol)
-
 (defconst phox-font-lock-keywords
-   (list
+  (list
 ;commands
    '("(\\*\\([^*]\\|\\*+[^*)]\\)*\\(\\*+)\\|\\**$\\)"
     0 'font-lock-comment-face t)
diff --git a/phox/phox.el b/phox/phox.el
index 07511184..8b22dafe 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -133,7 +133,7 @@
    proof-find-and-forget-fn        'phox-find-and-forget
    proof-find-theorems-command      "search \"%s\"."
    proof-auto-multiple-files       nil
-   font-lock-keywords              phox-font-lock-keywords 
+   font-lock-keywords              (append phox-font-lock-keywords proof-xsym-font-lock-keywords)
    )
   (phox-init-syntax-table)
 ;; the following is only useful for xemacs
@@ -203,7 +203,7 @@
 (define-derived-mode phox-response-mode proof-response-mode
   "PhoX response" nil
   (setq 
-   font-lock-keywords  phox-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)
   (add-hook 'proof-shell-handle-delayed-output-hook 'phox-sym-lock-font-lock-hook)
@@ -212,14 +212,14 @@
 (define-derived-mode phox-goals-mode proof-goals-mode
   "PhoX goals" nil
   (setq 
-   font-lock-keywords  phox-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)
   (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 to define them at all -- they
+;; 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".
 
 ;; A more sophisticated instantiation might set font-lock-keywords to
@@ -248,9 +248,22 @@
 
 ; (set-variable 'phox-completion-table 
 (defpgdefault completion-table
-(append phox-top-keywords phox-proof-keywords)
+  (append phox-top-keywords phox-proof-keywords)
 )
 
+(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 (proof-ass 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
index e67d8774..122ccf93 100644
--- a/phox/x-symbol-phox.el
+++ b/phox/x-symbol-phox.el
@@ -1,82 +1,202 @@
+;; 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.
+;;
 
-  
-(defvar x-symbol-phox-name "PhoX")
-(defvar phox-xsym-extra-modes '('phox-response-mode 'phox-goals-mode))
-(x-symbol-register-language 'phox 'x-symbol-phox '(phox-mode phox-shell-mode))
-
+;; 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)))
 
 (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.
+(defvar x-symbol-phox-name "PhoX Symbol")
 (defvar x-symbol-phox-modeline-name "phox")
-(defvar x-symbol-phox-class-alist
-  '((VALID "PhoX Symbol" (x-symbol-info-face))
-    (INVALID "no PhoX Symbol" (red x-symbol-info-face))))
-(defvar x-symbol-phox-font-lock-keywords nil)
+
+(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 nil
+;;  "[:'][A-Za-z]\\|<=\\|\\[\\[\\|\\]\\]\\|~="
+  "*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 nil
+       :decode-regexp "\\([_'a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)"
+       :token-list #'x-symbol-phox-default-token-list)))
+
+(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
+	    ;; CW: where are the shapes `id' and `op' used?
+	    ((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)
 
-(defvar x-symbol-phox-token-shape nil)
-(defvar x-symbol-phox-exec-specs nil)
-(defvar x-symbol-phox-decoding-regexp "\\([_'a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)")
-(defvar x-symbol-phox-surrounding-regexp "[ \n\t\r]")
+;;;===========================================================================
+;;;  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 x-symbol-nomule-font-lock-keywords)
+(defvar x-symbol-phox-font-lock-allowed-faces t)
+
+;;;===========================================================================
+;;;  The tables
+;;;===========================================================================
 
-(defvar x-symbol-phox-input-token-ignore nil)
-(defvar x-symbol-phox-header-groups-alist nil)
-(defvar x-symbol-phox-class-face-alist nil)
-(defvar x-symbol-phox-electric-ignore nil)
 (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 "<<")
+    (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)
+              (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)
+
+;;;===========================================================================
+;;;  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-ahash nil
-  "Internal.  Ahash.")
 (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)
 
-
-(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)
-
-  
-(defun x-symbol-phox-default-token-list (tokens) tokens)
-
-(defvar x-symbol-phox-token-list 'x-symbol-phox-default-token-list)
-(defvar x-symbol-phox-user-table nil)
-(defvar x-symbol-phox-xsymb0-table
-  '((greaterequal () ">=")
-    (lessequal () "<=")
-    (notequal () "!=")
-    (element () "in")
-    (notelement () "notin")
-    (propersubset () "<<")
-    (intersection () "inter")
-    (union () "union")
-    (backslash3 () "minus")
-    (universal1 () "/\\")
-    (existential1 () "\\/")
-    (logicalor () "or")
-    (logicaland () "&")
-    (arrowboth () "<->")
-    (arrowright () "->")
-    (arrowdblright () "=>")
-    (notsign () "~")
-    (lambda () "\\")
-))
-
-(defvar x-symbol-phox-table
-  (append x-symbol-phox-user-table x-symbol-phox-xsymb0-table))
-
-(provide 'x-symbol-phox)
\ No newline at end of file