improve hints on splash; fix quick options saving

- add menu entry to disable splash screen to quick options
- add info to the splash screen on how to leave and disable the splash
  screen
- add Proof-General menu to splash screen, such that the hints on the
  splash screen make sense
- fix saving of quick options for several options
- the CHANGES entry also describes commit ea0f007
- adapt manual

CHANGES

@@ -19,6 +19,9 @@ the Git ChangeLog, the GitHub repo https://github.com/ProofGeneral/PG
     changes below for more details.
 *** New command `proof-check-annotate' to annotate all failing proofs
     with FAIL comments.
+*** Improve splash screen, add menu entry to permanently disable it
+    (Proof-General -> Quick Options -> Display -> Disable Splash Screen),
+    reduce splash screen time to make it less annoying
 
 ** Coq changes
 *** support Coq 8.19

doc/ProofGeneral.texi

@@ -3567,6 +3567,18 @@ on the menu:
 @end lisp
 and you can save your preferred default. 
 
+The first option presented here is about the splash screen, which is
+shown by default on every launch of Proof General.
+
+@c TEXI DOCSTRING MAGIC: proof-splash-enable
+@defopt proof-splash-enable 
+If non-nil, display a splash screen when Proof General is loaded.@*
+See @samp{@code{proof-splash-time}} for configuring the time that the splash
+screen is shown.
+
+The default value is @code{t}.
+@end defopt
+
 If your screen is large enough, you may prefer to display all three of
 the interaction buffers at once.  This is useful, for example, to see
 output from the @code{proof-find-theorems} command at the same time as
@@ -3775,13 +3787,6 @@ Unless mentioned, all of these settings can be changed dynamically,
 without needing to restart Emacs to see the effect.  But you must use
 customize to be sure that Proof General reconfigures itself properly.
 
-@c TEXI DOCSTRING MAGIC: proof-splash-enable
-@defopt proof-splash-enable 
-If non-nil, display a splash screen when Proof General is loaded.
-
-The default value is @code{t}.
-@end defopt
-
 @c TEXI DOCSTRING MAGIC: proof-electric-terminator-enable
 @defopt proof-electric-terminator-enable 
 If non-nil, use electric terminator mode.@*

generic/proof-menu.el

@@ -25,6 +25,7 @@
 (require 'proof-utils)    ; proof-deftoggle, proof-eval-when-ready-for-assistant
 (require 'proof-useropts)
 (require 'proof-config)
+(require 'proof-splash)
 
 ;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
 ;;;
@@ -151,11 +152,21 @@ without adjusting window layout."
 
 ;; The main Proof-General generic menu
 
+;; Show the generic menu in `proof-mode' and modes derived from that
+;; (e.g., `coq-mode'). Show the menu also in `proof-splash-mode', such
+;; that the menu entries that the splash screen describes are
+;; accessible when viewing the splash screen.
+
+;; IMPORTANT: In order to make the `proof-quick-opts-save' and menu
+;; Proof-General -> Quick Options -> Save Options work, user options
+;; accessible in the menu must be added to `proof-quick-opts-vars'
+;; further below.
+
 ;;;###autoload
 (defun proof-menu-define-main ()
   (easy-menu-define
    proof-mode-menu
-   proof-mode-map
+   (list proof-mode-map proof-splash-mode-map)
    "The main Proof General menu"
    (proof-main-menu)))
 
@@ -335,6 +346,7 @@ without adjusting window layout."
 (proof-deftoggle proof-imenu-enable proof-imenu-toggle)
 (proof-deftoggle proof-keep-response-history)
 (proof-deftoggle proof-omit-proofs-option)
+(proof-deftoggle proof-splash-enable)
 
 (proof-eval-when-ready-for-assistant
  ;; togglers for settings separately configurable per-prover
@@ -356,6 +368,11 @@ without adjusting window layout."
    "Quick Options"
    `(
 
+;; IMPORTANT: In order to make the `proof-quick-opts-save' and menu
+;; Proof-General -> Quick Options -> Save Options work, user options
+;; accessible in the menu must be added to `proof-quick-opts-vars'
+;; further below.
+
 ;;; TODO: Add this in PG 4.0 once bufhist robust; see trac #169
 ;;;      ["Response history" proof-keep-response-history-toggle
 ;;;       :style toggle
@@ -469,6 +486,10 @@ without adjusting window layout."
        :style toggle
        :selected proof-disappearing-proofs
        :help "Hide proofs as they are completed"]
+      ["Disable Splash Screen" proof-splash-enable-toggle
+       :style toggle
+       :selected (not proof-splash-enable)
+       :help "Show splash screen when starting Proof General"]
       "----"
       ["Document Centred" proof-set-document-centred
        :help "Select options for document-centred working"]
@@ -579,6 +600,7 @@ without adjusting window layout."
 (defun proof-quick-opts-vars ()
   "Return a list of the quick option variables."
   (list
+   'proof-omit-proofs-option
    'proof-electric-terminator-enable
    'proof-autosend-enable
    'proof-fast-process-buffer
@@ -594,14 +616,16 @@ without adjusting window layout."
    'proof-shell-quiet-errors
    ;; Display sub-menu
    'proof-minibuffer-messages
+   'proof-output-tooltips
    'proof-auto-raise-buffers
    'proof-three-window-enable
+   'proof-layout-windows-on-visit-file
    'proof-delete-empty-windows
    'proof-multiple-frames-enable
    'proof-shrink-windows-tofit
-   'proof-multiple-frames-enable
    'proof-colour-locked
    'proof-sticky-errors
+   'proof-splash-enable
    ;; Follow mode sub-menu
    'proof-follow-mode
    ;; Deactivate scripting action

generic/proof-splash.el

@@ -32,15 +32,13 @@
 ;;; Code:
 
 (require 'proof-site)
+(require 'proof-useropts)
 
 ;;
 ;; Customization of splash screen
 ;;
 
-(defcustom proof-splash-enable t
-  "*If non-nil, display a splash screen when Proof General is loaded."
-  :type 'boolean
-  :group 'proof-user-options)
+;; see proof-useropts for proof-splash-enable
 
 (defcustom proof-splash-time 1
   "Minimum number of seconds to display splash screen for.
@@ -82,7 +80,15 @@ Proof General."
     :link '("Find out about Emacs on the Help menu -- start with the "
             "Emacs Tutorial" (lambda (button) (help-with-tutorial)))
     nil
-    "See this screen again with Proof-General -> About"
+    "Type q to leave this screen"
+    nil
+    "See this screen again with Proof-General -> Help -> About PG"
+    "or M-x proof-splash-display-screen"
+    nil
+    "To disable this splash screen permanently select"
+    "Proof-General -> Quick Options -> Display -> Disable Splash Screen"
+    "and save via Proof-General -> Quick Options -> Save Options"
+    "or customize proof-splash-enable"
     )
   "Evaluated to configure splash screen displayed when entering Proof General.
 A list of the screen contents.  If an element is a string or an image

generic/proof-useropts.el

@@ -505,6 +505,13 @@ Mac OS X."
   :type 'boolean
   :group 'proof-user-options)
 
+(defcustom proof-splash-enable t
+  "*If non-nil, display a splash screen when Proof General is loaded.
+See `proof-splash-time' for configuring the time that the splash
+screen is shown."
+  :type 'boolean
+  :group 'proof-user-options)
+
 
 
 (provide 'proof-useropts)