It turns out that VS Code sometimes hands us non-file/untitled URIs, e.g. 'output' URIs. I totally forgot about those. This PR ensures that instead of throwing an error when we encounter such a URI, the extension bails as soon as possible.
It also fixes a bug where untitled ExtUris did not correctly track the assigned file name of the untitled URI.
Bug originally reported at https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/VScode.20extension.20not.20showing.20infoview/near/435562684 and originally introduced in #428.
It turns out that VS Code sometimes hands us non-file/untitled URIs, e.g. 'output' URIs. I totally forgot about those. This PR ensures that instead of throwing an error when we encounter such a URI, the extension bails as soon as possible.
It also fixes a bug where untitled
ExtUris did not correctly track the assigned file name of the untitled URI.