search

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

Reduce splash time to 1s. #768

Closed Matafou closed 5 months ago

Matafou commented 6 months ago

The idea is that this splash screen annoys everyone, even in its new manga-style form.

I would even consider removing it completely but at least let us not have it last for 8 seconds by default.

hendriktews commented 6 months ago

I have (proof-splash-enable nil) since the second day I use PG. So yes, please merge. (IMO it would be better to have it 3 or 4 seconds together with a bit button "Disable this splash screen for the future" at the front, but I don't feel inclined to spend time on it.)

erikmd commented 6 months ago

AFAIAC, I only press q and it disappears immediately. Maybe this shortcut could just be made more visible? or improving this splash screen so that yet another shortcut is put forth, to dismiss the screen once and for all?

erikmd commented 6 months ago

YMMV anyway, and I don't object to merging this

Matafou commented 6 months ago

At the time this splash screen was created (before I ever used pg) emacs used to freeze for a few seconds while PG was initializing and the user was tempted to hit C-g pavlovly. PG was then in a horrific half-initialized state. I think this is the motivation behind this initially.

Even with a non compiled PG this takes less than a second now, so I think we can remove it completely, except for folklore. Btw I think we don't have credit for this image. It was drawn by a chinese student duiring a coq school (second hand credit here: https://youzicha.tumblr.com/post/145836286669/in-the-lastest-version-of-proof-general-the-mascot).

erikmd commented 5 months ago

@Matafou Ready to merge this now?

Even if Hendrik suggested a possible enhancement

(IMO it would be better to have it 3 or 4 seconds together with a bit button "Disable this splash screen for the future" at the front, but I don't feel inclined to spend time on it.)

it seems that the current version of this PR has the merit to be simple, and still greatly improve the situation

Matafou commented 5 months ago

Sure. Sooner is better imho.