From 739ebafc17e8b8974999bd5c9e6e53f6520ab6f7 Mon Sep 17 00:00:00 2001 From: Hendrik Tews Date: Wed, 2 Oct 2024 09:58:48 +0200 Subject: [PATCH] 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 ea0f007c - adapt manual --- CHANGES | 3 +++ doc/ProofGeneral.texi | 19 ++++++++++++------- generic/proof-menu.el | 28 ++++++++++++++++++++++++++-- generic/proof-splash.el | 16 +++++++++++----- generic/proof-useropts.el | 7 +++++++ 5 files changed, 59 insertions(+), 14 deletions(-) diff --git a/CHANGES b/CHANGES index 8e7720739..a02a77709 100644 --- a/CHANGES +++ b/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 diff --git a/doc/ProofGeneral.texi b/doc/ProofGeneral.texi index acaed3617..e960a7654 100644 --- a/doc/ProofGeneral.texi +++ b/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.@* diff --git a/generic/proof-menu.el b/generic/proof-menu.el index 09b6c3d51..db2a3b9d5 100644 --- a/generic/proof-menu.el +++ b/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 diff --git a/generic/proof-splash.el b/generic/proof-splash.el index 340cf3e50..e6ddadf82 100644 --- a/generic/proof-splash.el +++ b/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 diff --git a/generic/proof-useropts.el b/generic/proof-useropts.el index eb0e497c4..d14f29861 100644 --- a/generic/proof-useropts.el +++ b/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)