swap where the module and the type show

[ericrbg]

I made it so that the type and where the module are swap, e.g. see top for old behaviour bottom for new [waiting on Loogle to return for demo photos].

It'd be nice if we could make the quickpick items bigger instead so we can see the whole type, but at least now hovering shows the whole type.

[Shreyas4991]

I considered this change before. I didn't add it because:

1. I can get the tooltip even in the current setup for reading the full type.
2. I made it an option to turn off the display of the module name. When module names are not needed, the value of detail is some whitespace. With this, I get a nice extra line space in the quick view item which reduces clutter. Adding type signatures to detail removes this convenient decluttering.
3. For longer type signatures which many theorems have, showing the type signature as part of the detail makes little difference. The user gets to see a slightly longer prefix and still needs to hover the mouse over the type signature to get the tooltip.

Thoughts?

[Shreyas4991]

See the screenshot for what I mean by clutter free when I turn off module names.

[ericrbg]

I agree it looks really nice for small theorems, but for bigger theorems the space would be sorely needed:

Not that the second is a million times better, sadly...

[ericrbg]

I think we need to figure out a way to get rid of all the binders, or expand the quickpick options to make them bigger

[Shreyas4991]

My understanding is that the vscode devs are dragging their feet over adding multiline descriptions and inputs: microsoft/vscode#98098

[ericrbg]

that seems to be for input, as opposed to output, but I wouldn't be surprised if it was similar

[Shreyas4991]

In this case, we should probably make the display of type signatures optional with this PR. If people want to see it, they can keep it turned on. Otherwise the clutter becomes unbearable. As it is, the longer type signatures can only be seen on the tooltip. I suspect people on zulip will have opinions on this change. Maybe we should have a poll there (There are ~50 users of the extension so far).

[ericrbg]

I'm happy to talk about it on Zulip. I think the better option would be to show the statement with only explicit hypotheses before, whilst VSCode doesn't support multiline descriptions.

[Shreyas4991]

Awesome! About excluding implicits, the best place for that change would be in the backend since it is generated via lean metaprogramming. We probably shouldn't reinvent that wheel. It should not be difficult to add an extra field with implicits removed.

[ericrbg]

Yes, for sure. It would really be nice if quick-picks could be multiline, though.

[nomeata]

I created an issue at nomeata/loogle#7 to collect ideas

[Shreyas4991]

I think we should have a zulip poll about this soon, before the christmas vacation period. At least for me, January is a particularly busy month and I am sure I will forget about this completely by then. @nomeata or @ericrbg would one of you like to start the poll? I guess that since the solution to this depends on the loogle issue linked above, we need to get suggestions for those too.

[ericrbg]

sure, would you like me to start the poll?

[ericrbg]

oh sorry I should've read more carefully, I think Joachim should and link it with the Loogle issue.

[Shreyas4991]

sure, would you like me to start the poll?

I am fine with either option. There is more than one way to do this. On the one hand, we need to know how users would like loogle to show type signatures, and on the other hand how and where the extension should show it. The screenshots above can help with this. One possible way is for loogle to offer multiple type signatures in its API : shortened ones, full signatures, implicits removed etc. Then the web interface and extension can make choices tailoured to the corresponding constraints.

[Shreyas4991]

This PR has been around for a while. I haven't seen any strong opinions about this other than my own. I suggest making this change a non-default option which can be configured by users as they like it.