Fix 464: proof-autoloads not found by Emacs

3 files changed, 28 insertions, 31 deletions

diff --git a/generic/pg-autotest.el b/generic/pg-autotest.el
index 7a22c9f7..54fa8abb 100644
--- a/generic/pg-autotest.el
+++ b/generic/pg-autotest.el
@@ -45,7 +45,7 @@
 
 (defun pg-autotest-find-file (file)
   "Find FILE (relative to `proof-home-directory')."
-  (let* ((name   (concat proof-home-directory file)))
+  (let* ((name   (expand-file-name file proof-home-directory)))
     (if (file-exists-p name)
 	(find-file name)
       (error (format "autotest: requested file %s does not exist" name)))))
diff --git a/generic/pg-movie.el b/generic/pg-movie.el
index 755d41f5..2b2454d8 100644
--- a/generic/pg-movie.el
+++ b/generic/pg-movie.el
@@ -43,7 +43,7 @@
   "<?xml-stylesheet type=\"text/xsl\" href=\"proviola-spp.xsl\"?>")
 
 (defun pg-movie-stylesheet-location ()
-  (concat proof-home-directory "etc/proviola/proviola-spp.xsl"))
+  (expand-file-name "etc/proviola/proviola-spp.xsl" proof-home-directory))
   
 
 (defvar pg-movie-frame 0 "Frame counter for movie.")
diff --git a/generic/proof-site.el b/generic/proof-site.el
index 5fb9cdb8..f47d8800 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -114,34 +114,29 @@
 ;; Load path must be extended manually during compilation.
 ;;
 
-(defun proof-home-directory-fn ()
-  "Used to set `proof-home-directory'."
-  (let ((s (getenv  "PROOFGENERAL_HOME")))
-    (if s
-	(if (string-match "/$" s) s (concat s "/"))
-      (let ((curdir
-	     (or
-	      (and load-in-progress (file-name-directory load-file-name))
-	      (file-name-directory (buffer-file-name)))))
-	(file-name-directory (substring curdir 0 -1))))))
-
-(defcustom proof-home-directory
-  (proof-home-directory-fn)
-  "Directory where Proof General is installed.  Ends with slash.
-Default value taken from environment variable `PROOFGENERAL_HOME' if set,
-otherwise based on where the file `proof-site.el' was loaded from.
-You can use customize to set this variable."
-  :type 'directory
-  :group 'proof-general-internals)
+(defconst proof-home-directory
+  (let ((curfile
+	 (or
+	  (and load-in-progress load-file-name)
+	  buffer-file-name)))
+    (if curfile
+        (file-name-directory (directory-file-name
+                              (file-name-directory curfile)))
+      (let ((s (getenv "PROOFGENERAL_HOME")))
+	(if s (file-name-as-directory s)))))
+  "Directory where Proof General is installed.
+based on where the file `proof-site.el' was loaded from.
+Falls back to consulting the environment variable `PROOFGENERAL_HOME' if
+proof-site.el couldn't know where it was executed from.")
 
 (defcustom proof-images-directory
-  (concat proof-home-directory "images/")
+  (expand-file-name "images/" proof-home-directory)
     "Where Proof General image files are installed.  Ends with slash."
   :type 'directory
   :group 'proof-general-internals)
 
 (defcustom proof-info-directory
-  (concat proof-home-directory "doc/")
+  (expand-file-name "doc/" proof-home-directory)
   "Where Proof General Info files are installed.  Ends with slash."
   :type 'directory
   :group 'proof-general-internals)
@@ -159,8 +154,8 @@ You can use customize to set this variable."
   "Add DIR to `load-path' if not contained already."
   (add-to-list 'load-path dir))
 
-(proof-add-to-load-path (concat proof-home-directory "generic/"))
-(proof-add-to-load-path (concat proof-home-directory "lib/"))
+(proof-add-to-load-path (expand-file-name "generic/" proof-home-directory))
+(proof-add-to-load-path (expand-file-name "lib/" proof-home-directory))
 
 
 ;; Declare some global variables and autoloads
@@ -184,12 +179,12 @@ You can use customize to set this variable."
 
 (defcustom proof-assistant-table
   (apply
-   'append
+   #'append
    (mapcar
     ;; Discard entries whose directories have been removed.
     (lambda (dne)
-      (let ((atts (file-attributes (concat proof-home-directory
-					   (symbol-name (car dne))))))
+      (let ((atts (file-attributes (expand-file-name (symbol-name (car dne))
+					             proof-home-directory))))
 	(if (and atts (eq 't (car atts)))
 	    (list dne)
 	  nil)))
@@ -342,9 +337,11 @@ the Lisp variable `proof-assistants', or the contents of `proof-assistant-table'
   "Visit a standardly named example file for prover PROVER."
   (interactive
    (list (proof-chose-prover "Visit example file for prover: ")))
-  (find-file (concat proof-home-directory
-		     prover "/example."
-		     (nth 2 (assoc (intern prover) proof-assistant-table-default)))))
+  (find-file (expand-file-name
+	      (concat prover "/example."
+		      (nth 2 (assoc (intern prover)
+		                    proof-assistant-table-default)))
+	      proof-home-directory)))