More tweaks so that (proof-ass x-symbol-enable) is pervasive.

2 files changed, 11 insertions, 2 deletions

diff --git a/generic/proof-script.el b/generic/proof-script.el
index 44568bff..93a0b400 100644
--- a/generic/proof-script.el
+++ b/generic/proof-script.el
@@ -13,8 +13,8 @@
 (require 'span)				; abstraction of overlays/extents
 (require 'pg-user)			; user-level commands
 (require 'proof-menu)			; menus for script mode
-(require 'proof-x-symbol)		; x-symbol (maybe put on automode list)
-(require 'proof-mmm)			; mmm (ditto)
+(require 'proof-x-symbol)		; x-symbol (maybe initialize)
+(require 'proof-mmm)			; mmm (maybe put on automode list)
 
 
 ;; Nuke some byte-compiler warnings 
@@ -2714,6 +2714,11 @@ finish setup which depends on specific proof assistant configuration."
      ((and img proof-running-on-XEmacs)
       (set-glyph-image invisible-text-glyph img (current-buffer)))))
 
+  ;; FIXME: next expr shouldn't be needed, if loads happen in
+  ;; correct order.
+  (if (proof-ass x-symbol-enable)
+      (proof-x-symbol-enable))
+
   ;; Finally, make sure the user has been welcomed!
   ;; [NB: this doesn't work well, can get zapped by loading messages]
   (proof-splash-message))
diff --git a/generic/proof-x-symbol.el b/generic/proof-x-symbol.el
index fed1a5a4..58fd804f 100644
--- a/generic/proof-x-symbol.el
+++ b/generic/proof-x-symbol.el
@@ -185,6 +185,10 @@ in future if we have just activated it for this buffer."
 	(set (proof-ass-sym x-symbol-enable) nil) ; assume failure!
 	(proof-x-symbol-initialize 'giveerrors)
 	(set (proof-ass-sym x-symbol-enable) t)))
+  ;; FIXME: on startup, x-symbol-language should somehow be
+  ;; set automatically, but perhaps something loads too late.
+  ;; Hence the next line to ensure things work smoothly.
+  (setq x-symbol-language (proof-ass x-symbol-language))
   (x-symbol-mode)
   (proof-x-symbol-mode-associated-buffers))