feat: refinements for 185 (#553)

- Fixes a bug where InfoView would not appear in locked tab group after
restarting VS Code
- Adds a command to the forall menu for re-displaying a sticky setup
error in case it was closed by accident and users have no clue how to
re-open it (by selecting a new Lean tab)

vscode-lean4/package.json

@@ -198,6 +198,12 @@
                 "title": "Server: Refresh File Dependencies",
                 "description": "Restarts the Lean server for the file that is currently focused to refresh the dependencies."
             },
+            {
+                "command": "lean4.redisplaySetupError",
+                "category": "Lean 4",
+                "title": "Re-Display Active Setup Error",
+                "description": "Re-displays the currently active setup error if it was closed previously."
+            },
             {
                 "command": "lean4.input.convert",
                 "category": "Lean 4",
@@ -510,6 +516,10 @@
                     "command": "lean4.refreshFileDependencies",
                     "when": "lean4.isLeanFeatureSetActive"
                 },
+                {
+                    "command": "lean4.redisplaySetupError",
+                    "when": "lean4.isStickyNotificationActiveButHidden"
+                },
                 {
                     "command": "lean4.input.convert",
                     "when": "lean4.isLeanFeatureSetActive && lean4.input.isActive"
@@ -673,6 +683,11 @@
                     "submenu": "lean4.titlebar.documentation",
                     "when": "config.lean4.alwaysShowTitleBarMenu || lean4.isLeanFeatureSetActive",
                     "group": "8_documentation@1"
+                },
+                {
+                    "command": "lean4.redisplaySetupError",
+                    "when": "lean4.isStickyNotificationActiveButHidden",
+                    "group": "9_setupError@1"
                 }
             ],
             "lean4.titlebar.newProject": [

vscode-lean4/src/extension.ts

@@ -24,7 +24,12 @@ import { FileUri } from './utils/exturi'
 import { displayInternalErrorsIn } from './utils/internalErrors'
 import { lean, LeanEditor, registerLeanEditorProvider } from './utils/leanEditorProvider'
 import { LeanInstaller } from './utils/leanInstaller'
-import { displayNotification, displayNotificationWithInput } from './utils/notifs'
+import {
+    displayActiveStickyNotification,
+    displayNotification,
+    displayNotificationWithInput,
+    setStickyNotificationActiveButHidden,
+} from './utils/notifs'
 import { PathExtensionProvider } from './utils/pathExtensionProvider'
 import { findLeanProjectRoot } from './utils/projectInfo'
 
@@ -253,6 +258,10 @@ async function tryActivatingLean4Features(
 export async function activate(context: ExtensionContext): Promise<Exports> {
     await setLeanFeatureSetActive(false)
     registerLeanEditorProvider(context)
+    await setStickyNotificationActiveButHidden(false)
+    context.subscriptions.push(
+        commands.registerCommand('lean4.redisplaySetupError', async () => displayActiveStickyNotification()),
+    )
 
     const alwaysEnabledFeatures: AlwaysEnabledFeatures = await displayInternalErrorsIn(
         'activating Lean 4 extension',

vscode-lean4/src/utils/notifs.ts

@@ -28,6 +28,10 @@ function toNotif(severity: NotificationSeverity): Notification {
     }
 }
 
+export async function setStickyNotificationActiveButHidden(isActiveButHidden: boolean) {
+    await commands.executeCommand('setContext', 'lean4.isStickyNotificationActiveButHidden', isActiveButHidden)
+}
+
 export type StickyNotificationOptions<T> = {
     onInput: (lastChoice: T, continueDisplaying: boolean) => Promise<boolean>
     onDisplay: () => Promise<void>
@@ -40,6 +44,7 @@ type StickyNotification<T> = {
 
 let activeStickyNotification: StickyNotification<any> | undefined
 let nextStickyNotification: StickyNotification<any> | undefined
+let activeDisplayFn: (() => Promise<void>) | undefined
 
 function makeSticky<T>(n: StickyNotification<T>): Disposable {
     if (activeStickyNotification !== undefined) {
@@ -57,6 +62,7 @@ function makeSticky<T>(n: StickyNotification<T>): Disposable {
         if (isDisplaying) {
             return
         }
+        await setStickyNotificationActiveButHidden(false)
         isDisplaying = true
         try {
             await activeStickyNotification?.options.onDisplay()
@@ -76,25 +82,43 @@ function makeSticky<T>(n: StickyNotification<T>): Disposable {
             } while ((r !== undefined && continueDisplaying) || gotNewStickyNotification)
             if (!continueDisplaying) {
                 activeStickyNotification = undefined
+                await setStickyNotificationActiveButHidden(false)
                 d?.dispose()
+            } else {
+                await setStickyNotificationActiveButHidden(true)
             }
         } catch (e) {
             activeStickyNotification = undefined
             nextStickyNotification = undefined
+            await setStickyNotificationActiveButHidden(false)
             d?.dispose()
             console.log(e)
         } finally {
             isDisplaying = false
         }
     }
+    activeDisplayFn = display
 
-    d = lean.onDidRevealLeanEditor(async () => await display())
-
+    d = Disposable.from(
+        lean.onDidRevealLeanEditor(async () => await display()),
+        {
+            dispose: () => {
+                activeStickyNotification = undefined
+                activeDisplayFn = undefined
+            },
+        },
+    )
     void display()
 
     return d
 }
 
+export function displayActiveStickyNotification() {
+    if (activeDisplayFn !== undefined) {
+        void activeDisplayFn()
+    }
+}
+
 export function displayNotification(
     severity: NotificationSeverity,
     message: string,

vscode-lean4/src/utils/viewColumn.ts

@@ -9,7 +9,17 @@ export function viewColumnOfInfoView(): ViewColumn {
             return tabGroup.viewColumn
         }
     }
-    return ViewColumn.Beside
+
+    // We do not use `ViewColumn.Beside` here because `ViewColumn.Beside` will never
+    // add a tab to a locked tab group.
+    // This is especially problematic because locking the tab group of the InfoView
+    // is a workaround for https://github.com/microsoft/vscode/issues/212679
+    // and using `ViewColumn.Beside` will retain an empty locked tab group when restarting VS Code.
+    const activeColumn = window.activeTextEditor?.viewColumn
+    if (activeColumn === undefined) {
+        return ViewColumn.Two
+    }
+    return activeColumn + 1
 }
 
 export function viewColumnOfActiveTextEditor(): ViewColumn {