aboutsummaryrefslogtreecommitdiffhomepage
path: root/isa/interface-setup.el
blob: 2ed504cb0acb3dd5d394643d55b3bd7d5cb27f43 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
;; 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$
;;

;;;
;;; X-Symbol
;;;

(if (string-match "XEmacs" emacs-version)       ;current X-Symbol works with XEmacs only!
    (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)))
      ;; setup the x-symbol package, if not already present
      (if (and xsymbol-home
               (not (equal 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))
            (push (expand-file-name "lisp/x-symbol" xsymbol-home) load-path)
            (if (boundp 'data-directory-list)
                (push (expand-file-name "etc/" xsymbol-home) data-directory-list))
            (if (boundp 'Info-directory-list)
                (push (expand-file-name "info/" xsymbol-home) Info-directory-list))
            (if (not (boundp 'x-symbol-image-converter))     ;avoid confusing warning message
                (customize-set-variable 'x-symbol-image-converter nil))
            (x-symbol-initialize)))
      ;; tell Proof General about -x option
      (if (and xsymbol (not (equal xsymbol "")))
          (customize-set-variable enable-var (equal xsymbol "true")))))


;;
;; Proof General
;;

(if (not (featurep 'proof-site))
    (load (concat (getenv "PROOFGENERAL_HOME") "/generic/proof-site.el")))