Reduce the impact of proof-site, in case PG is not used

* generic/proof-autoloads.el: Remove `require`s; not needed.
* generic/proof-site.el: Don't require `pg-vars`.
(proof-ready-for-assistant): Move to proof-script.el.

* generic/proof-menu.el (proof-assistant-format): Make dynamically
scoped var explicit (preparation for lexical-binding).

* generic/proof-script.el: Require `pg-vars`.
(proof-ready-for-assistant): Move from proof-site.el.

* generic/proof-syntax.el (proof-replace-regexp-in-string):
* generic/proof-shell.el (proof-shell-live-buffer): Don't mark it
as inlinable: it's not performance sensitive.

1 files changed, 3 insertions, 54 deletions

diff --git a/generic/proof-site.el b/generic/proof-site.el
index 7c185b2f..5fb9cdb8 100644
--- a/generic/proof-site.el
+++ b/generic/proof-site.el
@@ -165,8 +165,9 @@ You can use customize to set this variable."
 
 ;; Declare some global variables and autoloads
 
-
-(require 'pg-vars)
+;; FIXME: Many of the autoloaded functions in there are internal to PG, and
+;; are useless until PG is loaded, so they shouldn't be defined just because
+;; proof-site is loaded!
 (require 'proof-autoloads)
 
 (defvar Info-dir-contents)
@@ -250,58 +251,6 @@ Note: to change proof assistant, you must start a new Emacs session.")
 		      proof-assistant-table))
   :group 'proof-general)
 
-;;;###autoload
-(defun proof-ready-for-assistant (assistantsym &optional assistant-name)
-  "Configure PG for symbol ASSISTANTSYM, name ASSISTANT-NAME.
-If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'."
-  (unless proof-assistant-symbol
-    (let*
-      ((sname		 (symbol-name assistantsym))
-       (assistant-name   (or assistant-name
-			     (car-safe
-			      (cdr-safe (assoc assistantsym
-					       proof-assistant-table)))
-			     sname))
-       (cusgrp-rt
-	;; Normalized a bit to remove spaces and funny characters
-	(replace-regexp-in-string "/\\|[ \t]+" "-" (downcase assistant-name)))
-       (cusgrp	      (intern cusgrp-rt))
-       (cus-internals (intern (concat cusgrp-rt "-config")))
-       (elisp-dir     sname)		; NB: dirname same as symbol name!
-       (loadpath-elt  (concat proof-home-directory elisp-dir "/")))
-    (eval `(progn
-       ;; Make a customization group for this assistant
-       (defgroup ,cusgrp nil
-	 ,(concat "Customization of user options for " assistant-name
-		  " Proof General.")
-	 :group 'proof-general)
-       ;; And another one for internals
-       (defgroup ,cus-internals nil
-	 ,(concat "Customization of internal settings for "
-		  assistant-name " configuration.")
-	 :group 'proof-general-internals
-	 :prefix ,(concat sname "-"))
-
-       ;; Set the proof-assistant configuration variables
-       ;; NB: tempting to use customize-set-variable: wrong!
-       ;; Here we treat customize as extended docs for these
-       ;; variables.
-       (setq proof-assistant-cusgrp (quote ,cusgrp))
-       (setq proof-assistant-internals-cusgrp (quote ,cus-internals))
-       (setq proof-assistant ,assistant-name)
-       (setq proof-assistant-symbol (quote ,assistantsym))
-       ;; define the per-prover settings which depend on above
-       (require 'pg-custom)
-       (setq proof-mode-for-shell (proof-ass-sym shell-mode))
-       (setq proof-mode-for-response (proof-ass-sym response-mode))
-       (setq proof-mode-for-goals (proof-ass-sym goals-mode))
-       (setq proof-mode-for-script (proof-ass-sym mode))
-       ;; Extend the load path if necessary
-       (proof-add-to-load-path ,loadpath-elt)
-       ;; Run hooks for late initialisation
-       (run-hooks 'proof-ready-for-assistant-hook))))))
-
-
 (defvar proof-general-configured-provers
   (or (mapcar 'intern (split-string (or (getenv "PROOFGENERAL_ASSISTANTS") "")))
       proof-assistants