Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Work on better system for goal ellipsis #846

Merged
merged 7 commits into from
Aug 5, 2024
Merged

Work on better system for goal ellipsis #846

merged 7 commits into from
Aug 5, 2024

Conversation

thery
Copy link
Contributor

@thery thery commented Jul 25, 2024

No description provided.

@rtetley
Copy link
Collaborator

rtetley commented Jul 25, 2024

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

@rtetley
Copy link
Collaborator

rtetley commented Jul 29, 2024

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 #809.
Do you really find this reasonable ?
Screenshot 2024-07-29 at 11 30 11

@TheoWinterhalter
Copy link

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

@rtetley
Copy link
Collaborator

rtetley commented Jul 29, 2024

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

@TheoWinterhalter
Copy link

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

@gares
Copy link
Member

gares commented Jul 29, 2024

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
Copy link
Collaborator

rtetley commented Jul 30, 2024

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
Copy link

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
Copy link
Collaborator

rtetley commented Aug 5, 2024

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
Copy link

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

@rtetley rtetley merged commit 2880bd8 into coq:main Aug 5, 2024
24 checks passed
@rtetley rtetley changed the title set the default max depth = coq max depth Work on better system for goal ellipsis Aug 5, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants