## Stream: new members

### Topic: I've messed up the VS Code Infoview

#### 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?

#### Kevin Buzzard (Feb 01 2021 at 15:27):

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

#### 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.

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

#### Johan Commelin (Feb 01 2021 at 15:31):

Did you install Lean back then? Or recently?

#### 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.

#### Johan Commelin (Feb 01 2021 at 15:32):

Hmm, let me check when we got widgets.

TY

#### 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.

#### Johan Commelin (Feb 01 2021 at 15:34):

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

#### 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.

#### 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.

#### Patrick Massot (Feb 01 2021 at 15:36):

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

#### 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