From fc774de804417a399094f61de1880e75b556c851 Mon Sep 17 00:00:00 2001
From: Christophe Raffalli <christophe.raffalli@univ-savoie.fr>
Date: Fri, 24 Feb 2006 17:16:02 +0000
Subject: back to using sym-lock ... x-symbol will not be supported anymore for
 PhoX + imporvment in proof by contextual menu

---
 phox/phox.el | 42 +++++++++++++++++++++++++++---------------
 1 file changed, 27 insertions(+), 15 deletions(-)

(limited to 'phox/phox.el')

diff --git a/phox/phox.el b/phox/phox.el
index fa25363a..2c51e434 100644
--- a/phox/phox.el
+++ b/phox/phox.el
@@ -33,13 +33,10 @@
   :type 'file
   :group 'phox)
 
-; da: I commented this out, it should be defined automatically
-; in proof-config.el.  If you want to change the default to t,
-; then perhaps:  (custom-set-default phox-x-symbol-enable t)
-;(defcustom phox-x-symbol-enable t
-;  "*Whether to use x-symbol or not."
-;  :type 'boolean
-;  :group 'phox)
+(defcustom phox-sym-lock-enabled t
+  "*Whether to use x-symbol or not."
+  :type 'boolean
+  :group 'phox)
 
 
 (defcustom phox-web-page
@@ -109,6 +106,10 @@
 
 (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)))
   (setq
    proof-terminal-char		?\.	; ends every command
    proof-script-command-end-regexp "[.]\\([ \t\n\r]\\)"
@@ -161,7 +162,7 @@
    proof-shell-quit-cmd            "quit."
    proof-shell-restart-cmd         "restart."
    proof-shell-proof-completed-regexp   "^.*^proved"
-))
+   ))
 
 
 ;;
@@ -185,12 +186,12 @@
     ;; 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)
+    ;(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 ??)
 
 )
 
@@ -204,15 +205,26 @@
   (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-enabled)
+      (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
   "PhoX goals" nil
   (setq 
-   font-lock-keywords  (append phox-font-lock-keywords proof-xsym-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)
+  (if (and (featurep 'phox-sym-lock) phox-sym-lock-enabled)
+      (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 t²o define them at all -- they
 ;; would simply default to "proof-response-mode" and "pg-goals-mode".
-- 
cgit v1.2.3