PG icon indicating copy to clipboard operation
PG copied to clipboard

Reduce splash time to 1s.

Open Matafou opened this issue 2 years ago • 4 comments

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.

Matafou avatar May 05 '24 16:05 Matafou

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.)

hendriktews avatar May 12 '24 13:05 hendriktews

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 avatar May 12 '24 21:05 erikmd

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

erikmd avatar May 12 '24 21:05 erikmd

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).

Matafou avatar May 13 '24 10:05 Matafou

@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

erikmd avatar Jun 15 '24 14:06 erikmd

Sure. Sooner is better imho.

Matafou avatar Jun 15 '24 15:06 Matafou