diff options
Diffstat (limited to 'generic/proof-site.el')
| -rw-r--r-- | generic/proof-site.el | 57 |
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 |