aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
authorGravatar Stefan Monnier <monnier@iro.umontreal.ca>2018-12-20 14:47:33 -0500
committerGravatar Stefan Monnier <monnier@iro.umontreal.ca>2018-12-25 14:48:54 -0500
commit7389d43893569ff0e1eff892254901876fc8225e (patch)
treeaff068ef99924c1170a14f876b3fe745dadf2301
parentf7cc8f1f76baf5e517e51f1db47510ed605064e8 (diff)
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.
-rw-r--r--generic/proof-autoloads.el149
-rw-r--r--generic/proof-menu.el7
-rw-r--r--generic/proof-script.el53
-rw-r--r--generic/proof-shell.el3
-rw-r--r--generic/proof-site.el57
-rw-r--r--generic/proof-syntax.el2
6 files changed, 136 insertions, 135 deletions
diff --git a/generic/proof-autoloads.el b/generic/proof-autoloads.el
index 302ad21e..4fb1f907 100644
--- a/generic/proof-autoloads.el
+++ b/generic/proof-autoloads.el
@@ -3,7 +3,7 @@
;; This file is part of Proof General.
;; Portions © Copyright 1994-2012 David Aspinall and University of Edinburgh
-;; Portions © Copyright 2003, 2012, 2014 Free Software Foundation, Inc.
+;; Portions © Copyright 2003-2018 Free Software Foundation, Inc.
;; Portions © Copyright 2001-2017 Pierre Courtieu
;; Portions © Copyright 2010, 2016 Erik Martin-Dorel
;; Portions © Copyright 2011-2013, 2016-2017 Hendrik Tews
@@ -14,17 +14,11 @@
;;; Code:
-
-(eval-when-compile
- (require 'pg-vars)
- (require 'proof-config)
- (require 'scomint))
-
(provide 'proof-autoloads)
-;;;### (autoloads nil "../coq/coq" "../coq/coq.el" (23576 63508 474604
-;;;;;; 77000))
+;;;### (autoloads nil "../coq/coq" "../coq/coq.el" (23586 34852 377773
+;;;;;; 600000))
;;; Generated autoloads from ../coq/coq.el
(autoload 'coq-pg-setup "../coq/coq" "\
@@ -35,7 +29,7 @@
;;;***
;;;### (autoloads nil "../coq/coq-autotest" "../coq/coq-autotest.el"
-;;;;;; (23571 9656 963235 821000))
+;;;;;; (23572 12262 140036 921000))
;;; Generated autoloads from ../coq/coq-autotest.el
(autoload 'coq-autotest "../coq/coq-autotest" "\
@@ -45,8 +39,8 @@
;;;***
-;;;### (autoloads nil "../coq/coq-mode" "../coq/coq-mode.el" (23576
-;;;;;; 63738 715506 60000))
+;;;### (autoloads nil "../coq/coq-mode" "../coq/coq-mode.el" (23586
+;;;;;; 34852 373773 560000))
;;; Generated autoloads from ../coq/coq-mode.el
(add-to-list 'auto-mode-alist '("\\.v\\'" . coq-mode))
@@ -60,8 +54,8 @@ Major mode for Coq scripts.
;;;***
-;;;### (autoloads nil "../lib/bufhist" "../lib/bufhist.el" (23576
-;;;;;; 10253 529610 111000))
+;;;### (autoloads nil "../lib/bufhist" "../lib/bufhist.el" (23586
+;;;;;; 34852 385773 680000))
;;; Generated autoloads from ../lib/bufhist.el
(autoload 'bufhist-mode "../lib/bufhist" "\
@@ -92,8 +86,8 @@ Stop keeping ring history for current buffer.
;;;***
-;;;### (autoloads nil "../lib/holes" "../lib/holes.el" (23569 22945
-;;;;;; 718351 699000))
+;;;### (autoloads nil "../lib/holes" "../lib/holes.el" (23571 60372
+;;;;;; 968579 788000))
;;; Generated autoloads from ../lib/holes.el
(autoload 'holes-set-make-active-hole "../lib/holes" "\
@@ -207,7 +201,7 @@ Insert S, expand it and replace #s and @{]s by holes.
;;;***
;;;### (autoloads nil "../lib/maths-menu" "../lib/maths-menu.el"
-;;;;;; (23575 9250 536416 363000))
+;;;;;; (23577 10400 919305 444000))
;;; Generated autoloads from ../lib/maths-menu.el
(autoload 'maths-menu-mode "../lib/maths-menu" "\
@@ -220,8 +214,8 @@ This mode is only useful with a font which can display the maths repertoire.
;;;***
-;;;### (autoloads nil "pg-assoc" "pg-assoc.el" (23569 41729 794421
-;;;;;; 324000))
+;;;### (autoloads nil "pg-assoc" "pg-assoc.el" (23572 10813 702789
+;;;;;; 96000))
;;; Generated autoloads from pg-assoc.el
(autoload 'proof-associated-buffers "pg-assoc" "\
@@ -245,8 +239,8 @@ Return the list of frames displaying at least one associated buffer.
;;;***
-;;;### (autoloads nil "../lib/pg-dev" "../lib/pg-dev.el" (23575 9250
-;;;;;; 536416 363000))
+;;;### (autoloads nil "../lib/pg-dev" "../lib/pg-dev.el" (23577 10400
+;;;;;; 919305 444000))
;;; Generated autoloads from ../lib/pg-dev.el
(autoload 'profile-pg "../lib/pg-dev" "\
@@ -256,8 +250,8 @@ Configure Proof General for profiling. Use \\[elp-results] to see results.
;;;***
-;;;### (autoloads nil "pg-goals" "pg-goals.el" (23575 9250 532416
-;;;;;; 428000))
+;;;### (autoloads nil "pg-goals" "pg-goals.el" (23577 10400 911305
+;;;;;; 269000))
;;; Generated autoloads from pg-goals.el
(autoload 'proof-goals-config-done "pg-goals" "\
@@ -267,8 +261,8 @@ Initialise the goals buffer after the child has been configured.
;;;***
-;;;### (autoloads nil "pg-movie" "pg-movie.el" (23575 9223 344856
-;;;;;; 367000))
+;;;### (autoloads nil "pg-movie" "pg-movie.el" (23572 12305 412526
+;;;;;; 903000))
;;; Generated autoloads from pg-movie.el
(autoload 'pg-movie-export "pg-movie" "\
@@ -290,8 +284,8 @@ Existing XML files are overwritten.
;;;***
-;;;### (autoloads nil "pg-pamacs" "pg-pamacs.el" (23576 62945 258166
-;;;;;; 137000))
+;;;### (autoloads nil "pg-pamacs" "pg-pamacs.el" (23577 10400 915305
+;;;;;; 356000))
;;; Generated autoloads from pg-pamacs.el
(autoload 'proof-defpacustom-fn "pg-pamacs" "\
@@ -341,7 +335,8 @@ This macro also extends the `proof-assistant-settings' list.
;;;***
-;;;### (autoloads nil "pg-pgip" "pg-pgip.el" (23575 9250 532416 428000))
+;;;### (autoloads nil "pg-pgip" "pg-pgip.el" (23577 10400 915305
+;;;;;; 356000))
;;; Generated autoloads from pg-pgip.el
(autoload 'pg-pgip-process-packet "pg-pgip" "\
@@ -362,8 +357,8 @@ Send an <askprefs> message to the prover.
;;;***
-;;;### (autoloads nil "pg-response" "pg-response.el" (23569 41729
-;;;;;; 794421 324000))
+;;;### (autoloads nil "pg-response" "pg-response.el" (23572 10813
+;;;;;; 706789 146000))
;;; Generated autoloads from pg-response.el
(autoload 'proof-response-mode "pg-response" "\
@@ -432,7 +427,8 @@ See `pg-next-error-regexp'.
;;;***
-;;;### (autoloads nil "pg-user" "pg-user.el" (23571 8540 515663 574000))
+;;;### (autoloads nil "pg-user" "pg-user.el" (23572 12262 148037
+;;;;;; 11000))
;;; Generated autoloads from pg-user.el
(autoload 'proof-script-new-command-advance "pg-user" "\
@@ -559,7 +555,7 @@ Enable or disable autosend behaviour.
;;;***
-;;;### (autoloads nil "pg-xml" "pg-xml.el" (23569 49953 922153 72000))
+;;;### (autoloads nil "pg-xml" "pg-xml.el" (23572 10813 706789 146000))
;;; Generated autoloads from pg-xml.el
(autoload 'pg-xml-parse-string "pg-xml" "\
@@ -569,8 +565,8 @@ Parse string in ARG, same as pg-xml-parse-buffer.
;;;***
-;;;### (autoloads nil "proof-depends" "proof-depends.el" (23575 9250
-;;;;;; 532416 428000))
+;;;### (autoloads nil "proof-depends" "proof-depends.el" (23577 10400
+;;;;;; 915305 356000))
;;; Generated autoloads from proof-depends.el
(autoload 'proof-depends-process-dependencies "proof-depends" "\
@@ -588,7 +584,7 @@ Make some menu entries showing proof dependencies of SPAN.
;;;***
;;;### (autoloads nil "proof-easy-config" "proof-easy-config.el"
-;;;;;; (23548 4656 374888 298000))
+;;;;;; (23553 26684 846646 250000))
;;; Generated autoloads from proof-easy-config.el
(autoload 'proof-easy-config "proof-easy-config" "\
@@ -601,8 +597,8 @@ Additional arguments are taken into account as a setq BODY.
;;;***
-;;;### (autoloads nil "proof-indent" "proof-indent.el" (23548 4656
-;;;;;; 374888 298000))
+;;;### (autoloads nil "proof-indent" "proof-indent.el" (23553 26684
+;;;;;; 846646 250000))
;;; Generated autoloads from proof-indent.el
(autoload 'proof-indent-line "proof-indent" "\
@@ -612,8 +608,8 @@ Indent current line of proof script, if indentation enabled.
;;;***
-;;;### (autoloads nil "proof-maths-menu" "proof-maths-menu.el" (23575
-;;;;;; 9250 532416 428000))
+;;;### (autoloads nil "proof-maths-menu" "proof-maths-menu.el" (23577
+;;;;;; 10400 915305 356000))
;;; Generated autoloads from proof-maths-menu.el
(autoload 'proof-maths-menu-set-global "proof-maths-menu" "\
@@ -633,8 +629,8 @@ in future if we have just activated it for this buffer.
;;;***
-;;;### (autoloads nil "proof-menu" "proof-menu.el" (23576 8979 193466
-;;;;;; 461000))
+;;;### (autoloads nil "proof-menu" "proof-menu.el" (23586 34852 449774
+;;;;;; 323000))
;;; Generated autoloads from proof-menu.el
(autoload 'proof-menu-define-keys "proof-menu" "\
@@ -659,10 +655,16 @@ Construct and return PG auxiliary menu used in non-scripting buffers.
;;;***
-;;;### (autoloads nil "proof-script" "proof-script.el" (23576 11228
-;;;;;; 990682 355000))
+;;;### (autoloads nil "proof-script" "proof-script.el" (23586 34852
+;;;;;; 461774 443000))
;;; Generated autoloads from proof-script.el
+(autoload 'proof-ready-for-assistant "proof-script" "\
+Configure PG for symbol ASSISTANTSYM, name ASSISTANT-NAME.
+If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'.
+
+\(fn ASSISTANTSYM &optional ASSISTANT-NAME)" nil nil)
+
(autoload 'proof-colour-locked "proof-script" "\
Alter the colour of all locked regions according to variable `proof-colour-locked'.
@@ -749,8 +751,8 @@ finish setup which depends on specific proof assistant configuration.
;;;***
-;;;### (autoloads nil "proof-shell" "proof-shell.el" (23575 9250
-;;;;;; 532416 428000))
+;;;### (autoloads nil "proof-shell" "proof-shell.el" (23586 34852
+;;;;;; 449774 323000))
;;; Generated autoloads from proof-shell.el
(autoload 'proof-shell-ready-prover "proof-shell" "\
@@ -762,8 +764,10 @@ No change to current buffer or point.
\(fn &optional QUEUEMODE)" nil nil)
-(defsubst proof-shell-live-buffer nil "\
-Return non-nil if ‘proof-shell-buffer’ is live." (and proof-shell-buffer (buffer-live-p proof-shell-buffer) (scomint-check-proc proof-shell-buffer)))
+(autoload 'proof-shell-live-buffer "proof-shell" "\
+Return non-nil if ‘proof-shell-buffer’ is live.
+
+\(fn)" nil nil)
(autoload 'proof-shell-available-p "proof-shell" "\
Return non-nil if there is a proof shell active and available.
@@ -883,20 +887,8 @@ processing.
;;;***
-;;;### (autoloads nil "proof-site" "proof-site.el" (23576 62228 993634
-;;;;;; 734000))
-;;; Generated autoloads from proof-site.el
-
-(autoload 'proof-ready-for-assistant "proof-site" "\
-Configure PG for symbol ASSISTANTSYM, name ASSISTANT-NAME.
-If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'.
-
-\(fn ASSISTANTSYM &optional ASSISTANT-NAME)" nil nil)
-
-;;;***
-
-;;;### (autoloads nil "proof-splash" "proof-splash.el" (23576 11450
-;;;;;; 619317 210000))
+;;;### (autoloads nil "proof-splash" "proof-splash.el" (23586 34852
+;;;;;; 381773 640000))
;;; Generated autoloads from proof-splash.el
(autoload 'proof-splash-display-screen "proof-splash" "\
@@ -914,12 +906,14 @@ Make sure the user gets welcomed one way or another.
;;;***
-;;;### (autoloads nil "proof-syntax" "proof-syntax.el" (23576 8794
-;;;;;; 396386 343000))
+;;;### (autoloads nil "proof-syntax" "proof-syntax.el" (23586 34852
+;;;;;; 453774 363000))
;;; Generated autoloads from proof-syntax.el
-(defsubst proof-replace-regexp-in-string (regexp rep string) "\
-Like ‘replace-regexp-in-string’, but set ‘case-fold-search’ to ‘proof-case-fold-search’." (let ((case-fold-search proof-case-fold-search)) (replace-regexp-in-string regexp rep string)))
+(autoload 'proof-replace-regexp-in-string "proof-syntax" "\
+Like ‘replace-regexp-in-string’, but set ‘case-fold-search’ to ‘proof-case-fold-search’.
+
+\(fn REGEXP REP STRING)" nil nil)
(autoload 'proof-format "proof-syntax" "\
Format a string by matching regexps in ALIST against STRING.
@@ -930,8 +924,8 @@ may be a string or sexp evaluated to get a string.
;;;***
-;;;### (autoloads nil "proof-toolbar" "proof-toolbar.el" (23548 4656
-;;;;;; 378888 227000))
+;;;### (autoloads nil "proof-toolbar" "proof-toolbar.el" (23553 26684
+;;;;;; 850646 288000))
;;; Generated autoloads from proof-toolbar.el
(autoload 'proof-toolbar-setup "proof-toolbar" "\
@@ -950,7 +944,7 @@ Menu made from the Proof General toolbar commands.
;;;***
;;;### (autoloads nil "proof-unicode-tokens" "proof-unicode-tokens.el"
-;;;;;; (23575 9250 536416 363000))
+;;;;;; (23577 10400 919305 444000))
;;; Generated autoloads from proof-unicode-tokens.el
(autoload 'proof-unicode-tokens-mode-if-enabled "proof-unicode-tokens" "\
@@ -977,8 +971,8 @@ is changed.
;;;***
-;;;### (autoloads nil "proof-utils" "proof-utils.el" (23576 62534
-;;;;;; 353957 67000))
+;;;### (autoloads nil "proof-utils" "proof-utils.el" (23586 34852
+;;;;;; 381773 640000))
;;; Generated autoloads from proof-utils.el
(autoload 'proof-debug "proof-utils" "\
@@ -989,8 +983,8 @@ If flag `proof-general-debug' is nil, do nothing.
;;;***
-;;;### (autoloads nil "../lib/scomint" "../lib/scomint.el" (23575
-;;;;;; 9250 536416 363000))
+;;;### (autoloads nil "../lib/scomint" "../lib/scomint.el" (23577
+;;;;;; 10400 919305 444000))
;;; Generated autoloads from ../lib/scomint.el
(autoload 'scomint-make-in-buffer "../lib/scomint" "\
@@ -1022,7 +1016,7 @@ If PROGRAM is a string, the remaining SWITCHES are arguments to PROGRAM.
;;;***
;;;### (autoloads nil "../lib/texi-docstring-magic" "../lib/texi-docstring-magic.el"
-;;;;;; (23575 9250 536416 363000))
+;;;;;; (23577 10400 919305 444000))
;;; Generated autoloads from ../lib/texi-docstring-magic.el
(autoload 'texi-docstring-magic "../lib/texi-docstring-magic" "\
@@ -1035,7 +1029,7 @@ With prefix arg, no errors on unknown symbols. (This results in
;;;***
;;;### (autoloads nil "../lib/unicode-chars" "../lib/unicode-chars.el"
-;;;;;; (23548 4656 382888 158000))
+;;;;;; (23553 26684 902646 787000))
;;; Generated autoloads from ../lib/unicode-chars.el
(autoload 'unicode-chars-list-chars "../lib/unicode-chars" "\
@@ -1048,7 +1042,7 @@ in your Emacs font.
;;;***
;;;### (autoloads nil "../lib/unicode-tokens" "../lib/unicode-tokens.el"
-;;;;;; (23575 9250 540416 298000))
+;;;;;; (23577 10400 923305 531000))
;;; Generated autoloads from ../lib/unicode-tokens.el
(autoload 'unicode-tokens-encode-str "../lib/unicode-tokens" "\
@@ -1065,8 +1059,9 @@ Return a unicode encoded version presentation of STR.
;;;;;; "../coq/coq-unicode-tokens.el" "../lib/local-vars-list.el"
;;;;;; "../lib/pg-fontsets.el" "../lib/proof-compat.el" "../lib/span.el"
;;;;;; "pg-autotest.el" "pg-custom.el" "pg-pbrpm.el" "pg-vars.el"
-;;;;;; "proof-auxmodes.el" "proof-config.el" "proof-faces.el" "proof-tree.el"
-;;;;;; "proof-useropts.el" "proof.el") (23577 1104 283265 664000))
+;;;;;; "proof-auxmodes.el" "proof-config.el" "proof-faces.el" "proof-site.el"
+;;;;;; "proof-tree.el" "proof-useropts.el" "proof.el") (23586 34852
+;;;;;; 457774 403000))
;;;***
diff --git a/generic/proof-menu.el b/generic/proof-menu.el
index dd3d05c8..2900a6b1 100644
--- a/generic/proof-menu.el
+++ b/generic/proof-menu.el
@@ -1006,7 +1006,7 @@ We first clear the dynamic settings from `proof-assistant-settings'."
(cons "%f" '(proof-assistant-format-float curvalue))
(cons "%s" '(proof-assistant-format-string curvalue)))
"Table to use with `proof-format' for formatting CURVALUE for assistant.
-NB: variable curvalue is dynamically scoped (used in `proof-assistant-format').")
+NB: variable `curvalue' is dynamically scoped (used in `proof-assistant-format').")
(defun proof-assistant-format-bool (value)
(if value proof-assistant-true-value proof-assistant-false-value))
@@ -1034,7 +1034,10 @@ value) and the second for false."
(let ((setting
(cond
((stringp string) ;; use % format characters
- (proof-format proof-assistant-format-table string))
+ ;; Dynbind for use in proof-assistant-format-table!
+ (with-no-warnings (defvar curvalue))
+ (let ((curvalue curvalue))
+ (proof-format proof-assistant-format-table string)))
((functionp string) ;; call the function
(funcall string curvalue))
((consp string) ;; true/false options
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)
diff --git a/generic/proof-shell.el b/generic/proof-shell.el
index 6287629c..a0e80fa7 100644
--- a/generic/proof-shell.el
+++ b/generic/proof-shell.el
@@ -221,10 +221,11 @@ No change to current buffer or point."
(error "Proof process busy!")))
;;;###autoload
-(defsubst proof-shell-live-buffer ()
+(defun proof-shell-live-buffer ()
"Return non-nil if ‘proof-shell-buffer’ is live."
(and proof-shell-buffer
(buffer-live-p proof-shell-buffer)
+ ;; FIXME: Use process-live-p?
(scomint-check-proc proof-shell-buffer)))
;;;###autoload
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
diff --git a/generic/proof-syntax.el b/generic/proof-syntax.el
index 2ba6b7b6..777d3858 100644
--- a/generic/proof-syntax.el
+++ b/generic/proof-syntax.el
@@ -65,7 +65,7 @@ nil if a region cannot be found."
(search-forward string bound noerror count)))
;;;###autoload
-(defsubst proof-replace-regexp-in-string (regexp rep string)
+(defun proof-replace-regexp-in-string (regexp rep string)
"Like ‘replace-regexp-in-string’, but set ‘case-fold-search’ to ‘proof-case-fold-search’."
(let ((case-fold-search proof-case-fold-search))
(replace-regexp-in-string regexp rep string)))