Remove worksheets when closed

Author: Duhemm

vscode-dotty/src/extension.ts

@@ -36,6 +36,11 @@ export function activate(context: ExtensionContext) {
       vscode.commands.executeCommand(worksheet.worksheetEvaluateAfterSaveKey)
     }
   })
+  vscode.workspace.onDidCloseTextDocument(document => {
+    if (worksheet.isWorksheet(document)) {
+      worksheet.removeWorksheet(document)
+    }
+  })
 
   vscode.commands.registerCommand(worksheet.worksheetEvaluateAfterSaveKey, () => {
     worksheet.evaluateCommand()

vscode-dotty/src/worksheet.ts

@@ -55,6 +55,11 @@ export const worksheetEvaluateAfterSaveKey = "worksheet.evaluateAfterSave"
  */
 export const worksheetCancelEvaluationKey = "worksheet.cancel"
 
+/** Remove the worksheet corresponding to the given document. */
+export function removeWorksheet(document: vscode.TextDocument) {
+  worksheets.delete(document)
+}
+
 /** Is this document a worksheet? */
 export function isWorksheet(document: vscode.TextDocument): boolean {
   return document.fileName.endsWith(".sc")