Open two editors with same file on ctrl+click

Stream: lean4

[Filippo A. E. Nuccio]

If I ctrl+click on a declaration that appears in the infoview, a new VSCode editor opens, with the file where the declaration is defined, already placed at the right point. Is there a way to open two (or more) editors with the same file, in case I want to ctrl+click on more than one declaration but both are defined in the same file? What happens now is that if both foo and bar are defined in file.lean, when I ctrl+click on foo the editors goes to the line of foo, and if I ctrl+click on bar the same editor moves to the line where bar is defined, but now I do not see foo any more. I would like to end up with two editors, one with file.lean at the foo line and the other with file.lean at the bar line.

[Filippo A. E. Nuccio]

Oh, found one trick! If after the first click (say, for foo) I go to View->Editor Layout->Split Right and I activate the right sub-window by clicking on it, it becomes the "active" sub-window, and if I click on bar it will be this new one that moves to the bar line.

[Sebastian Ullrich]

Ctrl+Alt+Click should do that I believe

[Filippo A. E. Nuccio]

Not for me, at least...

[Filippo A. E. Nuccio]

The ctrl+Alt+Click and simply ctrl+Click seem to have the same effect.

[Wojciech Nawrocki]

Oh yeah there is no support for Ctrl+alt+click in the infoview, only Ctrl+click.