Multiple Lean InfoViews in VScode?

Stream: lean4

[Ching-Tsun Chou]

I asked this question in the channel "new members" and no one replied (see this link). Perhaps I'll have more luck here?

I would like to have multiple InfoViews for the following reason: When I am working on a proof in file A, I may want to create a lemma in file B (which file A imports) that would be useful in the proof in A. It would be very convenient if I can look at the proof state in A while formulating the lemma in B. But this is impossible when there is only one InfoView window.

[Martin Dvořák]

I recently learnt to open VS Code twice.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

I don't think you can have multiple infoviews; for what you want, though, you could pin the tactic state in A so that it sticks around while you look at B.

[Ching-Tsun Chou]

Ah, thanks! I didn't know pinning works across files.