diff options
-rw-r--r-- | generic/proof-site.el | 35 |
1 files changed, 9 insertions, 26 deletions
diff --git a/generic/proof-site.el b/generic/proof-site.el index 2fa193c6..af59ff34 100644 --- a/generic/proof-site.el +++ b/generic/proof-site.el @@ -129,17 +129,13 @@ You can use customize to set this variable." (require 'proof-autoloads) ;; Add the info directory to the Info path -(if ;; NB: proof-info-directory is bogus in RPM distrib. - (file-exists-p proof-info-directory) - (if (and (boundp 'Info-directory-list) (consp Info-directory-list)) +(if (file-exists-p proof-info-directory) ; for safety + (if (and (boundp 'Info-directory-list) Info-directory-list) ;; Info is already initialized. Update its variables. - ;; This probably never happens in Emacs, but does in XEmacs. - (if (not (member proof-info-directory Info-directory-list)) - (progn - (add-to-list 'Info-directory-list proof-info-directory) - (setq Info-dir-contents nil))) + (progn + (add-to-list 'Info-directory-list proof-info-directory) + (setq Info-dir-contents nil)) ;; Info is not yet initialized. Change its default. - ;; Emacs uses Info-default-directory-list but it's deprecated in XEmacs (add-to-list 'Info-default-directory-list proof-info-directory))) (defcustom proof-assistant-table @@ -218,18 +214,7 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'." sname)) (cusgrp-rt ;; Normalized a bit to remove spaces and funny characters - ;; FIXME UGLY compatibility hack - ;; (can use cl macro `substitute' but want to avoid cl here) - ;; NOTE: GNU Emacs 22/XEmacs 21.5 both have replace-regexp-in-string - ;; PG 3.8: move version forward here. - (if (fboundp 'replace-in-string) - ;; XEmacs - (replace-in-string (downcase assistant-name) "/\\|[ \t]+" "-") - ;; GNU Emacs - (subst-char-in-string - ?/ ?\- - (subst-char-in-string ?\ ?\- (downcase assistant-name))))) - ;; END compatibility hack + (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! @@ -293,8 +278,7 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'." (proofgen-mode (intern (concat sname "-mode"))) ;; NB: Customization group for each prover is its l.c.'d name! - ;; Stub to do some automatic initialization and load - ;; the specific code. + ;; Stub to initialize and load specific code. (mode-stub `(lambda () ,(concat @@ -302,9 +286,8 @@ If ASSISTANT-NAME is omitted, look up in `proof-assistant-table'." assistant-name ".\nThis is a stub which loads the real function.") (interactive) - ;; Give a message and stop loading if proof-assistant is - ;; already set: things go wrong if proof general is - ;; loaded for more than one prover. + ;; Stop loading if proof-assistant is already set: + ;; cannot work for more than one prover. (cond ((and (boundp 'proof-assistant) (not (string-equal proof-assistant ""))) |