From 58d6ec212c96cfd1f3ace6e8be16b1c46c66c718 Mon Sep 17 00:00:00 2001
From: Hendrik Tews
Date: Sun, 24 Jan 2021 12:09:25 +0100
Subject: fix another make magic problem from 2018

In 7389d43893569ff0e1eff892254901876fc8225e
proof-ready-for-assistant was moved to proof-script.el, breaking
make magic in a complicated chain. The auto load for
proof-ready-for-assistant caused proof-script.el to be loaded
before proof-assistant was set, causing
proof-eval-when-ready-for-assistant, to put stuff into
proof-ready-for-assistant-hook. proof-ready-for-assistant loads
pg-custom.el by require, therefore, for the first proof assistant
in the loop in docstring-magic everything was defined when
executing the hooks at the end of proof-ready-for-assistant. The
second assistant caused errors than.

Fixes #542
---
 doc/docstring-magic.el | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

(limited to 'doc/docstring-magic.el')

diff --git a/doc/docstring-magic.el b/doc/docstring-magic.el
index 2943dd9f..7ff84883 100644
--- a/doc/docstring-magic.el
+++ b/doc/docstring-magic.el
@@ -48,17 +48,35 @@
 	 (sname		 (symbol-name assistant))
 	 (elisp-file   sname))
       (setq proof-assistant-symbol nil)
+
+      ;; proof-ready-for-assistant below loads pg-custom by require.
+      ;; pg-custom must be loaded for each proof assistant again,
+      ;; because it defines a lot with defpgcustom, which defines
+      ;; assistent specific variables by using assistant-symbol
+      ;; (called assistant here). Therefore, delete pg-custom from the
+      ;; featue list here, such that it is also loaded for the second
+      ;; proof assistant. Otherwise (proof-ass keymap) would fail
+      ;; because the symbol is not defined for the second proof
+      ;; assistant. And (proof-ass keymap) is put into
+      ;; proof-ready-for-assistant-hook by
+      ;; proof-eval-when-ready-for-assistant, when proof-script is
+      ;; loaded as autoload for proof-ready-for-assistant, because
+      ;; then proof-assistant is not yet set.
+      (setq features (delete 'pg-custom features))
       (proof-ready-for-assistant assistant assistant-name)
       ;; Must load proof-config each time to define proof assistant
       ;; specific variables
       (setq features (delete 'pg-custom features))
-      (load "pg-custom.el")
       (load-library elisp-file)
       (setq assistants (cdr assistants)))))
 
 ;; Now a fake proof assistant to document the automatically
 ;; specific variables
 (setq proof-assistant-symbol nil)
+
+;; ensure again, pg-custom is loaded inside proof-ready-for-assistant,
+;; see above
+(setq features (delete 'pg-custom features))
 (proof-ready-for-assistant 'PA "PROOF ASSISTANT")
 (setq features (delete 'pg-custom features))
 (load "pg-custom.el")
-- 
cgit v1.2.3