improve hints on splash; fix quick options saving

[hendriktews]

• 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

[hendriktews]

@Matafou @erikmd : With the information about how to disable the splash screen present on the splash screen, I think we can and also should increase the splash screen time again, maybe 3 or 4 seconds. With 1 second, it is impossible to see that there is information about how to disable it. What do you think? Having said that, I don't care too much and we can also leave as is -- I have disabled the splash screen for decades already.

[erikmd]

With the information about how to disable the splash screen present on the splash screen, I think we can and also should increase the splash screen time again, maybe 3 or 4 seconds. With 1 second, it is impossible to see that there is information about how to disable it. What do you think?

IMHO, I would not come back to a 3--4 seconds delay:

I would just disable the splash feature by default, or ideally (to be less "aggressive") modify the splash feature so that the *Proof General Welcome* buffer is still created, but in the background (i.e. similarly to calling M-x bury-buffer RET). Both approaches would be an acceptable workaround to me. WDYT?

[monnier]

FWIW, I'd vote to remove the splash screen.

I think it makes sense to display such a thing when the users ask "About Proof-General" or in response to a M-x proof-general command (maybe from which the user could choose different backends or some such), but doing it when opening a .v file is more annoying (and difficult to implement robustly) than it's worth.

For the record, I disabled it the first time I tried to use PG because it caused an error in my setup, probably due to either my minibuffer-only frame or my dedicated windows (I never bothered to track it down nor try and see if it had been fixed in the mean time).

[Matafou]

Agreed. A "about" command would be better.

[erikmd]

Hi, I was about to merge #793, where the discussion "converged", but I see that PR was built upon this PR #791, where the discussion stalled a bit.

To sum up, no one objected to "improving" the splash screen. Also, it was suggested to simply remove it. Actually I'd like to propose to merge this working solution for now (both PRs), and later on if we discuss this once more, we could remove it in another PR if everyone agrees.

So, if no one objects, I will merge #791 then #793 at the end of the week. Cc @ProofGeneral/core

[erikmd]

@Matafou approved this PR #791; @hendriktews do you also agree? or you would actually favor a more abrupt solution, where we disable the splash screen / make it opt-in?

[hendriktews]

Rebased to master, I'll merge when the tests are fine. I am in favor of not showing the splash screen on start as suggested here in the discussion. However, with the option of this PR to disable the splash screen, I don't feel motivated to work on this.

[Matafou]

Yes let us merge this and if someone feels motivated to replace it by a About buffer, feel free.