Moved proof-info-dir into proof-site and defcustom'd it.

Set the Info directory list there rather than after
proof.el has loaded.  Add the proof-info-dir onto the
end of Info-default-directory-list, not the start.

2 files changed, 18 insertions, 11 deletions

diff --git a/generic/proof-site.el b/generic/proof-site.el
index a31b8d1d..7e4560cf 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -10,6 +10,7 @@
 ;; different proof assistants in the same session.  Presently, the
 ;; code will only allow one assistant to be chosen for the whole
 ;; session.
+;; 
 
 (or (featurep 'custom)
     ;; Quick hack to support defcustom for Emacs 19
@@ -18,23 +19,37 @@
     (defmacro group (sym mems doc &rest args)))
 
 (defgroup proof nil
-  "Customization of generic parameters for proof mode."
+  "Customization of generic parameters for Proof General."
   :group 'external
   :group 'processes)
 
 (defcustom proof-home
   (or (getenv "PROOF_HOME") "~/devel/lego/elisp/")
-  "*Directory where proof mode is installed. Ends with slash.
+  "*Directory where Proof General is installed. Ends with slash.
 Default value taken from PROOF_HOME, or use customize to set it."
   :type 'directory
   :group 'proof)
 
 (defcustom proof-image-directory
   (concat proof-home "images/")
-    "*Where proof mode image files are installed. Ends with slash."
+    "*Where Proof General image files are installed. Ends with slash."
   :type 'directory
   :group 'proof)
 
+(defcustom proof-info-dir 
+  (concat proof-home "doc/")
+  "*Where Proof General Info files are installed."
+  :type 'directory
+  :group 'proof)
+
+;; Add the info directory to the end of Emacs Info path 
+;; if need be. 
+(or (memq proof-info-dir Info-default-directory-list)
+    (setq Info-default-directory-list
+	  (append 
+	   Info-default-directory-list 
+	   (list proof-info-dir))))
+
 (defcustom proof-assistants
   '(isa lego coq)
   "*Choice of proof assitants to use with Proof General.
diff --git a/generic/proof.el b/generic/proof.el
index 4b295248..309f9b6a 100644
--- a/generic/proof.el
+++ b/generic/proof.el
@@ -70,9 +70,6 @@ output format.")
 ;;   Proof mode variables                                           ;;
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 
-(defconst proof-info-dir "/usr/local/share/info"
-  "Directory to search for Info documents on Script Management.")
-
 (defconst proof-universal-keys
   (list (cons '[(control c) (control c)] 'proof-interrupt-process)
 	(cons '[(control c) (control v)]
@@ -1922,11 +1919,6 @@ current command."
        (push (cons major-mode 'fume-match-find-next-function-name)
 	     fume-find-function-name-method-alist))
 
-  ;; Info
-  (or (memq proof-info-dir Info-default-directory-list)
-      (setq Info-default-directory-list
-	    (cons proof-info-dir Info-default-directory-list)))
-
   ;; keymaps and menus
   (easy-menu-add proof-mode-menu proof-mode-map)