Lost a sidebar

Stream: new members

[Iris Rotarescu]

Hi everyone! I'm new to lean, using Visual Studio Code. I am working on the sheets of @Kevin Buzzard right now. I made the beginner's mistake of accidentally closing the side bar that shows the current goal. Upon restarting the entire editor I found out it's called 'lean infoview'. How can I get it back without restarting the editor?
Thanks in advance! Greetings from @Jana Göken

[Yaël Dillies]

Do you see the ∀ button in the tab with your Lean files? This is a menu containing among other things a button to start the infoview

[Iris Rotarescu]

I combed through all menus, except that one. Thank you so much!

[Yaël Dillies]

Ctrl + Shift + P and typing info should also give you a command to start the infoview.

[Damiano Testa]

Also, probably Ctrl + Shift + Enter may open the infoview directly.

[Yaël Dillies]

Didn't know about that one! Every day you learn...