feat: sticky notifications for extension startup errors (#547)

This PR changes the notifications for extension startup errors to a new
"sticky" notification mechanism.

Before this PR, when one of the precondition checks of the extension
failed (e.g. because Lean was not installed), we would issue a small
non-modal notification in the bottom right and then rely on users to
figure out that after fixing their setup, they need to open a new Lean
document to restart the check. If users closed this notification, there
would also be no further indication for why the extension is not
activating.
This is quite unintuitive, so we now instead issue a modal notification
when the error first occurs and then a sticky notification that
re-appears whenever a new Lean text editor is made visible. Clicking the
retry button on this notification will re-try the check. This way, it's
much harder to miss the error and how to restart the check.

Since these new sticky notifications invert the control flow, this PR
required a broad refactoring of the notification architecture.

This PR also fixes a bug where starting VS Code on an untitled Lean 4
file would not start the language server and introduces a new Lean 4
specific abstraction layer for VS Code API event handlers. This
abstraction layer is currently only in use in the code that had to be
refactored for this PR, but it will be introduced more broadly in
further PRs.

vscode-lean4/src/diagnostics/fullDiagnostics.ts

@@ -2,7 +2,7 @@ import { SemVer } from 'semver'
 import { Disposable, OutputChannel, TextDocument, commands, env, window, workspace } from 'vscode'
 import { ExecutionExitCode, ExecutionResult } from '../utils/batch'
 import { ExtUri, FileUri, extUriEquals, toExtUri } from '../utils/exturi'
-import { displayError, displayInformationWithInput } from '../utils/notifs'
+import { displayNotification, displayNotificationWithInput } from '../utils/notifs'
 import { findLeanProjectRoot } from '../utils/projectInfo'
 import {
     ElanVersionDiagnosis,
@@ -187,15 +187,16 @@ export class FullDiagnosticsProvider implements Disposable {
                 ? await findLeanProjectRoot(this.lastActiveLeanDocumentUri)
                 : undefined
         if (projectUri === 'FileNotFound') {
-            displayError(
+            displayNotification(
+                'Error',
                 `Cannot display setup information for file that does not exist in the file system: ${this.lastActiveLeanDocumentUri}. Please choose a different file to display the setup information for.`,
             )
             return
         }
         const fullDiagnostics = await performFullDiagnosis(this.outputChannel, projectUri)
         const formattedFullDiagnostics = formatFullDiagnostics(fullDiagnostics)
         const copyToClipboardInput = 'Copy to Clipboard'
-        const choice = await displayInformationWithInput(formattedFullDiagnostics, copyToClipboardInput)
+        const choice = await displayNotificationWithInput('Information', formattedFullDiagnostics, copyToClipboardInput)
         if (choice === copyToClipboardInput) {
             await env.clipboard.writeText(formattedFullDiagnostics)
         }