From 7389d43893569ff0e1eff892254901876fc8225e Mon Sep 17 00:00:00 2001 From: Stefan Monnier Date: Thu, 20 Dec 2018 14:47:33 -0500 Subject: 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. --- generic/proof-script.el | 53 +++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 53 insertions(+) (limited to 'generic/proof-script.el') diff --git a/generic/proof-script.el b/generic/proof-script.el index 178477cf..aa9841f0 100644 --- a/generic/proof-script.el +++ b/generic/proof-script.el @@ -26,6 +26,7 @@ (require 'cl-lib) ; various (require 'span) ; abstraction of overlays/extents +(require 'pg-vars) (require 'proof-utils) ; proof-utils macros (require 'proof-syntax) ; utils for manipulating syntax @@ -66,6 +67,58 @@ kill buffer hook. This variable is used when buffer-file-name is nil.") (deflocal pg-script-portions nil "Alist of hash tables for symbols naming processed script portions.") +;;;###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)))))) + + (defalias 'proof-active-buffer-fake-minor-mode 'proof-toggle-active-scripting) -- cgit v1.2.3