GitHub Pull Requests makes VS Code leak text documents

[mhuisi]

• Extension version: 0.114.3
• VSCode Version: 1.102.1
• OS: Linux/Fedora (also reproduces on Windows)
• Repository Clone Configuration (single repository/fork of an upstream repository): single repository
• GitHub Product (GitHub.com/GitHub Enterprise version x.x.x): GitHub.com

Steps to Reproduce:

1. Run the following minimal demo extension that displays a notification when the workspace.onDidCloseTextDocument event is fired: https://github.com/mhuisi/gh-prs-leak-example
2. Open a folder that is connected to GitHub (e.g. a clone of https://github.com/leanprover/lean4-cli)
3. Observe that opening and then closing editors displays a notification when all editors for a document are closed
4. Install GitHub Pull Requests
5. Re-run the demo extension
6. Open a folder that is connected to GitHub
7. Observe that opening and then closing editors displays no notification when all editors for a document are closed
8. Run the 'Hello World' command to output the set of open text documents
9. Observe that all documents that have been closed in the editor are still open in workspace.textDocuments

Context

The language extension for the Lean 4 theorem prover allocates resources for each opened text document and de-allocates resources for each closed text document. This is important because processing Lean files is quite expensive, so we need a reasonable signal from the client for when text documents are opened or closed (we certainly don't want to de-allocate pre-emptively). When users have GitHub Pull Requests installed, since none of the text documents are closed, the extension can't de-allocate resources associated with each file.