I've messed up the VS Code Infoview

Stream: new members

[Nicholas Dyson]

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?

[Kevin Buzzard]

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

[Nicholas Dyson]

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.

[Johan Commelin]

@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.)

[Johan Commelin]

Did you install Lean back then? Or recently?

[Nicholas Dyson]

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

[Johan Commelin]

Hmm, let me check when we got widgets.

[Nicholas Dyson]

TY

[Johan Commelin]

Hmm, no we already had those in the summer.

[Johan Commelin]

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.

[Johan Commelin]

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

[Johan Commelin]

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

[Nicholas Dyson]

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.

[Patrick Massot]

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

[Patrick Massot]

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