search

ejgallego / coq-lsp

Visual Studio Code Extension and Language Server Protocol for Coq
GNU Lesser General Public License v2.1
137 stars 31 forks source link

[code] Don't show goals type when details are closed. #730

Closed ejgallego closed 2 months ago

ejgallego commented 2 months ago

This is a workaround for #525 #652

For now, I disable this setting, so types are not displayed.

The right fix would be to add a checkbox in the view, so this can be toggled dynamically, but I don't have the cycles for that right now, and not worth delaying the release which is long overdue.

Alizter commented 2 months ago

Can you also tweak the unfocused goals to not be expanded? I believe it requires toggling some booleans but I had trouble working out which ones. When the subgoals are displayed for instance, they should always be collapsed.

ejgallego commented 2 months ago

I don't see what you mean: all the subgoals look like not expanded to me.

Do we have an example on examples/goals.v that I could look at?

ejgallego commented 2 months ago

Will merge this meanwhile.