Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

proof-shell: Don't ask about killing the proof assistant on exit #793

Open
wants to merge 2 commits into
base: master
Choose a base branch
from
Open

proof-shell: Don't ask about killing the proof assistant on exit #793

Show file tree
Hide file tree
Changes from all commits
Commits
Show all changes
2 commits
Select commit Hold shift + click to select a range
739ebaf
improve hints on splash; fix quick options saving
hendriktews Oct 2, 2024
ac5ae12
proof-shell: Don't ask about killing the proof assistant on exit
hendriktews Oct 2, 2024
File filter

Filter by extension

Filter by extension
Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
4 changes: 4 additions & 0 deletions CHANGES
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -19,6 +19,10 @@ 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
*** Don't ask about killing the proof assistant when quitting Proof General.

** Coq changes
*** support Coq 8.19
Expand Down
19 changes: 12 additions & 7 deletions doc/ProofGeneral.texi
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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
Expand Down Expand Up @@ -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.@*
Expand Down
28 changes: 26 additions & 2 deletions generic/proof-menu.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -25,6 +25,7 @@
(require 'proof-utils) ; proof-deftoggle, proof-eval-when-ready-for-assistant
(require 'proof-useropts)
(require 'proof-config)
(require 'proof-splash)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;
;;;
Expand Down Expand Up @@ -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)))

Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down Expand Up @@ -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"]
Expand Down Expand Up @@ -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
Expand All @@ -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
Expand Down
5 changes: 5 additions & 0 deletions generic/proof-shell.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -477,6 +477,11 @@ process command."
(erase-buffer)
(proof-shell-set-text-representation)

;; If one quits Proof General, it's clear that the proof
;; assistant needs to be killed - don't ask.
Comment on lines +480 to +481
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

On the one hand I agree with your remark;
but on the other hand I believe changing would be not "uniform" w.r.t. other emacs features?

e.g. if we do M-x shell RET
then C-x C-s, exactly as you say, "if we quit emacs, it's clear that the nested shell needs to be killed", but emacs will still ask for confirmation.

Would you agree to customize this?

(set-process-query-on-exit-flag
(get-buffer-process proof-shell-buffer) nil)

;; Initialise associated buffers
(with-current-buffer proof-response-buffer
(erase-buffer)
Expand Down
16 changes: 11 additions & 5 deletions generic/proof-splash.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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.
Expand Down Expand Up @@ -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
Expand Down
7 changes: 7 additions & 0 deletions generic/proof-useropts.el
View file
Open in desktop
Original file line number Diff line number Diff line change
Expand Up @@ -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)
Expand Down
Loading