Fix compilation: need proof-utils

1 files changed, 26 insertions, 24 deletions

diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el
index 0265567c..ffa71170 100644
--- a/generic/proof-x-symbol.el
+++ b/generic/proof-x-symbol.el
@@ -42,6 +42,9 @@
 ;;
 ;; =================================================================
 
+(eval-when-compile
+  (require 'proof-utils))	 ; proof-ass
+
 (defvar proof-x-symbol-initialized nil
   "Non-nil if x-symbol support has been initialized.")
 
@@ -299,30 +302,29 @@ Assumes that the current buffer is the proof shell buffer."
 ;;;###autoload
 (defun proof-x-symbol-config-output-buffer ()
   "Configure the current output buffer (goals/response/trace) for X-Symbol."
-  (if (proof-ass x-symbol-enable)
-      (progn
-	(proof-x-symbol-set-language)
-	;; BEGIN: Code below from x-symbol.el/x-symbol-mode-internal
-	(unless (or (not (boundp 'enable-multibyte-characters))
-		    (not (fboundp 'set-buffer-multibyte))
-		    enable-multibyte-characters)
-	  ;; Emacs: we need to convert the buffer from unibyte to multibyte
-	  ;; since we'll use multibyte support for the symbol charset.
-	  ;; TODO: try to do it less often
-	  (let ((modified (buffer-modified-p))
-		(inhibit-read-only t)
-		(inhibit-modification-hooks t))
-	    (unwind-protect
-		(progn
-		  (decode-coding-region (point-min) (point-max) 'undecided)
-		  (set-buffer-multibyte t))
-	      (set-buffer-modified-p modified))))
-	;; END code from x-symbol.el/x-symbol-mode-internal
-
-	;; If we're turning on x-symbol, attempt to convert to
-	;; characters.  (Only works if the buffer already contains
-	;; tokens!)  This breaks manual fontification, too.
-	(x-symbol-decode))))
+  (when (proof-ass x-symbol-enable)
+    (proof-x-symbol-set-language)
+    ;; BEGIN: Code below from x-symbol.el/x-symbol-mode-internal
+    (unless (or (not (boundp 'enable-multibyte-characters))
+		(not (fboundp 'set-buffer-multibyte))
+		enable-multibyte-characters)
+      ;; Emacs: we need to convert the buffer from unibyte to multibyte
+      ;; since we'll use multibyte support for the symbol charset.
+      ;; TODO: try to do it less often
+      (let ((modified (buffer-modified-p))
+	    (inhibit-read-only t)
+	    (inhibit-modification-hooks t))
+	(unwind-protect
+	    (progn
+	      (decode-coding-region (point-min) (point-max) 'undecided)
+	      (set-buffer-multibyte t))
+	  (set-buffer-modified-p modified))))
+    ;; END code from x-symbol.el/x-symbol-mode-internal
+    
+    ;; If we're turning on x-symbol, attempt to convert to
+    ;; characters.  (Only works if the buffer already contains
+    ;; tokens!)  NB: this removes previous fontification, too.
+    (x-symbol-decode)))
   ;; Encoding back to tokens doesn't work too well: needs to 
   ;; do some de-fontification to remove font properties, and
   ;; is flaky anyway because token -> char not nec injective.