fix: closing infoview can yield 'undefined' error (#756)

mhuisi · web-flow · commit 43c29e6a86cc · 2026-04-07T09:52:36.000+02:00
diff --git a/vscode-lean4/src/infoview.ts b/vscode-lean4/src/infoview.ts
@@ -951,7 +951,7 @@ export class InfoProvider implements Disposable {
                 },
                 processing,
             }
-            await this.webviewPanel.api.gotServerNotification('$/lean/fileProgress', params)
+            await this.webviewPanel?.api.gotServerNotification('$/lean/fileProgress', params)
         }
     }
 

Original file line number	Diff line number	Diff line change
`@@ -951,7 +951,7 @@ export class InfoProvider implements Disposable {`
`951`	`951`	`},`
`952`	`952`	`processing,`
`953`	`953`	`}`
`954`		`- await this.webviewPanel.api.gotServerNotification('$/lean/fileProgress', params)`
	`954`	`+ await this.webviewPanel?.api.gotServerNotification('$/lean/fileProgress', params)`
`955`	`955`	`}`
`956`	`956`	`}`
`957`	`957`