diff options
| -rw-r--r-- | generic/proof-menu.el | 14 | ||||
| -rw-r--r-- | generic/proof-shell.el | 8 |
2 files changed, 14 insertions, 8 deletions
diff --git a/generic/proof-menu.el b/generic/proof-menu.el index daa5bdc3..1838a723 100644 --- a/generic/proof-menu.el +++ b/generic/proof-menu.el @@ -807,14 +807,22 @@ evaluate can be provided instead." ;; Could also repeat last command if non-state destroying. ))) +(defun proof-maybe-askprefs () + "If `proof-assistant-settings' is unset, try to issue <askprefs>" + (if (and (not proof-assistant-settings) + proof-shell-issue-pgip-cmd) + (pg-pgip-askprefs))) + (defun proof-assistant-settings-cmd (&optional setting) "Return string for settings kept in Proof General customizations. If SETTING is non-nil, return a string for just that setting. Otherwise return a string for configuring all settings. - -If `proof-assistant-settings' is nil and PGIP is supported, then -first we query settings information from prover." +NB: if no settings are configured, we try to do <askprefs> first." + ;; NB: it may seem like this next line is unnecessary because we do + ;; proof-maybe-askprefs also in proof-shell-config-done. But + ;; the + (proof-maybe-askprefs) (let ((evalifneeded (lambda (expr) (if (and (cadr expr) ;; setting has PA string? diff --git a/generic/proof-shell.el b/generic/proof-shell.el index 88e1d0ac..3f8273bd 100644 --- a/generic/proof-shell.el +++ b/generic/proof-shell.el @@ -1,6 +1,6 @@ ; proof-shell.el Proof General shell mode. ;; -;; Copyright (C) 1994-2002 LFCS Edinburgh. +;; Copyright (C) 1994-2004 LFCS Edinburgh. ;; Authors: David Aspinall, Yves Bertot, Healfdene Goguen, ;; Thomas Kleymann and Dilip Sequeira ;; License: GPL (GNU GENERAL PUBLIC LICENSE) @@ -2037,10 +2037,8 @@ processing." ;; preferences are not configured, we may configure them. ;; (NB: this assumes that PGIP provers are ready-to-go, without ;; needing init-cmd before PGIP processing). We do - ;; this so that preferences may be set in proof-shell-init-cmd. - (if (and (not proof-assistant-settings) - proof-shell-issue-pgip-cmd) - (pg-pgip-askprefs)) + ;; this so that user preferences may be set in proof-shell-init-cmd. + (proof-maybe-askprefs) ;; Now send the init cmd proper. (if proof-shell-init-cmd (proof-shell-invisible-command proof-shell-init-cmd t)) |