When displaying an activation error, the popup can get too large, rendering VS Code unusable. We now only display the error message without the stack trace, but copy it when using the "Copy Error to Clipboard" button.
Activating the VS Code extension would sometimes crash when VS Code attempts to open a document with a file URI that does not exist on the file system anymore. This happens when a file has unsaved changes, VS Code is closed, the file is deleted and VS Code is re-opened.
This PR fixes two issues reported at https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/VS.20Code.20error.20too.20big.20to.20remove/near/447340051: