Don't hide menus

[Jürgen Spitzmüller]

Am Samstag, dem 14.10.2023 um 17:40 +0200 schrieb Jean-Marc Lasgouttes:
> Right. And in practice it is also a great tool for experienced users,
> because this can be used as keyboard shortcuts (with time you know
> which 
> 3 letters will trigger the right action).
> 
> We could also experiment adding labels or citation keys in there (to 
> insert references) or maybe section names (to go quickly to some
> place).

As a GNOME user I am quite used to this sort of UI (the search bar in
the shell follows a similar spirit and is great for keyboard
aficionados).

I suspect it is not easy to implement this properly, though. And I
suspect it will trigger once more the critique that we go again our own
UI path instead of duplicating what popular text processors do.

BTW this "HUD" will only show actions that are enabled in the given
context, right (coming back to the issue that is at stake in this
thread)?

-- 
Jürgen