search

coq / vscoq

Visual Studio Code extension for Coq
MIT License
335 stars 68 forks source link

Work on better system for goal ellipsis #846

Closed thery closed 2 months ago

rtetley commented 2 months ago

50 seems REALLY high, for example on the issue that was fixed by the ellipsis (#809) it has no effect.

rtetley commented 2 months ago

I checked and indeed it is the depth used by coq. This is the kind of goal display you get in coqc by using the example in https://github.com/coq-community/vscoq/issues/809. Do you really find this reasonable ?

Screenshot 2024-07-29 at 11 30 11
TheoWinterhalter commented 2 months ago

I think that as long as you can easily unfold it by clicking, it makes sense to have a smaller default depth.

rtetley commented 2 months ago

The problem being that right now it only unfolds on one level, so it can be quickly tiresome. Maybe add an unfold all ?

TheoWinterhalter commented 2 months ago

It could also maybe unfold something like 10? I don't know what would be the best…

gares commented 2 months ago

If you have the time to put the settings in the goal view, then it is easy to set it to 50 in one go

rtetley commented 2 months ago

It's not great practice to create your own settings page (https://code.visualstudio.com/api/ux-guidelines/settings). So I did the next best thing: I add a button that opens the settings page for the goals display.

TheoWinterhalter commented 2 months ago

I'm now going through a proof with a lot of ellipses, and it's actually quite a pain to unfold them all. One thing is that [...] will sometimes unfold to ([...]) which is a shame. So I think 10 is indeed too small, but also it would be nice to be able to unfold "faster".

rtetley commented 2 months ago

Okay I've added a mechanism so that an ellipsis opens at a +10 depth factor. I still think that 50 is too big for the default setting. By playing around I like the number 17. Maybe one of you can play around and tell me what you guys think @TheoWinterhalter @thery ?

TheoWinterhalter commented 2 months ago

That sounds good to me. If you make a new release, I'd be happy to test it. :)