Show theorems in parent namespace in the widget

Stream: lean4

[Ben]

If I have

theorem theorem1 : ...

theorem two (h1: ...) := by

When I have the cursor mode after the by, in tactic mode (that's what it's called right). The vscode widget shows the local h1 . Is there a way to also show additional theorems like theorem1. Only ones in the above namespace/file so it doesn't blow up :)

[Jannis Limperg]

No, that's not possible. VSCode has an "Outline" view that you might enjoy.

[Sky Wilshaw]

image.png
You can also pin things to your infoview with this button.

[Sky Wilshaw]

But that'll show the whole tactic state, so it's probably not what you're after.