first try to make x-symbol works

2 files changed, 56 insertions, 13 deletions

diff --git a/phox/phox.el b/phox/phox.el
index 1b9e85c0..b0b57f3e 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -32,8 +32,13 @@
   :type 'file
   :group 'phox)
 
-(defcustom phox-sym-lock t
-  "*Whether to use sym-lock or not."
+(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
   :group 'phox)
 
@@ -262,6 +267,24 @@
   (append phox-top-keywords phox-proof-keywords)
 )
 
+;;;
+;;; 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"
  ;; Add x-symbol tokens to phox-completion-table and rebuild
  ;; internal completion table if completion is already active
diff --git a/phox/x-symbol-phox.el b/phox/x-symbol-phox.el
index ac1cb658..38f98a71 100644
--- a/phox/x-symbol-phox.el
+++ b/phox/x-symbol-phox.el
@@ -11,15 +11,8 @@
 ;; NB: Part of Proof General distribution.
 ;;
 
-;; 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'
 ;;;===========================================================================
@@ -51,7 +44,6 @@ See `x-symbol-header-groups-alist'."
 (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 ...)
@@ -61,7 +53,8 @@ See `x-symbol-header-groups-alist'."
                     ((id . "[_'a-zA-Z0-9]") (op . "[]><=\\/~&+-*%!{}:-]")))
        :decode-spec nil
        :decode-regexp "\\([_'a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)"
-       :token-list #'x-symbol-phox-default-token-list)))
+       :token-list #'x-symbol-phox-default-token-list
+       :input-spec nil)))
 
 (defvar x-symbol-phox-input-token-grammar
   '("\\([_'a-zA-Z0-9]+\\)\\|\\([]><=\\/~&+-*%!{}:-]+\\)"
@@ -98,6 +91,7 @@ See `x-symbol-header-groups-alist'."
 (defvar x-symbol-phox-image-file-truename-alist nil)
 (defvar x-symbol-phox-image-keywords nil)
 
+
 ;;;===========================================================================
 ;;;  Charsym Info
 ;;;===========================================================================
@@ -148,7 +142,7 @@ See `x-symbol-language-access-alist' for details."
     (notequal "!=")
     (element "in")
     (notelement "notin")
-    (propersubset "<<")
+    (propersubset "subset")
     (intersection "inter")
     (union "union")
     (backslash3 "minus")
@@ -176,6 +170,32 @@ See `x-symbol-language-access-alist' for details."
 
 (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
+  '((proof-ass 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
 ;;;===========================================================================