Extension adds a "lean" button to *all* files

[RalfJung]

I installed this extension to experiment with Lean. Surprisingly, the extension adds a ∀ button to the editor in the top right corner for all file types, so now my Rust and LaTeX sessions have this useless button sitting there. That's not very polite; the other extensions I have installed generally stay our of my way when I am working on unrelated file types. For instance, the LaTeX extension has quite a few buttons it adds in the same place, but they only show up when editing a LaTeX file.

I know I can hide this button, but (a) then it is hidden even for Lean files, where it would actually be useful, and (b) it is still impolite to add this button to all file types by default. I would appreciate if the button could instead be made context-dependent and only show up when it is actually useful -- i.e. not for Rust or LaTeX or Markdown files.

[mhuisi]

You can disable this behavior by disabling the 'Lean 4: Always Show Title Bar Menu' setting, which was introduced back when the command menu was introduced. Please also see the corresponding section in the manual.

The reason why we display the command menu even outside of Lean files by default is because it has lots of functions that users want to use before they ever open a Lean file: Creating projects, opening and downloading projects, troubleshooting functionality for when something is wrong with Lean or the VS Code extension, managing Lean versions and documentation for setting up and using Lean.

[RalfJung]

That seems to work, thanks :)

The reason why we display the command menu even outside of Lean files by default is because it has lots of functions that users want to use before they ever open a Lean file: Creating projects, opening and downloading projects, troubleshooting functionality for when something is wrong with Lean or the VS Code extension, managing Lean versions and documentation for setting up and using Lean.

I can see that, but OTOH other extensions manage not using precious screen space in unrelated workspaces.

[mhuisi]

OTOH other extensions manage not using precious screen space in unrelated workspaces.

I don't find this to be a convincing argument. Most extensions simply do not have a "command menu" at all and instead use either the command palette for all of their commands, which is much harder to discover for less technically inclined users, or instead introduce a separate sidebar view, which also "uses precious screen space" in a similar manner as the command menu does and has worse UX for executing commands, as you need to switch away from your current sidebar view to use it.

Please also keep in mind that a lot of our users are not programmers, but mathematicians at any stage of their professional careers, including undergrads. A lot of our users also use VS Code exclusively for Lean.

[RalfJung]

FWIW sidebar views are also typically hidden when they do not fit the current file type.

[mhuisi]

I don't think that is an option for us, unfortunately. Our users need to be able to easily access a structured overview of all commands in contexts where they haven't opened a Lean file yet. In my experience, the command palette is not sufficient for this, especially for users who do not have a programming background.

I'm open to other suggestions that retain the discoverability and the usability of the command menu, though. I evaluated all the other alternatives that VS Code provides us with back when I implemented it, but perhaps I've missed something :-)