ProofGeneral / PG

This repo is the new home of Proof General
https://proofgeneral.github.io
GNU General Public License v3.0
492 stars 89 forks source link

improve hints on splash; fix quick options saving #791

Open hendriktews opened 1 month ago

hendriktews commented 1 month ago
hendriktews commented 1 month ago

@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 commented 1 month ago

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 commented 1 month ago

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 commented 1 month ago

Agreed. A "about" command would be better.