diff --git a/.github/workflows/on-push.yml b/.github/workflows/on-push.yml
index 8f868df54..7e61993ec 100644
--- a/.github/workflows/on-push.yml
+++ b/.github/workflows/on-push.yml
@@ -55,6 +55,18 @@ jobs:
         run: |
           npm publish --workspace=lean4-infoview --access=public
 
+      - name: Try publishing unicode-input
+        if: ${{ startsWith(github.ref, 'refs/tags/v') && !endsWith(github.ref, '-pre') && matrix.os == 'ubuntu-latest' }}
+        continue-on-error: true
+        run: |
+          npm publish --workspace=lean4-unicode-input --access=public
+
+      - name: Try publishing unicode-input-component
+        if: ${{ startsWith(github.ref, 'refs/tags/v') && !endsWith(github.ref, '-pre') && matrix.os == 'ubuntu-latest' }}
+        continue-on-error: true
+        run: |
+          npm publish --workspace=lean4-unicode-input-component --access=public
+
       - name: Package
         run: npm run package --workspace=lean4
         if: ${{ !startsWith(github.ref, 'refs/tags/v') || !endsWith(github.ref, '-pre') }}
diff --git a/lean4-infoview-api/package.json b/lean4-infoview-api/package.json
index 30e4a714d..e1b93efbc 100644
--- a/lean4-infoview-api/package.json
+++ b/lean4-infoview-api/package.json
@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/infoview-api",
-    "version": "0.6.0",
+    "version": "0.7.0",
     "description": "Types and API for @leanprover/infoview.",
     "scripts": {
         "watch": "tsc --watch",
diff --git a/lean4-infoview-api/src/infoviewApi.ts b/lean4-infoview-api/src/infoviewApi.ts
index 1a9ad9397..8167b7f43 100644
--- a/lean4-infoview-api/src/infoviewApi.ts
+++ b/lean4-infoview-api/src/infoviewApi.ts
@@ -7,6 +7,23 @@ import type {
     WorkspaceEdit,
 } from 'vscode-languageserver-protocol'
 
+export type ExpectedTypeVisibility = 'Expanded by default' | 'Collapsed by default' | 'Hidden'
+
+export interface InfoviewConfig {
+    allErrorsOnLine: boolean
+    autoOpenShowsGoal: boolean
+    debounceTime: number
+    expectedTypeVisibility: ExpectedTypeVisibility
+    showGoalNames: boolean
+    emphasizeFirstGoal: boolean
+    reverseTacticState: boolean
+    hideTypeAssumptions: boolean
+    hideInstanceAssumptions: boolean
+    hideInaccessibleAssumptions: boolean
+    hideLetValues: boolean
+    showTooltipOnHover: boolean
+}
+
 /**
  * An insert `here` should be written exactly at the specified position,
  * while one `above` should go on the preceding line.
@@ -15,6 +32,8 @@ export type TextInsertKind = 'here' | 'above'
 
 /** Interface that the InfoView WebView uses to talk to the hosting editor. */
 export interface EditorApi {
+    saveConfig(config: InfoviewConfig): Promise<any>
+
     /** Make a request to the LSP server. */
     sendClientRequest(uri: string, method: string, params: any): Promise<any>
     /** Send a notification to the LSP server. */
@@ -77,25 +96,18 @@ export interface InfoviewTacticStateFilter {
     flags: string
 }
 
-export interface InfoviewConfig {
-    allErrorsOnLine: boolean
-    autoOpenShowsGoal: boolean
-    debounceTime: number
-    showExpectedType: boolean
-    showGoalNames: boolean
-    emphasizeFirstGoal: boolean
-    reverseTacticState: boolean
-    showTooltipOnHover: boolean
-}
-
 export const defaultInfoviewConfig: InfoviewConfig = {
     allErrorsOnLine: true,
     autoOpenShowsGoal: true,
     debounceTime: 50,
-    showExpectedType: true,
+    expectedTypeVisibility: 'Expanded by default',
     showGoalNames: true,
     emphasizeFirstGoal: false,
     reverseTacticState: false,
+    hideTypeAssumptions: false,
+    hideInstanceAssumptions: false,
+    hideInaccessibleAssumptions: false,
+    hideLetValues: false,
     showTooltipOnHover: true,
 }
 
@@ -108,7 +120,35 @@ export type InfoviewActionKind =
 
 export type InfoviewAction = { kind: InfoviewActionKind }
 
-export type ContextMenuEntry = 'goToDefinition' | 'select' | 'unselect' | 'unselectAll'
+export type ContextMenuEntry =
+    | 'goToDefinition'
+    | 'select'
+    | 'unselect'
+    | 'unselectAll'
+    | 'pause'
+    | 'unpause'
+    | 'pin'
+    | 'unpin'
+    | 'refresh'
+    | 'pauseAllMessages'
+    | 'unpauseAllMessages'
+    | 'goToPinnedLocation'
+    | 'goToMessageLocation'
+    | 'displayTargetBeforeAssumptions'
+    | 'displayAssumptionsBeforeTarget'
+    | 'hideTypeAssumptions'
+    | 'showTypeAssumptions'
+    | 'hideInstanceAssumptions'
+    | 'showInstanceAssumptions'
+    | 'hideInaccessibleAssumptions'
+    | 'showInaccessibleAssumptions'
+    | 'hideLetValues'
+    | 'showLetValues'
+    | 'hideGoalNames'
+    | 'showGoalNames'
+    | 'emphasizeFirstGoal'
+    | 'deemphasizeFirstGoal'
+    | 'saveSettings'
 
 export interface ContextMenuAction {
     entry: ContextMenuEntry
diff --git a/lean4-infoview/package.json b/lean4-infoview/package.json
index bd5b5b5aa..804136f10 100644
--- a/lean4-infoview/package.json
+++ b/lean4-infoview/package.json
@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/infoview",
-    "version": "0.8.3",
+    "version": "0.8.5",
     "description": "An interactive display for the Lean 4 theorem prover.",
     "scripts": {
         "watch": "rollup --config --environment NODE_ENV:development --watch",
@@ -49,7 +49,7 @@
         "typescript": "^5.4.5"
     },
     "dependencies": {
-        "@leanprover/infoview-api": "~0.6.0",
+        "@leanprover/infoview-api": "~0.7.0",
         "@vscode/codicons": "^0.0.32",
         "@vscode-elements/react-elements": "^0.5.0",
         "es-module-lexer": "^1.5.4",
diff --git a/lean4-infoview/src/infoview/collapsing.tsx b/lean4-infoview/src/infoview/collapsing.tsx
index 14880cdea..90bb4a9e8 100644
--- a/lean4-infoview/src/infoview/collapsing.tsx
+++ b/lean4-infoview/src/infoview/collapsing.tsx
@@ -26,7 +26,7 @@ export function useIsVisible(): [(element: HTMLElement) => void, boolean] {
     return [node, isVisible]
 }
 
-interface DetailsProps {
+interface DetailsProps extends React.PropsWithoutRef<React.HTMLProps<HTMLDetailsElement>> {
     initiallyOpen?: boolean
     children: [React.ReactNode, ...React.ReactNode[]]
     setOpenRef?: (_: React.Dispatch<React.SetStateAction<boolean>>) => void
@@ -34,11 +34,16 @@ interface DetailsProps {
 
 /** Like `<details>` but can be programatically revealed using `setOpenRef`.
  * The first child is placed inside the `<summary>` node. */
-export function Details({ initiallyOpen, children: [summary, ...children], setOpenRef }: DetailsProps): JSX.Element {
+export function Details({
+    initiallyOpen,
+    children: [summary, ...children],
+    setOpenRef,
+    ...props
+}: DetailsProps): JSX.Element {
     const [isOpen, setOpen] = React.useState<boolean>(initiallyOpen === undefined ? false : initiallyOpen)
     if (setOpenRef) setOpenRef(setOpen)
     return (
-        <details open={isOpen}>
+        <details open={isOpen} {...props}>
             <summary
                 className="mv2 pointer "
                 onClick={e => {
diff --git a/lean4-infoview/src/infoview/goals.tsx b/lean4-infoview/src/infoview/goals.tsx
index d1c91c1d8..5d5adf3a4 100644
--- a/lean4-infoview/src/infoview/goals.tsx
+++ b/lean4-infoview/src/infoview/goals.tsx
@@ -1,5 +1,6 @@
 import {
     InfoviewActionKind,
+    InfoviewConfig,
     InteractiveGoal,
     InteractiveGoals,
     InteractiveHypothesisBundle,
@@ -46,9 +47,13 @@ export function goalsToString(goals: InteractiveGoals): string {
     return goals.goals.map(goalToString).join('\n\n')
 }
 
-interface GoalFilterState {
+interface GoalSettingsState {
     /** If true reverse the list of hypotheses, if false present the order received from LSP. */
     reverse: boolean
+    /** If true hide the names of goals, otherwise show them. */
+    hideGoalNames: boolean
+    /** If true emphasize the first goal, otherwise don't emphasize it. */
+    emphasizeFirstGoal: boolean
     /** If true show hypotheses that have isType=True, otherwise hide them. */
     showType: boolean
     /** If true show hypotheses that have isInstance=True, otherwise hide them. */
@@ -59,15 +64,27 @@ interface GoalFilterState {
     showLetValue: boolean
 }
 
+function goalSettingsStateOfConfig(config: InfoviewConfig): GoalSettingsState {
+    return {
+        reverse: config.reverseTacticState,
+        hideGoalNames: !config.showGoalNames,
+        emphasizeFirstGoal: config.emphasizeFirstGoal,
+        showType: !config.hideTypeAssumptions,
+        showInstance: !config.hideInstanceAssumptions,
+        showHiddenAssumption: !config.hideInaccessibleAssumptions,
+        showLetValue: !config.hideLetValues,
+    }
+}
+
 function getFilteredHypotheses(
     hyps: InteractiveHypothesisBundle[],
-    filter: GoalFilterState,
+    settings: GoalSettingsState,
 ): InteractiveHypothesisBundle[] {
     return hyps.reduce((acc: InteractiveHypothesisBundle[], h) => {
-        if (h.isInstance && !filter.showInstance) return acc
-        if (h.isType && !filter.showType) return acc
-        const names = filter.showHiddenAssumption ? h.names : h.names.filter(n => !isInaccessibleName(n))
-        const hNew: InteractiveHypothesisBundle = filter.showLetValue
+        if (h.isInstance && !settings.showInstance) return acc
+        if (h.isType && !settings.showType) return acc
+        const names = settings.showHiddenAssumption ? h.names : h.names.filter(n => !isInaccessibleName(n))
+        const hNew: InteractiveHypothesisBundle = settings.showLetValue
             ? { ...h, names }
             : { ...h, names, val: undefined }
         if (names.length !== 0) acc.push(hNew)
@@ -181,7 +198,7 @@ function Hyp({ hyp: h, mvarId }: HypProps) {
 
 interface GoalProps {
     goal: InteractiveGoal
-    filter: GoalFilterState
+    settings: GoalSettingsState
     additionalClassNames: string
 }
 
@@ -189,12 +206,12 @@ interface GoalProps {
  * Displays the hypotheses, target type and optional case label of a goal according to the
  * provided `filter`. */
 export const Goal = React.memo((props: GoalProps) => {
-    const { goal, filter, additionalClassNames } = props
+    const { goal, settings, additionalClassNames } = props
     const config = React.useContext(ConfigContext)
 
     const prefix = goal.goalPrefix ?? '⊢ '
-    const filteredList = getFilteredHypotheses(goal.hyps, filter)
-    const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList
+    const filteredList = getFilteredHypotheses(goal.hyps, settings)
+    const hyps = settings.reverse ? filteredList.slice().reverse() : filteredList
     const locs = React.useContext(LocationsContext)
     const goalLocs = React.useMemo(
         () =>
@@ -217,12 +234,12 @@ export const Goal = React.memo((props: GoalProps) => {
     if (props.goal.isRemoved) cn += ' b--removed '
 
     const children: React.ReactNode[] = [
-        filter.reverse && goalLi,
+        settings.reverse && goalLi,
         hyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />),
-        !filter.reverse && goalLi,
+        !settings.reverse && goalLi,
     ]
 
-    if (goal.userName && config.showGoalNames) {
+    if (goal.userName && !settings.hideGoalNames) {
         return (
             <details open className={cn}>
                 <summary className="mv1 pointer">
@@ -237,12 +254,12 @@ export const Goal = React.memo((props: GoalProps) => {
 
 interface GoalsProps {
     goals: InteractiveGoals
-    filter: GoalFilterState
+    settings: GoalSettingsState
     /** Whether or not to display the number of goals. */
     displayCount: boolean
 }
 
-function Goals({ goals, filter, displayCount }: GoalsProps) {
+function Goals({ goals, settings, displayCount }: GoalsProps) {
     const nGoals = goals.goals.length
     const config = React.useContext(ConfigContext)
     if (nGoals === 0) {
@@ -260,8 +277,8 @@ function Goals({ goals, filter, displayCount }: GoalsProps) {
                     <Goal
                         key={i}
                         goal={g}
-                        filter={filter}
-                        additionalClassNames={i !== 0 && config.emphasizeFirstGoal ? unemphasizeCn : ''}
+                        settings={settings}
+                        additionalClassNames={i !== 0 && settings.emphasizeFirstGoal ? unemphasizeCn : ''}
                     />
                 ))}
             </>
@@ -295,50 +312,41 @@ export const FilteredGoals = React.memo(
         const ec = React.useContext(EditorContext)
         const config = React.useContext(ConfigContext)
 
-        const copyToCommentButton = (
-            <a
-                className="link pointer mh2 dim codicon codicon-quote"
-                data-id="copy-goal-to-comment"
-                onClick={_ => {
-                    if (goals) void ec.copyToComment(goalsToString(goals))
-                }}
-                title="copy state to comment"
-            />
-        )
-
-        const [goalFilters, setGoalFilters] = React.useState<GoalFilterState>({
-            reverse: config.reverseTacticState,
-            showType: true,
-            showInstance: true,
-            showHiddenAssumption: true,
-            showLetValue: true,
-        })
-        const sortClasses =
-            'link pointer mh2 dim codicon ' + (goalFilters.reverse ? 'codicon-arrow-up ' : 'codicon-arrow-down ')
-        const sortButton = (
-            <a
-                className={sortClasses}
-                title="reverse list"
-                onClick={_ => {
-                    setGoalFilters(s => ({ ...s, reverse: !s.reverse }))
-                }}
-            />
-        )
-
-        const mkFilterButton = (
-            filterFn: React.SetStateAction<GoalFilterState>,
-            filledFn: (_: GoalFilterState) => boolean,
+        const [goalSettings, setGoalSettings] = React.useState<GoalSettingsState>(goalSettingsStateOfConfig(config))
+
+        const goalSettingsDifferFromDefaultConfig =
+            JSON.stringify(goalSettings) !== JSON.stringify(goalSettingsStateOfConfig(config))
+        const disabledSaveStyle: React.CSSProperties = goalSettingsDifferFromDefaultConfig
+            ? {}
+            : { color: 'var(--vscode-disabledForeground)', pointerEvents: 'none' }
+
+        const saveConfig = React.useCallback(async () => {
+            await ec.api.saveConfig({
+                ...config,
+                reverseTacticState: goalSettings.reverse,
+                showGoalNames: !goalSettings.hideGoalNames,
+                emphasizeFirstGoal: goalSettings.emphasizeFirstGoal,
+                hideTypeAssumptions: !goalSettings.showType,
+                hideInstanceAssumptions: !goalSettings.showInstance,
+                hideInaccessibleAssumptions: !goalSettings.showHiddenAssumption,
+                hideLetValues: !goalSettings.showLetValue,
+            })
+        }, [config, ec.api, goalSettings])
+
+        const mkSettingButton = (
+            settingFn: React.SetStateAction<GoalSettingsState>,
+            filledFn: (_: GoalSettingsState) => boolean,
             name: string,
         ) => (
             <a
                 className="link pointer tooltip-menu-content"
                 onClick={_ => {
-                    setGoalFilters(filterFn)
+                    setGoalSettings(settingFn)
                 }}
             >
                 <span
                     className={
-                        'tooltip-menu-icon codicon ' + (filledFn(goalFilters) ? 'codicon-check ' : 'codicon-blank ')
+                        'tooltip-menu-icon codicon ' + (filledFn(goalSettings) ? 'codicon-check ' : 'codicon-blank ')
                     }
                 >
                     &nbsp;
@@ -348,47 +356,113 @@ export const FilteredGoals = React.memo(
         )
         const filterMenu = (
             <span>
-                {mkFilterButton(
+                {mkSettingButton(
+                    s => ({ ...s, reverse: !s.reverse }),
+                    gs => gs.reverse,
+                    'Display target before assumptions',
+                )}
+                <br />
+                {mkSettingButton(
                     s => ({ ...s, showType: !s.showType }),
-                    gf => gf.showType,
-                    'types',
+                    gs => !gs.showType,
+                    'Hide type assumptions',
                 )}
                 <br />
-                {mkFilterButton(
+                {mkSettingButton(
                     s => ({ ...s, showInstance: !s.showInstance }),
-                    gf => gf.showInstance,
-                    'instances',
+                    gs => !gs.showInstance,
+                    'Hide instance assumptions',
                 )}
                 <br />
-                {mkFilterButton(
+                {mkSettingButton(
                     s => ({ ...s, showHiddenAssumption: !s.showHiddenAssumption }),
-                    gf => gf.showHiddenAssumption,
-                    'hidden assumptions',
+                    gs => !gs.showHiddenAssumption,
+                    'Hide inaccessible assumptions',
                 )}
                 <br />
-                {mkFilterButton(
+                {mkSettingButton(
                     s => ({ ...s, showLetValue: !s.showLetValue }),
-                    gf => gf.showLetValue,
-                    'let-values',
+                    gs => !gs.showLetValue,
+                    'Hide let-values',
+                )}
+                <br />
+                {mkSettingButton(
+                    s => ({ ...s, hideGoalNames: !s.hideGoalNames }),
+                    gs => gs.hideGoalNames,
+                    'Hide goal names',
+                )}
+                <br />
+                {mkSettingButton(
+                    s => ({ ...s, emphasizeFirstGoal: !s.emphasizeFirstGoal }),
+                    gs => gs.emphasizeFirstGoal,
+                    'Emphasize first goal',
                 )}
+                <br className="saveConfigLineBreak" style={disabledSaveStyle} />
+                <a
+                    className="link pointer tooltip-menu-content saveConfigButton"
+                    style={disabledSaveStyle}
+                    onClick={_ => saveConfig()}
+                >
+                    <span className="tooltip-menu-icon codicon codicon-save">&nbsp;</span>
+                    <span className="tooltip-menu-text">Save current settings to default settings</span>
+                </a>
             </span>
         )
 
-        const isFiltered =
-            !goalFilters.showInstance ||
-            !goalFilters.showType ||
-            !goalFilters.showHiddenAssumption ||
-            !goalFilters.showLetValue
-        const filterButton = (
+        const settingsButton = (
             <WithTooltipOnHover tooltipChildren={filterMenu} className="dim ">
-                <a
-                    className={
-                        'link pointer mh2 codicon ' + (isFiltered ? 'codicon-filter-filled ' : 'codicon-filter ')
-                    }
-                />
+                <a className={'link pointer mh2 codicon codicon-settings-gear'} />
             </WithTooltipOnHover>
         )
 
+        const context: { [k: string]: any } = {}
+        const id = React.useId()
+        const useContextMenuEvent = (
+            name: string,
+            action: () => void,
+            isEnabled: boolean,
+            dependencies?: React.DependencyList,
+        ) => {
+            if (isEnabled) {
+                context[name + 'Id'] = id
+            }
+            useEvent(ec.events.clickedContextMenu, _ => action(), dependencies, `${name}:${id}`)
+        }
+        const useSettingsContextMenuEvent = (name: string, setting: any, isEnabled: boolean) =>
+            useContextMenuEvent(name, () => setGoalSettings(s => ({ ...s, ...setting })), isEnabled)
+
+        useSettingsContextMenuEvent('displayTargetBeforeAssumptions', { reverse: true }, !goalSettings.reverse)
+        useSettingsContextMenuEvent('displayAssumptionsBeforeTarget', { reverse: false }, goalSettings.reverse)
+        useSettingsContextMenuEvent('hideTypeAssumptions', { showType: false }, goalSettings.showType)
+        useSettingsContextMenuEvent('showTypeAssumptions', { showType: true }, !goalSettings.showType)
+        useSettingsContextMenuEvent('hideInstanceAssumptions', { showInstance: false }, goalSettings.showInstance)
+        useSettingsContextMenuEvent('showInstanceAssumptions', { showInstance: true }, !goalSettings.showInstance)
+        useSettingsContextMenuEvent(
+            'hideInaccessibleAssumptions',
+            { showHiddenAssumption: false },
+            goalSettings.showHiddenAssumption,
+        )
+        useSettingsContextMenuEvent(
+            'showInaccessibleAssumptions',
+            { showHiddenAssumption: true },
+            !goalSettings.showHiddenAssumption,
+        )
+        useSettingsContextMenuEvent('hideLetValues', { showLetValues: false }, goalSettings.showLetValue)
+        useSettingsContextMenuEvent('showLetValues', { showLetValues: true }, !goalSettings.showLetValue)
+        useSettingsContextMenuEvent('hideGoalNames', { hideGoalNames: true }, !goalSettings.hideGoalNames)
+        useSettingsContextMenuEvent('showGoalNames', { hideGoalNames: false }, goalSettings.hideGoalNames)
+        useSettingsContextMenuEvent(
+            'emphasizeFirstGoal',
+            { emphasizeFirstGoal: true },
+            !goalSettings.emphasizeFirstGoal,
+        )
+        useSettingsContextMenuEvent(
+            'deemphasizeFirstGoal',
+            { emphasizeFirstGoal: false },
+            goalSettings.emphasizeFirstGoal,
+        )
+        useContextMenuEvent('saveSettings', () => saveConfig(), goalSettingsDifferFromDefaultConfig, [saveConfig])
+
         const setOpenRef = React.useRef<React.Dispatch<React.SetStateAction<boolean>>>()
         useEvent(
             ec.events.requestedAction,
@@ -402,7 +476,10 @@ export const FilteredGoals = React.memo(
         )
 
         return (
-            <div style={{ display: goals !== undefined ? 'block' : 'none' }}>
+            <div
+                style={{ display: goals !== undefined ? 'block' : 'none' }}
+                data-vscode-context={JSON.stringify(context)}
+            >
                 <Details setOpenRef={r => (setOpenRef.current = r)} initiallyOpen={initiallyOpen}>
                     <>
                         {headerChildren}
@@ -412,13 +489,11 @@ export const FilteredGoals = React.memo(
                                 e.preventDefault()
                             }}
                         >
-                            {copyToCommentButton}
-                            {sortButton}
-                            {filterButton}
+                            {settingsButton}
                         </span>
                     </>
                     <div className="ml1">
-                        {goals && <Goals goals={goals} filter={goalFilters} displayCount={displayCount}></Goals>}
+                        {goals && <Goals goals={goals} settings={goalSettings} displayCount={displayCount}></Goals>}
                     </div>
                 </Details>
             </div>
diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx
index f89eda23e..b350552f6 100644
--- a/lean4-infoview/src/infoview/info.tsx
+++ b/lean4-infoview/src/infoview/info.tsx
@@ -80,7 +80,7 @@ const InfoStatusBar = React.memo((props: InfoStatusBarProps) => {
             {isPinned && !isPaused && ' (pinned)'}
             {!isPinned && isPaused && ' (paused)'}
             {isPinned && isPaused && ' (pinned and paused)'}
-            <span style={spinnerStyle} className="mh2 codicon codicon-loading" title="updating">
+            <span style={spinnerStyle} className="mh2 codicon codicon-loading" title="Updating ...">
                 <style>
                     {`
                         @keyframes spin {
@@ -103,7 +103,17 @@ const InfoStatusBar = React.memo((props: InfoStatusBarProps) => {
                         onClick={_ => {
                             void ec.revealPosition(pos)
                         }}
-                        title="reveal file location"
+                        title="Go to pinned location in file"
+                    />
+                )}
+                {isPaused && (
+                    <a
+                        className="link pointer mh2 dim codicon codicon-refresh"
+                        data-id="update"
+                        onClick={_ => {
+                            void triggerUpdate()
+                        }}
+                        title="Refresh paused state"
                     />
                 )}
                 <a
@@ -112,7 +122,7 @@ const InfoStatusBar = React.memo((props: InfoStatusBarProps) => {
                     onClick={_ => {
                         onPin(pos)
                     }}
-                    title={isPinned ? 'unpin' : 'pin'}
+                    title={isPinned ? 'Unpin state' : 'Pin state to top'}
                 />
                 <a
                     className={
@@ -123,15 +133,7 @@ const InfoStatusBar = React.memo((props: InfoStatusBarProps) => {
                     onClick={_ => {
                         setPaused(!isPaused)
                     }}
-                    title={isPaused ? 'continue updating' : 'pause updating'}
-                />
-                <a
-                    className="link pointer mh2 dim codicon codicon-refresh"
-                    data-id="update"
-                    onClick={_ => {
-                        void triggerUpdate()
-                    }}
-                    title="update"
+                    title={isPaused ? 'Unpause state' : 'Pause state'}
                 />
             </span>
         </summary>
@@ -190,18 +192,20 @@ function GoalInfoDisplay(props: GoalInfoDisplayProps) {
     return (
         <>
             <LocationsContext.Provider value={locs}>
-                <span data-vscode-context={JSON.stringify({ selectedLocationsId })}>
+                <span data-vscode-context={JSON.stringify(selectedLocs.length === 0 ? {} : { selectedLocationsId })}>
                     <FilteredGoals key="goals" headerChildren="Tactic state" initiallyOpen goals={goals} displayCount />
                 </span>
             </LocationsContext.Provider>
-            <FilteredGoals
-                key="term-goal"
-                headerChildren="Expected type"
-                goals={termGoal !== undefined ? { goals: [termGoal] } : undefined}
-                initiallyOpen={config.showExpectedType}
-                displayCount={false}
-                togglingAction="toggleExpectedType"
-            />
+            {config.expectedTypeVisibility !== 'Hidden' && (
+                <FilteredGoals
+                    key="term-goal"
+                    headerChildren="Expected type"
+                    goals={termGoal !== undefined ? { goals: [termGoal] } : undefined}
+                    initiallyOpen={config.expectedTypeVisibility === 'Expanded by default'}
+                    displayCount={false}
+                    togglingAction="toggleExpectedType"
+                />
+            )}
             {userWidgets.map(widget => {
                 const inner = (
                     <PanelWidgetDisplay
@@ -327,7 +331,7 @@ function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) {
         setShouldRefresh(true)
     }
 
-    const { kind, goals, rpcSess } = props
+    const { kind, pos, onPin, goals, rpcSess } = props
 
     const ec = React.useContext(EditorContext)
 
@@ -353,10 +357,70 @@ function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) {
         'togglePaused',
     )
 
+    const id = React.useId()
+    useEvent(
+        ec.events.clickedContextMenu,
+        _ => {
+            setPaused(true)
+        },
+        [setPaused],
+        `pause:${id}`,
+    )
+    useEvent(
+        ec.events.clickedContextMenu,
+        _ => {
+            setPaused(false)
+        },
+        [setPaused],
+        `unpause:${id}`,
+    )
+    useEvent(
+        ec.events.clickedContextMenu,
+        _ => {
+            if (isCursor) {
+                onPin(pos)
+            }
+        },
+        [isCursor, onPin, pos],
+        `pin:${id}`,
+    )
+    useEvent(
+        ec.events.clickedContextMenu,
+        _ => {
+            if (!isCursor) {
+                onPin(pos)
+            }
+        },
+        [isCursor, onPin, pos],
+        `unpin:${id}`,
+    )
+    useEvent(
+        ec.events.clickedContextMenu,
+        _ => {
+            void triggerDisplayUpdate()
+        },
+        [isCursor, onPin, pos],
+        `refresh:${id}`,
+    )
+    useEvent(ec.events.clickedContextMenu, async _ => void ec.revealPosition(pos), [pos], `goToPinnedLocation:${id}`)
+
+    const pauseContext = isPaused ? { unpauseId: id } : { pauseId: id }
+    const pinContext = isCursor ? { pinId: id } : { unpinId: id }
+    const refreshContext = isPaused ? { refreshId: id } : {}
+    const goToPinnedLocationContext = !isCursor ? { goToPinnedLocationId: id } : {}
+
     return (
         <RpcContext.Provider value={rpcSess}>
-            <EnvPosContext.Provider value={props.pos}>
-                <details open>
+            <EnvPosContext.Provider value={pos}>
+                <details
+                    data-vscode-context={JSON.stringify({
+                        ...pauseContext,
+                        ...pinContext,
+                        ...refreshContext,
+                        ...goToPinnedLocationContext,
+                    })}
+                    open
+                >
                     <InfoStatusBar
                         {...props}
                         triggerUpdate={triggerDisplayUpdate}
diff --git a/lean4-infoview/src/infoview/messages.tsx b/lean4-infoview/src/infoview/messages.tsx
index 7ecd5f6a5..49a87da1f 100644
--- a/lean4-infoview/src/infoview/messages.tsx
+++ b/lean4-infoview/src/infoview/messages.tsx
@@ -45,8 +45,17 @@ const MessageView = React.memo(({ uri, diag }: MessageViewProps) => {
         () => ({ uri, ...(diag.fullRange?.start || diag.range.start) }),
         [uri, diag.fullRange, diag.range],
     )
+
+    const goToMessageLocationId = React.useId()
+    useEvent(
+        ec.events.clickedContextMenu,
+        async _ => void ec.revealLocation(loc),
+        [loc],
+        `goToMessageLocation:${goToMessageLocationId}`,
+    )
+
     return (
-        <Details initiallyOpen>
+        <Details initiallyOpen data-vscode-context={JSON.stringify({ goToMessageLocationId })}>
             <span className={severityClass}>
                 {title}
                 <span className="fr" onClick={e => e.preventDefault()}>
@@ -55,22 +64,7 @@ const MessageView = React.memo(({ uri, diag }: MessageViewProps) => {
                         onClick={_ => {
                             void ec.revealLocation(loc)
                         }}
-                        title="reveal file location"
-                    ></a>
-                    <a
-                        className="link pointer mh2 dim codicon codicon-quote"
-                        data-id="copy-to-comment"
-                        onClick={_ => {
-                            if (node.current) void ec.copyToComment(node.current.innerText)
-                        }}
-                        title="copy message to comment"
-                    ></a>
-                    <a
-                        className="link pointer mh2 dim codicon codicon-clippy"
-                        onClick={_ => {
-                            if (node.current) void ec.api.copyToClipboard(node.current.innerText)
-                        }}
-                        title="copy message to clipboard"
+                        title="Go to source location of message"
                     ></a>
                 </span>
             </span>
@@ -186,9 +180,19 @@ export function AllMessages({ uri: uri0 }: { uri: DocumentUri }) {
     // When `undefined`, we can approximate it by `diags.length`.
     const [numDiags, setNumDiags] = React.useState<number | undefined>(undefined)
 
+    const id = React.useId()
+    useEvent(ec.events.clickedContextMenu, _ => setPaused(true), [], `pauseAllMessages:${id}`)
+    useEvent(ec.events.clickedContextMenu, _ => setPaused(false), [], `unpauseAllMessages:${id}`)
+
+    const context = isPaused ? { unpauseAllMessagesId: id } : { pauseAllMessagesId: id }
+
     return (
         <RpcContext.Provider value={rs}>
-            <Details setOpenRef={r => (setOpenRef.current = r)} initiallyOpen={!config.autoOpenShowsGoal}>
+            <Details
+                setOpenRef={r => (setOpenRef.current = r)}
+                initiallyOpen={!config.autoOpenShowsGoal}
+                data-vscode-context={JSON.stringify(context)}
+            >
                 <>
                     All Messages ({numDiags ?? diags.length})
                     <span
@@ -205,7 +209,7 @@ export function AllMessages({ uri: uri0 }: { uri: DocumentUri }) {
                             onClick={_ => {
                                 setPaused(p => !p)
                             }}
-                            title={isPaused ? 'continue updating' : 'pause updating'}
+                            title={isPaused ? "Unpause 'All Messages'" : "Pause 'All Messages'"}
                         ></a>
                     </span>
                 </>
diff --git a/lean4-infoview/src/infoview/tooltips.tsx b/lean4-infoview/src/infoview/tooltips.tsx
index ba4a1f0f3..d43c0304e 100644
--- a/lean4-infoview/src/infoview/tooltips.tsx
+++ b/lean4-infoview/src/infoview/tooltips.tsx
@@ -280,7 +280,9 @@ export function useHoverTooltip(
     }
 
     const onPointerOver = (e: React.PointerEvent<HTMLSpanElement>) => {
-        if (!isModifierHeld(e)) {
+        // eslint-disable-next-line no-bitwise
+        const isSelectionHover = (e.buttons & 1) !== 0
+        if (!isModifierHeld(e) && !isSelectionHover) {
             guardMouseEvent(_ => startShowTimeout(), e)
         }
     }
diff --git a/lean4-infoview/src/infoview/traceExplorer.tsx b/lean4-infoview/src/infoview/traceExplorer.tsx
index 6afc6e32f..fa7a33f8d 100644
--- a/lean4-infoview/src/infoview/traceExplorer.tsx
+++ b/lean4-infoview/src/infoview/traceExplorer.tsx
@@ -175,8 +175,10 @@ function InteractiveMessageTag({ tag: embed }: InteractiveTagProps<MsgEmbed>): J
         return (
             <Goal
                 goal={embed.goal}
-                filter={{
+                settings={{
                     reverse: false,
+                    hideGoalNames: false,
+                    emphasizeFirstGoal: false,
                     showType: true,
                     showInstance: true,
                     showHiddenAssumption: true,
diff --git a/lean4-unicode-input-component/package.json b/lean4-unicode-input-component/package.json
index a32008b8f..52a857384 100644
--- a/lean4-unicode-input-component/package.json
+++ b/lean4-unicode-input-component/package.json
@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/unicode-input-component",
-    "version": "0.1.2",
+    "version": "0.1.4",
     "description": "Typescript support for contenteditable divs with the Unicode input support of the Lean 4 theorem prover",
     "scripts": {
         "watch": "tsc --watch",
@@ -14,7 +14,7 @@
     ],
     "license": "Apache-2.0",
     "dependencies": {
-        "@leanprover/unicode-input": "^0.1.2"
+        "@leanprover/unicode-input": "^0.1.4"
     },
     "devDependencies": {
         "typescript": "^5.4.5"
diff --git a/lean4-unicode-input/package.json b/lean4-unicode-input/package.json
index a682157af..16644628c 100644
--- a/lean4-unicode-input/package.json
+++ b/lean4-unicode-input/package.json
@@ -1,6 +1,6 @@
 {
     "name": "@leanprover/unicode-input",
-    "version": "0.1.2",
+    "version": "0.1.4",
     "description": "Unicode input mechanism for the Lean 4 theorem prover",
     "scripts": {
         "watch": "tsc --watch",
diff --git a/lean4-unicode-input/src/abbreviations.json b/lean4-unicode-input/src/abbreviations.json
index 65ae7905d..669a7f830 100644
--- a/lean4-unicode-input/src/abbreviations.json
+++ b/lean4-unicode-input/src/abbreviations.json
@@ -579,7 +579,6 @@
     "pitchfork": "⋔",
     "psi": "ψ",
     "phi": "φ",
-    "8<": "✂",
     "leqn": "≰",
     "leqq": "≦",
     "leqslant": "≤",
@@ -710,6 +709,7 @@
     ">~": "≳",
     ">>": "⟫",
     "root": "√",
+    "scissor": "✂",
     "ssubn": "⊄",
     "ssub": "⊂",
     "ssupn": "⊅",
@@ -1819,6 +1819,7 @@
     "X": "⨯",
     "vectorproduct": "⨯",
     "crossproduct": "⨯",
+    "xs": "×ˢ",
     "coprod": "⨿",
     "sigmaobj": "∐",
     "xf": "×ᶠ",
@@ -1829,5 +1830,7 @@
     "goal": "⊢",
     "Vdash": "⊩",
     "Vert": "‖",
-    "Vvdash": "⊪"
+    "Vvdash": "⊪",
+    "tiny": "⧾",
+    "miny": "⧿"
 }
diff --git a/package-lock.json b/package-lock.json
index aaefc8fc2..f89f7e539 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -28,10 +28,10 @@
         },
         "lean4-infoview": {
             "name": "@leanprover/infoview",
-            "version": "0.8.3",
+            "version": "0.8.5",
             "license": "Apache-2.0",
             "dependencies": {
-                "@leanprover/infoview-api": "~0.6.0",
+                "@leanprover/infoview-api": "~0.7.0",
                 "@vscode-elements/react-elements": "^0.5.0",
                 "@vscode/codicons": "^0.0.32",
                 "es-module-lexer": "^1.5.4",
@@ -67,7 +67,7 @@
         },
         "lean4-infoview-api": {
             "name": "@leanprover/infoview-api",
-            "version": "0.6.0",
+            "version": "0.7.0",
             "license": "Apache-2.0",
             "devDependencies": {
                 "typescript": "^5.4.5",
@@ -76,7 +76,7 @@
         },
         "lean4-unicode-input": {
             "name": "@leanprover/unicode-input",
-            "version": "0.1.2",
+            "version": "0.1.4",
             "license": "Apache-2.0",
             "devDependencies": {
                 "typescript": "^5.4.5"
@@ -84,10 +84,10 @@
         },
         "lean4-unicode-input-component": {
             "name": "@leanprover/unicode-input-component",
-            "version": "0.1.2",
+            "version": "0.1.4",
             "license": "Apache-2.0",
             "dependencies": {
-                "@leanprover/unicode-input": "^0.1.2"
+                "@leanprover/unicode-input": "^0.1.4"
             },
             "devDependencies": {
                 "typescript": "^5.4.5"
@@ -16903,13 +16903,13 @@
         },
         "vscode-lean4": {
             "name": "lean4",
-            "version": "0.0.195",
+            "version": "0.0.204",
             "license": "Apache-2.0",
             "dependencies": {
-                "@leanprover/infoview": "~0.8.3",
-                "@leanprover/infoview-api": "~0.6.0",
-                "@leanprover/unicode-input": "~0.1.2",
-                "@leanprover/unicode-input-component": "~0.1.2",
+                "@leanprover/infoview": "~0.8.5",
+                "@leanprover/infoview-api": "~0.7.0",
+                "@leanprover/unicode-input": "~0.1.4",
+                "@leanprover/unicode-input-component": "~0.1.4",
                 "@vscode-elements/elements": "^1.7.1",
                 "@vscode/codicons": "^0.0.36",
                 "markdown-it": "^14.1.0",
@@ -17034,4 +17034,4 @@
             }
         }
     }
-}
\ No newline at end of file
+}
diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json
index de845a894..aad826e0e 100644
--- a/vscode-lean4/package.json
+++ b/vscode-lean4/package.json
@@ -2,7 +2,7 @@
     "name": "lean4",
     "displayName": "Lean 4",
     "description": "Lean 4 language support for VS Code",
-    "version": "0.0.196",
+    "version": "0.0.207",
     "publisher": "leanprover",
     "engines": {
         "vscode": "^1.75.0"
@@ -95,6 +95,17 @@
                         "description": "an argument to pass to the server"
                     }
                 },
+                "lean4.trace.server": {
+                    "type": "string",
+                    "default": "off",
+                    "enum": [
+                        "off",
+                        "messages",
+                        "compact",
+                        "verbose"
+                    ],
+                    "markdownDescription": "Whether to enable client-side logging for language server messages."
+                },
                 "lean4.serverLogging.enabled": {
                     "type": "boolean",
                     "default": false,
@@ -139,7 +150,18 @@
                 "lean4.infoview.showExpectedType": {
                     "type": "boolean",
                     "default": true,
-                    "markdownDescription": "Show the expected type by default."
+                    "markdownDescription": "Show the expected type by default.",
+                    "deprecationMessage": "Superseded by the 'InfoView: Expected Type Visibility' setting."
+                },
+                "lean4.infoview.expectedTypeVisibility": {
+                    "type": "string",
+                    "enum": [
+                        "Expanded by default",
+                        "Collapsed by default",
+                        "Hidden"
+                    ],
+                    "default": "Expanded by default",
+                    "markdownDescription": "Default visibility of the expected type."
                 },
                 "lean4.infoview.showGoalNames": {
                     "type": "boolean",
@@ -152,10 +174,31 @@
                     "markdownDescription": "Display goals other than the main goal in a smaller font size."
                 },
                 "lean4.infoview.reverseTacticState": {
+                    "title": "Display Target Before Assumptions",
                     "type": "boolean",
                     "default": false,
                     "markdownDescription": "Default to showing the goal type first and then the local context."
                 },
+                "lean4.infoview.hideTypeAssumptions": {
+                    "type": "boolean",
+                    "default": false,
+                    "markdownDescription": "Default to hiding type assumptions from the local context."
+                },
+                "lean4.infoview.hideInstanceAssumptions": {
+                    "type": "boolean",
+                    "default": false,
+                    "markdownDescription": "Default to filtering instance assumptions from the local context."
+                },
+                "lean4.infoview.hideInaccessibleAssumptions": {
+                    "type": "boolean",
+                    "default": false,
+                    "markdownDescription": "Default to filtering hidden assumptions from the local context."
+                },
+                "lean4.infoview.hideLetValues": {
+                    "type": "boolean",
+                    "default": false,
+                    "markdownDescription": "Default to filtering type assumptions from the local context."
+                },
                 "lean4.infoview.showTooltipOnHover": {
                     "type": "boolean",
                     "default": true,
@@ -188,13 +231,13 @@
                 },
                 "lean4.unsolvedGoalsDecorationLightThemeColor": {
                     "type": "string",
-                    "default": "#1A85FF88",
-                    "markdownDescription": "Color used in unsolved goal decorations when using a light theme."
+                    "default": "editorInfo.foreground",
+                    "markdownDescription": "Color used in unsolved goal decorations when using a light theme. Can either denote a CSS color or a [VS Code theme color](https://code.visualstudio.com/api/references/theme-color)."
                 },
                 "lean4.unsolvedGoalsDecorationDarkThemeColor": {
                     "type": "string",
-                    "default": "#3794FF88",
-                    "markdownDescription": "Color used in unsolved goal decorations when using a dark theme."
+                    "default": "editorInfo.foreground",
+                    "markdownDescription": "Color used in unsolved goal decorations when using a dark theme. Can either denote a CSS color or a [VS Code theme color](https://code.visualstudio.com/api/references/theme-color)."
                 },
                 "lean4.goalsAccomplishedDecorationKind": {
                     "type": "string",
@@ -207,6 +250,11 @@
                     ],
                     "default": "Double Checkmark",
                     "markdownDescription": "Style of icon used in 'Goals accomplished' decoration."
+                },
+                "lean4.decorationEditDelay": {
+                    "type": "number",
+                    "default": 750,
+                    "markdownDescription": "Delay after an edit in milliseconds until certain editor decorations (like the 'unsolved goals' decoration) update."
                 }
             }
         },
@@ -215,13 +263,13 @@
                 "command": "lean4.restartServer",
                 "category": "Lean 4",
                 "title": "Server: Restart Server",
-                "description": "Restart the Lean server (for all files)."
+                "description": "Restarts the Lean server (for all files)."
             },
             {
                 "command": "lean4.stopServer",
                 "category": "Lean 4",
                 "title": "Server: Stop Server",
-                "description": "Stop the Lean server (for all files)."
+                "description": "Stops the Lean server (for all files)."
             },
             {
                 "command": "lean4.restartFile",
@@ -321,6 +369,150 @@
                 "title": "Unselect All",
                 "description": "This command is an implementation detail of the 'Unselect All' context menu option in the infoview."
             },
+            {
+                "command": "lean4.infoview.pause",
+                "category": "Lean 4",
+                "title": "Pause State",
+                "description": "This command is an implementation detail of the 'Pause State' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.unpause",
+                "category": "Lean 4",
+                "title": "Unpause State",
+                "description": "This command is an implementation detail of the 'Unpause State' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.pin",
+                "category": "Lean 4",
+                "title": "Pin State to Top",
+                "description": "This command is an implementation detail of the 'Pin State to Top' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.unpin",
+                "category": "Lean 4",
+                "title": "Unpin State",
+                "description": "This command is an implementation detail of the 'Unpin State' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.refresh",
+                "category": "Lean 4",
+                "title": "Refresh Paused State",
+                "description": "This command is an implementation detail of the 'Refresh Paused State' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.pauseAllMessages",
+                "category": "Lean 4",
+                "title": "Pause 'All Messages'",
+                "description": "This command is an implementation detail of the 'Pause 'All Messages'' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.unpauseAllMessages",
+                "category": "Lean 4",
+                "title": "Unpause 'All Messages'",
+                "description": "This command is an implementation detail of the 'Unpause 'All Messages'' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.goToPinnedLocation",
+                "category": "Lean 4",
+                "title": "Go to Pinned Location",
+                "description": "This command is an implementation detail of the 'Go to Pinned Location' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.goToMessageLocation",
+                "category": "Lean 4",
+                "title": "Go to Source Location of Message",
+                "description": "This command is an implementation detail of the 'Go to Source Location of Message' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.displayTargetBeforeAssumptions",
+                "category": "Lean 4",
+                "title": "Display Target Before Assumptions",
+                "description": "This command is an implementation detail of the 'Display Target Before Assumptions' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.displayAssumptionsBeforeTarget",
+                "category": "Lean 4",
+                "title": "Display Assumptions Before Target",
+                "description": "This command is an implementation detail of the 'Display Assumptions Before Target' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.hideTypeAssumptions",
+                "category": "Lean 4",
+                "title": "Hide Type Assumptions",
+                "description": "This command is an implementation detail of the 'Hide Type Assumptions' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.showTypeAssumptions",
+                "category": "Lean 4",
+                "title": "Show Type Assumptions",
+                "description": "This command is an implementation detail of the 'Show Type Assumptions' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.hideInstanceAssumptions",
+                "category": "Lean 4",
+                "title": "Hide Instance Assumptions",
+                "description": "This command is an implementation detail of the 'Hide Instance Assumptions' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.showInstanceAssumptions",
+                "category": "Lean 4",
+                "title": "Show Instance Assumptions",
+                "description": "This command is an implementation detail of the 'Show Instance Assumptions' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.hideInaccessibleAssumptions",
+                "category": "Lean 4",
+                "title": "Hide Inaccessible Assumptions",
+                "description": "This command is an implementation detail of the 'Hide Inaccessible Assumptions' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.showInaccessibleAssumptions",
+                "category": "Lean 4",
+                "title": "Show Inaccessible Assumptions",
+                "description": "This command is an implementation detail of the 'Show Inaccessible Assumptions' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.hideLetValues",
+                "category": "Lean 4",
+                "title": "Hide Let-Values",
+                "description": "This command is an implementation detail of the 'Hide Let-Values' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.showLetValues",
+                "category": "Lean 4",
+                "title": "Show Let-Values",
+                "description": "This command is an implementation detail of the 'Show Let-Values' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.hideGoalNames",
+                "category": "Lean 4",
+                "title": "Hide Goal Names",
+                "description": "This command is an implementation detail of the 'Hide Goal Names' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.showGoalNames",
+                "category": "Lean 4",
+                "title": "Show Goal Names",
+                "description": "This command is an implementation detail of the 'Show Goal Names' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.emphasizeFirstGoal",
+                "category": "Lean 4",
+                "title": "Emphasize First Goal",
+                "description": "This command is an implementation detail of the 'Emphasize First Goal' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.deemphasizeFirstGoal",
+                "category": "Lean 4",
+                "title": "De-Emphasize First Goal",
+                "description": "This command is an implementation detail of the 'De-Emphasize First Goal' context menu option in the infoview."
+            },
+            {
+                "command": "lean4.infoview.saveSettings",
+                "category": "Lean 4",
+                "title": "Save Current Settings to Default Settings",
+                "description": "This command is an implementation detail of the 'Save Current Settings to Default Settings' context menu option in the infoview."
+            },
             {
                 "command": "lean4.loogle.search",
                 "category": "Lean 4",
@@ -659,6 +851,102 @@
                     "command": "lean4.infoview.unselectAll",
                     "when": "false"
                 },
+                {
+                    "command": "lean4.infoview.pause",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.unpause",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.pin",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.unpin",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.refresh",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.pauseAllMessages",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.unpauseAllMessages",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.goToPinnedLocation",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.goToMessageLocation",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.displayTargetBeforeAssumptions",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.displayAssumptionsBeforeTarget",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.hideTypeAssumptions",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.showTypeAssumptions",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.hideInstanceAssumptions",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.showInstanceAssumptions",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.hideInaccessibleAssumptions",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.showInaccessibleAssumptions",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.hideLetValues",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.showLetValues",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.hideGoalNames",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.showGoalNames",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.emphasizeFirstGoal",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.deemphasizeFirstGoal",
+                    "when": "false"
+                },
+                {
+                    "command": "lean4.infoview.saveSettings",
+                    "when": "false"
+                },
                 {
                     "command": "lean4.loogle.search"
                 },
@@ -937,19 +1225,150 @@
             "webview/context": [
                 {
                     "command": "lean4.infoview.goToDefinition",
-                    "when": "webviewId == 'lean4_infoview' && interactiveCodeTagId"
+                    "when": "webviewId == 'lean4_infoview' && interactiveCodeTagId",
+                    "group": "0_term@1"
+                },
+                {
+                    "command": "lean4.infoview.goToPinnedLocation",
+                    "when": "webviewId == 'lean4_infoview' && goToPinnedLocationId",
+                    "group": "0_term@2"
+                },
+                {
+                    "command": "lean4.infoview.goToMessageLocation",
+                    "when": "webviewId == 'lean4_infoview' && goToMessageLocationId",
+                    "group": "0_term@3"
                 },
                 {
                     "command": "lean4.infoview.select",
-                    "when": "webviewId == 'lean4_infoview' && selectableLocationId"
+                    "when": "webviewId == 'lean4_infoview' && selectableLocationId",
+                    "group": "0_term@4"
                 },
                 {
                     "command": "lean4.infoview.unselect",
-                    "when": "webviewId == 'lean4_infoview' && unselectableLocationId"
+                    "when": "webviewId == 'lean4_infoview' && unselectableLocationId",
+                    "group": "0_term@5"
                 },
                 {
                     "command": "lean4.infoview.unselectAll",
-                    "when": "webviewId == 'lean4_infoview' && selectedLocationsId"
+                    "when": "webviewId == 'lean4_infoview' && selectedLocationsId",
+                    "group": "0_term@6"
+                },
+                {
+                    "command": "lean4.infoview.pin",
+                    "when": "webviewId == 'lean4_infoview' && pinId",
+                    "group": "1_info@1"
+                },
+                {
+                    "command": "lean4.infoview.unpin",
+                    "when": "webviewId == 'lean4_infoview' && unpinId",
+                    "group": "1_info@2"
+                },
+                {
+                    "command": "lean4.infoview.pause",
+                    "when": "webviewId == 'lean4_infoview' && pauseId",
+                    "group": "1_info@3"
+                },
+                {
+                    "command": "lean4.infoview.unpause",
+                    "when": "webviewId == 'lean4_infoview' && unpauseId",
+                    "group": "1_info@4"
+                },
+                {
+                    "command": "lean4.infoview.refresh",
+                    "when": "webviewId == 'lean4_infoview' && refreshId",
+                    "group": "1_info@5"
+                },
+                {
+                    "command": "lean4.infoview.pauseAllMessages",
+                    "when": "webviewId == 'lean4_infoview' && pauseAllMessagesId",
+                    "group": "1_info@6"
+                },
+                {
+                    "command": "lean4.infoview.unpauseAllMessages",
+                    "when": "webviewId == 'lean4_infoview' && unpauseAllMessagesId",
+                    "group": "1_info@7"
+                },
+                {
+                    "submenu": "lean4.infoview.contextMenuSettings",
+                    "when": "webviewId == 'lean4_infoview'",
+                    "group": "z_settings@1"
+                }
+            ],
+            "lean4.infoview.contextMenuSettings": [
+                {
+                    "command": "lean4.infoview.displayTargetBeforeAssumptions",
+                    "when": "webviewId == 'lean4_infoview' && displayTargetBeforeAssumptionsId",
+                    "group": "0_settings@1"
+                },
+                {
+                    "command": "lean4.infoview.displayAssumptionsBeforeTarget",
+                    "when": "webviewId == 'lean4_infoview' && displayAssumptionsBeforeTargetId",
+                    "group": "0_settings@2"
+                },
+                {
+                    "command": "lean4.infoview.hideTypeAssumptions",
+                    "when": "webviewId == 'lean4_infoview' && hideTypeAssumptionsId",
+                    "group": "0_settings@3"
+                },
+                {
+                    "command": "lean4.infoview.showTypeAssumptions",
+                    "when": "webviewId == 'lean4_infoview' && showTypeAssumptionsId",
+                    "group": "0_settings@4"
+                },
+                {
+                    "command": "lean4.infoview.hideInstanceAssumptions",
+                    "when": "webviewId == 'lean4_infoview' && hideInstanceAssumptionsId",
+                    "group": "0_settings@5"
+                },
+                {
+                    "command": "lean4.infoview.showInstanceAssumptions",
+                    "when": "webviewId == 'lean4_infoview' && showInstanceAssumptionsId",
+                    "group": "0_settings@6"
+                },
+                {
+                    "command": "lean4.infoview.hideInaccessibleAssumptions",
+                    "when": "webviewId == 'lean4_infoview' && hideInaccessibleAssumptionsId",
+                    "group": "0_settings@7"
+                },
+                {
+                    "command": "lean4.infoview.showInaccessibleAssumptions",
+                    "when": "webviewId == 'lean4_infoview' && showInaccessibleAssumptionsId",
+                    "group": "0_settings@8"
+                },
+                {
+                    "command": "lean4.infoview.hideLetValues",
+                    "when": "webviewId == 'lean4_infoview' && hideLetValuesId",
+                    "group": "0_settings@9"
+                },
+                {
+                    "command": "lean4.infoview.showLetValues",
+                    "when": "webviewId == 'lean4_infoview' && showLetValuesId",
+                    "group": "0_settings@10"
+                },
+                {
+                    "command": "lean4.infoview.hideGoalNames",
+                    "when": "webviewId == 'lean4_infoview' && hideGoalNamesId",
+                    "group": "0_settings@11"
+                },
+                {
+                    "command": "lean4.infoview.showGoalNames",
+                    "when": "webviewId == 'lean4_infoview' && showGoalNamesId",
+                    "group": "0_settings@12"
+                },
+                {
+                    "command": "lean4.infoview.emphasizeFirstGoal",
+                    "when": "webviewId == 'lean4_infoview' && emphasizeFirstGoalId",
+                    "group": "0_settings@13"
+                },
+                {
+                    "command": "lean4.infoview.deemphasizeFirstGoal",
+                    "when": "webviewId == 'lean4_infoview' && deemphasizeFirstGoalId",
+                    "group": "0_settings@14"
+                },
+                {
+                    "command": "lean4.infoview.saveSettings",
+                    "when": "webviewId == 'lean4_infoview' && saveSettingsId",
+                    "group": "1_save@1"
                 }
             ]
         },
@@ -981,6 +1400,10 @@
             {
                 "id": "lean4.titlebar.documentation",
                 "label": "Documentation…"
+            },
+            {
+                "id": "lean4.infoview.contextMenuSettings",
+                "label": "Settings…"
             }
         ],
         "semanticTokenScopes": [
@@ -993,6 +1416,10 @@
             }
         ],
         "configurationDefaults": {
+            "files.readonlyInclude": {
+                "**/.lake/**/*.lean": true,
+                "**/.elan/**/*.lean": true
+            },
             "[lean4]": {
                 "editor.unicodeHighlight.ambiguousCharacters": false,
                 "editor.tabSize": 2,
@@ -1113,10 +1540,10 @@
         "test": "node ./out/test/suite/runTest.js"
     },
     "dependencies": {
-        "@leanprover/infoview": "~0.8.3",
-        "@leanprover/infoview-api": "~0.6.0",
-        "@leanprover/unicode-input": "~0.1.2",
-        "@leanprover/unicode-input-component": "~0.1.2",
+        "@leanprover/infoview": "~0.8.5",
+        "@leanprover/infoview-api": "~0.7.0",
+        "@leanprover/unicode-input": "~0.1.4",
+        "@leanprover/unicode-input-component": "~0.1.4",
         "@vscode/codicons": "^0.0.36",
         "@vscode-elements/elements": "^1.7.1",
         "markdown-it": "^14.1.0",
diff --git a/vscode-lean4/src/abbreviation/VSCodeAbbreviationRewriter.ts b/vscode-lean4/src/abbreviation/VSCodeAbbreviationRewriter.ts
index d9b302fc5..f54b8d4ce 100644
--- a/vscode-lean4/src/abbreviation/VSCodeAbbreviationRewriter.ts
+++ b/vscode-lean4/src/abbreviation/VSCodeAbbreviationRewriter.ts
@@ -59,6 +59,10 @@ export class VSCodeAbbreviationRewriter implements AbbreviationTextSource {
                     newText: changeEvent.text,
                 }))
                 this.rewriter.changeInput(changes)
+
+                // lean4monaco: We need to wait for changes to take effect. Otherwise, the cursor will be at the wrong position.
+                await new Promise(resolve => setTimeout(resolve, 0));
+
                 await this.rewriter.triggerAbbreviationReplacement()
 
                 this.updateState()
@@ -89,7 +93,8 @@ export class VSCodeAbbreviationRewriter implements AbbreviationTextSource {
     }
 
     selectionMoveMode(): SelectionMoveMode {
-        return { kind: 'OnlyMoveCursorSelections', updateUnchangedSelections: this.isVimExtensionInstalled }
+        // lean4monaco: This setting ensures that the cursor will move correctly in the browser.
+        return { kind: 'MoveAllSelections' }
     }
 
     collectSelections(): Range[] {
diff --git a/vscode-lean4/src/config.ts b/vscode-lean4/src/config.ts
index 0dc885c37..a13cb1e8b 100644
--- a/vscode-lean4/src/config.ts
+++ b/vscode-lean4/src/config.ts
@@ -1,9 +1,13 @@
-import { ConfigurationTarget, workspace } from 'vscode'
+import { ConfigurationTarget, ThemeColor, workspace } from 'vscode'
 import { elanStableChannel } from './utils/elan'
 import { PATH } from './utils/envPath'
 
-// TODO: does currently not contain config options for `./abbreviation`
-// so that it is easy to keep it in sync with vscode-lean.
+function processConfigColor(c: string): ThemeColor | string {
+    if (c.match(/^(#|rgb\(|rgba\(|hsl\(|hsla\()/)) {
+        return c
+    }
+    return new ThemeColor(c)
+}
 
 export function getPowerShellPath(): string {
     const windir = process.env.windir
@@ -77,10 +81,19 @@ export function getInfoViewDebounceTime(): number {
     return workspace.getConfiguration('lean4.infoview').get('debounceTime', 50)
 }
 
-export function getInfoViewShowExpectedType(): boolean {
+function getInfoViewShowExpectedType(): boolean {
     return workspace.getConfiguration('lean4.infoview').get('showExpectedType', true)
 }
 
+export function getInfoViewExpectedTypeVisibility(): 'Expanded by default' | 'Collapsed by default' | 'Hidden' {
+    const show = getInfoViewShowExpectedType()
+    const visibility = workspace.getConfiguration('lean4.infoview').get('expectedTypeVisibility', 'Expanded by default')
+    if (!show && visibility === 'Expanded by default') {
+        return 'Collapsed by default'
+    }
+    return visibility
+}
+
 export function getInfoViewShowGoalNames(): boolean {
     return workspace.getConfiguration('lean4.infoview').get('showGoalNames', true)
 }
@@ -93,6 +106,22 @@ export function getInfoViewReverseTacticState(): boolean {
     return workspace.getConfiguration('lean4.infoview').get('reverseTacticState', false)
 }
 
+export function getInfoViewHideTypeAssumptions(): boolean {
+    return workspace.getConfiguration('lean4.infoview').get('hideTypeAssumptions', false)
+}
+
+export function getInfoViewHideInstanceAssumptions(): boolean {
+    return workspace.getConfiguration('lean4.infoview').get('hideInstanceAssumptions', false)
+}
+
+export function getInfoViewHideInaccessibleAssumptions(): boolean {
+    return workspace.getConfiguration('lean4.infoview').get('hideInaccessibleAssumptions', false)
+}
+
+export function getInfoViewHideLetValues(): boolean {
+    return workspace.getConfiguration('lean4.infoview').get('hideLetValues', false)
+}
+
 export function getInfoViewShowTooltipOnHover(): boolean {
     return workspace.getConfiguration('lean4.infoview').get('showTooltipOnHover', true)
 }
@@ -117,18 +146,26 @@ export function showUnsolvedGoalsDecoration(): boolean {
     return workspace.getConfiguration('lean4').get('showUnsolvedGoalsDecoration', true)
 }
 
-export function unsolvedGoalsDecorationLightThemeColor(): string {
-    return workspace.getConfiguration('lean4').get('unsolvedGoalsDecorationLightThemeColor', '#1A85FF88')
+export function unsolvedGoalsDecorationLightThemeColor(): ThemeColor | string {
+    return processConfigColor(
+        workspace.getConfiguration('lean4').get('unsolvedGoalsDecorationLightThemeColor', 'editorInfo.foreground'),
+    )
 }
 
-export function unsolvedGoalsDecorationDarkThemeColor(): string {
-    return workspace.getConfiguration('lean4').get('unsolvedGoalsDecorationDarkThemeColor', '#3794FF88')
+export function unsolvedGoalsDecorationDarkThemeColor(): ThemeColor | string {
+    return processConfigColor(
+        workspace.getConfiguration('lean4').get('unsolvedGoalsDecorationDarkThemeColor', 'editorInfo.foreground'),
+    )
 }
 
 export function goalsAccomplishedDecorationKind(): string {
     return workspace.getConfiguration('lean4').get('goalsAccomplishedDecorationKind', 'Double Checkmark')
 }
 
+export function decorationEditDelay(): number {
+    return workspace.getConfiguration('lean4').get('decorationEditDelay', 750)
+}
+
 export function isRunningTest(): boolean {
     return typeof process.env.LEAN4_TEST_FOLDER === 'string'
 }
diff --git a/vscode-lean4/src/diagnostics/fullDiagnostics.ts b/vscode-lean4/src/diagnostics/fullDiagnostics.ts
index 0ab72590b..9beef9ff6 100644
--- a/vscode-lean4/src/diagnostics/fullDiagnostics.ts
+++ b/vscode-lean4/src/diagnostics/fullDiagnostics.ts
@@ -1,11 +1,11 @@
 import { SemVer } from 'semver'
-import { Disposable, OutputChannel, commands, env } from 'vscode'
+import { commands, Disposable, env, OutputChannel } from 'vscode'
 import { ExecutionExitCode, ExecutionResult } from '../utils/batch'
 import { ElanInstalledToolchain, ElanToolchains, ElanUnresolvedToolchain } from '../utils/elan'
-import { FileUri } from '../utils/exturi'
+import { extUriToCwdUri, FileUri } from '../utils/exturi'
 import { lean } from '../utils/leanEditorProvider'
 import { displayNotification, displayNotificationWithInput } from '../utils/notifs'
-import { findLeanProjectRoot } from '../utils/projectInfo'
+import { findLeanProjectRootInfo } from '../utils/projectInfo'
 import {
     ElanDumpStateWithoutNetQueryResult,
     ElanVersionDiagnosis,
@@ -228,17 +228,25 @@ export class FullDiagnosticsProvider implements Disposable {
         // in which case we still want to provide adequate diagnostics. Hence, we use the last active Lean document,
         // regardless of whether there is an actual `LeanClient` managing it.
         const lastActiveLeanDocumentUri = lean.lastActiveLeanDocument?.extUri
-        const projectUri =
-            lastActiveLeanDocumentUri !== undefined && lastActiveLeanDocumentUri.scheme === 'file'
-                ? await findLeanProjectRoot(lastActiveLeanDocumentUri)
+        const projectInfo =
+            lastActiveLeanDocumentUri !== undefined
+                ? await findLeanProjectRootInfo(lastActiveLeanDocumentUri)
                 : undefined
-        if (projectUri === 'FileNotFound') {
+        if (projectInfo?.kind === 'FileNotFound') {
             displayNotification(
                 'Error',
                 `Cannot display setup information for file that does not exist in the file system: ${lastActiveLeanDocumentUri}. Please choose a different file to display the setup information for.`,
             )
             return
         }
+        if (projectInfo?.kind === 'LakefileWithoutToolchain') {
+            displayNotification(
+                'Error',
+                `Cannot display setup information for file in invalid project: Project at ${projectInfo.projectRootUri} has a Lakefile, but no 'lean-toolchain' file. Please create one with the Lean version that you would like the project to use.`,
+            )
+            return
+        }
+        const projectUri = projectInfo !== undefined ? extUriToCwdUri(projectInfo.projectRootUri) : undefined
         const fullDiagnostics = await performFullDiagnosis(this.outputChannel, projectUri)
         const formattedFullDiagnostics = formatFullDiagnostics(fullDiagnostics)
         const copyToClipboardInput = 'Copy to Clipboard'
diff --git a/vscode-lean4/src/diagnostics/setupDiagnoser.ts b/vscode-lean4/src/diagnostics/setupDiagnoser.ts
index 74d39212c..12cfe4ad6 100644
--- a/vscode-lean4/src/diagnostics/setupDiagnoser.ts
+++ b/vscode-lean4/src/diagnostics/setupDiagnoser.ts
@@ -27,6 +27,11 @@ export type VersionQueryResult =
     | { kind: 'Cancelled' }
     | { kind: 'InvalidVersion'; versionResult: string }
 
+export type LakeAvailabilityResult =
+    | { kind: 'Available' }
+    | { kind: 'NotAvailable' }
+    | { kind: 'Error'; message: string }
+    | { kind: 'Cancelled' }
 export type ElanDumpStateWithoutNetQueryResult = ElanDumpStateWithoutNetResult | { kind: 'PreEagerResolutionVersion' }
 export type ElanDumpStateWithNetQueryResult = ElanDumpStateWithNetResult | { kind: 'PreEagerResolutionVersion' }
 
@@ -176,14 +181,18 @@ export class SetupDiagnoser {
         return gitVersionResult.exitCode === ExecutionExitCode.Success
     }
 
-    async queryLakeVersion(): Promise<VersionQueryResult> {
+    async checkLakeAvailable(): Promise<LakeAvailabilityResult> {
         const lakeVersionResult = await this.runLeanCommand('lake', ['--version'], 'Checking Lake version')
-        return versionQueryResult(lakeVersionResult, /version (\d+\.\d+\.\d+(\w|-)*)/)
-    }
-
-    async checkLakeAvailable(): Promise<boolean> {
-        const lakeVersionResult = await this.queryLakeVersion()
-        return lakeVersionResult.kind === 'Success'
+        switch (lakeVersionResult.exitCode) {
+            case ExecutionExitCode.Success:
+                return { kind: 'Available' }
+            case ExecutionExitCode.CannotLaunch:
+                return { kind: 'NotAvailable' }
+            case ExecutionExitCode.ExecutionError:
+                return { kind: 'Error', message: lakeVersionResult.combined }
+            case ExecutionExitCode.Cancelled:
+                return { kind: 'Cancelled' }
+        }
     }
 
     querySystemInformation(): SystemQueryResult {
diff --git a/vscode-lean4/src/diagnostics/setupDiagnostics.ts b/vscode-lean4/src/diagnostics/setupDiagnostics.ts
index be09f94c4..09e5b1372 100644
--- a/vscode-lean4/src/diagnostics/setupDiagnostics.ts
+++ b/vscode-lean4/src/diagnostics/setupDiagnostics.ts
@@ -1,6 +1,7 @@
 import { SemVer } from 'semver'
 import { OutputChannel, commands } from 'vscode'
 import { ExtUri, FileUri, extUriToCwdUri } from '../utils/exturi'
+import { displayInternalError } from '../utils/internalErrors'
 import { ToolchainUpdateMode } from '../utils/leanCmdRunner'
 import { LeanInstaller } from '../utils/leanInstaller'
 import { diagnose } from './setupDiagnoser'
@@ -32,6 +33,22 @@ const ancientLean4ProjectWarningMessage = (origin: string, projectVersion: SemVe
     `${origin} is using a Lean 4 version (${projectVersion.toString()}) from before the first Lean 4 stable release (4.0.0).
 Pre-stable Lean 4 versions are increasingly less supported, so please consider updating to a newer Lean 4 version.`
 
+const oldServerFolderContainsNewServerFolderErrorMessage = (
+    folderUri: FileUri,
+    fileUri: FileUri,
+    clientFolderUri: FileUri,
+) =>
+    `Error while starting language server: The project at '${folderUri.fsPath}' of the file '${fileUri.baseName()}' is contained inside of another project at '${clientFolderUri.fsPath}', for which a language server is already running.
+The Lean 4 VS Code extension does not support nested Lean projects.`
+
+const newServerFolderContainsOldServerFolderErrorMessage = (
+    folderUri: FileUri,
+    fileUri: FileUri,
+    clientFolderUri: FileUri,
+) =>
+    `Error while starting language server: The project at '${folderUri.fsPath}' of the file '${fileUri.baseName()}' contains another project at '${clientFolderUri.fsPath}', for which a language server is already running.
+The Lean 4 VS Code extension does not support nested Lean projects.`
+
 export class SetupDiagnostics {
     private n: SetupNotifier
 
@@ -163,6 +180,56 @@ export class SetupDiagnostics {
         }
     }
 
+    async checkIsNestedProjectFolder(
+        existingFolderUris: ExtUri[],
+        folderUri: ExtUri,
+        fileUri: ExtUri,
+        stopOtherServer: (folderUri: FileUri) => Promise<void>,
+    ): Promise<PreconditionCheckResult> {
+        if (folderUri.scheme === 'untitled' || fileUri.scheme === 'untitled') {
+            if (existingFolderUris.some(existingFolderUri => existingFolderUri.scheme === 'untitled')) {
+                await displayInternalError(
+                    'starting language server',
+                    'Attempting to start new untitled language server while one already exists.',
+                )
+                return 'Fatal'
+            }
+            return 'Fulfilled'
+        }
+
+        for (const existingFolderUri of existingFolderUris) {
+            if (existingFolderUri.scheme !== 'file') {
+                continue
+            }
+            if (existingFolderUri.isInFolder(folderUri)) {
+                return await this.n.displaySetupErrorWithInput(
+                    newServerFolderContainsOldServerFolderErrorMessage(folderUri, fileUri, existingFolderUri),
+                    [
+                        {
+                            input: 'Stop Other Server',
+                            continueDisplaying: false,
+                            action: () => stopOtherServer(existingFolderUri),
+                        },
+                    ],
+                )
+            }
+            if (folderUri.isInFolder(existingFolderUri)) {
+                return await this.n.displaySetupErrorWithInput(
+                    oldServerFolderContainsNewServerFolderErrorMessage(folderUri, fileUri, existingFolderUri),
+                    [
+                        {
+                            input: 'Stop Other Server',
+                            continueDisplaying: false,
+                            action: () => stopOtherServer(existingFolderUri),
+                        },
+                    ],
+                )
+            }
+        }
+
+        return 'Fulfilled'
+    }
+
     async checkIsLeanVersionUpToDate(
         channel: OutputChannel,
         context: string,
@@ -217,33 +284,30 @@ export class SetupDiagnostics {
         folderUri: ExtUri,
         options: { toolchainOverride?: string | undefined; toolchainUpdateMode: ToolchainUpdateMode },
     ): Promise<PreconditionCheckResult> {
-        const lakeVersionResult = await diagnose({
+        const lakeAvailabilityResult = await diagnose({
             channel,
             cwdUri: extUriToCwdUri(folderUri),
             toolchain: options.toolchainOverride,
             context,
             toolchainUpdateMode: options.toolchainUpdateMode,
-        }).queryLakeVersion()
-        switch (lakeVersionResult.kind) {
-            case 'CommandNotFound':
+        }).checkLakeAvailable()
+        switch (lakeAvailabilityResult.kind) {
+            case 'NotAvailable':
                 return this.n.displaySetupErrorWithOutput(
-                    "Error while checking Lake version: 'lake' command was not found.",
+                    "Error while checking Lake availability: 'lake' command was not found.",
                 )
 
-            case 'CommandError':
+            case 'Error':
                 return this.n.displaySetupErrorWithOutput(
-                    `Error while checking Lake version: ${lakeVersionResult.message}`,
+                    `Error while checking Lake availability: ${lakeAvailabilityResult.message}`,
                 )
 
             case 'Cancelled':
-                return this.n.displaySetupErrorWithOutput('Error while checking Lake version: Operation cancelled.')
-
-            case 'InvalidVersion':
                 return this.n.displaySetupErrorWithOutput(
-                    `Error while checking Lake version: Invalid Lake version format: '${lakeVersionResult.versionResult}'`,
+                    'Error while checking Lake availability: Operation cancelled.',
                 )
 
-            case 'Success':
+            case 'Available':
                 return 'Fulfilled'
         }
     }
diff --git a/vscode-lean4/src/extension.ts b/vscode-lean4/src/extension.ts
index 6f1b0a3b6..5b6b5a700 100644
--- a/vscode-lean4/src/extension.ts
+++ b/vscode-lean4/src/extension.ts
@@ -21,10 +21,10 @@ import { LeanConfigWatchService } from './utils/configwatchservice'
 import { ElanCommandProvider } from './utils/elanCommands'
 import { PATH, setProcessEnvPATH } from './utils/envPath'
 import { onEventWhile, withoutReentrancy } from './utils/events'
-import { FileUri } from './utils/exturi'
+import { ExtUri, extUriToCwdUri, FileUri } from './utils/exturi'
 import { displayInternalErrorsIn } from './utils/internalErrors'
 import { registerLeanCommandRunner } from './utils/leanCmdRunner'
-import { lean, LeanEditor, registerLeanEditorProvider } from './utils/leanEditorProvider'
+import { lean, registerLeanEditorProvider } from './utils/leanEditorProvider'
 import { LeanInstaller } from './utils/leanInstaller'
 import {
     displayActiveStickyNotification,
@@ -33,36 +33,28 @@ import {
     setStickyNotificationActiveButHidden,
 } from './utils/notifs'
 import { PathExtensionProvider } from './utils/pathExtensionProvider'
-import { findLeanProjectRoot } from './utils/projectInfo'
+import { findLeanProjectRootInfo } from './utils/projectInfo'
+import { UriHandlerService } from './utils/uriHandlerService'
 
 async function setLeanFeatureSetActive(isActive: boolean) {
     await commands.executeCommand('setContext', 'lean4.isLeanFeatureSetActive', isActive)
 }
 
-async function findLeanEditorProjectUri(editor: LeanEditor): Promise<FileUri | undefined | 'InvalidProject'> {
-    const docUri = editor.documentExtUri
-    const projectUri = docUri.scheme === 'file' ? await findLeanProjectRoot(docUri) : undefined
-    if (projectUri === 'FileNotFound') {
-        return 'InvalidProject'
-    }
-    return projectUri
-}
-
-async function findOpenLeanProjectUri(): Promise<FileUri | undefined | 'NoValidDocument'> {
+async function findOpenLeanProjectUri(): Promise<ExtUri | 'NoValidDocument'> {
     const activeEditor = lean.activeLeanEditor
     if (activeEditor !== undefined) {
-        const projectUri = await findLeanEditorProjectUri(activeEditor)
-        if (projectUri !== 'InvalidProject') {
-            return projectUri
+        const info = await findLeanProjectRootInfo(activeEditor.documentExtUri)
+        if (info.kind !== 'FileNotFound') {
+            return info.projectRootUri
         }
     }
 
     // This happens if vscode starts with a lean file open
     // but the "Getting Started" page is active.
     for (const editor of lean.visibleLeanEditors) {
-        const projectUri = await findLeanEditorProjectUri(editor)
-        if (projectUri !== 'InvalidProject') {
-            return projectUri
+        const info = await findLeanProjectRootInfo(editor.documentExtUri)
+        if (info.kind !== 'FileNotFound') {
+            return info.projectRootUri
         }
     }
 
@@ -152,6 +144,9 @@ function activateAlwaysEnabledFeatures(context: ExtensionContext): AlwaysEnabled
     const elanCommandProvider = new ElanCommandProvider(outputChannel)
     context.subscriptions.push(elanCommandProvider)
 
+    const uriHandlerService = new UriHandlerService()
+    context.subscriptions.push(uriHandlerService)
+
     return { projectInitializationProvider, outputChannel, installer, fullDiagnosticsProvider, elanCommandProvider }
 }
 
@@ -216,12 +211,12 @@ async function tryActivatingLean4FeaturesInProject(
     elanCommandProvider: ElanCommandProvider,
     resolve: (value: Lean4EnabledFeatures) => void,
     d: SetupDiagnostics,
-    projectUri: FileUri | undefined,
+    projectUri: ExtUri,
 ) {
     const preconditionCheckResult = await checkLean4FeaturePreconditions(
         installer,
         'Activate Lean 4 Extension',
-        projectUri,
+        extUriToCwdUri(projectUri),
         d,
     )
     if (preconditionCheckResult === 'Fatal') {
@@ -256,8 +251,8 @@ async function tryActivatingLean4Features(
         onEventWhile(
             lean.onDidRevealLeanEditor,
             withoutReentrancy('Continue', async editor => {
-                const projectUri = await findLeanEditorProjectUri(editor)
-                if (projectUri === 'InvalidProject') {
+                const info = await findLeanProjectRootInfo(editor.documentExtUri)
+                if (info.kind === 'FileNotFound') {
                     return 'Continue'
                 }
                 await tryActivatingLean4FeaturesInProject(
@@ -266,7 +261,7 @@ async function tryActivatingLean4Features(
                     elanCommandProvider,
                     resolve,
                     d,
-                    projectUri,
+                    info.projectRootUri,
                 )
                 return 'Stop'
             }),
diff --git a/vscode-lean4/src/infoview.ts b/vscode-lean4/src/infoview.ts
index b6a5a6b97..62d04586c 100644
--- a/vscode-lean4/src/infoview.ts
+++ b/vscode-lean4/src/infoview.ts
@@ -1,6 +1,7 @@
 import {
     EditorApi,
     InfoviewApi,
+    InfoviewConfig,
     LeanFileProgressParams,
     RpcConnected,
     RpcConnectParams,
@@ -12,16 +13,19 @@ import {
 import { join } from 'path'
 import {
     commands,
+    ConfigurationTarget,
     Diagnostic,
     Disposable,
     env,
     ExtensionContext,
+    Event,
     Position,
     Range,
     Selection,
     TextEditor,
     TextEditorRevealType,
     Uri,
+    ViewColumn,
     WebviewPanel,
     window,
     workspace,
@@ -34,8 +38,12 @@ import {
     getInfoViewAutoOpenShowsGoal,
     getInfoViewDebounceTime,
     getInfoViewEmphasizeFirstGoal,
+    getInfoViewExpectedTypeVisibility,
+    getInfoViewHideInaccessibleAssumptions,
+    getInfoViewHideInstanceAssumptions,
+    getInfoViewHideLetValues,
+    getInfoViewHideTypeAssumptions,
     getInfoViewReverseTacticState,
-    getInfoViewShowExpectedType,
     getInfoViewShowGoalNames,
     getInfoViewShowTooltipOnHover,
     getInfoViewStyle,
@@ -51,6 +59,7 @@ import { lean, LeanEditor } from './utils/leanEditorProvider'
 import { logger } from './utils/logger'
 import { displayNotification } from './utils/notifs'
 import { viewColumnOfActiveTextEditor, viewColumnOfInfoView } from './utils/viewColumn'
+import { IFrameInfoWebview, IFrameInfoWebviewFactory } from '../../../infowebview'
 
 const keepAlivePeriodMs = 10000
 
@@ -60,7 +69,7 @@ async function rpcConnect(client: LeanClient, uri: ls.DocumentUri): Promise<stri
     return result.sessionId
 }
 
-class RpcSessionAtPos implements Disposable {
+export class RpcSessionAtPos implements Disposable {
     keepAliveInterval?: NodeJS.Timeout
     client: LeanClient
 
@@ -89,7 +98,7 @@ class RpcSessionAtPos implements Disposable {
 
 export class InfoProvider implements Disposable {
     /** Instance of the panel, if it is open. Otherwise `undefined`. */
-    private webviewPanel?: WebviewPanel & { rpc: Rpc; api: InfoviewApi }
+    private webviewPanel?: IFrameInfoWebview
     private subscriptions: Disposable[] = []
     private clientSubscriptions: Disposable[] = []
 
@@ -138,6 +147,44 @@ export class InfoProvider implements Disposable {
     }
 
     private editorApi: EditorApi = {
+        saveConfig: async (config: InfoviewConfig) => {
+            await workspace
+                .getConfiguration('lean4.infoview')
+                .update('allErrorsOnLine', config.allErrorsOnLine, ConfigurationTarget.Global)
+            await workspace
+                .getConfiguration('lean4.infoview')
+                .update('autoOpenShowsGoal', config.autoOpenShowsGoal, ConfigurationTarget.Global)
+            await workspace
+                .getConfiguration('lean4.infoview')
+                .update('debounceTime', config.debounceTime, ConfigurationTarget.Global)
+            await workspace
+                .getConfiguration('lean4.infoview')
+                .update('expectedTypeVisibility', config.expectedTypeVisibility, ConfigurationTarget.Global)
+            await workspace
+                .getConfiguration('lean4.infoview')
+                .update('showGoalNames', config.showGoalNames, ConfigurationTarget.Global)
+            await workspace
+                .getConfiguration('lean4.infoview')
+                .update('emphasizeFirstGoal', config.emphasizeFirstGoal, ConfigurationTarget.Global)
+            await workspace
+                .getConfiguration('lean4.infoview')
+                .update('reverseTacticState', config.reverseTacticState, ConfigurationTarget.Global)
+            await workspace
+                .getConfiguration('lean4.infoview')
+                .update('hideTypeAssumptions', config.hideTypeAssumptions, ConfigurationTarget.Global)
+            await workspace
+                .getConfiguration('lean4.infoview')
+                .update('hideInstanceAssumptions', config.hideInstanceAssumptions, ConfigurationTarget.Global)
+            await workspace
+                .getConfiguration('lean4.infoview')
+                .update('hideInaccessibleAssumptions', config.hideInaccessibleAssumptions, ConfigurationTarget.Global)
+            await workspace
+                .getConfiguration('lean4.infoview')
+                .update('hideLetValues', config.hideLetValues, ConfigurationTarget.Global)
+            await workspace
+                .getConfiguration('lean4.infoview')
+                .update('showTooltipOnHover', config.showTooltipOnHover, ConfigurationTarget.Global)
+        },
         sendClientRequest: async (uri: string, method: string, params: any): Promise<any> => {
             const extUri = parseExtUri(uri)
             if (extUri === undefined) {
@@ -319,6 +366,7 @@ export class InfoProvider implements Disposable {
     constructor(
         private clientProvider: LeanClientProvider,
         private context: ExtensionContext,
+        private infoWebviewFactory: IFrameInfoWebviewFactory,
     ) {
         this.updateStylesheet()
 
@@ -375,6 +423,126 @@ export class InfoProvider implements Disposable {
             commands.registerCommand('lean4.infoview.unselectAll', args =>
                 this.webviewPanel?.api.clickedContextMenu({ entry: 'unselectAll', id: args.selectedLocationsId }),
             ),
+            commands.registerCommand('lean4.infoview.pause', args =>
+                this.webviewPanel?.api.clickedContextMenu({ entry: 'pause', id: args.pauseId }),
+            ),
+            commands.registerCommand('lean4.infoview.unpause', args =>
+                this.webviewPanel?.api.clickedContextMenu({ entry: 'unpause', id: args.unpauseId }),
+            ),
+            commands.registerCommand('lean4.infoview.pin', args =>
+                this.webviewPanel?.api.clickedContextMenu({ entry: 'pin', id: args.pinId }),
+            ),
+            commands.registerCommand('lean4.infoview.unpin', args =>
+                this.webviewPanel?.api.clickedContextMenu({ entry: 'unpin', id: args.unpinId }),
+            ),
+            commands.registerCommand('lean4.infoview.refresh', args =>
+                this.webviewPanel?.api.clickedContextMenu({ entry: 'refresh', id: args.refreshId }),
+            ),
+            commands.registerCommand('lean4.infoview.pauseAllMessages', args =>
+                this.webviewPanel?.api.clickedContextMenu({
+                    entry: 'pauseAllMessages',
+                    id: args.pauseAllMessagesId,
+                }),
+            ),
+            commands.registerCommand('lean4.infoview.unpauseAllMessages', args =>
+                this.webviewPanel?.api.clickedContextMenu({
+                    entry: 'unpauseAllMessages',
+                    id: args.unpauseAllMessagesId,
+                }),
+            ),
+            commands.registerCommand('lean4.infoview.goToPinnedLocation', args =>
+                this.webviewPanel?.api.clickedContextMenu({
+                    entry: 'goToPinnedLocation',
+                    id: args.goToPinnedLocationId,
+                }),
+            ),
+            commands.registerCommand('lean4.infoview.goToMessageLocation', args =>
+                this.webviewPanel?.api.clickedContextMenu({
+                    entry: 'goToMessageLocation',
+                    id: args.goToMessageLocationId,
+                }),
+            ),
+            commands.registerCommand('lean4.infoview.displayTargetBeforeAssumptions', args =>
+                this.webviewPanel?.api.clickedContextMenu({
+                    entry: 'displayTargetBeforeAssumptions',
+                    id: args.displayTargetBeforeAssumptionsId,
+                }),
+            ),
+            commands.registerCommand('lean4.infoview.displayAssumptionsBeforeTarget', args =>
+                this.webviewPanel?.api.clickedContextMenu({
+                    entry: 'displayAssumptionsBeforeTarget',
+                    id: args.displayAssumptionsBeforeTargetId,
+                }),
+            ),
+            commands.registerCommand('lean4.infoview.hideTypeAssumptions', args =>
+                this.webviewPanel?.api.clickedContextMenu({
+                    entry: 'hideTypeAssumptions',
+                    id: args.hideTypeAssumptionsId,
+                }),
+            ),
+            commands.registerCommand('lean4.infoview.showTypeAssumptions', args =>
+                this.webviewPanel?.api.clickedContextMenu({
+                    entry: 'showTypeAssumptions',
+                    id: args.showTypeAssumptionsId,
+                }),
+            ),
+            commands.registerCommand('lean4.infoview.hideInstanceAssumptions', args =>
+                this.webviewPanel?.api.clickedContextMenu({
+                    entry: 'hideInstanceAssumptions',
+                    id: args.hideInstanceAssumptionsId,
+                }),
+            ),
+            commands.registerCommand('lean4.infoview.showInstanceAssumptions', args =>
+                this.webviewPanel?.api.clickedContextMenu({
+                    entry: 'showInstanceAssumptions',
+                    id: args.showInstanceAssumptionsId,
+                }),
+            ),
+            commands.registerCommand('lean4.infoview.hideInaccessibleAssumptions', args =>
+                this.webviewPanel?.api.clickedContextMenu({
+                    entry: 'hideInaccessibleAssumptions',
+                    id: args.hideInaccessibleAssumptionsId,
+                }),
+            ),
+            commands.registerCommand('lean4.infoview.showInaccessibleAssumptions', args =>
+                this.webviewPanel?.api.clickedContextMenu({
+                    entry: 'showInaccessibleAssumptions',
+                    id: args.showInaccessibleAssumptionsId,
+                }),
+            ),
+            commands.registerCommand('lean4.infoview.hideLetValues', args =>
+                this.webviewPanel?.api.clickedContextMenu({ entry: 'hideLetValues', id: args.hideLetValuesId }),
+            ),
+            commands.registerCommand('lean4.infoview.showLetValues', args =>
+                this.webviewPanel?.api.clickedContextMenu({ entry: 'showLetValues', id: args.showLetValuesId }),
+            ),
+            commands.registerCommand('lean4.infoview.hideGoalNames', args =>
+                this.webviewPanel?.api.clickedContextMenu({
+                    entry: 'hideGoalNames',
+                    id: args.hideGoalNamesId,
+                }),
+            ),
+            commands.registerCommand('lean4.infoview.showGoalNames', args =>
+                this.webviewPanel?.api.clickedContextMenu({
+                    entry: 'showGoalNames',
+                    id: args.showGoalNamesId,
+                }),
+            ),
+            commands.registerCommand('lean4.infoview.emphasizeFirstGoal', args =>
+                this.webviewPanel?.api.clickedContextMenu({
+                    entry: 'emphasizeFirstGoal',
+                    id: args.emphasizeFirstGoalId,
+                }),
+            ),
+            commands.registerCommand('lean4.infoview.deemphasizeFirstGoal', args =>
+                this.webviewPanel?.api.clickedContextMenu({
+                    entry: 'deemphasizeFirstGoal',
+                    id: args.deemphasizeFirstGoalId,
+                }),
+            ),
+            commands.registerCommand('lean4.infoview.saveSettings', args =>
+                this.webviewPanel?.api.clickedContextMenu({ entry: 'saveSettings', id: args.saveSettingsId }),
+            ),
         )
     }
 
@@ -590,9 +758,11 @@ export class InfoProvider implements Disposable {
         if (this.webviewPanel) {
             this.webviewPanel.reveal(undefined, true)
         } else {
-            const webviewPanel = window.createWebviewPanel(
+            const webviewPanel = this.infoWebviewFactory.make(this.editorApi, this.stylesheet)
+            /*
+            window.createWebviewPanel(
                 'lean4_infoview',
-                'Lean Infoview',
+                'Lean InfoView',
                 { viewColumn: viewColumnOfInfoView(), preserveFocus: true },
                 {
                     enableFindWidget: true,
@@ -625,13 +795,13 @@ export class InfoProvider implements Disposable {
                 }
             })
             webviewPanel.api = webviewPanel.rpc.getApi()
+            */
             webviewPanel.onDidDispose(() => {
                 this.webviewPanel = undefined
                 this.clearNotificationHandlers()
                 this.clearRpcSessions(null) // should be after `webviewPanel = undefined`
             })
             this.webviewPanel = webviewPanel
-            webviewPanel.webview.html = this.initialHtml()
 
             const client = this.clientProvider.findClient(leanEditor.documentExtUri)
             await this.initInfoView(leanEditor, client)
@@ -669,10 +839,14 @@ export class InfoProvider implements Disposable {
             allErrorsOnLine: getInfoViewAllErrorsOnLine(),
             autoOpenShowsGoal: getInfoViewAutoOpenShowsGoal(),
             debounceTime: getInfoViewDebounceTime(),
-            showExpectedType: getInfoViewShowExpectedType(),
+            expectedTypeVisibility: getInfoViewExpectedTypeVisibility(),
             showGoalNames: getInfoViewShowGoalNames(),
             emphasizeFirstGoal: getInfoViewEmphasizeFirstGoal(),
             reverseTacticState: getInfoViewReverseTacticState(),
+            hideTypeAssumptions: getInfoViewHideTypeAssumptions(),
+            hideInstanceAssumptions: getInfoViewHideInstanceAssumptions(),
+            hideInaccessibleAssumptions: getInfoViewHideInaccessibleAssumptions(),
+            hideLetValues: getInfoViewHideLetValues(),
             showTooltipOnHover: getInfoViewShowTooltipOnHover(),
         })
     }
@@ -830,7 +1004,7 @@ export class InfoProvider implements Disposable {
 
     private getLocalPath(path: string): string | undefined {
         if (this.webviewPanel) {
-            return this.webviewPanel.webview.asWebviewUri(Uri.file(join(this.context.extensionPath, path))).toString()
+            // return this.webviewPanel.webview.asWebviewUri(Uri.file(join(this.context.extensionPath, path))).toString()
         }
         return undefined
     }
diff --git a/vscode-lean4/src/leanclient.ts b/vscode-lean4/src/leanclient.ts
index 408a1bdd2..c9024e073 100644
--- a/vscode-lean4/src/leanclient.ts
+++ b/vscode-lean4/src/leanclient.ts
@@ -13,16 +13,17 @@ import {
     WorkspaceFolder,
 } from 'vscode'
 import {
+    BaseLanguageClient,
     ClientCapabilities,
     DiagnosticSeverity,
     DidChangeTextDocumentParams,
     DidCloseTextDocumentParams,
     DocumentFilter,
+    Executable,
     InitializeResult,
     LanguageClient,
     LanguageClientOptions,
     RevealOutputChannelOn,
-    ServerOptions,
     State,
     StaticFeature,
 } from 'vscode-languageclient/node'
@@ -43,8 +44,8 @@ import {
 } from './config'
 import { logger } from './utils/logger'
 // @ts-ignore
-import path from 'path'
 import { SemVer } from 'semver'
+import { formatCommandExecutionOutput } from './utils/batch'
 import {
     c2pConverter,
     LeanPublishDiagnosticsParams,
@@ -62,6 +63,7 @@ import {
     displayNotificationWithOutput,
 } from './utils/notifs'
 import { willUseLakeServer } from './utils/projectInfo'
+import { LanguageClientWrapper } from 'monaco-editor-wrapper'
 
 interface LeanClientCapabilties {
     silentDiagnosticSupport?: boolean | undefined
@@ -77,7 +79,7 @@ export type ServerProgress = Map<ExtUri, LeanFileProgressProcessingInfo[]>
 
 export class LeanClient implements Disposable {
     running: boolean
-    private client: LanguageClient | undefined
+    private client: BaseLanguageClient | undefined
     private outputChannel: OutputChannel
     folderUri: ExtUri
     private subscriptions: Disposable[] = []
@@ -125,8 +127,9 @@ export class LeanClient implements Disposable {
     private serverFailedEmitter = new EventEmitter<string>()
     serverFailed = this.serverFailedEmitter.event
 
-    constructor(folderUri: ExtUri, outputChannel: OutputChannel) {
-        this.outputChannel = outputChannel
+    constructor(folderUri: ExtUri, outputChannel: OutputChannel,
+        private setupLanguageClient: (clientOptions: LanguageClientOptions) => Promise<BaseLanguageClient>
+    ) {        this.outputChannel = outputChannel
         this.folderUri = folderUri
         this.subscriptions.push(new Disposable(() => this.staleDepNotifier?.dispose()))
     }
@@ -215,7 +218,7 @@ export class LeanClient implements Disposable {
 
             const progressOptions: ProgressOptions = {
                 location: ProgressLocation.Notification,
-                title: '[Server Startup] Starting Lean language client',
+                title: '[Server Startup] Starting Lean language server and cloning missing packages [(Click for details)](command:lean4.troubleshooting.showOutput)',
                 cancellable: false,
             }
             await window.withProgress(
@@ -230,6 +233,7 @@ export class LeanClient implements Disposable {
     private async determineToolchainOverride(
         defaultToolchain: string | undefined,
     ): Promise<{ kind: 'Override'; toolchain: string } | { kind: 'NoOverride' } | { kind: 'Error'; message: string }> {
+        /*
         const cwdUri = this.folderUri.scheme === 'file' ? this.folderUri : undefined
         const toolchainDecision = await leanRunner.decideToolchain({
             channel: this.outputChannel,
@@ -253,6 +257,7 @@ export class LeanClient implements Disposable {
             // which is not what we want.  For adhoc files we want the (default) toolchain instead.
             return { kind: 'Override', toolchain: defaultToolchain }
         }
+        */
         return { kind: 'NoOverride' }
     }
 
@@ -272,7 +277,7 @@ export class LeanClient implements Disposable {
         const toolchainOverride: string | undefined =
             toolchainOverrideResult.kind === 'Override' ? toolchainOverrideResult.toolchain : undefined
 
-        this.client = await this.setupClient(toolchainOverride)
+        this.client = await this.setupLanguageClient(this.obtainClientOptions())
 
         let insideRestart = true
         try {
@@ -368,7 +373,7 @@ export class LeanClient implements Disposable {
             return
         }
 
-        const fileName = fileUri.scheme === 'file' ? path.basename(fileUri.fsPath) : 'untitled'
+        const fileName = fileUri.scheme === 'file' ? fileUri.baseName() : 'untitled'
         const isImportsOutdatedError = params.diagnostics.some(
             d =>
                 d.severity === DiagnosticSeverity.Error &&
@@ -427,7 +432,9 @@ export class LeanClient implements Disposable {
             return true
         }
         if (this.folderUri.scheme === 'file' && uri.scheme === 'file') {
-            return uri.isInFolder(this.folderUri)
+            // lean4monaco: To avoid file system issues, we let any client manage any file:
+            return true
+            // return uri.isInFolder(this.folderUri)
         }
         return false
     }
@@ -471,14 +478,32 @@ export class LeanClient implements Disposable {
     }
 
     async restartFile(leanDoc: LeanDocument): Promise<void> {
-        if (this.client === undefined || !this.running) return // there was a problem starting lean server.
+        const extUri = leanDoc.extUri
+        const formattedFileName = extUri.scheme === 'file' ? extUri.baseName() : extUri.toString()
+        const formattedProjectName =
+            this.folderUri.scheme === 'file' ? this.folderUri.fsPath : this.folderUri.toString()
+        if (this.client === undefined || !this.running) {
+            displayNotification(
+                'Error',
+                `Cannot restart '${formattedFileName}': The language server for the project at '${formattedProjectName}' is stopped.`,
+            )
+            return
+        }
 
-        if (!this.isInFolderManagedByThisClient(leanDoc.extUri)) {
+        if (!this.isInFolderManagedByThisClient(extUri)) {
+            displayNotification(
+                'Error',
+                `Cannot restart '${formattedFileName}': The project at '${formattedProjectName}' does not contain the file.`,
+            )
             return
         }
 
-        const uri = leanDoc.extUri.toString()
+        const uri = extUri.toString()
         if (!this.openServerDocuments.delete(uri)) {
+            displayNotification(
+                'Error',
+                `Cannot restart '${formattedFileName}': The file has never been opened in the language server for the project at '${formattedProjectName}'.`,
+            )
             return
         }
         logger.log(`[LeanClient] Restarting File: ${uri}`)
@@ -488,6 +513,10 @@ export class LeanClient implements Disposable {
         )
 
         if (this.openServerDocuments.has(uri)) {
+            displayNotification(
+                'Error',
+                `Cannot restart '${formattedFileName}': The file has already been opened in the language server for the project at '${formattedProjectName}' since initiating the restart.`,
+            )
             return
         }
         this.openServerDocuments.add(uri)
@@ -521,7 +550,7 @@ export class LeanClient implements Disposable {
         return this.running ? this.client?.initializeResult : undefined
     }
 
-    private async determineServerOptions(toolchainOverride: string | undefined): Promise<ServerOptions> {
+    private async determineServerOptions(toolchainOverride: string | undefined): Promise<Executable> {
         const env = Object.assign({}, process.env)
         if (serverLoggingEnabled()) {
             env.LEAN_SERVER_LOG_DIR = serverLoggingPath()
@@ -570,7 +599,7 @@ export class LeanClient implements Disposable {
             documentSelector.pattern = `${escapedPath}/**/*`
             workspaceFolder = {
                 uri: this.folderUri.asUri(),
-                name: path.basename(this.folderUri.fsPath),
+                name: this.folderUri.baseName(),
                 index: 0, // the language client library does not actually need this index
             }
         }
@@ -690,9 +719,12 @@ export class LeanClient implements Disposable {
     }
 
     private async setupClient(toolchainOverride: string | undefined): Promise<LanguageClient> {
-        const serverOptions: ServerOptions = await this.determineServerOptions(toolchainOverride)
+        const serverOptions: Executable = await this.determineServerOptions(toolchainOverride)
         const clientOptions: LanguageClientOptions = this.obtainClientOptions()
 
+        this.outputChannel.appendLine(
+            formatCommandExecutionOutput(serverOptions.options?.cwd, serverOptions.command, serverOptions.args ?? []),
+        )
         const client = new LanguageClient('lean4', 'Lean 4', serverOptions, clientOptions)
         const leanCapabilityFeature: StaticFeature = {
             initialize(_1, _2) {},
@@ -702,7 +734,7 @@ export class LeanClient implements Disposable {
             fillClientCapabilities(capabilities: ClientCapabilities & { lean?: LeanClientCapabilties | undefined }) {
                 capabilities.lean = leanClientCapabilities
             },
-            dispose() {},
+            clear() {},
         }
         client.registerFeature(leanCapabilityFeature)
 
diff --git a/vscode-lean4/src/projectinit.ts b/vscode-lean4/src/projectinit.ts
index 41b014e6f..f6ed1d819 100644
--- a/vscode-lean4/src/projectinit.ts
+++ b/vscode-lean4/src/projectinit.ts
@@ -14,7 +14,6 @@ import { lake } from './utils/lake'
 import { LeanInstaller } from './utils/leanInstaller'
 import { displayNotification, displayNotificationWithInput } from './utils/notifs'
 import { checkParentFoldersForLeanProject, isValidLeanProject } from './utils/projectInfo'
-import path from 'path'
 
 const projectInitNotificationOptions: SetupNotificationOptions = {
     errorMode: { mode: 'NonModal' },
@@ -192,7 +191,7 @@ export class ProjectInitializationProvider implements Disposable {
             return 'DidNotComplete'
         }
 
-        const projectName: string = path.basename(projectFolder.fsPath)
+        const projectName: string = projectFolder.baseName()
         const result: ExecutionResult = await lake({
             channel: this.channel,
             cwdUri: projectFolder,
@@ -431,7 +430,7 @@ Open this project instead?`
     }
 
     private static async openNewFolder(projectFolder: FileUri) {
-        const message = `Project initialized. Open new project folder '${path.basename(projectFolder.fsPath)}'?`
+        const message = `Project initialized. Open new project folder '${projectFolder.baseName()}'?`
         const input = 'Open project folder'
         const choice: string | undefined = await displayNotificationWithInput('Information', message, [input])
         if (choice === input) {
diff --git a/vscode-lean4/src/taskgutter.ts b/vscode-lean4/src/taskgutter.ts
index 474e4dc72..7e9acc7b0 100644
--- a/vscode-lean4/src/taskgutter.ts
+++ b/vscode-lean4/src/taskgutter.ts
@@ -13,6 +13,7 @@ import {
 } from 'vscode'
 import { DiagnosticSeverity, Range as LspRange } from 'vscode-languageclient'
 import {
+    decorationEditDelay,
     goalsAccomplishedDecorationKind,
     showDiagnosticGutterDecorations,
     showUnsolvedGoalsDecoration,
@@ -34,9 +35,10 @@ interface DecorationState {
 }
 
 class LeanFileTaskGutter implements Disposable {
-    private readonly editDelayMs: number = 3000
+    private readonly editDelayMs: number = decorationEditDelay()
     private timeout: NodeJS.Timeout | undefined
     private editDelayTimeout: NodeJS.Timeout | undefined
+    private lastEditTimestampMs: number | undefined
     private subscriptions: Disposable[] = []
     private decorationStates: DecorationState[] = []
 
@@ -51,10 +53,7 @@ class LeanFileTaskGutter implements Disposable {
 
     private onDidChange() {
         clearTimeout(this.editDelayTimeout)
-        this.editDelayTimeout = setTimeout(() => {
-            this.editDelayTimeout = undefined
-            this.displayDecorations('EditDelayed')
-        }, this.editDelayMs)
+        this.lastEditTimestampMs = Date.now()
     }
 
     onDidReveal() {
@@ -62,7 +61,7 @@ class LeanFileTaskGutter implements Disposable {
     }
 
     onDidUpdateState(newDecorationStates: DecorationState[]) {
-        this.scheduleUpdate(newDecorationStates, 20)
+        this.scheduleUpdate(newDecorationStates, 100)
     }
 
     clear(clearedDecorationTypes: TextEditorDecorationType[]) {
@@ -85,9 +84,15 @@ class LeanFileTaskGutter implements Disposable {
                 this.displayDecorations('Instantaneous')
             }, ms)
         }
-        if (this.editDelayTimeout === undefined) {
+        clearTimeout(this.editDelayTimeout)
+        const remainingDelayMs =
+            this.lastEditTimestampMs !== undefined
+                ? Math.max(ms, this.editDelayMs - (Date.now() - this.lastEditTimestampMs))
+                : ms
+        this.editDelayTimeout = setTimeout(() => {
+            this.editDelayTimeout = undefined
             this.displayDecorations('EditDelayed')
-        }
+        }, remainingDelayMs)
     }
 
     private updateDecorationStates(newDecorationStates: DecorationState[]) {
@@ -207,19 +212,7 @@ function mergeDiagnosticGutterDecos(a: DiagnosticGutterDeco, b: DiagnosticGutter
 }
 
 function isGoalsAccomplishedDiagnostic(d: LeanDiagnostic): boolean {
-    return (
-        d.leanTags !== undefined &&
-        d.leanTags.some(t => t === LeanTag.GoalsAccomplished) &&
-        goalsAccomplishedDecorationKind() !== 'Off'
-    )
-}
-
-function isGutterDecoDiagnostic(d: LeanDiagnostic): boolean {
-    return (
-        d.severity === DiagnosticSeverity.Error ||
-        d.severity === DiagnosticSeverity.Warning ||
-        isGoalsAccomplishedDiagnostic(d)
-    )
+    return d.leanTags !== undefined && d.leanTags.some(t => t === LeanTag.GoalsAccomplished)
 }
 
 function determineDiagStart(d: LeanDiagnostic, startLine: number, endLine: number, line: number): DiagStart {
@@ -269,29 +262,14 @@ function determineDiagnosticGutterDeco(
     }
 }
 
-function computeDiagnosticGutterDecos(diagnostics: LeanDiagnostic[]): DiagnosticGutterDeco[] {
-    const decos: Map<number, DiagnosticGutterDeco> = new Map()
-    for (const d of diagnostics) {
-        if (!isGutterDecoDiagnostic(d)) {
-            continue
-        }
-        const range = diagRange(d)
-        const startLine = range.start.line
-        const endLine = inclusiveEndLine(range)
-        for (let line = startLine; line <= endLine; line++) {
-            const deco = determineDiagnosticGutterDeco(d, startLine, endLine, line)
-            const oldDeco = decos.get(deco.line)
-            if (oldDeco === undefined) {
-                decos.set(deco.line, deco)
-            } else {
-                const mergedDeco = mergeDiagnosticGutterDecos(oldDeco, deco)
-                decos.set(deco.line, mergedDeco)
-            }
-        }
+function updateDecos(decos: Map<number, DiagnosticGutterDeco>, deco: DiagnosticGutterDeco) {
+    const oldDeco = decos.get(deco.line)
+    if (oldDeco === undefined) {
+        decos.set(deco.line, deco)
+    } else {
+        const mergedDeco = mergeDiagnosticGutterDecos(oldDeco, deco)
+        decos.set(deco.line, mergedDeco)
     }
-    const result: DiagnosticGutterDeco[] = [...decos.values()]
-    result.sort((a, b) => a.line - b.line)
-    return result
 }
 
 const diagnosticGutterDecoKinds = [
@@ -326,103 +304,6 @@ const diagnosticGutterDecoKinds = [
 ] as const
 type DiagnosticGutterDecoKind = (typeof diagnosticGutterDecoKinds)[number]
 
-function getGoalsAccomplishedDiagnosticGutterDecoKindName(): string {
-    const configName = goalsAccomplishedDecorationKind()
-    if (configName === 'Double Checkmark') {
-        return 'goals-accomplished-checkmark'
-    }
-    if (configName === 'Circled Checkmark') {
-        return 'goals-accomplished-circled-checkmark'
-    }
-    if (configName === 'Octopus') {
-        return 'goals-accomplished-octopus'
-    }
-    if (configName === 'Tada') {
-        return 'goals-accomplished-tada'
-    }
-    return 'goals-accomplished-checkmark'
-}
-
-function determineSingleLineDiagnosticGutterDecoKind(d: DiagnosticGutterDeco, name: string): DiagnosticGutterDecoKind {
-    const c = d.isPreviousDiagContinue
-    const e = d.isPreviousDiagEnd
-    if (!c && !e) {
-        return name as DiagnosticGutterDecoKind
-    }
-    if (!c && e) {
-        return `${name}-l-passthrough` as DiagnosticGutterDecoKind
-    }
-    if (c && !e) {
-        return `${name}-i-passthrough` as DiagnosticGutterDecoKind
-    }
-    if (c && e) {
-        return `${name}-t-passthrough` as DiagnosticGutterDecoKind
-    }
-    assert(false)
-}
-
-function determineDiagnosticGutterDecoKind(d: DiagnosticGutterDeco): DiagnosticGutterDecoKind | undefined {
-    const s = d.diagStart
-    const c = d.isPreviousDiagContinue
-    const e = d.isPreviousDiagEnd
-    if (s !== 'None') {
-        const k = s.kind
-        const r = s.range
-        if (k === 'Error') {
-            if (!c && !e) {
-                if (r === 'SingleLine') {
-                    return 'error'
-                }
-                if (r === 'MultiLine') {
-                    return 'error-init'
-                }
-                r satisfies never
-            }
-            if (!c && e) {
-                if (r === 'SingleLine') {
-                    return 'error-l-passthrough'
-                }
-                if (r === 'MultiLine') {
-                    return 'error-t-passthrough'
-                }
-                r satisfies never
-            }
-            if (c && !e) {
-                // All designs I can think of that would distinguish `SingleLine` and `MultiLine` in this case
-                // have too much visual complexity for the small gutter.
-                return 'error-i-passthrough'
-            }
-            if (c && e) {
-                // All designs I can think of that would distinguish `SingleLine` and `MultiLine` in this case
-                // have too much visual complexity for the small gutter.
-                return 'error-t-passthrough'
-            }
-            assert(false)
-        }
-        if (k === 'Warning') {
-            return determineSingleLineDiagnosticGutterDecoKind(d, 'warning')
-        }
-        if (k === 'GoalsAccomplished') {
-            return determineSingleLineDiagnosticGutterDecoKind(d, getGoalsAccomplishedDiagnosticGutterDecoKindName())
-        }
-        k satisfies never
-    }
-    assert(s === 'None')
-    if (!c && !e) {
-        return undefined
-    }
-    if (!c && e) {
-        return 'error-l'
-    }
-    if (c && !e) {
-        return 'error-i'
-    }
-    if (c && e) {
-        return 'error-t'
-    }
-    assert(false)
-}
-
 export class LeanTaskGutter implements Disposable {
     private processingDecorationType: TextEditorDecorationType
     private fatalErrorDecorationType: TextEditorDecorationType
@@ -432,6 +313,7 @@ export class LeanTaskGutter implements Disposable {
     private gutters: Map<string, LeanFileTaskGutter> = new Map()
     private subscriptions: Disposable[] = []
     private showDiagnosticGutterDecorations: boolean = true
+    private goalsAccomplishedDecorationKind: string
     private showUnsolvedGoalsDecoration: boolean = true
 
     constructor(
@@ -467,14 +349,14 @@ export class LeanTaskGutter implements Disposable {
                 after: {
                     contentText: '🛠',
                     color: unsolvedGoalsDecorationDarkThemeColor(),
-                    margin: '0 0 0 1em',
+                    margin: '0 0 0 1ch',
                 },
             },
             light: {
                 after: {
                     contentText: '🛠',
                     color: unsolvedGoalsDecorationLightThemeColor(),
-                    margin: '0 0 0 1em',
+                    margin: '0 0 0 1ch',
                 },
             },
             isWholeLine: true,
@@ -535,6 +417,7 @@ export class LeanTaskGutter implements Disposable {
             errorLensExtensions.isActive &&
             workspace.getConfiguration('errorLens').get('gutterIconsEnabled', false)
         this.showDiagnosticGutterDecorations = !isErrorLensGutterEnabled && showDiagnosticGutterDecorations()
+        this.goalsAccomplishedDecorationKind = goalsAccomplishedDecorationKind()
         this.showUnsolvedGoalsDecoration = showUnsolvedGoalsDecoration()
         if (!this.showDiagnosticGutterDecorations) {
             for (const gutter of this.gutters.values()) {
@@ -615,9 +498,9 @@ export class LeanTaskGutter implements Disposable {
                 decos: [],
             })
         }
-        const decos = computeDiagnosticGutterDecos(diagnostics)
+        const decos = this.computeDiagnosticGutterDecos(diagnostics)
         for (const deco of decos) {
-            const kind = determineDiagnosticGutterDecoKind(deco)
+            const kind = this.determineDiagnosticGutterDecoKind(deco)
             if (kind === undefined) {
                 continue
             }
@@ -628,6 +511,138 @@ export class LeanTaskGutter implements Disposable {
         return [...decoStates.values()]
     }
 
+    computeDiagnosticGutterDecos(diagnostics: LeanDiagnostic[]): DiagnosticGutterDeco[] {
+        const decos: Map<number, DiagnosticGutterDeco> = new Map()
+        for (const d of diagnostics) {
+            if (!this.isGutterDecoDiagnostic(d)) {
+                continue
+            }
+            const range = diagRange(d)
+            const startLine = range.start.line
+            const endLine = inclusiveEndLine(range)
+            const startDeco = determineDiagnosticGutterDeco(d, startLine, endLine, startLine)
+            updateDecos(decos, startDeco)
+            if (startDeco.diagStart !== 'None' && startDeco.diagStart.range === 'SingleLine') {
+                continue
+            }
+            for (let line = startLine + 1; line <= endLine; line++) {
+                const deco = determineDiagnosticGutterDeco(d, startLine, endLine, line)
+                updateDecos(decos, deco)
+            }
+        }
+        const result: DiagnosticGutterDeco[] = [...decos.values()]
+        result.sort((a, b) => a.line - b.line)
+        return result
+    }
+
+    isGutterDecoDiagnostic(d: LeanDiagnostic): boolean {
+        return (
+            d.severity === DiagnosticSeverity.Error ||
+            d.severity === DiagnosticSeverity.Warning ||
+            (isGoalsAccomplishedDiagnostic(d) && this.goalsAccomplishedDecorationKind !== 'Off')
+        )
+    }
+
+    getGoalsAccomplishedDiagnosticGutterDecoKindName(): string {
+        const configName = this.goalsAccomplishedDecorationKind
+        if (configName === 'Double Checkmark') {
+            return 'goals-accomplished-checkmark'
+        }
+        if (configName === 'Circled Checkmark') {
+            return 'goals-accomplished-circled-checkmark'
+        }
+        if (configName === 'Octopus') {
+            return 'goals-accomplished-octopus'
+        }
+        if (configName === 'Tada') {
+            return 'goals-accomplished-tada'
+        }
+        return 'goals-accomplished-checkmark'
+    }
+
+    determineSingleLineDiagnosticGutterDecoKind(d: DiagnosticGutterDeco, name: string): DiagnosticGutterDecoKind {
+        const c = d.isPreviousDiagContinue
+        const e = d.isPreviousDiagEnd
+        if (!c && !e) {
+            return name as DiagnosticGutterDecoKind
+        }
+        if (!c && e) {
+            return `${name}-l-passthrough` as DiagnosticGutterDecoKind
+        }
+        if (c && !e) {
+            return `${name}-i-passthrough` as DiagnosticGutterDecoKind
+        }
+        if (c && e) {
+            return `${name}-t-passthrough` as DiagnosticGutterDecoKind
+        }
+        assert(false)
+    }
+
+    determineDiagnosticGutterDecoKind(d: DiagnosticGutterDeco): DiagnosticGutterDecoKind | undefined {
+        const s = d.diagStart
+        const c = d.isPreviousDiagContinue
+        const e = d.isPreviousDiagEnd
+        if (s !== 'None') {
+            const k = s.kind
+            const r = s.range
+            if (k === 'Error') {
+                if (!c && !e) {
+                    if (r === 'SingleLine') {
+                        return 'error'
+                    }
+                    if (r === 'MultiLine') {
+                        return 'error-init'
+                    }
+                    r satisfies never
+                }
+                if (!c && e) {
+                    if (r === 'SingleLine') {
+                        return 'error-l-passthrough'
+                    }
+                    if (r === 'MultiLine') {
+                        return 'error-t-passthrough'
+                    }
+                    r satisfies never
+                }
+                if (c && !e) {
+                    // All designs I can think of that would distinguish `SingleLine` and `MultiLine` in this case
+                    // have too much visual complexity for the small gutter.
+                    return 'error-i-passthrough'
+                }
+                if (c && e) {
+                    // All designs I can think of that would distinguish `SingleLine` and `MultiLine` in this case
+                    // have too much visual complexity for the small gutter.
+                    return 'error-t-passthrough'
+                }
+                assert(false)
+            }
+            if (k === 'Warning') {
+                return this.determineSingleLineDiagnosticGutterDecoKind(d, 'warning')
+            }
+            if (k === 'GoalsAccomplished') {
+                return this.determineSingleLineDiagnosticGutterDecoKind(
+                    d,
+                    this.getGoalsAccomplishedDiagnosticGutterDecoKindName(),
+                )
+            }
+            k satisfies never
+        }
+        assert(s === 'None')
+        if (!c && !e) {
+            return undefined
+        }
+        if (!c && e) {
+            return 'error-l'
+        }
+        if (c && !e) {
+            return 'error-i'
+        }
+        if (c && e) {
+            return 'error-t'
+        }
+        assert(false)
+    }
+
     private computeUnsolvedGoalsDecoState(diagnostics: LeanDiagnostic[]): DecorationState {
         const unsolvedGoalsLines = diagnostics
             .filter(d => {
diff --git a/vscode-lean4/src/utils/batch.ts b/vscode-lean4/src/utils/batch.ts
index 23bc00b73..e9050aa1a 100644
--- a/vscode-lean4/src/utils/batch.ts
+++ b/vscode-lean4/src/utils/batch.ts
@@ -32,6 +32,16 @@ function createCannotLaunchExecutionResult(message: string): ExecutionResult {
     }
 }
 
+export function formatCommandExecutionOutput(
+    workingDirectory: string | undefined,
+    executablePath: string,
+    args: string[],
+) {
+    const formattedCwd = workingDirectory ? `${workingDirectory}` : ''
+    const formattedArgs = args.map(arg => (arg.includes(' ') ? `"${arg}"` : arg)).join(' ')
+    return `${formattedCwd}> ${executablePath} ${formattedArgs}`
+}
+
 export function batchExecuteWithProc(
     executablePath: string,
     args: string[],
@@ -39,6 +49,8 @@ export function batchExecuteWithProc(
     channel?: ExecutionChannel | undefined,
     envExtensions?: { [key: string]: string } | undefined,
 ): [ChildProcessWithoutNullStreams | 'CannotLaunch', Promise<ExecutionResult>] {
+    return ["CannotLaunch", new Promise(() => {})]
+    /*
     let stdout: string = ''
     let stderr: string = ''
     let combined: string = ''
@@ -54,9 +66,7 @@ export function batchExecuteWithProc(
         options = { ...options, env }
     }
     if (channel?.combined) {
-        const formattedCwd = workingDirectory ? `${workingDirectory}` : ''
-        const formattedArgs = args.map(arg => (arg.includes(' ') ? `"${arg}"` : arg)).join(' ')
-        channel.combined.appendLine(`${formattedCwd}> ${executablePath} ${formattedArgs}`)
+        channel.combined.appendLine(formatCommandExecutionOutput(workingDirectory, executablePath, args))
     }
 
     let proc: ChildProcessWithoutNullStreams
@@ -133,6 +143,7 @@ export function batchExecuteWithProc(
     })
 
     return [proc, execPromise]
+    */
 }
 
 export async function batchExecute(
diff --git a/vscode-lean4/src/utils/clientProvider.ts b/vscode-lean4/src/utils/clientProvider.ts
index e6426647c..d1005af37 100644
--- a/vscode-lean4/src/utils/clientProvider.ts
+++ b/vscode-lean4/src/utils/clientProvider.ts
@@ -1,21 +1,24 @@
 import { LeanFileProgressProcessingInfo, ServerStoppedReason } from '@leanprover/infoview-api'
-import path from 'path'
-import { Disposable, EventEmitter, OutputChannel, commands, workspace } from 'vscode'
+import { Disposable, EventEmitter, OutputChannel, commands } from 'vscode'
 import { SetupDiagnostics, checkAll } from '../diagnostics/setupDiagnostics'
 import { PreconditionCheckResult, SetupNotificationOptions } from '../diagnostics/setupNotifs'
 import { LeanClient } from '../leanclient'
 import { LeanPublishDiagnosticsParams } from './converters'
-import { ExtUri, FileUri, UntitledUri, getWorkspaceFolderUri } from './exturi'
+import { ExtUri, FileUri } from './exturi'
 import { lean } from './leanEditorProvider'
 import { LeanInstaller } from './leanInstaller'
 import { logger } from './logger'
 import { displayNotification } from './notifs'
-import { findLeanProjectRoot, willUseLakeServer } from './projectInfo'
+import { findLeanProjectRootInfo, willUseLakeServer } from './projectInfo'
+import { BaseLanguageClient, LanguageClientOptions } from 'vscode-languageclient/node'
 
 async function checkLean4ProjectPreconditions(
     channel: OutputChannel,
     context: string,
+    existingFolderUris: ExtUri[],
     folderUri: ExtUri,
+    fileUri: ExtUri,
+    stopOtherServer: (folderUri: FileUri) => Promise<void>,
 ): Promise<PreconditionCheckResult> {
     const options: SetupNotificationOptions = {
         errorMode: { mode: 'NonModal' },
@@ -33,6 +36,7 @@ async function checkLean4ProjectPreconditions(
                 toolchainUpdateMode: 'PromptAboutUpdate',
             })
         },
+        () => d.checkIsNestedProjectFolder(existingFolderUris, folderUri, fileUri, stopOtherServer),
     )
 }
 
@@ -62,7 +66,11 @@ export class LeanClientProvider implements Disposable {
     private clientStoppedEmitter = new EventEmitter<[LeanClient, boolean, ServerStoppedReason]>()
     clientStopped = this.clientStoppedEmitter.event
 
-    constructor(installer: LeanInstaller, outputChannel: OutputChannel) {
+    constructor(
+        installer: LeanInstaller,
+        outputChannel: OutputChannel,
+        private setupClient: (clientOptions: LanguageClientOptions) => Promise<BaseLanguageClient>,
+    ) {
         this.outputChannel = outputChannel
         this.installer = installer
 
@@ -84,29 +92,10 @@ export class LeanClientProvider implements Disposable {
             commands.registerCommand('lean4.restartFile', () => this.restartActiveFile()),
             commands.registerCommand('lean4.refreshFileDependencies', () => this.restartActiveFile()),
             commands.registerCommand('lean4.restartServer', () => this.restartActiveClient()),
-            commands.registerCommand('lean4.stopServer', () => this.stopActiveClient()),
+            commands.registerCommand('lean4.stopServer', () => this.stopClient(undefined)),
         )
 
         this.subscriptions.push(lean.onDidOpenLeanDocument(document => this.ensureClient(document.extUri)))
-
-        this.subscriptions.push(
-            workspace.onDidChangeWorkspaceFolders(event => {
-                // Remove all clients that are not referenced by any folder anymore
-                if (event.removed.length === 0) {
-                    return
-                }
-                this.clients.forEach((client, key) => {
-                    if (client.folderUri.scheme === 'untitled' || getWorkspaceFolderUri(client.folderUri)) {
-                        return
-                    }
-
-                    logger.log(`[ClientProvider] onDidChangeWorkspaceFolders removing client for ${key}`)
-                    this.clients.delete(key)
-                    client.dispose()
-                    this.clientRemovedEmitter.fire(client)
-                })
-            }),
-        )
     }
 
     getActiveClient(): LeanClient | undefined {
@@ -115,8 +104,6 @@ export class LeanClientProvider implements Disposable {
     }
 
     private async onInstallChanged(uri: FileUri) {
-        // Uri is a package Uri in the case a lean package file was changed.
-        logger.log(`[ClientProvider] installChanged for ${uri}`)
         this.pendingInstallChanged.push(uri)
         if (this.processingInstallChanged) {
             // avoid re-entrancy.
@@ -130,23 +117,9 @@ export class LeanClientProvider implements Disposable {
                 break
             }
             try {
-                const projectUri = await findLeanProjectRoot(uri)
-                if (projectUri === 'FileNotFound') {
-                    continue
-                }
-
-                const preconditionCheckResult = await checkLean4ProjectPreconditions(
-                    this.outputChannel,
-                    'Client Restart',
-                    projectUri,
-                )
-                if (preconditionCheckResult !== 'Fatal') {
-                    logger.log('[ClientProvider] got lean version 4')
-                    const [cached, client] = await this.ensureClient(uri)
-                    if (cached && client) {
-                        await client.restart()
-                        logger.log('[ClientProvider] restart complete')
-                    }
+                const [cached, client] = await this.ensureClient(uri)
+                if (cached && client) {
+                    await client.restart()
                 }
             } catch (e) {
                 logger.log(`[ClientProvider] Exception checking lean version: ${e}`)
@@ -156,7 +129,7 @@ export class LeanClientProvider implements Disposable {
     }
 
     restartFile(uri: ExtUri) {
-        const fileName = uri.scheme === 'file' ? path.basename(uri.fsPath) : 'untitled file'
+        const fileName = uri.scheme === 'file' ? uri.baseName() : 'untitled file'
 
         const client: LeanClient | undefined = this.findClient(uri)
         if (!client || !client.isRunning()) {
@@ -185,9 +158,33 @@ export class LeanClientProvider implements Disposable {
         this.restartFile(doc.extUri)
     }
 
-    private async stopActiveClient() {
-        if (this.activeClient && this.activeClient.isStarted()) {
-            await this.activeClient?.stop()
+    private async stopClient(folderUri: ExtUri | undefined) {
+        let clientToStop: LeanClient
+        if (folderUri === undefined) {
+            if (this.activeClient === undefined) {
+                displayNotification('Error', 'Cannot stop language server: No active client.')
+                return
+            }
+            clientToStop = this.activeClient
+        } else {
+            const foundClient = this.getClientForFolder(folderUri)
+            if (foundClient === undefined) {
+                displayNotification(
+                    'Error',
+                    `Cannot stop language server: No client for project at '${folderUri.toString()}'.`,
+                )
+                return
+            }
+            clientToStop = foundClient
+        }
+        if (clientToStop.isStarted()) {
+            await clientToStop.stop()
+        }
+        const key = clientToStop.folderUri.toString()
+        this.clients.delete(key)
+        this.pending.delete(key)
+        if (clientToStop === this.activeClient) {
+            this.activeClient = undefined
         }
     }
 
@@ -245,10 +242,18 @@ export class LeanClientProvider implements Disposable {
     }
 
     async ensureClient(uri: ExtUri): Promise<[boolean, LeanClient | undefined]> {
-        const folderUri = uri.scheme === 'file' ? await findLeanProjectRoot(uri) : new UntitledUri()
-        if (folderUri === 'FileNotFound') {
+        const projectInfo = await findLeanProjectRootInfo(uri)
+        if (projectInfo.kind === 'FileNotFound') {
             return [false, undefined]
         }
+        if (projectInfo.kind === 'LakefileWithoutToolchain') {
+            displayNotification(
+                'Error',
+                `Project at ${projectInfo.projectRootUri} has a Lakefile, but lacks a 'lean-toolchain' file. Please create one with the Lean version that you would like the project to use.`,
+            )
+            return [false, undefined]
+        }
+        const folderUri = projectInfo.projectRootUri
         let client = this.getClientForFolder(folderUri)
         if (client) {
             this.activeClient = client
@@ -260,20 +265,28 @@ export class LeanClientProvider implements Disposable {
             return [false, undefined]
         }
         this.pending.set(key, true)
-
+        // lean4monaco: The precondition checks require a file system or executables, which we don't have in the browser.
+        /*
         const preconditionCheckResult = await checkLean4ProjectPreconditions(
             this.outputChannel,
             'Client Startup',
+            this.getClients().map(client => client.folderUri),
             folderUri,
+            uri,
+            async (folderUriToStop: FileUri) => {
+                await this.stopClient(folderUriToStop)
+                await this.ensureClient(uri)
+            },
         )
         if (preconditionCheckResult === 'Fatal') {
             this.pending.delete(key)
             this.activeClient = undefined
             return [false, undefined]
         }
+        */
 
         logger.log('[ClientProvider] Creating LeanClient for ' + folderUri.toString())
-        client = new LeanClient(folderUri, this.outputChannel)
+        client = new LeanClient(folderUri, this.outputChannel, this.setupClient)
         this.subscriptions.push(client)
         this.clients.set(key, client)
 
diff --git a/vscode-lean4/src/utils/configwatchservice.ts b/vscode-lean4/src/utils/configwatchservice.ts
index 0d519ce3b..5233968f4 100644
--- a/vscode-lean4/src/utils/configwatchservice.ts
+++ b/vscode-lean4/src/utils/configwatchservice.ts
@@ -1,7 +1,7 @@
 import * as path from 'path'
 import { Disposable, EventEmitter, Uri, window, workspace } from 'vscode'
 import { FileUri } from './exturi'
-import { findLeanProjectInfo, findLeanProjectRoot } from './projectInfo'
+import { findLeanProjectInfo, findLeanProjectRootInfo } from './projectInfo'
 
 // This service monitors the Lean package root folders for changes to any
 // lean-toolchail, lakefile.lean or lakefile.toml files found there.
@@ -78,8 +78,12 @@ export class LeanConfigWatchService implements Disposable {
         // Note: just opening the file fires this event sometimes which is annoying, so
         // we compare the contents just to be sure and normalize whitespace so that
         // just adding a new line doesn't trigger the prompt.
-        const projectUri = await findLeanProjectRoot(fileUri)
-        if (projectUri === 'FileNotFound') {
+        const info = await findLeanProjectRootInfo(fileUri)
+        if (
+            info.kind === 'FileNotFound' ||
+            info.kind === 'LakefileWithoutToolchain' ||
+            info.projectRootUri.scheme === 'untitled'
+        ) {
             return
         }
 
@@ -96,7 +100,7 @@ export class LeanConfigWatchService implements Disposable {
         this.normalizedLakeFileContents.set(key, contents)
         if (raiseEvent) {
             // raise an event so the extension triggers handleLakeFileChanged.
-            this.lakeFileChangedEmitter.fire(projectUri)
+            this.lakeFileChangedEmitter.fire(info.projectRootUri)
         }
     }
 
@@ -111,6 +115,8 @@ export class LeanConfigWatchService implements Disposable {
         const projectInfo = await findLeanProjectInfo(fileUri)
         if (
             projectInfo.kind === 'FileNotFound' ||
+            projectInfo.kind === 'LakefileWithoutToolchain' ||
+            projectInfo.projectRootUri.scheme === 'untitled' ||
             projectInfo.toolchainInfo === undefined ||
             projectInfo.toolchainInfo.toolchain === undefined
         ) {
diff --git a/vscode-lean4/src/utils/elan.ts b/vscode-lean4/src/utils/elan.ts
index c26f5727f..acb9574fb 100644
--- a/vscode-lean4/src/utils/elan.ts
+++ b/vscode-lean4/src/utils/elan.ts
@@ -4,6 +4,7 @@ import { z, ZodTypeAny } from 'zod'
 import { batchExecute, batchExecuteWithProgress, ExecutionExitCode, ExecutionResult } from './batch'
 import { FileUri } from './exturi'
 import { groupByUniqueKey } from './groupBy'
+import { semVerRegex } from './semverRegex'
 
 export const elanStableChannel = 'leanprover/lean4:stable'
 export const elanNightlyChannel = 'leanprover/lean4:nightly'
@@ -14,11 +15,6 @@ export function isElanEagerResolutionVersion(version: SemVer) {
     return version.major >= elanEagerResolutionMajorVersion
 }
 
-// Suggested at https://semver.org/#is-there-a-suggested-regular-expression-regex-to-check-a-semver-string
-
-const semVerRegex =
-    /^(0|[1-9]\d*)\.(0|[1-9]\d*)\.(0|[1-9]\d*)(?:-((?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*)(?:\.(?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*))*))?(?:\+([0-9a-zA-Z-]+(?:\.[0-9a-zA-Z-]+)*))?$/
-
 const elanVersionRegex =
     /^elan ((0|[1-9]\d*)\.(0|[1-9]\d*)\.(0|[1-9]\d*)(?:-((?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*)(?:\.(?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*))*))?(?:\+([0-9a-zA-Z-]+(?:\.[0-9a-zA-Z-]+)*))?)/
 
diff --git a/vscode-lean4/src/utils/elanCommands.ts b/vscode-lean4/src/utils/elanCommands.ts
index 1936d5de0..3fe68eeba 100644
--- a/vscode-lean4/src/utils/elanCommands.ts
+++ b/vscode-lean4/src/utils/elanCommands.ts
@@ -1,4 +1,6 @@
+import assert from 'assert'
 import { promises } from 'fs'
+import { SemVer, valid } from 'semver'
 import { commands, Disposable, OutputChannel, QuickPickItem, QuickPickItemKind, window } from 'vscode'
 import { ExecutionExitCode } from './batch'
 import { LeanClientProvider } from './clientProvider'
@@ -27,6 +29,89 @@ function displayElanNotInstalledError() {
     displayNotification('Error', 'Elan is not installed.')
 }
 
+type LeanToolchain =
+    | { kind: 'Unknown'; fullName: string }
+    | { kind: 'Release'; fullName: string; version: SemVer }
+    | { kind: 'Nightly'; fullName: string; date: Date }
+    | { kind: 'PRRelease'; fullName: string; pr: number }
+
+function parseToolchain(toolchain: string): LeanToolchain {
+    const releaseMatch = toolchain.match(/leanprover\/lean4:(.+)/)
+    if (releaseMatch) {
+        let version = releaseMatch[1]
+        if (version[0] === 'v') {
+            version = version.substring(1)
+        }
+        if (valid(version)) {
+            return { kind: 'Release', fullName: toolchain, version: new SemVer(version) }
+        }
+    }
+
+    const nightlyMatch = toolchain.match(/leanprover\/lean4-nightly:nightly-(.+)/)
+    if (nightlyMatch) {
+        const date = new Date(nightlyMatch[1])
+        if (!isNaN(date.valueOf())) {
+            return { kind: 'Nightly', fullName: toolchain, date }
+        }
+    }
+
+    const prReleaseMatch = toolchain.match(/leanprover\/lean4-pr-releases:pr-release-(\d+)/)
+    if (prReleaseMatch) {
+        const pr = Number.parseInt(prReleaseMatch[1])
+        return { kind: 'PRRelease', fullName: toolchain, pr }
+    }
+
+    return { kind: 'Unknown', fullName: toolchain }
+}
+
+function toolchainKindPrio(k: 'Unknown' | 'Release' | 'Nightly' | 'PRRelease'): number {
+    switch (k) {
+        case 'Unknown':
+            return 3
+        case 'Release':
+            return 2
+        case 'Nightly':
+            return 1
+        case 'PRRelease':
+            return 0
+    }
+}
+
+function compareToolchainKinds(
+    k1: 'Unknown' | 'Release' | 'Nightly' | 'PRRelease',
+    k2: 'Unknown' | 'Release' | 'Nightly' | 'PRRelease',
+): number {
+    return toolchainKindPrio(k1) - toolchainKindPrio(k2)
+}
+
+function compareToolchains(t1: LeanToolchain, t2: LeanToolchain): number {
+    const kindComparison = compareToolchainKinds(t1.kind, t2.kind)
+    if (kindComparison !== 0) {
+        return kindComparison
+    }
+    switch (t1.kind) {
+        case 'Unknown':
+            assert(t2.kind === 'Unknown')
+            return -1 * t1.fullName.localeCompare(t2.fullName)
+        case 'Release':
+            assert(t2.kind === 'Release')
+            return t1.version.compare(t2.version)
+        case 'Nightly':
+            assert(t2.kind === 'Nightly')
+            return t1.date.valueOf() - t2.date.valueOf()
+        case 'PRRelease':
+            assert(t2.kind === 'PRRelease')
+            return t1.pr - t2.pr
+    }
+}
+
+function sortToolchains(ts: string[]): string[] {
+    return ts
+        .map(t => parseToolchain(t))
+        .sort((t1, t2) => -1 * compareToolchains(t1, t2))
+        .map(t => t.fullName)
+}
+
 export class ElanCommandProvider implements Disposable {
     private subscriptions: Disposable[] = []
 
@@ -212,7 +297,7 @@ export class ElanCommandProvider implements Disposable {
         if (toolchainInfo === undefined) {
             return
         }
-        const installedToolchains = toolchainInfo.toolchains
+        const installedToolchains = sortToolchains(toolchainInfo.toolchains)
         if (installedToolchains.length === 0) {
             displayNotification('Information', 'No Lean versions installed.')
             return
@@ -375,7 +460,7 @@ export class ElanCommandProvider implements Disposable {
         if (toolchainInfo === undefined) {
             return undefined
         }
-        const installedToolchains = toolchainInfo.toolchains
+        const installedToolchains = sortToolchains(toolchainInfo.toolchains)
         const installedToolchainIndex = new Set(installedToolchains)
 
         let stableToolchains: string[] = []
diff --git a/vscode-lean4/src/utils/exturi.ts b/vscode-lean4/src/utils/exturi.ts
index 5ec3501be..1b4259a36 100644
--- a/vscode-lean4/src/utils/exturi.ts
+++ b/vscode-lean4/src/utils/exturi.ts
@@ -1,3 +1,4 @@
+import path from 'path'
 import { Uri, workspace } from 'vscode'
 import { isFileInFolder, relativeFilePathInFolder } from './fsHelper'
 
@@ -49,6 +50,10 @@ export class FileUri {
         return this.asUri().toString()
     }
 
+    baseName(): string {
+        return path.basename(this.fsPath)
+    }
+
     join(...pathSegments: string[]): FileUri {
         return FileUri.fromUriOrError(Uri.joinPath(this.asUri(), ...pathSegments))
     }
@@ -66,16 +71,15 @@ export class FileUri {
     }
 }
 
-export function getWorkspaceFolderUri(uri: FileUri): FileUri | undefined {
-    const folder = workspace.getWorkspaceFolder(uri.asUri())
-    if (folder === undefined) {
-        return undefined
-    }
-    const folderUri = FileUri.fromUri(folder.uri)
-    if (folderUri === undefined) {
-        return undefined
+export function isInWorkspaceFolder(uri: FileUri): boolean {
+    return workspace.getWorkspaceFolder(uri.asUri()) !== undefined
+}
+
+export function isWorkspaceFolder(uri: FileUri): boolean {
+    if (workspace.workspaceFolders === undefined) {
+        return false
     }
-    return folderUri
+    return workspace.workspaceFolders.some(folder => uri.equalsUri(folder.uri))
 }
 
 export class UntitledUri {
diff --git a/vscode-lean4/src/utils/internalErrors.ts b/vscode-lean4/src/utils/internalErrors.ts
index 3cd111fd1..360a52cfe 100644
--- a/vscode-lean4/src/utils/internalErrors.ts
+++ b/vscode-lean4/src/utils/internalErrors.ts
@@ -1,23 +1,38 @@
 import { env } from 'vscode'
-import { displayNotificationWithInput } from './notifs'
+import { displayModalNotification, displayNotificationWithInput } from './notifs'
+
+export async function displayInternalError(scope: string, e: any) {
+    let msg: string = `Internal error (while ${scope}): ${e}`
+    let fullMsg: string = msg
+    if (e instanceof Error && e.stack !== undefined) {
+        fullMsg += `\n\n${e.stack}`
+    }
+    msg +=
+        "\n\nIf you are using an up-to-date version of the Lean 4 VS Code extension, please copy the full error message using the 'Copy Error to Clipboard' button and report it at https://github.com/leanprover/vscode-lean4/ or https://leanprover.zulipchat.com/."
+    const copyToClipboardInput = 'Copy Error to Clipboard'
+    const closeInput = 'Close'
+    const choice = await displayNotificationWithInput('Error', msg, [copyToClipboardInput], closeInput)
+    if (choice === copyToClipboardInput) {
+        await env.clipboard.writeText(fullMsg)
+    }
+}
+
+const duplicateCommandError = (scope: string) =>
+    `Error (while ${scope}): Two separate Lean 4 VS Code extensions that register the same VS Code functionality are installed.
+Please uninstall or disable one of them and restart VS Code.
+
+The 'Lean 4' extension by the 'leanprover' organization is the only official Lean 4 VS Code extension.`
 
 export async function displayInternalErrorsIn<T>(scope: string, f: () => Promise<T>): Promise<T> {
     try {
         return await f()
     } catch (e) {
-        let msg: string = `Internal error (while ${scope}): ${e}`
-        let fullMsg: string = msg
-        if (e instanceof Error && e.stack !== undefined) {
-            fullMsg += `\n\n${e.stack}`
-        }
-        msg +=
-            "\n\nIf you are using an up-to-date version of the Lean 4 VS Code extension, please copy the full error message using the 'Copy Error to Clipboard' button and report it at https://github.com/leanprover/vscode-lean4/ or https://leanprover.zulipchat.com/."
-        const copyToClipboardInput = 'Copy Error to Clipboard'
-        const closeInput = 'Close'
-        const choice = await displayNotificationWithInput('Error', msg, [copyToClipboardInput], closeInput)
-        if (choice === copyToClipboardInput) {
-            await env.clipboard.writeText(fullMsg)
+        const msg = e.message
+        if (msg !== undefined && typeof msg === 'string' && msg.match(/command '.*' already exists/)) {
+            await displayModalNotification('Error', duplicateCommandError(scope))
+            throw e
         }
+        await displayInternalError(scope, e)
         throw e
     }
 }
diff --git a/vscode-lean4/src/utils/lake.ts b/vscode-lean4/src/utils/lake.ts
index a139a711d..732e2fb8a 100644
--- a/vscode-lean4/src/utils/lake.ts
+++ b/vscode-lean4/src/utils/lake.ts
@@ -1,4 +1,3 @@
-import path from 'path'
 import { OutputChannel } from 'vscode'
 import { ExecutionExitCode, ExecutionResult } from './batch'
 import { FileUri } from './exturi'
@@ -50,7 +49,7 @@ export class LakeRunner {
     }
 
     async fetchMathlibCacheForFile(projectRelativeFileUri: FileUri): Promise<ExecutionResult> {
-        const prompt = `Fetching Mathlib build artifact cache for ${path.basename(projectRelativeFileUri.fsPath)}`
+        const prompt = `Fetching Mathlib build artifact cache for ${projectRelativeFileUri.baseName()}`
         return this.runLakeCommandWithProgress('exe', ['cache', 'get', projectRelativeFileUri.fsPath], prompt)
     }
 
diff --git a/vscode-lean4/src/utils/leanCmdRunner.ts b/vscode-lean4/src/utils/leanCmdRunner.ts
index a567a486a..17adaeb91 100644
--- a/vscode-lean4/src/utils/leanCmdRunner.ts
+++ b/vscode-lean4/src/utils/leanCmdRunner.ts
@@ -43,7 +43,7 @@ function overrideReason(activeOverride: ElanOverrideReason | undefined): string
         case 'Environment':
             return undefined
         case 'Manual':
-            return `set by \`elan override\` in folder '${path.basename(activeOverride.directoryPath.fsPath)}'`
+            return `set by \`elan override\` in folder '${activeOverride.directoryPath.baseName()}'`
         case 'ToolchainFile':
             return `of Lean project '${path.dirname(activeOverride.toolchainPath.fsPath)}'`
         case 'LeanpkgFile':
diff --git a/vscode-lean4/src/utils/manifest.ts b/vscode-lean4/src/utils/manifest.ts
index dedd7d880..c2c58867f 100644
--- a/vscode-lean4/src/utils/manifest.ts
+++ b/vscode-lean4/src/utils/manifest.ts
@@ -3,10 +3,7 @@ import { SemVer } from 'semver'
 import { Uri } from 'vscode'
 import { z } from 'zod'
 import { FileUri } from './exturi'
-
-// Suggested at https://semver.org/#is-there-a-suggested-regular-expression-regex-to-check-a-semver-string
-const semVerRegex =
-    /^(0|[1-9]\d*)\.(0|[1-9]\d*)\.(0|[1-9]\d*)(?:-((?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*)(?:\.(?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*))*))?(?:\+([0-9a-zA-Z-]+(?:\.[0-9a-zA-Z-]+)*))?$/
+import { semVerRegex } from './semverRegex'
 
 export interface DirectGitDependency {
     name: string
diff --git a/vscode-lean4/src/utils/projectInfo.ts b/vscode-lean4/src/utils/projectInfo.ts
index d4e3a5fb9..11025b5cd 100644
--- a/vscode-lean4/src/utils/projectInfo.ts
+++ b/vscode-lean4/src/utils/projectInfo.ts
@@ -1,7 +1,7 @@
 import * as fs from 'fs'
-import { ExtUri, FileUri, getWorkspaceFolderUri } from './exturi'
-import { dirExists, fileExists } from './fsHelper'
 import path from 'path'
+import { ExtUri, FileUri, isWorkspaceFolder, UntitledUri } from './exturi'
+import { dirExists, fileExists } from './fsHelper'
 
 // Detect lean4 root directory (works for both lean4 repo and nightly distribution)
 
@@ -30,20 +30,25 @@ export async function isCoreLean4Directory(path: FileUri): Promise<boolean> {
 }
 
 type ProjectRootInfo =
-    | { kind: 'Success'; projectRootUri: FileUri; toolchainUri: FileUri | undefined }
+    | { kind: 'Success'; projectRootUri: ExtUri; toolchainUri: FileUri | undefined }
     | { kind: 'FileNotFound' }
+    | { kind: 'LakefileWithoutToolchain'; projectRootUri: FileUri; lakefileUri: FileUri }
 type ToolchainInfo = { uri: FileUri; toolchain: string | undefined }
 type ProjectInfo =
-    | { kind: 'Success'; projectRootUri: FileUri; toolchainInfo: ToolchainInfo | undefined }
+    | { kind: 'Success'; projectRootUri: ExtUri; toolchainInfo: ToolchainInfo | undefined }
     | { kind: 'FileNotFound' }
+    | { kind: 'LakefileWithoutToolchain'; projectRootUri: FileUri; lakefileUri: FileUri }
 
 // Find the root of a Lean project and the Uri for the 'lean-toolchain' file found there.
-export async function findLeanProjectRootInfo(uri: FileUri): Promise<ProjectRootInfo> {
-    const toolchainFileName = 'lean-toolchain'
+export async function findLeanProjectRootInfo(uri: ExtUri): Promise<ProjectRootInfo> {
 
+    if (uri.scheme === 'untitled') {
+        return { kind: 'Success', projectRootUri: new UntitledUri(), toolchainUri: undefined }
+    }
+    // lean4monaco: Prevent filesystem access:
+    return { kind: 'Success', projectRootUri: uri.join('..'), toolchainUri: undefined }
+    /*
     let path = uri
-    const containingWsFolderUri = getWorkspaceFolderUri(uri)
-
     try {
         if ((await fs.promises.stat(path.fsPath)).isFile()) {
             path = uri.join('..')
@@ -55,7 +60,9 @@ export async function findLeanProjectRootInfo(uri: FileUri): Promise<ProjectRoot
     let bestFolder = path
     let bestLeanToolchain: FileUri | undefined
     while (true) {
-        const leanToolchain = path.join(toolchainFileName)
+        const leanToolchain = path.join('lean-toolchain')
+        const lakefileLean = path.join('lakefile.lean')
+        const lakefileToml = path.join('lakefile.toml')
         if (await fileExists(leanToolchain.fsPath)) {
             bestFolder = path
             bestLeanToolchain = leanToolchain
@@ -64,8 +71,12 @@ export async function findLeanProjectRootInfo(uri: FileUri): Promise<ProjectRoot
             bestLeanToolchain = undefined
             // Stop searching in case users accidentally created a lean-toolchain file above the core directory
             break
+        } else if (await fileExists(lakefileLean.fsPath)) {
+            return { kind: 'LakefileWithoutToolchain', projectRootUri: path, lakefileUri: lakefileLean }
+        } else if (await fileExists(lakefileToml.fsPath)) {
+            return { kind: 'LakefileWithoutToolchain', projectRootUri: path, lakefileUri: lakefileToml }
         }
-        if (containingWsFolderUri !== undefined && path.equals(containingWsFolderUri)) {
+        if (isWorkspaceFolder(path)) {
             if (bestLeanToolchain === undefined) {
                 // If we haven't found a toolchain yet, prefer the workspace folder as the project scope for the file,
                 // but keep looking in case there is a lean-toolchain above the workspace folder
@@ -85,16 +96,7 @@ export async function findLeanProjectRootInfo(uri: FileUri): Promise<ProjectRoot
     }
 
     return { kind: 'Success', projectRootUri: bestFolder, toolchainUri: bestLeanToolchain }
-}
-
-export async function findLeanProjectRoot(uri: FileUri): Promise<FileUri | 'FileNotFound'> {
-    const info = await findLeanProjectRootInfo(uri)
-    switch (info.kind) {
-        case 'Success':
-            return info.projectRootUri
-        case 'FileNotFound':
-            return 'FileNotFound'
-    }
+    */
 }
 
 export async function findLeanProjectInfo(uri: FileUri): Promise<ProjectInfo> {
@@ -107,7 +109,9 @@ export async function findLeanProjectInfo(uri: FileUri): Promise<ProjectInfo> {
             }
             return { kind: 'Success', projectRootUri: info.projectRootUri, toolchainInfo }
         case 'FileNotFound':
-            return { kind: 'FileNotFound' }
+            return info
+        case 'LakefileWithoutToolchain':
+            return info
     }
 }
 
diff --git a/vscode-lean4/src/utils/semverRegex.ts b/vscode-lean4/src/utils/semverRegex.ts
new file mode 100644
index 000000000..9779ca8ac
--- /dev/null
+++ b/vscode-lean4/src/utils/semverRegex.ts
@@ -0,0 +1,3 @@
+// Suggested at https://semver.org/#is-there-a-suggested-regular-expression-regex-to-check-a-semver-string
+export const semVerRegex =
+    /^(0|[1-9]\d*)\.(0|[1-9]\d*)\.(0|[1-9]\d*)(?:-((?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*)(?:\.(?:0|[1-9]\d*|\d*[a-zA-Z-][0-9a-zA-Z-]*))*))?(?:\+([0-9a-zA-Z-]+(?:\.[0-9a-zA-Z-]+)*))?$/
diff --git a/vscode-lean4/src/utils/uriHandlerService.ts b/vscode-lean4/src/utils/uriHandlerService.ts
new file mode 100644
index 000000000..d51a493fb
--- /dev/null
+++ b/vscode-lean4/src/utils/uriHandlerService.ts
@@ -0,0 +1,27 @@
+import { commands, Disposable, Uri, window } from 'vscode'
+
+export class UriHandlerService implements Disposable {
+    private subscriptions: Disposable[] = []
+
+    constructor() {
+        this.registerUriHandler()
+    }
+
+    dispose(): void {
+        for (const s of this.subscriptions) {
+            s.dispose()
+        }
+    }
+
+    private registerUriHandler() {
+        this.subscriptions.push(
+            window.registerUriHandler({
+                async handleUri(uri: Uri) {
+                    if (uri.path === '/setup-guide') {
+                        await commands.executeCommand('lean4.docs.showSetupGuide')
+                    }
+                },
+            }),
+        )
+    }
+}
diff --git a/vscode-lean4/test/suite/bootstrap/bootstrap.test.ts b/vscode-lean4/test/suite/bootstrap/bootstrap.test.ts
index c5042bdce..4a06acccc 100644
--- a/vscode-lean4/test/suite/bootstrap/bootstrap.test.ts
+++ b/vscode-lean4/test/suite/bootstrap/bootstrap.test.ts
@@ -10,7 +10,7 @@ import {
     initLean4Untitled,
     waitForActiveClient,
     waitForActiveClientRunning,
-    waitForInfoviewHtml,
+    waitForInfoviewHtmlAt,
 } from '../utils/helpers'
 
 suite('Lean4 Bootstrap Test Suite', () => {
@@ -32,20 +32,7 @@ suite('Lean4 Bootstrap Test Suite', () => {
         await waitForActiveClient(features.clientProvider, 120)
         await waitForActiveClientRunning(features.clientProvider, 300)
 
-        const hackNeeded = false
-        if (hackNeeded) {
-            // this is a hack we can do if it turns out this bootstrap test is unreliable.
-            // The hack would be covering a product bug, which is why we'd prefer not to use it.
-            // if it times out at 600 seconds then waitForInfoviewHtml prints the contents of the InfoView so we can see what happened.
-            // await waitForInfoviewHtml(info, expected, 10, 60000, true, async () => {
-            //     // 60 seconds elapsed, and infoview is not updating, try and re-edit
-            //     // the file to force the LSP to update.
-            //     await deleteAllText();
-            //     await insertText('#eval Lean.versionString');
-            // });
-        } else {
-            await waitForInfoviewHtml(info, expected, 600)
-        }
+        await waitForInfoviewHtmlAt('#eval', info, expected, 600)
 
         logger.log('Lean installation is complete.')
 
@@ -74,7 +61,7 @@ suite('Lean4 Bootstrap Test Suite', () => {
         assert(info, 'No InfoProvider export')
 
         logger.log('Wait for Lean nightly build server to start...')
-        await waitForInfoviewHtml(info, '4.0.0-nightly-', 120)
+        await waitForInfoviewHtmlAt('#eval', info, '4.0.0-nightly-', 120)
         logger.log('Lean nightly build server is running.')
 
         // make sure test is always run in predictable state, which is no file or folder open
diff --git a/vscode-lean4/test/suite/info/info.test.ts b/vscode-lean4/test/suite/info/info.test.ts
index 17f9027a2..99172aada 100644
--- a/vscode-lean4/test/suite/info/info.test.ts
+++ b/vscode-lean4/test/suite/info/info.test.ts
@@ -4,44 +4,22 @@ import * as vscode from 'vscode'
 import { logger } from '../../../src/utils/logger'
 import {
     assertStringInInfoview,
+    assertStringInInfoviewAt,
     clickInfoViewButton,
     closeActiveEditor,
     closeAllEditors,
-    findWord,
     gotoDefinition,
     gotoPosition,
     initLean4Untitled,
     insertText,
+    insertTextAfter,
     waitForActiveEditor,
     waitForInfoviewHtml,
+    waitForInfoviewHtmlAt,
     waitForInfoviewNotHtml,
 } from '../utils/helpers'
 
 suite('InfoView Test Suite', () => {
-    test('Copy to Comment', async () => {
-        logger.log('=================== Copy to Comment ===================')
-
-        const a = 37
-        const b = 22
-        const expectedEval1 = (a * b).toString()
-
-        const features = await initLean4Untitled(`#eval ${a}*${b}`)
-        const info = features.infoProvider
-        assert(info, 'No InfoProvider export')
-
-        await assertStringInInfoview(info, expectedEval1)
-
-        logger.log('Clicking copyToComment button in InfoView')
-        await clickInfoViewButton(info, 'copy-to-comment')
-
-        logger.log(`Checking editor contains ${expectedEval1}`)
-        const editor = vscode.window.activeTextEditor
-        assert(editor !== undefined, 'no active editor')
-        await findWord(editor, expectedEval1)
-
-        await closeAllEditors()
-    }).timeout(60000)
-
     test('Pinning and unpinning', async () => {
         logger.log('=================== Pinning and unpinning ===================')
 
@@ -50,7 +28,8 @@ suite('InfoView Test Suite', () => {
         const c = 77
         const d = 7
 
-        const features = await initLean4Untitled(`#eval ${a}*${b}`)
+        const evalLine1 = `#eval ${a}*${b}`
+        const features = await initLean4Untitled(evalLine1)
         const info = features.infoProvider
         assert(info, 'No InfoProvider export')
 
@@ -61,11 +40,12 @@ suite('InfoView Test Suite', () => {
         await clickInfoViewButton(info, 'toggle-pinned')
 
         logger.log('Insert another couple lines and another eval')
-        await insertText(`\n\n/- add another unpinned eval -/\n#eval ${c}*${d}`)
+        const evalLine2 = `#eval ${c}*${d}`
+        await insertTextAfter(evalLine1, `\n\n/- add another unpinned eval -/\n${evalLine2}`)
 
         logger.log('wait for the new expression to appear')
         const expectedEval2 = (c * d).toString()
-        await assertStringInInfoview(info, expectedEval2)
+        await assertStringInInfoviewAt(evalLine2, info, expectedEval2)
 
         logger.log('make sure pinned expression is still there')
         await assertStringInInfoview(info, expectedEval1)
@@ -75,7 +55,7 @@ suite('InfoView Test Suite', () => {
 
         logger.log('Make sure pinned eval is gone, but unpinned eval remains')
         await waitForInfoviewNotHtml(info, expectedEval1)
-        await assertStringInInfoview(info, expectedEval2)
+        await assertStringInInfoviewAt(evalLine2, info, expectedEval2)
 
         await closeAllEditors()
     }).timeout(60000)
@@ -92,7 +72,7 @@ suite('InfoView Test Suite', () => {
 
         const info = features.infoProvider
         assert(info, 'No InfoProvider export')
-        await waitForInfoviewHtml(info, expectedEval, 30, 1000, false)
+        await waitForInfoviewHtmlAt('#eval', info, expectedEval, 30, 1000, false)
 
         logger.log('Pin this info')
         await clickInfoViewButton(info, 'toggle-pinned')
@@ -106,7 +86,7 @@ suite('InfoView Test Suite', () => {
 
         logger.log('wait for the new expression to appear')
         const expectedEval2 = '[4, 1, 2, 3]'
-        await waitForInfoviewHtml(info, expectedEval2, 30, 1000, false)
+        await waitForInfoviewHtmlAt('#eval', info, expectedEval2, 30, 1000, false)
 
         logger.log('make sure pinned expression is not showing an error')
         await waitForInfoviewNotHtml(info, 'Incorrect position')
@@ -116,7 +96,7 @@ suite('InfoView Test Suite', () => {
         editor.selection = new vscode.Selection(newLastLine.start, newLastLine.start)
 
         logger.log('make sure pinned value reverts after an undo')
-        await waitForInfoviewHtml(info, expectedEval, 30, 1000, false)
+        await waitForInfoviewHtmlAt('#eval', info, expectedEval, 30, 1000, false)
 
         await closeAllEditors()
     }).timeout(60000)
@@ -128,21 +108,22 @@ suite('InfoView Test Suite', () => {
         const b = 95
         const prefix = 'Lean version is:'
 
-        const features = await initLean4Untitled(`#eval ${a}*${b}`)
+        const evalLine = `#eval ${a}*${b}`
+        const features = await initLean4Untitled(evalLine)
         const info = features.infoProvider
         assert(info, 'No InfoProvider export')
 
         const expectedEval = (a * b).toString()
-        await assertStringInInfoview(info, expectedEval)
+        await assertStringInInfoviewAt('#eval', info, expectedEval)
 
         logger.log('Pin this info')
         await clickInfoViewButton(info, 'toggle-pinned')
 
         logger.log('Insert another eval')
-        await insertText('\n\n#eval s!"' + prefix + ': {Lean.versionString}"')
+        await insertTextAfter(evalLine, '\n\n#eval s!"' + prefix + ': {Lean.versionString}"')
 
         logger.log('make sure output of versionString is also there')
-        await assertStringInInfoview(info, prefix)
+        await assertStringInInfoviewAt('#eval s!', info, prefix)
 
         logger.log('make sure pinned expression is not showing an error')
         await waitForInfoviewNotHtml(info, 'Incorrect position')
@@ -177,7 +158,7 @@ suite('InfoView Test Suite', () => {
         const info = features.infoProvider
         assert(info, 'No InfoProvider export')
 
-        gotoPosition(0, text.indexOf('by'))
+        gotoPosition('by')
         await assertStringInInfoview(info, 'issue461')
 
         logger.log('Opening tooltip for goal type')
diff --git a/vscode-lean4/test/suite/multi/multi.test.ts b/vscode-lean4/test/suite/multi/multi.test.ts
index 067371982..c44f0946b 100644
--- a/vscode-lean4/test/suite/multi/multi.test.ts
+++ b/vscode-lean4/test/suite/multi/multi.test.ts
@@ -4,7 +4,7 @@ import * as path from 'path'
 import * as vscode from 'vscode'
 import { logger } from '../../../src/utils/logger'
 import { displayNotification } from '../../../src/utils/notifs'
-import { assertStringInInfoview, closeAllEditors, getAltBuildVersion, initLean4 } from '../utils/helpers'
+import { assertStringInInfoviewAt, closeAllEditors, getAltBuildVersion, initLean4 } from '../utils/helpers'
 
 suite('Multi-Folder Test Suite', () => {
     test('Load a multi-project workspace', async () => {
@@ -19,7 +19,7 @@ suite('Multi-Folder Test Suite', () => {
         // verify we have a nightly build running in this folder.
         const info = features.infoProvider
         assert(info, 'No InfoProvider export')
-        await assertStringInInfoview(info, '4.0.0-nightly-')
+        await assertStringInInfoviewAt('#eval Lean.versionString', info, '4.0.0-nightly-')
 
         // Now open a file from the other project
         const doc2 = await vscode.workspace.openTextDocument(path.join(multiRoot, 'foo', 'Foo.lean'))
@@ -28,7 +28,7 @@ suite('Multi-Folder Test Suite', () => {
         await vscode.window.showTextDocument(doc2, options)
 
         logger.log(`wait for version ${version} to load...`)
-        await assertStringInInfoview(info, version)
+        await assertStringInInfoviewAt('#eval', info, version)
 
         // Now verify we have 2 LeanClients running.
         const clients = features.clientProvider
diff --git a/vscode-lean4/test/suite/restarts/restarts.test.ts b/vscode-lean4/test/suite/restarts/restarts.test.ts
index aeecc5ca0..7be61a433 100644
--- a/vscode-lean4/test/suite/restarts/restarts.test.ts
+++ b/vscode-lean4/test/suite/restarts/restarts.test.ts
@@ -7,12 +7,14 @@ import { logger } from '../../../src/utils/logger'
 import { displayNotification } from '../../../src/utils/notifs'
 import {
     assertStringInInfoview,
+    assertStringInInfoviewAt,
     closeAllEditors,
     deleteAllText,
     extractPhrase,
     initLean4,
     initLean4Untitled,
     insertText,
+    insertTextAfter,
     restartFile,
     restartLeanServer,
     waitForActiveClient,
@@ -29,18 +31,19 @@ suite('Lean Server Restart Test Suite', () => {
 
         // add normal values to initialize lean4 file
         const hello = 'Hello World'
-        const features = await initLean4Untitled(`#eval "${hello}"`)
+        const evalLine = `#eval "${hello}"`
+        const features = await initLean4Untitled(evalLine)
         const info = features.infoProvider
         assert(info, 'No InfoProvider export')
 
         logger.log('make sure language server is up and running.')
-        await assertStringInInfoview(info, hello)
+        await assertStringInInfoviewAt('#eval', info, hello)
 
         const clients = features.clientProvider
         assert(clients, 'No LeanClientProvider export')
 
         logger.log('Insert eval that causes crash.')
-        await insertText('\n\n#eval (unsafeCast 0 : String)')
+        await insertTextAfter(evalLine, '\n\n#eval (unsafeCast 0 : String)')
 
         const expectedMessage = 'The Lean Server has stopped processing this file'
         await assertStringInInfoview(info, expectedMessage)
@@ -60,7 +63,7 @@ suite('Lean Server Restart Test Suite', () => {
         await restartLeanServer(client)
 
         logger.log('checking that Hello World comes back after restart')
-        await assertStringInInfoview(info, hello)
+        await assertStringInInfoviewAt('#eval', info, hello)
 
         // make sure test is always run in predictable state, which is no file or folder open
         await closeAllEditors()
@@ -74,18 +77,19 @@ suite('Lean Server Restart Test Suite', () => {
 
         // add normal values to initialize lean4 file
         const hello = 'Hello World'
-        const features = await initLean4Untitled(`#eval "${hello}"`)
+        const evalLine = `#eval "${hello}"`
+        const features = await initLean4Untitled(evalLine)
         const info = features.infoProvider
         assert(info, 'No InfoProvider export')
 
         logger.log('make sure language server is up and running.')
-        await assertStringInInfoview(info, hello)
+        await assertStringInInfoviewAt('#eval', info, hello)
 
         const clients = features.clientProvider
         assert(clients, 'No LeanClientProvider export')
 
         logger.log('Insert eval that causes crash.')
-        await insertText('\n\n#eval (unsafeCast 0 : String)')
+        await insertTextAfter(evalLine, '\n\n#eval (unsafeCast 0 : String)')
 
         const expectedMessage = 'The Lean Server has stopped processing this file'
         await assertStringInInfoview(info, expectedMessage)
@@ -105,7 +109,7 @@ suite('Lean Server Restart Test Suite', () => {
         await restartFile()
 
         logger.log('checking that Hello World comes back after restart')
-        await assertStringInInfoview(info, hello)
+        await assertStringInInfoviewAt('#eval', info, hello)
 
         // make sure test is always run in predictable state, which is no file or folder open
         await closeAllEditors()
diff --git a/vscode-lean4/test/suite/simple/simple.test.ts b/vscode-lean4/test/suite/simple/simple.test.ts
index 513495504..3bc9c2dbe 100644
--- a/vscode-lean4/test/suite/simple/simple.test.ts
+++ b/vscode-lean4/test/suite/simple/simple.test.ts
@@ -6,7 +6,7 @@ import { elanInstalledToolchains } from '../../../src/utils/elan'
 import { logger } from '../../../src/utils/logger'
 import { displayNotification } from '../../../src/utils/notifs'
 import {
-    assertStringInInfoview,
+    assertStringInInfoviewAt,
     closeAllEditors,
     extractPhrase,
     gotoDefinition,
@@ -14,6 +14,7 @@ import {
     initLean4Untitled,
     waitForActiveEditor,
     waitForInfoviewHtml,
+    waitForInfoviewHtmlAt,
 } from '../utils/helpers'
 
 suite('Lean4 Basics Test Suite', () => {
@@ -25,7 +26,7 @@ suite('Lean4 Basics Test Suite', () => {
         const info = features.infoProvider
         assert(info, 'No InfoProvider export')
 
-        await assertStringInInfoview(info, '4.0.0-nightly-')
+        await assertStringInInfoviewAt('#eval', info, '4.0.0-nightly-')
 
         // test goto definition to lean toolchain works
         await waitForActiveEditor()
@@ -60,7 +61,7 @@ suite('Lean4 Basics Test Suite', () => {
         const info = features.infoProvider
         assert(info, 'No InfoProvider export')
         const expectedVersion = '5040' // the factorial function works.
-        const html = await waitForInfoviewHtml(info, expectedVersion)
+        const html = await waitForInfoviewHtmlAt('#eval factorial 7', info, expectedVersion)
 
         const installer = features.installer
         assert(installer, 'No LeanInstaller export')
@@ -73,7 +74,7 @@ suite('Lean4 Basics Test Suite', () => {
             defaultToolchain = defaultToolchain.replace('/', '--')
             defaultToolchain = defaultToolchain.replace(':', '---')
             // make sure this string exists in the info view.
-            await waitForInfoviewHtml(info, defaultToolchain)
+            await waitForInfoviewHtmlAt('#eval IO.appPath', info, defaultToolchain)
         }
 
         // make sure test is always run in predictable state, which is no file or folder open
@@ -97,7 +98,7 @@ suite('Lean4 Basics Test Suite', () => {
         const info = features.infoProvider
         assert(info, 'No InfoProvider export')
         let expectedVersion = 'Hello:'
-        let html = await waitForInfoviewHtml(info, expectedVersion)
+        let html = await waitForInfoviewHtmlAt('#eval main', info, expectedVersion)
         const versionString = extractPhrase(html, 'Hello:', '<').trim()
         logger.log(`>>> Found "${versionString}" in infoview`)
 
@@ -106,7 +107,7 @@ suite('Lean4 Basics Test Suite', () => {
 
         // if goto definition worked, then we are in Version.lean and we should see the Lake version string.
         expectedVersion = 'Lake Version:'
-        html = await waitForInfoviewHtml(info, expectedVersion)
+        html = await waitForInfoviewHtmlAt('#eval s!"Lake', info, expectedVersion)
 
         // make sure test is always run in predictable state, which is no file or folder open
         await closeAllEditors()
diff --git a/vscode-lean4/test/suite/toolchains/toolchain.test.ts b/vscode-lean4/test/suite/toolchains/toolchain.test.ts
index 90173bf65..76fe66ed3 100644
--- a/vscode-lean4/test/suite/toolchains/toolchain.test.ts
+++ b/vscode-lean4/test/suite/toolchains/toolchain.test.ts
@@ -5,12 +5,12 @@ import * as path from 'path'
 import { logger } from '../../../src/utils/logger'
 import { displayNotification } from '../../../src/utils/notifs'
 import {
-    assertStringInInfoview,
+    assertStringInInfoviewAt,
     closeAllEditors,
     extractPhrase,
     getAltBuildVersion,
     initLean4,
-    waitForInfoviewHtml,
+    waitForInfoviewHtmlAt,
 } from '../utils/helpers'
 
 // Expects to be launched with folder: ${workspaceFolder}/vscode-lean4/test/suite/simple
@@ -30,11 +30,11 @@ suite('Toolchain Test Suite', () => {
         assert(installer, 'No LeanInstaller export')
 
         // wait for info view to show up.
-        await assertStringInInfoview(info, 'Hello')
+        await assertStringInInfoviewAt('#eval main', info, 'Hello')
 
         // verify we have a nightly build running in this folder.
         const expectedVersion = '4.0.0-nightly-'
-        const html = await waitForInfoviewHtml(info, expectedVersion)
+        const html = await waitForInfoviewHtmlAt('#eval main', info, expectedVersion)
         const foundVersion = extractPhrase(html, expectedVersion, '\n')
 
         // Now edit the lean-toolchain file.
@@ -48,7 +48,7 @@ suite('Toolchain Test Suite', () => {
 
         try {
             logger.log(`verify that we switched to alt version ${version}`)
-            const html = await assertStringInInfoview(info, version)
+            const html = await assertStringInInfoviewAt('#eval main', info, version)
 
             // check the path to lean.exe from the `eval IO.appPath`
             const leanPath = extractPhrase(html, 'FilePath.mk', '<').trim()
@@ -61,7 +61,7 @@ suite('Toolchain Test Suite', () => {
         }
 
         logger.log(`Wait for version to appear, it should be ${foundVersion}`)
-        await assertStringInInfoview(info, foundVersion)
+        await assertStringInInfoviewAt('#eval main', info, foundVersion)
 
         // make sure test is always run in predictable state, which is no file or folder open
         await closeAllEditors()
diff --git a/vscode-lean4/test/suite/utils/helpers.ts b/vscode-lean4/test/suite/utils/helpers.ts
index 14c5db816..673e9a008 100644
--- a/vscode-lean4/test/suite/utils/helpers.ts
+++ b/vscode-lean4/test/suite/utils/helpers.ts
@@ -90,13 +90,23 @@ export async function deleteAllText(): Promise<void> {
     })
 }
 
-export function gotoPosition(line: number, character: number): void {
+export function gotoPosition(searchString: string, after: boolean = false): void {
     const editor = vscode.window.activeTextEditor
     assertAndLog(editor !== undefined, 'no active editor')
-    const position = new vscode.Position(line, character)
+    const text = editor.document.getText()
+    let offset = text.indexOf(searchString)
+    if (after) {
+        offset += searchString.length
+    }
+    const position = editor.document.positionAt(offset)
     editor.selection = new vscode.Selection(position, position)
 }
 
+export async function insertTextAfter(searchString: string, text: string): Promise<void> {
+    gotoPosition(searchString, true)
+    await insertText(text)
+}
+
 export async function initLean4Untitled(contents: string): Promise<EnabledFeatures> {
     // make sure test is always run in predictable state, which is no file or folder open
     await closeAllEditors()
@@ -371,6 +381,19 @@ export async function waitForInfoviewHtml(
     assertAndLog(false, `Missing "${toFind}" in infoview after ${timeout} seconds`)
 }
 
+export async function waitForInfoviewHtmlAt(
+    positionSearchString: string,
+    infoView: InfoProvider,
+    toFind: string,
+    retries = 60,
+    delay = 1000,
+    expand = true,
+    retryHandler = nullHandler,
+): Promise<string> {
+    gotoPosition(positionSearchString)
+    return await waitForInfoviewHtml(infoView, toFind, retries, delay, expand, retryHandler)
+}
+
 export async function waitForInfoviewNotHtml(
     infoView: InfoProvider,
     toFind: string,
@@ -499,6 +522,14 @@ export async function assertStringInInfoview(infoView: InfoProvider, expectedVer
     return await waitForInfoviewHtml(infoView, expectedVersion)
 }
 
+export async function assertStringInInfoviewAt(
+    positionSearchString: string,
+    infoView: InfoProvider,
+    expectedVersion: string,
+): Promise<string> {
+    return await waitForInfoviewHtmlAt(positionSearchString, infoView, expectedVersion)
+}
+
 export async function clickInfoViewButton(info: InfoProvider, name: string): Promise<void> {
     await assertStringInInfoview(info, name)
     let retries = 5
diff --git a/vscode-lean4/tsconfig.json b/vscode-lean4/tsconfig.json
index 3c7c8e187..cb0c6b277 100644
--- a/vscode-lean4/tsconfig.json
+++ b/vscode-lean4/tsconfig.json
@@ -8,7 +8,7 @@
         "lib": ["es6", "ES2021", "es2020.string"],
         "sourceMap": true,
         "alwaysStrict": true,
-        "rootDir": "./",
+        "rootDir": "../..",
         "noImplicitAny": true,
         "noFallthroughCasesInSwitch": true,
         "strictNullChecks": true,