smart setup of X-Symbol mode;

1 files changed, 32 insertions, 6 deletions

diff --git a/isa/interface-setup.el b/isa/interface-setup.el
index d6646fd4..aa8f344d 100644
--- a/isa/interface-setup.el
+++ b/isa/interface-setup.el
@@ -1,11 +1,37 @@
+;; interface-setup.el Interface wrapper for Isabelle Proof General
+;;
+;; This file is free software; you can redistribute it and/or modify
+;; it under the terms of the GNU General Public License as published by
+;; the Free Software Foundation; either version 2, or (at your option)
+;; any later version.
+;;
+;; Author: Markus Wenzel <wenzelm@in.tum.de>
 ;;
 ;; $Id$
 ;;
 
-(let ((xsymbol (getenv "PROOFGENERAL_XSYMBOL")))
-  (if (and xsymbol (not (equal xsymbol "")))
-      (customize-set-variable
+;;;
+;;; X-Symbol mode
+;;;
+
+(let ((xsymbol-home (getenv "XSYMBOL_HOME"))
+      (xsymbol (getenv "PROOFGENERAL_XSYMBOL"))
+      (enable-var
        (if (equal (getenv "PROOFGENERAL_ASSISTANTS") "isa")
-           'isa-x-symbol-enable
-         'isar-x-symbol-enable)
-       (equal xsymbol "true"))))
+           'isa-x-symbol-enable 'isar-x-symbol-enable)))
+  ;; setup the x-symbol package, if not already present
+  (if (and xsymbol-home
+           (not (fboundp 'x-symbol-initialize))
+           (not (get 'x-symbol 'x-symbol-initialized)))
+      (progn
+        (load (expand-file-name "lisp/x-symbol/auto-autoloads" xsymbol-home))
+        (setq load-path
+              (cons (expand-file-name "lisp/x-symbol" xsymbol-home) load-path))
+        (if (boundp 'data-directory-list)
+            (setq data-directory-list
+                  (cons (expand-file-name "etc/" xsymbol-home) data-directory-list)))
+        (require 'x-symbol-hooks)
+        (x-symbol-initialize)))
+  ;; tell Proof General about -x option
+  (if (and xsymbol (not (equal xsymbol "")))
+      (customize-set-variable enable-var (equal xsymbol "true"))))