fix: 'no active Lean tab' error when Lean tab is active#674

mhuisi merged 1 commit intoleanprover:masterleanprover/vscode-lean4:masterfrom

mhuisi:mhuisi/lean-editor-provider-initializationmhuisi/vscode-lean4:mhuisi/lean-editor-provider-initializationCopy head branch name to clipboard