Zulip Chat Archive

Stream: new members

Topic: I've messed up the VS Code Infoview


view this post on Zulip Nicholas Dyson (Feb 01 2021 at 15:26):

Well, this is annoying. I'm using VS Code, and I guess I pressed some keyboard shortcut (although I've looked at the keyboard shortcuts and can't find anything) or something, because instead of the Infoview being formatted like:

f (g x) y

it's suddenly started displaying more like:

f
   (g x
   )
   y

and I can see how that could be clearer sometimes to some people, but I don't want it like that. Can I change it back?

view this post on Zulip Kevin Buzzard (Feb 01 2021 at 15:27):

Make the window a bit bigger or decrease the font size -- does the problem go away?

view this post on Zulip Nicholas Dyson (Feb 01 2021 at 15:29):

Somewhat - there's now not a linebreak before every single close bracket, just some of them - but it's definitely still not like it used to be. Something has been toggled, because I can go back to proofs I've already done and it looks different to how it did. It seems to be that it's trying to keep open brackets on the same line as the matching close bracket.

view this post on Zulip Johan Commelin (Feb 01 2021 at 15:30):

@Nicholas Dyson did you upgrade your lean extension? The behaviour you described sounds like what it was before we got extensions. (A couple of months ago.)

view this post on Zulip Johan Commelin (Feb 01 2021 at 15:31):

Did you install Lean back then? Or recently?

view this post on Zulip Nicholas Dyson (Feb 01 2021 at 15:31):

I haven't deliberately touched my installation for a few months. I think it would have been September-October that I installed it.

view this post on Zulip Johan Commelin (Feb 01 2021 at 15:32):

Hmm, let me check when we got widgets.

view this post on Zulip Nicholas Dyson (Feb 01 2021 at 15:33):

TY

view this post on Zulip Johan Commelin (Feb 01 2021 at 15:34):

Hmm, no we already had those in the summer.

view this post on Zulip Johan Commelin (Feb 01 2021 at 15:34):

But it still sounds like you had a VScode extension upgrade. I understand that you might not like the formatting. On the other hand, widgets bring lots of cool functionality.

view this post on Zulip Johan Commelin (Feb 01 2021 at 15:34):

I don't know how to control their formatting though.

view this post on Zulip Johan Commelin (Feb 01 2021 at 15:35):

Example of cool functionality: you can now click on terms in the infoview, and get popup messages about the type. This works recursively.

view this post on Zulip Nicholas Dyson (Feb 01 2021 at 15:35):

OK, if there's nothing I can do about it then I'll learn to live with it. I did just import the tactic.basic library for the first time, so I suppose that could have triggered an upgrade somehow.

view this post on Zulip Patrick Massot (Feb 01 2021 at 15:36):

It didn't trigger an update, it imported things you didn't import before.

view this post on Zulip Patrick Massot (Feb 01 2021 at 15:37):

And what you're seeing is a bug, not a feature.


Last updated: May 09 2021 at 19:11 UTC