diff options
| -rw-r--r-- | doc/docstring-magic.el | 20 |
1 files changed, 19 insertions, 1 deletions
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") |