* pg-init.el: Add subdirs during compilation (bug #413)

* generic/pg-user.el (proof-add-completions): `proof-assistant` can
also be the empty string :-(

2 files changed, 22 insertions, 4 deletions

diff --git a/generic/pg-user.el b/generic/pg-user.el
index 57d29f18..d2259ef8 100644
--- a/generic/pg-user.el
+++ b/generic/pg-user.el
@@ -3,7 +3,7 @@
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2019  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -558,7 +558,7 @@ last use time, to discourage saving these into the users database."
   (defvar completion-min-length)
   (declare-function add-completion "completion"
                     (string &optional num-uses last-use-time))
-  (when proof-assistant
+  (when (> (length proof-assistant) 0)
     (mapcar (lambda (cmpl)
 	      ;; completion gives error; trapping is tricky so test again
 	      (if (>= (length cmpl) completion-min-length)
diff --git a/pg-init.el b/pg-init.el
index 3a2e5492..0634de0b 100644
--- a/pg-init.el
+++ b/pg-init.el
@@ -1,9 +1,9 @@
-;;; pg-init.el --- PG init file for package.el and ELPA compatibility -*- lexical-binding: t; -*-
+;;; pg-init.el --- PG init file for package.el and ELPA compatibility -*- lexical-binding:t; -*-
 
 ;; This file is part of Proof General.
 
 ;; Portions © Copyright 1994-2012  David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003-2018  Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2019  Free Software Foundation, Inc.
 ;; Portions © Copyright 2001-2017  Pierre Courtieu
 ;; Portions © Copyright 2010, 2016  Erik Martin-Dorel
 ;; Portions © Copyright 2011-2013, 2016-2017  Hendrik Tews
@@ -47,5 +47,23 @@
                                  (file-name-directory
                                   (or load-file-name buffer-file-name)))))
 
+(eval-when-compile
+  ;; FIXME: This is used during installation of the ELPA package:
+  ;; we presume that this file will be compiled before any of the files in
+  ;; sub-directories and we presume that all files are compiled within the same
+  ;; session, so we here add to load-path all the subdirectories so
+  ;; that files in (say) coq/ can (require 'coq-foo) and the compiler will find
+  ;; the corresponding file.
+  (let ((byte-compile-directories
+         '("generic" "lib"
+           "coq" "easycrypt" "pghaskell" "pgocaml" "pgshell" "phox"
+           ;; FIXME: These dirs used to not be listed, but I needed to add
+           ;; them for the compilation to succeed for me.  --Stef
+           "isar" "lego" "twelf" "obsolete/plastic"))
+        (root (file-name-directory
+               (or load-file-name byte-compile-current-file buffer-file-name))))
+    (dolist (dir byte-compile-directories)
+      (add-to-list 'load-path (expand-file-name dir root)))))
+
 (provide 'pg-init)
 ;;; pg-init.el ends here