"Show Proof" opens an empty new tab

[glacode]

VSCode opens a new empty tab "Untitled-n" and the cursor blinks at the beginning of the new tab

[tirix]

This is strange - it might be because when you tried this functionality, the LSP server had already crashed because of other issues, and was not there to provide the proof.

I'd suggest to try this again on an error-free set.mm or when crash issues are solved...