From eab4711d9f931f8347c0556c33d6e149755236e1 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Mon, 12 Dec 2022 23:40:56 -0500
Subject: [PATCH 01/13] doc: update some docs

---
 lean4-infoview-api/src/rpcApi.ts              | 14 +++++++------
 lean4-infoview-api/src/util.ts                |  5 +++--
 lean4-infoview/src/infoview/goals.tsx         |  6 +++---
 .../src/infoview/interactiveCode.tsx          | 21 +++++++++----------
 lean4-infoview/src/infoview/traceExplorer.tsx |  2 +-
 5 files changed, 25 insertions(+), 23 deletions(-)

diff --git a/lean4-infoview-api/src/rpcApi.ts b/lean4-infoview-api/src/rpcApi.ts
index 6997accb1..12d5d91f9 100644
--- a/lean4-infoview-api/src/rpcApi.ts
+++ b/lean4-infoview-api/src/rpcApi.ts
@@ -38,16 +38,18 @@ export interface InfoPopup {
     doc?: string
 }
 
+export type FVarId = string
+export type MVarId = string
+
 export interface InteractiveHypothesisBundle {
     isInstance?: boolean,
     isType?: boolean,
-    /** The pretty names of the variables in the bundle.
-     * If the name is inaccessible this will be `"[anonymous]"`.
-     * Use `InteractiveHypothesis_accessibleNames` to filter these out.
-     */
+    /** The pretty names of the variables in the bundle. Anonymous names are rendered
+     * as `"[anonymous]"` whereas inaccessible ones have a `✝` appended at the end.
+     * Use `InteractiveHypothesisBundle_nonAnonymousNames` to filter these out. */
     names: string[]
     /** The free variable id associated with each of the vars listed in `names`. */
-    fvarIds?: string[]
+    fvarIds?: FVarId[]
     type: CodeWithInfos
     val?: CodeWithInfos
     /** If true, the hypothesis was not present on the previous tactic state. */
@@ -64,7 +66,7 @@ export interface InteractiveGoal {
     /** metavariable id associated with the goal.
      * This is undefined when the goal is a term goal
      * or if we are using an older version of lean. */
-    mvarId?: string
+    mvarId?: MVarId
     /** If true, the goal was not present on the previous tactic state. */
     isInserted?: boolean;
     /** If true, the goal will be deleted on the next tactic state. */
diff --git a/lean4-infoview-api/src/util.ts b/lean4-infoview-api/src/util.ts
index 8b22179f8..55279a782 100644
--- a/lean4-infoview-api/src/util.ts
+++ b/lean4-infoview-api/src/util.ts
@@ -1,5 +1,6 @@
 import { InteractiveHypothesisBundle, TaggedText } from './rpcApi'
 
+/** Reduce a `TaggedText` into its text contents without tags. */
 export function TaggedText_stripTags<T>(tt: TaggedText<T>): string {
     const go = (t: TaggedText<T>): string => {
         if ('append' in t)
@@ -13,7 +14,7 @@ export function TaggedText_stripTags<T>(tt: TaggedText<T>): string {
     return go(tt)
 }
 
-/** Filter out inaccessible / anonymous pretty names from the names list. */
-export function InteractiveHypothesisBundle_accessibleNames(ih : InteractiveHypothesisBundle) : string[] {
+/** Filter out anonymous pretty names from the names list. */
+export function InteractiveHypothesisBundle_nonAnonymousNames(ih : InteractiveHypothesisBundle) : string[] {
     return ih.names.filter(x => !x.includes('[anonymous]'))
 }
diff --git a/lean4-infoview/src/infoview/goals.tsx b/lean4-infoview/src/infoview/goals.tsx
index 06915ec2c..5e3fb1742 100644
--- a/lean4-infoview/src/infoview/goals.tsx
+++ b/lean4-infoview/src/infoview/goals.tsx
@@ -1,6 +1,6 @@
 import * as React from 'react'
 import { InteractiveCode } from './interactiveCode'
-import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle, InteractiveHypothesisBundle_accessibleNames, TaggedText_stripTags } from '@leanprover/infoview-api'
+import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle, InteractiveHypothesisBundle_nonAnonymousNames, TaggedText_stripTags } from '@leanprover/infoview-api'
 
 interface HypProps {
     hyp: InteractiveHypothesisBundle
@@ -18,7 +18,7 @@ export function Hyp({ hyp: h }: HypProps) {
     } else if (h.isRemoved) {
         namecls += 'removed-text '
     }
-    const names = InteractiveHypothesisBundle_accessibleNames(h).map((n, i) =>
+    const names = InteractiveHypothesisBundle_nonAnonymousNames(h).map((n, i) =>
         <span className={ 'mr1 ' + (isInaccessibleName(n) ? 'goal-inaccessible ' : '') + namecls} key={i}>{n}</span>
     )
     return <div>
@@ -37,7 +37,7 @@ function goalToString(g: InteractiveGoal): string {
     }
 
     for (const h of g.hyps) {
-        const names = InteractiveHypothesisBundle_accessibleNames(h).join(' ')
+        const names = InteractiveHypothesisBundle_nonAnonymousNames(h).join(' ')
         ret += `${names} : ${TaggedText_stripTags(h.type)}`
         if (h.val) {
             ret += ` := ${TaggedText_stripTags(h.val)}`
diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx
index 780ddfd9c..2db1b6384 100644
--- a/lean4-infoview/src/infoview/interactiveCode.tsx
+++ b/lean4-infoview/src/infoview/interactiveCode.tsx
@@ -1,7 +1,7 @@
 import * as React from 'react'
 
 import { EditorContext } from './contexts'
-import { DocumentPosition, useAsync, mapRpcError } from './util'
+import { useAsync, mapRpcError } from './util'
 import { SubexprInfo, CodeWithInfos, InteractiveDiagnostics_infoToInteractive, getGoToLocation, TaggedText, DiffTag } from '@leanprover/infoview-api'
 import { DetectHoverSpan, HoverState, WithTooltipOnHover } from './tooltips'
 import { Location } from 'vscode-languageserver-protocol'
@@ -21,8 +21,8 @@ export interface InteractiveTaggedTextProps<T> extends InteractiveTextComponentP
 }
 
 /**
- * Core loop to display `TaggedText` objects. Invokes `InnerTagUi` on `tag` nodes in order to support
- * various embedded information such as `InfoTree`s and `Expr`s.
+ * Core loop to display {@link TaggedText} objects. Invokes `InnerTagUi` on `tag` nodes in order to support
+ * various embedded information, for example subexpression information stored in {@link CodeWithInfos}.
  * */
 export function InteractiveTaggedText<T>({fmt, InnerTagUi}: InteractiveTaggedTextProps<T>) {
   if ('text' in fmt) return <>{fmt.text}</>
@@ -73,10 +73,11 @@ function TypePopupContents({ info, redrawTooltip }: TypePopupContentsProps) {
   // otherwise a 'loading' message.
   const interactive = useAsync(
     () => InteractiveDiagnostics_infoToInteractive(rs, info.info),
-    [rs, info.info, info.subexprPos])
+    [rs, info.info])
 
-  // We let the tooltip know to redo its layout whenever our contents change.
-  React.useEffect(() => { void redrawTooltip() }, [interactive.state, (interactive as any)?.value, (interactive as any)?.error, redrawTooltip])
+  // We ask the tooltip parent component to relayout whenever our contents change.
+  React.useEffect(() => { void redrawTooltip() },
+    [interactive.state, (interactive as any)?.value, (interactive as any)?.error, redrawTooltip])
 
   return <div className="tooltip-code-content">
     {interactive.state === 'resolved' ? <>
@@ -170,11 +171,9 @@ function InteractiveCodeTag({tag: ct, fmt}: InteractiveTagProps<SubexprInfo>) {
   )
 }
 
-export interface InteractiveCodeProps {
-  fmt: CodeWithInfos
-}
+export type InteractiveCodeProps = InteractiveTextComponentProps<SubexprInfo>
 
 /** Displays a {@link CodeWithInfos} obtained via RPC from the Lean server. */
-export function InteractiveCode({fmt}: InteractiveCodeProps) {
-  return <InteractiveTaggedText InnerTagUi={InteractiveCodeTag} fmt={fmt} />
+export function InteractiveCode(props: InteractiveCodeProps) {
+  return InteractiveTaggedText({...props, InnerTagUi: InteractiveCodeTag})
 }
diff --git a/lean4-infoview/src/infoview/traceExplorer.tsx b/lean4-infoview/src/infoview/traceExplorer.tsx
index 5b32f81b2..ce8293aee 100644
--- a/lean4-infoview/src/infoview/traceExplorer.tsx
+++ b/lean4-infoview/src/infoview/traceExplorer.tsx
@@ -10,7 +10,7 @@
 import * as React from 'react'
 import { Goal } from './goals'
 import { InteractiveCode, InteractiveTaggedText, InteractiveTagProps, InteractiveTextComponentProps } from './interactiveCode'
-import { InteractiveDiagnostics_msgToInteractive, lazyTraceChildrenToInteractive, MessageData, MsgEmbed, TaggedText, TraceEmbed } from '@leanprover/infoview-api'
+import { InteractiveDiagnostics_msgToInteractive, lazyTraceChildrenToInteractive, MessageData, MsgEmbed, TraceEmbed } from '@leanprover/infoview-api'
 import { mapRpcError, useAsyncWithTrigger } from './util'
 import { RpcContext } from './rpcSessions'
 

From d38e48a28607327ee91fc8cb01c90011e36403ef Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Tue, 13 Dec 2022 23:55:56 -0500
Subject: [PATCH 02/13] refactor: move state down into goal component

---
 lean4-infoview-api/src/rpcSessions.ts      |   2 +
 lean4-infoview/src/infoview/collapsing.tsx |  21 +++-
 lean4-infoview/src/infoview/goals.tsx      | 120 +++++++++++++++-----
 lean4-infoview/src/infoview/info.tsx       | 126 +++++----------------
 4 files changed, 144 insertions(+), 125 deletions(-)

diff --git a/lean4-infoview-api/src/rpcSessions.ts b/lean4-infoview-api/src/rpcSessions.ts
index 377d6d972..d5d447e42 100644
--- a/lean4-infoview-api/src/rpcSessions.ts
+++ b/lean4-infoview-api/src/rpcSessions.ts
@@ -148,6 +148,8 @@ class RpcSessionForFile {
         try {
             const result = await this.sessions.iface.call({ method, params, sessionId, ... pos });
             this.registerRefs(result);
+            // HACK: most of our types are `T | undefined` so try to return something matching that interface
+            if (result === null) return undefined;
             return result;
         } catch (ex: any) {
             if (ex?.code === RpcErrorCode.WorkerCrashed || ex?.code === RpcErrorCode.WorkerExited ||
diff --git a/lean4-infoview/src/infoview/collapsing.tsx b/lean4-infoview/src/infoview/collapsing.tsx
index ded9ffdf6..8f70641c7 100644
--- a/lean4-infoview/src/infoview/collapsing.tsx
+++ b/lean4-infoview/src/infoview/collapsing.tsx
@@ -25,10 +25,11 @@ export function useIsVisible(): [(element: HTMLElement) => void, boolean] {
 
 interface DetailsProps {
     initiallyOpen?: boolean;
-    children: [JSX.Element, ...JSX.Element[]];
+    children: [React.ReactNode, ...React.ReactNode[]];
     setOpenRef?: React.MutableRefObject<React.Dispatch<React.SetStateAction<boolean>>>;
 }
 
+/** Like `<details>` but can be programatically revealed using `setOpenRef`. */
 export function Details({initiallyOpen, children: [summary, ...children], setOpenRef}: DetailsProps): JSX.Element {
     const [isOpen, setOpen] = React.useState<boolean>(initiallyOpen === undefined ? false : initiallyOpen);
     const setupEventListener = React.useCallback((node: HTMLDetailsElement | null) => {
@@ -43,3 +44,21 @@ export function Details({initiallyOpen, children: [summary, ...children], setOpe
         { isOpen && children }
     </details>;
 }
+
+interface CollapsibleProps {
+    children: [React.ReactNode, ...React.ReactNode[]]
+}
+
+/**
+ * A header with collapsible contents component that we use everywhere in the infoview.
+ * The first child is the header. The other children are contents. */
+export function Collapsible({children: [header, ...children]}: CollapsibleProps): JSX.Element {
+    return <details open>
+        <summary className='mv2 pointer'>
+            {header}
+        </summary>
+        <div className='ml1'>
+            {children}
+        </div>
+    </details>
+}
diff --git a/lean4-infoview/src/infoview/goals.tsx b/lean4-infoview/src/infoview/goals.tsx
index 5e3fb1742..2797e3f02 100644
--- a/lean4-infoview/src/infoview/goals.tsx
+++ b/lean4-infoview/src/infoview/goals.tsx
@@ -1,34 +1,15 @@
 import * as React from 'react'
 import { InteractiveCode } from './interactiveCode'
 import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle, InteractiveHypothesisBundle_nonAnonymousNames, TaggedText_stripTags } from '@leanprover/infoview-api'
-
-interface HypProps {
-    hyp: InteractiveHypothesisBundle
-}
+import { WithTooltipOnHover } from './tooltips';
+import { Collapsible } from './collapsing';
+import { EditorContext } from './contexts';
 
 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
 function isInaccessibleName(h: string): boolean {
     return h.indexOf('✝') >= 0;
 }
 
-export function Hyp({ hyp: h }: HypProps) {
-    let namecls : string = ''
-    if (h.isInserted) {
-        namecls += 'inserted-text '
-    } else if (h.isRemoved) {
-        namecls += 'removed-text '
-    }
-    const names = InteractiveHypothesisBundle_nonAnonymousNames(h).map((n, i) =>
-        <span className={ 'mr1 ' + (isInaccessibleName(n) ? 'goal-inaccessible ' : '') + namecls} key={i}>{n}</span>
-    )
-    return <div>
-        <strong className="goal-hyp">{names}</strong>
-        :&nbsp;
-        <InteractiveCode fmt={h.type} />
-        {h.val && <>&nbsp;:=&nbsp;<InteractiveCode fmt={h.val} /></>}
-    </div>
-}
-
 function goalToString(g: InteractiveGoal): string {
     let ret = ''
 
@@ -54,7 +35,7 @@ export function goalsToString(goals: InteractiveGoals): string {
     return goals.goals.map(goalToString).join('\n\n')
 }
 
-export interface GoalFilterState {
+interface GoalFilterState {
     /** If true reverse the list of hypotheses, if false present the order received from LSP. */
     reverse: boolean,
     /** If true show hypotheses that have isType=True, otherwise hide them. */
@@ -78,13 +59,36 @@ function getFilteredHypotheses(hyps: InteractiveHypothesisBundle[], filter: Goal
     }, [])
 }
 
+interface HypProps {
+    hyp: InteractiveHypothesisBundle
+}
+
+function Hyp({ hyp: h }: HypProps) {
+    let namecls : string = ''
+    if (h.isInserted) {
+        namecls += 'inserted-text '
+    } else if (h.isRemoved) {
+        namecls += 'removed-text '
+    }
+    const names = InteractiveHypothesisBundle_nonAnonymousNames(h).map((n, i) =>
+        <span className={ 'mr1 ' + (isInaccessibleName(n) ? 'goal-inaccessible ' : '') + namecls} key={i}>{n}</span>
+    )
+    return <div>
+        <strong className="goal-hyp">{names}</strong>
+        :&nbsp;
+        <InteractiveCode fmt={h.type} />
+        {h.val && <>&nbsp;:=&nbsp;<InteractiveCode fmt={h.val} /></>}
+    </div>
+}
+
 interface GoalProps {
     goal: InteractiveGoal
     filter: GoalFilterState
-    /** Where the goal appears in the goal list. Or none if not present. */
-    index?: number
 }
 
+/**
+ * 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 } = props
     const prefix = goal.goalPrefix ?? '⊢ '
@@ -114,12 +118,74 @@ interface GoalsProps {
     filter: GoalFilterState
 }
 
-export function Goals({ goals, filter }: GoalsProps) {
+function Goals({ goals, filter }: GoalsProps) {
     if (goals.goals.length === 0) {
         return <>Goals accomplished 🎉</>
     } else {
         return <>
-            {goals.goals.map((g, i) => <Goal key={i} goal={g} filter={filter} index={i} />)}
+            {goals.goals.map((g, i) => <Goal key={i} goal={g} filter={filter} />)}
         </>
     }
 }
+
+interface FilteredGoalsProps {
+    header: React.ReactNode
+    /**
+     * When this is `undefined`, the component will not appear at all but will remember its state
+     * by virtue of still being mounted in the React tree. When it does appear again, the filter
+     * settings and collapsed state will be as before. */
+    goals?: InteractiveGoals
+}
+
+/**
+ * Display goals together with a header containing custom contents as well as buttons to control
+ * how the goals are displayed.
+ */
+export function FilteredGoals({ header, goals }: FilteredGoalsProps) {
+    const ec = React.useContext(EditorContext)
+
+    const copyToCommentButton =
+        <a className="link pointer mh2 dim codicon codicon-quote"
+            data-id="copy-goal-to-comment"
+            onClick={e => {
+                e.preventDefault();
+                if (goals) ec.copyToComment(goalsToString(goals))
+            }}
+            title="copy state to comment" />
+
+    const [goalFilters, setGoalFilters] = React.useState<GoalFilterState>(
+        { reverse: false, 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, name: string) =>
+        <a className='link pointer tooltip-menu-content' onClick={_ => { setGoalFilters(filterFn) }}>
+            <span className={'tooltip-menu-icon codicon ' + (filledFn(goalFilters) ? 'codicon-check ' : 'codicon-blank ')}>&nbsp;</span>
+            <span className='tooltip-menu-text '>{name}</span>
+        </a>
+    const filterMenu = <span>
+        {mkFilterButton(s => ({ ...s, showType: !s.showType }), gf => gf.showType, 'types')}
+        <br/>
+        {mkFilterButton(s => ({ ...s, showInstance: !s.showInstance }), gf => gf.showInstance, 'instances')}
+        <br/>
+        {mkFilterButton(s => ({ ...s, showHiddenAssumption: !s.showHiddenAssumption }), gf => gf.showHiddenAssumption, 'hidden assumptions')}
+        <br/>
+        {mkFilterButton(s => ({ ...s, showLetValue: !s.showLetValue }), gf => gf.showLetValue, 'let-values')}
+    </span>
+
+    const isFiltered = !goalFilters.showInstance || !goalFilters.showType || !goalFilters.showHiddenAssumption || !goalFilters.showLetValue
+    const filterButton =
+        <WithTooltipOnHover mkTooltipContent={() => filterMenu}>
+            <a className={'link pointer mh2 dim codicon ' + (isFiltered ? 'codicon-filter-filled ': 'codicon-filter ')}/>
+        </WithTooltipOnHover>
+
+    return <div style={{display: goals !== undefined ? 'block' : 'none'}}>
+        <Collapsible>
+            <>{header} <span className='fr'>{copyToCommentButton}{sortButton}{filterButton}</span></>
+            {goals && <Goals goals={goals} filter={goalFilters}></Goals>}
+        </Collapsible>
+    </div>
+}
diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx
index a38b4ca07..6d4ac32b9 100644
--- a/lean4-infoview/src/infoview/info.tsx
+++ b/lean4-infoview/src/infoview/info.tsx
@@ -1,14 +1,15 @@
 import * as React from 'react';
 import type { Location, Diagnostic } from 'vscode-languageserver-protocol';
 
-import { Goals as GoalsUi, Goal as GoalUi, goalsToString, GoalFilterState } from './goals';
-import { basename, DocumentPosition, RangeHelpers, useEvent, usePausableState, discardMethodNotFound, mapRpcError, useAsyncWithTrigger, PausableProps } from './util';
-import { Details } from './collapsing';
+import { FilteredGoals, goalsToString } from './goals';
+import { basename, DocumentPosition, RangeHelpers, useEvent, usePausableState, discardMethodNotFound,
+    mapRpcError, useAsyncWithTrigger, PausableProps } from './util';
+import { Collapsible, Details } from './collapsing';
 import { ConfigContext, EditorContext, LspDiagnosticsContext, ProgressContext } from './contexts';
 import { lspDiagToInteractive, MessagesList } from './messages';
 import { getInteractiveGoals, getInteractiveTermGoal, InteractiveDiagnostic, InteractiveGoal,
-    InteractiveGoals, UserWidgets, Widget_getWidgets, RpcSessionAtPos, isRpcError, RpcErrorCode, getInteractiveDiagnostics } from '@leanprover/infoview-api';
-import { WithTooltipOnHover } from './tooltips'
+    InteractiveGoals, UserWidgetInstance, Widget_getWidgets, RpcSessionAtPos, isRpcError,
+    RpcErrorCode, getInteractiveDiagnostics } from '@leanprover/infoview-api';
 import { UserWidgetDisplay } from './userWidget'
 import { RpcContext, useRpcSessionAtPos } from './rpcSessions';
 
@@ -24,12 +25,11 @@ interface InfoPinnable {
 interface InfoStatusBarProps extends InfoPinnable, PausableProps {
     pos: DocumentPosition;
     status: InfoStatus;
-    copyGoalToComment?: () => void;
     triggerUpdate: () => Promise<void>;
 }
 
 const InfoStatusBar = React.memo((props: InfoStatusBarProps) => {
-    const { kind, onPin, status, pos, isPaused, copyGoalToComment, setPaused, triggerUpdate } = props;
+    const { kind, onPin, status, pos, isPaused, setPaused, triggerUpdate } = props;
 
     const ec = React.useContext(EditorContext);
 
@@ -49,11 +49,6 @@ const InfoStatusBar = React.memo((props: InfoStatusBarProps) => {
         {!isPinned && isPaused && ' (paused)'}
         {isPinned && isPaused && ' (pinned and paused)'}
         <span className="fr">
-            {copyGoalToComment &&
-                <a className="link pointer mh2 dim codicon codicon-quote"
-                   data-id="copy-goal-to-comment"
-                   onClick={e => { e.preventDefault(); copyGoalToComment(); }}
-                   title="copy state to comment" />}
             {isPinned &&
                 <a className="link pointer mh2 dim codicon codicon-go-to-file"
                    data-id="reveal-file-location"
@@ -82,51 +77,18 @@ interface InfoDisplayContentProps extends PausableProps {
     goals?: InteractiveGoals;
     termGoal?: InteractiveGoal;
     error?: string;
-    userWidgets?: UserWidgets;
+    userWidgets: UserWidgetInstance[];
     triggerUpdate: () => Promise<void>;
 }
 
 const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
     const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused} = props;
 
-    const widgets = userWidgets && userWidgets.widgets
-    const hasWidget = (widgets !== undefined) && (widgets.length > 0)
-
-    const nothingToShow = !error && !goals && !termGoal && messages.length === 0 && !hasWidget;
-
+    const hasWidget = userWidgets.length > 0;
     const hasError = !!error;
-    const hasGoals = !!goals;
-    const hasTermGoal = !!termGoal;
     const hasMessages = messages.length !== 0;
 
-    const [goalFilters, setGoalFilters] = React.useState<GoalFilterState>(
-        { reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true });
-    const sortClasses = 'link pointer mh2 dim codicon fr ' + (goalFilters.reverse ? 'codicon-arrow-up ' : 'codicon-arrow-down ');
-    const sortButton = <a className={sortClasses} title="reverse list" onClick={e => {
-        setGoalFilters(s => {
-            return { ...s, reverse: !s.reverse }
-        } ); }
-    } />
-
-    const mkFilterButton = (filterFn: React.SetStateAction<GoalFilterState>, filledFn: (_: GoalFilterState) => boolean, name: string) =>
-        <a className='link pointer tooltip-menu-content' onClick={_ => { setGoalFilters(filterFn) }}>
-            <span className={'tooltip-menu-icon codicon ' + (filledFn(goalFilters) ? 'codicon-check ' : 'codicon-blank ')}>&nbsp;</span>
-            <span className='tooltip-menu-text '>{name}</span>
-        </a>
-    const filterMenu = <span>
-        {mkFilterButton(s => ({ ...s, showType: !s.showType }), gf => gf.showType, 'types')}
-        <br/>
-        {mkFilterButton(s => ({ ...s, showInstance: !s.showInstance }), gf => gf.showInstance, 'instances')}
-        <br/>
-        {mkFilterButton(s => ({ ...s, showHiddenAssumption: !s.showHiddenAssumption }), gf => gf.showHiddenAssumption, 'hidden assumptions')}
-        <br/>
-        {mkFilterButton(s => ({ ...s, showLetValue: !s.showLetValue }), gf => gf.showLetValue, 'let-values')}
-    </span>
-    const isFiltered = !goalFilters.showInstance || !goalFilters.showType || !goalFilters.showHiddenAssumption || !goalFilters.showLetValue
-    const filterButton = <span className='fr'>
-        <WithTooltipOnHover mkTooltipContent={() => {return filterMenu}}>
-            <a className={'link pointer mh2 dim codicon ' + (isFiltered ? 'codicon-filter-filled ': 'codicon-filter ')}/>
-        </WithTooltipOnHover></span>
+    const nothingToShow = !hasError && !goals && !termGoal && !hasMessages && !hasWidget;
 
     /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */
     return <>
@@ -136,48 +98,20 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
                     Error updating:{' '}{error}.
                     <a className="link pointer dim" onClick={e => { e.preventDefault(); void triggerUpdate(); }}>{' '}Try again.</a>
                 </div>}
-            <div style={{display: hasGoals ? 'block' : 'none'}} key="goals">
-                <Details initiallyOpen>
-                    <summary className="mv2 pointer">
-                        Tactic state {sortButton} {filterButton}
-                    </summary>
-                    <div className='ml1'>
-                        {hasGoals && <GoalsUi goals={goals} filter={goalFilters} />}
-                    </div>
-                </Details>
-            </div>
-            <div style={{display: hasTermGoal ? 'block' : 'none'}} key="term-goal">
-                <Details initiallyOpen>
-                    <summary className="mv2 pointer">
-                        Expected type {sortButton} {filterButton}
-                    </summary>
-                    <div className='ml1'>
-                        {hasTermGoal && <GoalUi goal={termGoal} filter={goalFilters} />}
-                    </div>
-                </Details>
-            </div>
-            {widgets && widgets.map(widget =>
-                <div style={{display: hasWidget ? 'block' : 'none'}}
-                     key={`widget::${widget.id}::${widget.range?.toString()}`}>
-                    <Details initiallyOpen>
-                        <summary className="mv2 pointer">
-                            {widget.name}
-                        </summary>
-                        <div className="ml1">
-                             <UserWidgetDisplay pos={pos} widget={widget}/>
-                        </div>
-                    </Details>
-                </div>
+            <FilteredGoals header={"Tactic state"} key="goals" goals={goals} />
+            <FilteredGoals header={"Expected type"} key="term-goal"
+                goals={termGoal !== undefined ? {goals: [termGoal]} : undefined} />
+            {userWidgets.map(widget =>
+                <Collapsible key={`widget::${widget.id}::${widget.range?.toString()}`}>
+                    <>{widget.name}</>
+                    <UserWidgetDisplay pos={pos} widget={widget}/>
+                </Collapsible>
             )}
             <div style={{display: hasMessages ? 'block' : 'none'}} key="messages">
-                <Details initiallyOpen>
-                    <summary className="mv2 pointer">
-                        Messages ({messages.length})
-                    </summary>
-                    <div className="ml1">
-                        <MessagesList uri={pos.uri} messages={messages} />
-                    </div>
-                </Details>
+                <Collapsible key="messages">
+                    <>Messages ({messages.length})</>
+                    <MessagesList uri={pos.uri} messages={messages} />
+                </Collapsible>
             </div>
             {nothingToShow && (
                 isPaused ?
@@ -199,7 +133,7 @@ interface InfoDisplayProps {
     goals?: InteractiveGoals;
     termGoal?: InteractiveGoal;
     error?: string;
-    userWidgets?: UserWidgets;
+    userWidgets: UserWidgetInstance[];
     rpcSess: RpcSessionAtPos;
     triggerUpdate: () => Promise<void>;
 }
@@ -222,8 +156,6 @@ function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) {
     const {kind, goals, rpcSess} = props;
 
     const ec = React.useContext(EditorContext);
-    let copyGoalToComment: (() => void) | undefined
-    if (goals) copyGoalToComment = () => void ec.copyToComment(goalsToString(goals));
 
     // If we are the cursor infoview, then we should subscribe to
     // some commands from the editor extension
@@ -231,7 +163,7 @@ function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) {
     useEvent(ec.events.requestedAction, act => {
         if (!isCursor) return;
         if (act.kind !== 'copyToComment') return;
-        if (copyGoalToComment) copyGoalToComment();
+        if (goals) void ec.copyToComment(goalsToString(goals));
     }, [goals]);
     useEvent(ec.events.requestedAction, act => {
         if (!isCursor) return;
@@ -242,7 +174,7 @@ function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) {
     return (
     <RpcContext.Provider value={rpcSess}>
     <Details initiallyOpen>
-        <InfoStatusBar {...props} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} copyGoalToComment={copyGoalToComment} />
+        <InfoStatusBar {...props} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} />
         <InfoDisplayContent {...props} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} />
     </Details>
     </RpcContext.Provider>
@@ -336,7 +268,7 @@ function InfoAux(props: InfoProps) {
                 goals: undefined,
                 termGoal: undefined,
                 error: undefined,
-                userWidgets: undefined,
+                userWidgets: [],
                 rpcSess
             }), 500)
         }
@@ -351,7 +283,7 @@ function InfoAux(props: InfoProps) {
                 goals,
                 termGoal,
                 error: undefined,
-                userWidgets,
+                userWidgets: userWidgets?.widgets ?? [],
                 rpcSess
             }),
             ex => {
@@ -381,7 +313,7 @@ function InfoAux(props: InfoProps) {
                     goals: undefined,
                     termGoal: undefined,
                     error: `Error fetching goals: ${errorString}`,
-                    userWidgets: undefined,
+                    userWidgets: [],
                     rpcSess
                 })
             }
@@ -417,7 +349,7 @@ function InfoAux(props: InfoProps) {
         goals: undefined,
         termGoal: undefined,
         error: undefined,
-        userWidgets: undefined,
+        userWidgets: [],
         rpcSess,
         triggerUpdate
     })

From d5288005271dca0ec247ddaaff684437b02adb61 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Wed, 14 Dec 2022 00:36:15 -0500
Subject: [PATCH 03/13] feat: collapsible `case`s

---
 lean4-infoview/src/infoview/collapsing.tsx | 18 ------
 lean4-infoview/src/infoview/goals.tsx      | 45 +++++++++------
 lean4-infoview/src/infoview/info.tsx       | 67 +++++++++++-----------
 3 files changed, 61 insertions(+), 69 deletions(-)

diff --git a/lean4-infoview/src/infoview/collapsing.tsx b/lean4-infoview/src/infoview/collapsing.tsx
index 8f70641c7..61e0188bb 100644
--- a/lean4-infoview/src/infoview/collapsing.tsx
+++ b/lean4-infoview/src/infoview/collapsing.tsx
@@ -44,21 +44,3 @@ export function Details({initiallyOpen, children: [summary, ...children], setOpe
         { isOpen && children }
     </details>;
 }
-
-interface CollapsibleProps {
-    children: [React.ReactNode, ...React.ReactNode[]]
-}
-
-/**
- * A header with collapsible contents component that we use everywhere in the infoview.
- * The first child is the header. The other children are contents. */
-export function Collapsible({children: [header, ...children]}: CollapsibleProps): JSX.Element {
-    return <details open>
-        <summary className='mv2 pointer'>
-            {header}
-        </summary>
-        <div className='ml1'>
-            {children}
-        </div>
-    </details>
-}
diff --git a/lean4-infoview/src/infoview/goals.tsx b/lean4-infoview/src/infoview/goals.tsx
index 2797e3f02..6b0aeccf7 100644
--- a/lean4-infoview/src/infoview/goals.tsx
+++ b/lean4-infoview/src/infoview/goals.tsx
@@ -2,7 +2,6 @@ import * as React from 'react'
 import { InteractiveCode } from './interactiveCode'
 import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle, InteractiveHypothesisBundle_nonAnonymousNames, TaggedText_stripTags } from '@leanprover/infoview-api'
 import { WithTooltipOnHover } from './tooltips';
-import { Collapsible } from './collapsing';
 import { EditorContext } from './contexts';
 
 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
@@ -98,15 +97,20 @@ export const Goal = React.memo((props: GoalProps) => {
         <strong className="goal-vdash">{prefix}</strong>
         <InteractiveCode fmt={goal.type} />
     </div>
-    let cn = 'font-code tl pre-wrap mv1 bl bw1 pl1 b--transparent '
-    if (props.goal.isInserted) {
-        cn += 'b--inserted '
-    }
-    if (props.goal.isRemoved) {
-        cn += 'b--removed '
-    }
-    return <div className={cn}>
-        {goal.userName && <div key={'case'}><strong className="goal-case">case </strong>{goal.userName}</div>}
+    let cn = 'font-code tl pre-wrap bl bw1 pl1 b--transparent '
+    if (props.goal.isInserted) cn += 'b--inserted '
+    if (props.goal.isRemoved) cn += 'b--removed '
+
+    if (goal.userName) {
+        return <details open className={cn}>
+            <summary className='mv1 pointer'>
+                <strong className="goal-case">case </strong>{goal.userName}
+            </summary>
+            {filter.reverse && goalLi}
+            {hyps.map((h, i) => <Hyp hyp={h} key={i} />)}
+            {!filter.reverse && goalLi}
+        </details>
+    } else return <div className={cn}>
         {filter.reverse && goalLi}
         {hyps.map((h, i) => <Hyp hyp={h} key={i} />)}
         {!filter.reverse && goalLi}
@@ -129,7 +133,7 @@ function Goals({ goals, filter }: GoalsProps) {
 }
 
 interface FilteredGoalsProps {
-    header: React.ReactNode
+    headerChildren: React.ReactNode
     /**
      * When this is `undefined`, the component will not appear at all but will remember its state
      * by virtue of still being mounted in the React tree. When it does appear again, the filter
@@ -138,10 +142,10 @@ interface FilteredGoalsProps {
 }
 
 /**
- * Display goals together with a header containing custom contents as well as buttons to control
- * how the goals are displayed.
+ * Display goals together with a header containing the provided children as well as buttons
+ * to control how the goals are displayed.
  */
-export function FilteredGoals({ header, goals }: FilteredGoalsProps) {
+export function FilteredGoals({ headerChildren, goals }: FilteredGoalsProps) {
     const ec = React.useContext(EditorContext)
 
     const copyToCommentButton =
@@ -183,9 +187,14 @@ export function FilteredGoals({ header, goals }: FilteredGoalsProps) {
         </WithTooltipOnHover>
 
     return <div style={{display: goals !== undefined ? 'block' : 'none'}}>
-        <Collapsible>
-            <>{header} <span className='fr'>{copyToCommentButton}{sortButton}{filterButton}</span></>
-            {goals && <Goals goals={goals} filter={goalFilters}></Goals>}
-        </Collapsible>
+        <details open>
+            <summary className='mv2 pointer'>
+                {headerChildren}
+                <span className='fr'>{copyToCommentButton}{sortButton}{filterButton}</span>
+            </summary>
+            <div className='ml1'>
+                {goals && <Goals goals={goals} filter={goalFilters}></Goals>}
+            </div>
+        </details>
     </div>
 }
diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx
index 6d4ac32b9..69a227c9c 100644
--- a/lean4-infoview/src/infoview/info.tsx
+++ b/lean4-infoview/src/infoview/info.tsx
@@ -4,7 +4,6 @@ import type { Location, Diagnostic } from 'vscode-languageserver-protocol';
 import { FilteredGoals, goalsToString } from './goals';
 import { basename, DocumentPosition, RangeHelpers, useEvent, usePausableState, discardMethodNotFound,
     mapRpcError, useAsyncWithTrigger, PausableProps } from './util';
-import { Collapsible, Details } from './collapsing';
 import { ConfigContext, EditorContext, LspDiagnosticsContext, ProgressContext } from './contexts';
 import { lspDiagToInteractive, MessagesList } from './messages';
 import { getInteractiveGoals, getInteractiveTermGoal, InteractiveDiagnostic, InteractiveGoal,
@@ -92,37 +91,37 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
 
     /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */
     return <>
-        <div className="ml1">
-            {hasError &&
-                <div className="error" key="errors">
-                    Error updating:{' '}{error}.
-                    <a className="link pointer dim" onClick={e => { e.preventDefault(); void triggerUpdate(); }}>{' '}Try again.</a>
-                </div>}
-            <FilteredGoals header={"Tactic state"} key="goals" goals={goals} />
-            <FilteredGoals header={"Expected type"} key="term-goal"
-                goals={termGoal !== undefined ? {goals: [termGoal]} : undefined} />
-            {userWidgets.map(widget =>
-                <Collapsible key={`widget::${widget.id}::${widget.range?.toString()}`}>
-                    <>{widget.name}</>
-                    <UserWidgetDisplay pos={pos} widget={widget}/>
-                </Collapsible>
-            )}
-            <div style={{display: hasMessages ? 'block' : 'none'}} key="messages">
-                <Collapsible key="messages">
-                    <>Messages ({messages.length})</>
+        {hasError &&
+            <div className="error" key="errors">
+                Error updating:{' '}{error}.
+                <a className="link pointer dim" onClick={e => { e.preventDefault(); void triggerUpdate(); }}>{' '}Try again.</a>
+            </div>}
+        <FilteredGoals headerChildren={"Tactic state"} key="goals" goals={goals} />
+        <FilteredGoals headerChildren={"Expected type"} key="term-goal"
+            goals={termGoal !== undefined ? {goals: [termGoal]} : undefined} />
+        {userWidgets.map(widget =>
+            <details key={`widget::${widget.id}::${widget.range?.toString()}`} open>
+                <summary className='mv2 pointer'>{widget.name}</summary>
+                <UserWidgetDisplay pos={pos} widget={widget}/>
+            </details>
+        )}
+        <div style={{display: hasMessages ? 'block' : 'none'}} key="messages">
+            <details key="messages" open>
+                <summary className='mv2 pointer'>Messages ({messages.length})</summary>
+                <div className='ml1'>
                     <MessagesList uri={pos.uri} messages={messages} />
-                </Collapsible>
-            </div>
-            {nothingToShow && (
-                isPaused ?
-                    /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */
-                    <span>Updating is paused.{' '}
-                        <a className="link pointer dim" onClick={e => { e.preventDefault(); void triggerUpdate(); }}>Refresh</a>
-                        {' '}or <a className="link pointer dim" onClick={e => { e.preventDefault(); setPaused(false); }}>resume updating</a>
-                        {' '}to see information.
-                    </span> :
-                    'No info found.')}
+                </div>
+            </details>
         </div>
+        {nothingToShow && (
+            isPaused ?
+                /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */
+                <span>Updating is paused.{' '}
+                    <a className="link pointer dim" onClick={e => { e.preventDefault(); void triggerUpdate(); }}>Refresh</a>
+                    {' '}or <a className="link pointer dim" onClick={e => { e.preventDefault(); setPaused(false); }}>resume updating</a>
+                    {' '}to see information.
+                </span> :
+                'No info found.')}
     </>
 })
 
@@ -173,10 +172,12 @@ function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) {
 
     return (
     <RpcContext.Provider value={rpcSess}>
-    <Details initiallyOpen>
+    <details open>
         <InfoStatusBar {...props} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} />
-        <InfoDisplayContent {...props} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} />
-    </Details>
+        <div className='ml1'>
+            <InfoDisplayContent {...props} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} />
+        </div>
+    </details>
     </RpcContext.Provider>
     );
 }

From f9cef2aa2809c048b6a29ed28023031dfc5a8cb8 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Fri, 16 Dec 2022 22:49:04 -0500
Subject: [PATCH 04/13] feat: multi-expression contexts

---
 lean4-infoview-api/src/rpcApi.ts              |   5 +-
 lean4-infoview/src/infoview/exprContext.tsx   | 105 ++++++++++++++++++
 lean4-infoview/src/infoview/goals.tsx         |  65 ++++++++---
 lean4-infoview/src/infoview/index.css         |   5 +
 lean4-infoview/src/infoview/info.tsx          |  17 ++-
 .../src/infoview/interactiveCode.tsx          |  43 +++++--
 lean4-infoview/src/infoview/messages.tsx      |   4 +-
 lean4-infoview/src/infoview/tooltips.tsx      |  43 ++++---
 lean4-infoview/src/infoview/userWidget.tsx    |   8 +-
 lean4-infoview/src/infoview/util.ts           |  45 ++++++--
 10 files changed, 272 insertions(+), 68 deletions(-)
 create mode 100644 lean4-infoview/src/infoview/exprContext.tsx

diff --git a/lean4-infoview-api/src/rpcApi.ts b/lean4-infoview-api/src/rpcApi.ts
index 12d5d91f9..9d4e1681a 100644
--- a/lean4-infoview-api/src/rpcApi.ts
+++ b/lean4-infoview-api/src/rpcApi.ts
@@ -22,9 +22,12 @@ export type DiffTag =
   | 'wasDeleted'  | 'willDelete'
   | 'wasInserted' | 'willInsert'
 
+// This is an arbitrary-size `Nat` in Lean which in JS we represent as `string`
+export type SubexprPos = string
+
 export interface SubexprInfo {
     info: InfoWithCtx
-    subexprPos?: number
+    subexprPos?: SubexprPos
     diffStatus?: DiffTag
 }
 
diff --git a/lean4-infoview/src/infoview/exprContext.tsx b/lean4-infoview/src/infoview/exprContext.tsx
new file mode 100644
index 000000000..893e6d5de
--- /dev/null
+++ b/lean4-infoview/src/infoview/exprContext.tsx
@@ -0,0 +1,105 @@
+/*
+Copyright (c) 2022 E.W.Ayers. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: E.W.Ayers, Wojciech Nawrocki
+*/
+import { FVarId, MVarId, SubexprPos } from "@leanprover/infoview-api";
+import * as React from 'react';
+
+/**
+ * A location within a goal. It is either:
+ * - one of the hypotheses; or
+ * - (a subexpression of) the type of one of the hypotheses; or
+ * - (a subexpression of) the value of one of the let-bound hypotheses; or
+ * - (a subexpression of) the goal type. */
+export type GoalLocation =
+  { hyp: FVarId }
+  | { hypType: [FVarId, SubexprPos] }
+  | { hypValue: [FVarId, SubexprPos] }
+  | { target: SubexprPos }
+
+export namespace GoalLocation {
+  export function isEqual(l1: GoalLocation, l2: GoalLocation): boolean {
+    if ('hyp' in l1) return 'hyp' in l2 ? l1.hyp === l2.hyp : false
+    else if ('hypType' in l1) return 'hypType' in l2 ? l1.hypType[0] === l2.hypType[0] && l1.hypType[1] === l2.hypType[1] : false
+    else if ('hypValue' in l1) return 'hypValue' in l2 ? l1.hypValue[0] === l2.hypValue[0] && l1.hypValue[1] === l2.hypValue[1] : false
+    else if ('target' in l1) return 'target' in l2 ? l1.target === l2.target : false
+    else return false
+  }
+
+  export function withSubexprPos(l: GoalLocation, p: SubexprPos): GoalLocation {
+    if ('hyp' in l) return l
+    else if ('hypType' in l) return { hypType: [ l.hypType[0], p ] }
+    else if ('hypValue' in l) return { hypValue: [ l.hypValue[0], p ] }
+    else if ('target' in l) return { target: p }
+    else throw new Error(`unrecognized GoalLocation variant ${JSON.stringify(l)}`)
+  }
+}
+
+/**
+ * A location within a goal state. It identifies a specific goal together with a {@link GoalLocation}
+ * within it.  */
+export interface GoalsLocation {
+    /** Which goal the location is in. */
+    mvarId: MVarId;
+    loc: GoalLocation;
+}
+
+export namespace GoalsLocation {
+  export function isEqual(l1: GoalsLocation, l2: GoalsLocation): boolean {
+    return l1.mvarId === l2.mvarId && GoalLocation.isEqual(l1.loc, l2.loc)
+  }
+
+  export function withSubexprPos(l: GoalsLocation, p: SubexprPos): GoalsLocation {
+    return { ...l, loc: GoalLocation.withSubexprPos(l.loc, p) }
+  }
+}
+
+/**
+ * An interface available through a React context in components where selecting subexpressions
+ * makes sense. Currently this is only the goal state display in which {@link GoalLocation}s
+ * can be selected. */
+export interface Locations {
+  isSelected: (l: GoalsLocation) => void
+  setSelected: (l: GoalsLocation, on: boolean) => void
+  /**
+   * A template for the location of the current component. It is defined if and only if the current
+   * component is a subexpression of a selectable expression. We use
+   * {@link GoalsLocation.withSubexprPos} to map this template to a complete location. */
+  subexprTemplate?: GoalsLocation
+}
+
+export const LocationsContext = React.createContext<Locations | undefined>(undefined)
+
+type SelectableLocationProps =
+    React.PropsWithoutRef<React.DetailedHTMLProps<React.HTMLAttributes<HTMLSpanElement>, HTMLSpanElement>> &
+    { locs: Locations, loc: GoalsLocation }
+
+export function SelectableLocation(props: SelectableLocationProps): JSX.Element {
+    const [isSelected, setSelected] = React.useState<boolean>(false)
+
+    const spanClassName: string = 'highlightable '
+        + (isSelected ? 'highlight-selected ' : '')
+        + (props.className ? props.className : '')
+
+    return <span {...props}
+        className={spanClassName}
+        onClick={e => {
+            if (e.shiftKey) {
+              setSelected(on => {
+                props.locs.setSelected(props.loc, !on)
+                return !on
+              })
+              e.stopPropagation()
+            }
+            if (props.onClick) props.onClick(e)
+        }}
+        onPointerDown={e => {
+          // Since shift-click on this component is a custom selection, when shift is held prevent
+          // the default action which on text is to start a text selection.
+          if (e.shiftKey) e.preventDefault()
+        }}
+      >
+        {props.children}
+      </span>
+}
diff --git a/lean4-infoview/src/infoview/goals.tsx b/lean4-infoview/src/infoview/goals.tsx
index 6b0aeccf7..518e738eb 100644
--- a/lean4-infoview/src/infoview/goals.tsx
+++ b/lean4-infoview/src/infoview/goals.tsx
@@ -1,8 +1,9 @@
 import * as React from 'react'
 import { InteractiveCode } from './interactiveCode'
-import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle, InteractiveHypothesisBundle_nonAnonymousNames, TaggedText_stripTags } from '@leanprover/infoview-api'
+import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle, InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_stripTags } from '@leanprover/infoview-api'
 import { WithTooltipOnHover } from './tooltips';
 import { EditorContext } from './contexts';
+import { LocationsContext, SelectableLocation } from './exprContext';
 
 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
 function isInaccessibleName(h: string): boolean {
@@ -60,23 +61,45 @@ function getFilteredHypotheses(hyps: InteractiveHypothesisBundle[], filter: Goal
 
 interface HypProps {
     hyp: InteractiveHypothesisBundle
+    mvarId?: MVarId
 }
 
-function Hyp({ hyp: h }: HypProps) {
-    let namecls : string = ''
-    if (h.isInserted) {
-        namecls += 'inserted-text '
-    } else if (h.isRemoved) {
-        namecls += 'removed-text '
-    }
+function Hyp({ hyp: h, mvarId }: HypProps) {
+    const locs = React.useContext(LocationsContext)
+    const hasLoc = locs && mvarId && h.fvarIds && h.fvarIds.length > 0
+
+    const namecls: string = 'mr1 ' +
+        (h.isInserted ? 'inserted-text ' : '') +
+        (h.isRemoved ? 'removed-text ' : '')
+
     const names = InteractiveHypothesisBundle_nonAnonymousNames(h).map((n, i) =>
-        <span className={ 'mr1 ' + (isInaccessibleName(n) ? 'goal-inaccessible ' : '') + namecls} key={i}>{n}</span>
-    )
+        <span className={namecls + (isInaccessibleName(n) ? 'goal-inaccessible ' : '')} key={i}>
+            {hasLoc ?
+                <SelectableLocation
+                    locs={locs}
+                    loc={{ mvarId, loc: { hyp: h.fvarIds![i] }}}
+                >
+                    {n}
+                </SelectableLocation> :
+                n}
+        </span>)
+
     return <div>
         <strong className="goal-hyp">{names}</strong>
         :&nbsp;
-        <InteractiveCode fmt={h.type} />
-        {h.val && <>&nbsp;:=&nbsp;<InteractiveCode fmt={h.val} /></>}
+        <LocationsContext.Provider value={hasLoc ?
+            { ...locs, subexprTemplate: { mvarId, loc: { hypType: [h.fvarIds![0], ''] }}} :
+            undefined
+        }>
+            <InteractiveCode fmt={h.type} />
+        </LocationsContext.Provider>
+        {h.val &&
+            <LocationsContext.Provider value={hasLoc ?
+                { ...locs, subexprTemplate: { mvarId, loc: { hypValue: [h.fvarIds![0], ''] }}} :
+                undefined
+            }>
+                &nbsp;:=&nbsp;<InteractiveCode fmt={h.val} />
+            </LocationsContext.Provider>}
     </div>
 }
 
@@ -93,9 +116,16 @@ export const Goal = React.memo((props: GoalProps) => {
     const prefix = goal.goalPrefix ?? '⊢ '
     const filteredList = getFilteredHypotheses(goal.hyps, filter);
     const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList;
+    const locs = React.useContext(LocationsContext)
     const goalLi = <div key={'goal'}>
         <strong className="goal-vdash">{prefix}</strong>
-        <InteractiveCode fmt={goal.type} />
+        <LocationsContext.Provider value={
+            locs && goal.mvarId ?
+                { ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} :
+                undefined
+        }>
+            <InteractiveCode fmt={goal.type} />
+        </LocationsContext.Provider>
     </div>
     let cn = 'font-code tl pre-wrap bl bw1 pl1 b--transparent '
     if (props.goal.isInserted) cn += 'b--inserted '
@@ -107,12 +137,12 @@ export const Goal = React.memo((props: GoalProps) => {
                 <strong className="goal-case">case </strong>{goal.userName}
             </summary>
             {filter.reverse && goalLi}
-            {hyps.map((h, i) => <Hyp hyp={h} key={i} />)}
+            {hyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
             {!filter.reverse && goalLi}
         </details>
     } else return <div className={cn}>
         {filter.reverse && goalLi}
-        {hyps.map((h, i) => <Hyp hyp={h} key={i} />)}
+        {hyps.map((h, i) => <Hyp hyp={h} mvarId={goal.mvarId} key={i} />)}
         {!filter.reverse && goalLi}
     </div>
 })
@@ -133,6 +163,7 @@ function Goals({ goals, filter }: GoalsProps) {
 }
 
 interface FilteredGoalsProps {
+    /** Components to render in the header. */
     headerChildren: React.ReactNode
     /**
      * When this is `undefined`, the component will not appear at all but will remember its state
@@ -145,7 +176,7 @@ interface FilteredGoalsProps {
  * Display goals together with a header containing the provided children as well as buttons
  * to control how the goals are displayed.
  */
-export function FilteredGoals({ headerChildren, goals }: FilteredGoalsProps) {
+export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoalsProps) => {
     const ec = React.useContext(EditorContext)
 
     const copyToCommentButton =
@@ -197,4 +228,4 @@ export function FilteredGoals({ headerChildren, goals }: FilteredGoalsProps) {
             </div>
         </details>
     </div>
-}
+})
diff --git a/lean4-infoview/src/infoview/index.css b/lean4-infoview/src/infoview/index.css
index 31ba482b7..0c6cb414f 100644
--- a/lean4-infoview/src/infoview/index.css
+++ b/lean4-infoview/src/infoview/index.css
@@ -51,10 +51,15 @@ html,body {
     border-radius: 2pt;
     transition: background-color 100ms ease-in-out;
 }
+
 .highlight {
     background-color: var(--vscode-editor-selectionBackground) !important;
 }
 
+.highlight-selected {
+    background-color: var(--vscode-editorOverviewRuler-rangeHighlightForeground);
+}
+
 /* Interactive traces */
 .trace-line:hover {
     background-color: #dbeeff;
diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx
index 69a227c9c..b5dd314c0 100644
--- a/lean4-infoview/src/infoview/info.tsx
+++ b/lean4-infoview/src/infoview/info.tsx
@@ -11,6 +11,7 @@ import { getInteractiveGoals, getInteractiveTermGoal, InteractiveDiagnostic, Int
     RpcErrorCode, getInteractiveDiagnostics } from '@leanprover/infoview-api';
 import { UserWidgetDisplay } from './userWidget'
 import { RpcContext, useRpcSessionAtPos } from './rpcSessions';
+import { GoalsLocation, LocationsContext } from './exprContext';
 
 type InfoStatus = 'updating' | 'error' | 'ready';
 type InfoKind = 'cursor' | 'pin';
@@ -89,6 +90,8 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
 
     const nothingToShow = !hasError && !goals && !termGoal && !hasMessages && !hasWidget;
 
+    const [selectedLocs, setSelectedLocs] = React.useState<GoalsLocation[]>([])
+
     /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */
     return <>
         {hasError &&
@@ -96,13 +99,23 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
                 Error updating:{' '}{error}.
                 <a className="link pointer dim" onClick={e => { e.preventDefault(); void triggerUpdate(); }}>{' '}Try again.</a>
             </div>}
-        <FilteredGoals headerChildren={"Tactic state"} key="goals" goals={goals} />
+
+        <LocationsContext.Provider value ={{
+            isSelected: l => selectedLocs.some(v => GoalsLocation.isEqual(v, l)),
+            setSelected: (l, on) => {
+                if (on) setSelectedLocs(ls => ls.filter(v => !GoalsLocation.isEqual(v, l)).concat([l]))
+                else setSelectedLocs(ls => ls.filter(v => !GoalsLocation.isEqual(v, l)))
+            },
+            subexprTemplate: undefined
+        }}>
+            <FilteredGoals headerChildren={"Tactic state"} key="goals" goals={goals} />
+        </LocationsContext.Provider>
         <FilteredGoals headerChildren={"Expected type"} key="term-goal"
             goals={termGoal !== undefined ? {goals: [termGoal]} : undefined} />
         {userWidgets.map(widget =>
             <details key={`widget::${widget.id}::${widget.range?.toString()}`} open>
                 <summary className='mv2 pointer'>{widget.name}</summary>
-                <UserWidgetDisplay pos={pos} widget={widget}/>
+                <UserWidgetDisplay pos={pos} selectedLocations={selectedLocs} widget={widget}/>
             </details>
         )}
         <div style={{display: hasMessages ? 'block' : 'none'}} key="messages">
diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx
index 2db1b6384..24adba67f 100644
--- a/lean4-infoview/src/infoview/interactiveCode.tsx
+++ b/lean4-infoview/src/infoview/interactiveCode.tsx
@@ -7,6 +7,7 @@ import { DetectHoverSpan, HoverState, WithTooltipOnHover } from './tooltips'
 import { Location } from 'vscode-languageserver-protocol'
 import { marked } from 'marked'
 import { RpcContext } from './rpcSessions'
+import { GoalsLocation, LocationsContext } from './exprContext'
 
 export interface InteractiveTextComponentProps<T> {
   fmt: TaggedText<T>
@@ -111,17 +112,21 @@ const DIFF_TAG_TO_EXPLANATION : {[K in DiffTag] : string} = {
   'willDelete': 'This subexpression will be deleted.',
 }
 
-/** Tagged spans can be hovered over to display extra info stored in the associated `SubexprInfo`. */
+/**
+ * Tagged spans can be hovered over to display extra info stored in the associated `SubexprInfo`.
+ * Moreover if this component is rendered in a context where locations can be selected, the span
+ * can be shift-clicked to select it.
+ */
 function InteractiveCodeTag({tag: ct, fmt}: InteractiveTagProps<SubexprInfo>) {
   const mkTooltip = React.useCallback((redrawTooltip: () => void) =>
     <TypePopupContents info={ct} redrawTooltip={redrawTooltip} />,
     [ct.info])
 
-  // We mimick the VSCode ctrl-hover and ctrl-click UI for go-to-definition
   const rs = React.useContext(RpcContext)
   const ec = React.useContext(EditorContext)
   const [hoverState, setHoverState] = React.useState<HoverState>('off')
 
+  // We mimick the VSCode ctrl-hover and ctrl-click UI for go-to-definition
   const [goToLoc, setGoToLoc] = React.useState<Location | undefined>(undefined)
   const fetchGoToLoc = React.useCallback(async () => {
     if (goToLoc !== undefined) return goToLoc
@@ -137,10 +142,20 @@ function InteractiveCodeTag({tag: ct, fmt}: InteractiveTagProps<SubexprInfo>) {
     }
     return undefined
   }, [rs, ct.info, goToLoc])
+  // Eagerly fetch the location as soon as the pointer enters this area so that we can show
+  // an underline if a jump target is available.
   React.useEffect(() => { if (hoverState === 'ctrlOver') void fetchGoToLoc() }, [hoverState])
 
-  let spanClassName : any = 'highlightable '
-    + (hoverState !== 'off' ? 'highlight ' : '')
+  const locs = React.useContext(LocationsContext)
+  const ourLoc = locs && locs.subexprTemplate && ct.subexprPos ?
+    GoalsLocation.withSubexprPos(locs.subexprTemplate, ct.subexprPos) :
+    undefined
+  const [isSelected, setSelected] = React.useState<boolean>(false)
+  const innerSpanClassName: string = 'highlightable ' +
+    (isSelected ? 'highlight-selected ' : '')
+
+  let spanClassName: string = 'highlightable '
+    + (hoverState != 'off' ? 'highlight ' : '')
     + (hoverState === 'ctrlOver' && goToLoc !== undefined ? 'underline ' : '')
   if (ct.diffStatus) {
     spanClassName += DIFF_TAG_TO_CLASS[ct.diffStatus] + ' '
@@ -150,22 +165,34 @@ function InteractiveCodeTag({tag: ct, fmt}: InteractiveTagProps<SubexprInfo>) {
     <WithTooltipOnHover
       mkTooltipContent={mkTooltip}
       onClick={(e, next) => {
-        // On ctrl-click, if location is known, go to it in the editor
+        // On ctrl-click or ⌘-click, if location is known, go to it in the editor
         if (e.ctrlKey || e.metaKey) {
           setHoverState(st => st === 'over' ? 'ctrlOver' : st)
           void fetchGoToLoc().then(loc => {
             if (loc === undefined) return
             void ec.revealPosition({ uri: loc.uri, ...loc.range.start })
           })
-        }
-        if (!e.ctrlKey) next(e)
+        // On shift-click, if we are in a context where selecting subexpressions makes sense,
+        // (un)select the current subexpression.
+        } else if (e.shiftKey) {
+          if (ourLoc) {
+            setSelected(on => {
+              locs!.setSelected(ourLoc, !on)
+              return !on
+            })
+          }
+        } else next(e)
       }}
     >
       <DetectHoverSpan
         setHoverState={setHoverState}
         className={spanClassName}
       >
-        <InteractiveCode fmt={fmt} />
+        {/* Note: we use two spans so that if the outer one already has a background-color,
+        the inner color still shows (with transparency). */}
+        <span className={innerSpanClassName}>
+          <InteractiveCode fmt={fmt} />
+        </span>
       </DetectHoverSpan>
     </WithTooltipOnHover>
   )
diff --git a/lean4-infoview/src/infoview/messages.tsx b/lean4-infoview/src/infoview/messages.tsx
index fbc99a718..8991f9912 100644
--- a/lean4-infoview/src/infoview/messages.tsx
+++ b/lean4-infoview/src/infoview/messages.tsx
@@ -68,7 +68,7 @@ function mkMessageViewProps(uri: DocumentUri, messages: InteractiveDiagnostic[])
 }
 
 /** Shows the given messages assuming they are for the given file. */
-export function MessagesList({uri, messages}: {uri: DocumentUri, messages: InteractiveDiagnostic[]}) {
+export const MessagesList = React.memo(({uri, messages}: {uri: DocumentUri, messages: InteractiveDiagnostic[]}) => {
     const should_hide = messages.length === 0;
     if (should_hide) { return <>No messages.</> }
 
@@ -77,7 +77,7 @@ export function MessagesList({uri, messages}: {uri: DocumentUri, messages: Inter
         {mkMessageViewProps(uri, messages).map(m => <MessageView {...m} />)}
     </div>
     );
-}
+})
 
 function lazy<T>(f: () => T): () => T {
     let state: {t: T} | undefined
diff --git a/lean4-infoview/src/infoview/tooltips.tsx b/lean4-infoview/src/infoview/tooltips.tsx
index 25b486ece..d72bf49c1 100644
--- a/lean4-infoview/src/infoview/tooltips.tsx
+++ b/lean4-infoview/src/infoview/tooltips.tsx
@@ -4,7 +4,7 @@ import * as ReactDOM from 'react-dom'
 import * as Popper from '@popperjs/core'
 import { usePopper } from 'react-popper'
 
-import { forwardAndUseRef, LogicalDomContext, useLogicalDom } from './util'
+import { forwardAndUseRef, LogicalDomContext, useLogicalDom, useOnClickOutside } from './util'
 
 /** Tooltip contents should call `redrawTooltip` whenever their layout changes. */
 export type MkTooltipContentFn = (redrawTooltip: () => void) => React.ReactNode
@@ -83,11 +83,12 @@ export type HoverState = 'off' | 'over' | 'ctrlOver'
  * only the smallest (deepest in the DOM tree) {@link DetectHoverSpan} has an enabled hover state. */
 export const DetectHoverSpan =
   forwardAndUseRef<HTMLSpanElement,
-    React.HTMLProps<HTMLSpanElement> & {setHoverState: React.Dispatch<React.SetStateAction<HoverState>>}>((props_, ref, setRef) => {
+    React.DetailedHTMLProps<React.HTMLAttributes<HTMLSpanElement>, HTMLSpanElement> &
+    {setHoverState: React.Dispatch<React.SetStateAction<HoverState>>}>((props_, ref, setRef) => {
   const {setHoverState, ...props} = props_;
 
   const onPointerEvent = (b: boolean) => (e: React.PointerEvent<HTMLSpanElement>) => {
-    // It's more composable to let pointer events bubble up rather than to `stopPropagating`,
+    // It's more composable to let pointer events bubble up rather than to call `stopPropagation`,
     // but we only want to handle hovers in the innermost component. So we record that the
     // event was handled with a property.
     // The `contains` check ensures that the node hovered over is a child in the DOM
@@ -147,7 +148,7 @@ const TipChainContext = React.createContext<TipChainContext>({pinParent: () => {
  *
  * An `onClick` middleware can optionally be given in order to control what happens when the
  * hoverable area is clicked. The middleware can invoke `next` to execute the default action
- * (show the tooltip). */
+ * which is to pin the tooltip open. */
 export const WithTooltipOnHover =
   forwardAndUseRef<HTMLSpanElement,
     Omit<React.HTMLProps<HTMLSpanElement>, 'onClick'> & {
@@ -176,7 +177,7 @@ export const WithTooltipOnHover =
   // hoverable area in the DOM tree, and the `contains` check fails for elements within tooltip
   // contents. We can use this to distinguish these elements.
   const isWithinHoverable = (el: EventTarget) => ref.current && el instanceof Node && ref.current.contains(el)
-  const [logicalDom, logicalDomStorage] = useLogicalDom(ref)
+  const [logicalElt, logicalDomStorage] = useLogicalDom(ref)
 
   // We use timeouts for debouncing hover events.
   const timeout = React.useRef<number>()
@@ -189,29 +190,18 @@ export const WithTooltipOnHover =
   const showDelay = 500
   const hideDelay = 300
 
+  const isModifierHeld = (e: React.MouseEvent) => (e.altKey || e.ctrlKey || e.shiftKey || e.metaKey)
+
   const onClick = (e: React.MouseEvent<HTMLSpanElement>) => {
     clearTimeout()
     setState(state => state === 'pin' ? 'hide' : 'pin')
   }
 
-  React.useEffect(() => {
-    const onClickAnywhere = (e: Event) => {
-      if (e.target instanceof Node && !logicalDom.contains(e.target)) {
-        if (e.target instanceof Element && e.target.tagName === 'HTML'){
-          // then user might be clicking in a scrollbar, otherwise
-          // e.target would be a tag other than 'HTML' so we do not want to hide the popup
-          // so user can scroll and read it all otherwise popup disappears
-          // when you click on the scrollbar!
-        } else {
-          clearTimeout()
-          setState('hide')
-        }
-      }
-    }
-
-    document.addEventListener('pointerdown', onClickAnywhere)
-    return () => document.removeEventListener('pointerdown', onClickAnywhere)
-  }, [ref, logicalDom])
+  const onClickOutside = React.useCallback(() => {
+    clearTimeout()
+    setState('hide')
+  }, [])
+  useOnClickOutside(logicalElt, onClickOutside)
 
   const isPointerOverTooltip = React.useRef<boolean>(false)
   const startShowTimeout = () => {
@@ -257,8 +247,13 @@ export const WithTooltipOnHover =
         if (props.onClick !== undefined) props.onClick(e, onClick)
         else onClick(e)
       }}
+      onPointerDown={e => {
+        // We have special handling for some modifier+click events, so prevent default browser
+        // events from interfering when a modifier is held.
+        if (isModifierHeld(e)) e.preventDefault()
+      }}
       onPointerOver={e => {
-        onPointerEvent(startShowTimeout, e)
+        if (!isModifierHeld(e)) onPointerEvent(startShowTimeout, e)
         if (props.onPointerOver !== undefined) props.onPointerOver(e)
       }}
       onPointerOut={e => {
diff --git a/lean4-infoview/src/infoview/userWidget.tsx b/lean4-infoview/src/infoview/userWidget.tsx
index 9f4f8d064..95fd721b9 100644
--- a/lean4-infoview/src/infoview/userWidget.tsx
+++ b/lean4-infoview/src/infoview/userWidget.tsx
@@ -4,6 +4,7 @@ import { Widget_getWidgetSource, UserWidgetInstance } from '@leanprover/infoview
 import { RpcContext } from './rpcSessions';
 import { DocumentPosition, mapRpcError, useAsync } from './util';
 import { ErrorBoundary } from './errors';
+import { GoalsLocation } from './exprContext';
 
 function dynamicallyLoadComponent(hash: string, code: string) {
     return React.lazy(async () => {
@@ -17,6 +18,7 @@ const componentCache = new Map<string, React.LazyExoticComponent<React.Component
 
 interface UserWidgetDisplayProps {
     pos: DocumentPosition
+    selectedLocations: GoalsLocation[]
     widget: UserWidgetInstance
 }
 
@@ -24,9 +26,11 @@ interface UserWidgetDisplayProps {
 export interface UserWidgetProps {
     /** Cursor position in the file at which the widget is being displayed. */
     pos: DocumentPosition
+    /** Locations currently selected in the goal state. */
+    selectedLocations: GoalsLocation[]
 }
 
-export function UserWidgetDisplay({ pos, widget }: UserWidgetDisplayProps) {
+export function UserWidgetDisplay({ pos, selectedLocations, widget }: UserWidgetDisplayProps) {
     const rs = React.useContext(RpcContext);
     const hash = widget.javascriptHash
     const component = useAsync(
@@ -42,7 +46,7 @@ export function UserWidgetDisplay({ pos, widget }: UserWidgetDisplayProps) {
         },
         [hash])
 
-    const componentProps: UserWidgetProps = { pos, ...widget.props }
+    const componentProps: UserWidgetProps = { pos, selectedLocations, ...widget.props }
 
     return (
         <React.Suspense fallback={`Loading widget: ${widget.id} ${component.state}.`}>
diff --git a/lean4-infoview/src/infoview/util.ts b/lean4-infoview/src/infoview/util.ts
index f6716f463..201086d6b 100644
--- a/lean4-infoview/src/infoview/util.ts
+++ b/lean4-infoview/src/infoview/util.ts
@@ -190,7 +190,7 @@ export function addUniqueKeys<T>(elems: T[], getId: (el: T) => string): Keyed<T>
 
 /** Like `React.forwardRef`, but also allows using the ref inside the forwarding component.
  * Adapted from https://itnext.io/reusing-the-ref-from-forwardref-with-react-hooks-4ce9df693dd */
-export function forwardAndUseRef<T, P extends {children? : React.ReactNode} = {}>(render: (props: React.PropsWithChildren<P>, ref: React.RefObject<T>, setRef: (_: T | null) => void)
+export function forwardAndUseRef<T, P>(render: (props: P, ref: React.RefObject<T>, setRef: (_: T | null) => void)
     => React.ReactElement | null): React.ForwardRefExoticComponent<React.PropsWithoutRef<P> & React.RefAttributes<T>> {
   return React.forwardRef<T, P>((props, ref) => {
     const thisRef = React.useRef<T | null>(null)
@@ -206,7 +206,7 @@ export function forwardAndUseRef<T, P extends {children? : React.ReactNode} = {}
   })
 }
 
-export interface LogicalDomTraverser {
+export interface LogicalDomElement {
   contains(el: Node): boolean
 }
 
@@ -220,16 +220,17 @@ export const LogicalDomContext = React.createContext<LogicalDomStorage>({registe
 /** Suppose a component B appears as a React child of the component A. For layout reasons,
  * we sometimes don't want B to appear as an actual child of A in the DOM. We may still however
  * want to carry out `contains` checks as if B were there, i.e. according to the React tree
- * structure rather than the DOM structure. Logical DOM nodes make this work. Note this is not
- * shadow DOM, although it is similar.
+ * structure rather than the DOM structure. While React already correctly propagates DOM events
+ * up this logical tree, other functionality such as `contains` is not provided.
  *
- * For the method to work, each component introducing a *logical* (React-but-not-DOM) child must
- * register it in the `LogicalDomContext`.
+ * This method creates a {@link LogicalDomElement} corresponding to the given {@link HTMLElement}
+ * which provides the missing functionality for that element. For this to work, the element
+ * must be wrapped in a {@link LogicalDomContext} set to the {@link LogicalDomStorage} returned
+ * from this call.
  *
- * To carry out checks, call `useLogicalDom` with a ref to the node for which you want to carry
- * out `contains` checks and wrap that node in a `LogicalDomContext` using the resulting
- * `LogicalDomStorage`. */
-export function useLogicalDom(ref: React.RefObject<HTMLElement>): [LogicalDomTraverser, LogicalDomStorage] {
+ * Additionally, any component which actually introduces React-but-not-DOM children must
+ * call `registerDescendant` in the {@link LogicalDomContext}. */
+export function useLogicalDom(ref: React.RefObject<HTMLElement>): [LogicalDomElement, LogicalDomStorage] {
   const parentCtx = React.useContext(LogicalDomContext)
   React.useEffect(() => {
     if (ref.current) {
@@ -257,11 +258,31 @@ export function useLogicalDom(ref: React.RefObject<HTMLElement>): [LogicalDomTra
   }
 
   return [
-    React.useMemo(() => ({contains}), [ref]),
-    React.useMemo(() => ({registerDescendant}), [parentCtx])
+    React.useMemo(() => ({ contains }), [ref]),
+    React.useMemo(() => ({ registerDescendant }), [parentCtx])
   ]
 }
 
+/**
+ * An effect which calls `onClickOutside` whenever an element not logically descending from `ld`
+ * (see {@link useLogicalDom}) is clicked. Note that `onClickOutside` is not called on clicks
+ * on the scrollbar since these should usually not impact the app's state. */
+export function useOnClickOutside(ld: LogicalDomElement, onClickOutside: (_: PointerEvent) => void) {
+  React.useEffect(() => {
+    const onClickAnywhere = (e: PointerEvent) => {
+      if (e.target instanceof Node && !ld.contains(e.target)) {
+        if (e.target instanceof Element && e.target.tagName === 'HTML') {
+          // then user might be clicking in a scrollbar, otherwise
+          // e.target would be a tag other than 'HTML'
+        } else onClickOutside(e)
+      }
+    }
+
+    document.addEventListener('pointerdown', onClickAnywhere)
+    return () => document.removeEventListener('pointerdown', onClickAnywhere)
+  }, [ld, onClickOutside])
+}
+
 /** Sends an exception object to a throwable error.
  * Maps JSON Rpc errors to throwable errors.
  */

From 4fe0946054e43f0c9e56d98f6c9a6f7ae3c4107f Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Sun, 18 Dec 2022 02:14:33 -0500
Subject: [PATCH 05/13] fix: selection fixes

---
 lean4-infoview/src/infoview/exprContext.tsx   |  4 +--
 lean4-infoview/src/infoview/info.tsx          |  1 +
 .../src/infoview/interactiveCode.tsx          | 30 +++++++++++--------
 3 files changed, 21 insertions(+), 14 deletions(-)

diff --git a/lean4-infoview/src/infoview/exprContext.tsx b/lean4-infoview/src/infoview/exprContext.tsx
index 893e6d5de..3ac5c4994 100644
--- a/lean4-infoview/src/infoview/exprContext.tsx
+++ b/lean4-infoview/src/infoview/exprContext.tsx
@@ -57,8 +57,8 @@ export namespace GoalsLocation {
 
 /**
  * An interface available through a React context in components where selecting subexpressions
- * makes sense. Currently this is only the goal state display in which {@link GoalLocation}s
- * can be selected. */
+ * makes sense. Currently this is only the goal state display. There, {@link GoalLocation}s can be
+ * selected. */
 export interface Locations {
   isSelected: (l: GoalsLocation) => void
   setSelected: (l: GoalsLocation, on: boolean) => void
diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx
index b5dd314c0..403a349f3 100644
--- a/lean4-infoview/src/infoview/info.tsx
+++ b/lean4-infoview/src/infoview/info.tsx
@@ -91,6 +91,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
     const nothingToShow = !hasError && !goals && !termGoal && !hasMessages && !hasWidget;
 
     const [selectedLocs, setSelectedLocs] = React.useState<GoalsLocation[]>([])
+    React.useEffect(() => setSelectedLocs([]), [pos.uri, pos.line, pos.character])
 
     /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */
     return <>
diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx
index 24adba67f..395666d9b 100644
--- a/lean4-infoview/src/infoview/interactiveCode.tsx
+++ b/lean4-infoview/src/infoview/interactiveCode.tsx
@@ -80,18 +80,24 @@ function TypePopupContents({ info, redrawTooltip }: TypePopupContentsProps) {
   React.useEffect(() => { void redrawTooltip() },
     [interactive.state, (interactive as any)?.value, (interactive as any)?.error, redrawTooltip])
 
-  return <div className="tooltip-code-content">
-    {interactive.state === 'resolved' ? <>
-      <div className="font-code tl pre-wrap">
-      {interactive.value.exprExplicit && <InteractiveCode fmt={interactive.value.exprExplicit} />} : {
-        interactive.value.type && <InteractiveCode fmt={interactive.value.type} />}
-      </div>
-      {interactive.value.doc && <><hr /><Markdown contents={interactive.value.doc}/></>}
-      {info.diffStatus && <><hr/><div>{DIFF_TAG_TO_EXPLANATION[info.diffStatus]}</div></>}
-    </> :
-    interactive.state === 'rejected' ? <>Error: {mapRpcError(interactive.error).message}</> :
-    <>Loading..</>}
-  </div>
+  // Even when subexpressions are selectable in our parent component, it doesn't make sense
+  // to select things inside the *type* of the parent, so we clear the context.
+  // NOTE: selecting in the explicit term does make sense but it complicates the implementation
+  // so let's not add it until someone really wants it.
+  return <LocationsContext.Provider value={undefined}>
+    <div className="tooltip-code-content">
+      {interactive.state === 'resolved' ? <>
+        <div className="font-code tl pre-wrap">
+        {interactive.value.exprExplicit && <InteractiveCode fmt={interactive.value.exprExplicit} />} : {
+          interactive.value.type && <InteractiveCode fmt={interactive.value.type} />}
+        </div>
+        {interactive.value.doc && <><hr /><Markdown contents={interactive.value.doc}/></>}
+        {info.diffStatus && <><hr/><div>{DIFF_TAG_TO_EXPLANATION[info.diffStatus]}</div></>}
+      </> :
+      interactive.state === 'rejected' ? <>Error: {mapRpcError(interactive.error).message}</> :
+      <>Loading..</>}
+    </div>
+  </LocationsContext.Provider>
 }
 
 const DIFF_TAG_TO_CLASS : {[K in DiffTag] : string} = {

From 35bf7a82b871a2c4f6fc6c99c626d1a7d58c4a27 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Sun, 18 Dec 2022 03:14:21 -0500
Subject: [PATCH 06/13] feat: match new goal types

---
 lean4-infoview-api/src/rpcApi.ts           | 42 +++++++++++++---------
 lean4-infoview/src/infoview/errors.tsx     |  5 +--
 lean4-infoview/src/infoview/info.tsx       |  9 ++---
 lean4-infoview/src/infoview/userWidget.tsx | 12 +++++--
 4 files changed, 42 insertions(+), 26 deletions(-)

diff --git a/lean4-infoview-api/src/rpcApi.ts b/lean4-infoview-api/src/rpcApi.ts
index 9d4e1681a..61f602a26 100644
--- a/lean4-infoview-api/src/rpcApi.ts
+++ b/lean4-infoview-api/src/rpcApi.ts
@@ -45,35 +45,43 @@ export type FVarId = string
 export type MVarId = string
 
 export interface InteractiveHypothesisBundle {
-    isInstance?: boolean,
-    isType?: boolean,
     /** The pretty names of the variables in the bundle. Anonymous names are rendered
      * as `"[anonymous]"` whereas inaccessible ones have a `✝` appended at the end.
-     * Use `InteractiveHypothesisBundle_nonAnonymousNames` to filter these out. */
+     * Use `InteractiveHypothesisBundle_nonAnonymousNames` to filter anonymouse ones out. */
     names: string[]
-    /** The free variable id associated with each of the vars listed in `names`. */
+    /** Present since server version 1.1.2. */
     fvarIds?: FVarId[]
     type: CodeWithInfos
     val?: CodeWithInfos
-    /** If true, the hypothesis was not present on the previous tactic state. */
-    isInserted?: boolean;
-    /** If true, the hypothesis will be deleted on the next tactic state. */
-    isRemoved?: boolean;
+    isInstance?: boolean
+    isType?: boolean
+    isInserted?: boolean
+    isRemoved?: boolean
 }
 
-export interface InteractiveGoal {
+export type ContextInfo = RpcPtr<'Lean.Elab.ContextInfo'>
+export type TermInfo = RpcPtr<'Lean.Elab.TermInfo'>
+
+export interface InteractiveGoalCore {
     hyps: InteractiveHypothesisBundle[]
     type: CodeWithInfos
+    /** Present since server version 1.1.2. */
+    ctx?: ContextInfo
+}
+
+export interface InteractiveGoal extends InteractiveGoalCore {
     userName?: string
     goalPrefix?: string
-    /** metavariable id associated with the goal.
-     * This is undefined when the goal is a term goal
-     * or if we are using an older version of lean. */
+    /** Present since server version 1.1.2. */
     mvarId?: MVarId
-    /** If true, the goal was not present on the previous tactic state. */
-    isInserted?: boolean;
-    /** If true, the goal will be deleted on the next tactic state. */
-    isRemoved?: boolean;
+    isInserted?: boolean
+    isRemoved?: boolean
+}
+
+export interface InteractiveTermGoal extends InteractiveGoalCore {
+    range?: Range
+    /** Present since server version 1.1.2. */
+    term?: TermInfo
 }
 
 export interface InteractiveGoals {
@@ -84,7 +92,7 @@ export function getInteractiveGoals(rs: RpcSessionAtPos, pos: TextDocumentPositi
     return rs.call('Lean.Widget.getInteractiveGoals', pos);
 }
 
-export function getInteractiveTermGoal(rs: RpcSessionAtPos, pos: TextDocumentPositionParams): Promise<InteractiveGoal | undefined> {
+export function getInteractiveTermGoal(rs: RpcSessionAtPos, pos: TextDocumentPositionParams): Promise<InteractiveTermGoal | undefined> {
     return rs.call('Lean.Widget.getInteractiveTermGoal', pos);
 }
 
diff --git a/lean4-infoview/src/infoview/errors.tsx b/lean4-infoview/src/infoview/errors.tsx
index a1a82ee0b..6db4b7ff7 100644
--- a/lean4-infoview/src/infoview/errors.tsx
+++ b/lean4-infoview/src/infoview/errors.tsx
@@ -22,8 +22,9 @@ export class ErrorBoundary extends React.Component<{children?: React.ReactNode},
     if (this.state.error) {
       // You can render any custom fallback UI
       return <div>
-          <h1>Error:</h1>{this.state.error}<br/>
-          <a onClick={() => this.setState({ error: undefined })}>Click to reload.</a>
+          <h1>Error:</h1>{this.state.error}<br/><br/>
+          <a className='pointer dim '
+            onClick={() => this.setState({ error: undefined })}>Click to reload.</a>
         </div>;
     }
 
diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx
index 403a349f3..0ba16adb5 100644
--- a/lean4-infoview/src/infoview/info.tsx
+++ b/lean4-infoview/src/infoview/info.tsx
@@ -8,7 +8,7 @@ import { ConfigContext, EditorContext, LspDiagnosticsContext, ProgressContext }
 import { lspDiagToInteractive, MessagesList } from './messages';
 import { getInteractiveGoals, getInteractiveTermGoal, InteractiveDiagnostic, InteractiveGoal,
     InteractiveGoals, UserWidgetInstance, Widget_getWidgets, RpcSessionAtPos, isRpcError,
-    RpcErrorCode, getInteractiveDiagnostics } from '@leanprover/infoview-api';
+    RpcErrorCode, getInteractiveDiagnostics, InteractiveTermGoal } from '@leanprover/infoview-api';
 import { UserWidgetDisplay } from './userWidget'
 import { RpcContext, useRpcSessionAtPos } from './rpcSessions';
 import { GoalsLocation, LocationsContext } from './exprContext';
@@ -75,7 +75,7 @@ interface InfoDisplayContentProps extends PausableProps {
     pos: DocumentPosition;
     messages: InteractiveDiagnostic[];
     goals?: InteractiveGoals;
-    termGoal?: InteractiveGoal;
+    termGoal?: InteractiveTermGoal;
     error?: string;
     userWidgets: UserWidgetInstance[];
     triggerUpdate: () => Promise<void>;
@@ -116,7 +116,8 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
         {userWidgets.map(widget =>
             <details key={`widget::${widget.id}::${widget.range?.toString()}`} open>
                 <summary className='mv2 pointer'>{widget.name}</summary>
-                <UserWidgetDisplay pos={pos} selectedLocations={selectedLocs} widget={widget}/>
+                <UserWidgetDisplay pos={pos} goals={goals ? goals.goals : []} termGoal={termGoal}
+                    selectedLocations={selectedLocs} widget={widget}/>
             </details>
         )}
         <div style={{display: hasMessages ? 'block' : 'none'}} key="messages">
@@ -144,7 +145,7 @@ interface InfoDisplayProps {
     status: InfoStatus;
     messages: InteractiveDiagnostic[];
     goals?: InteractiveGoals;
-    termGoal?: InteractiveGoal;
+    termGoal?: InteractiveTermGoal;
     error?: string;
     userWidgets: UserWidgetInstance[];
     rpcSess: RpcSessionAtPos;
diff --git a/lean4-infoview/src/infoview/userWidget.tsx b/lean4-infoview/src/infoview/userWidget.tsx
index 95fd721b9..56e5a0afb 100644
--- a/lean4-infoview/src/infoview/userWidget.tsx
+++ b/lean4-infoview/src/infoview/userWidget.tsx
@@ -1,6 +1,6 @@
 import * as React from 'react';
 
-import { Widget_getWidgetSource, UserWidgetInstance } from '@leanprover/infoview-api';
+import { Widget_getWidgetSource, UserWidgetInstance, InteractiveGoal, InteractiveTermGoal } from '@leanprover/infoview-api';
 import { RpcContext } from './rpcSessions';
 import { DocumentPosition, mapRpcError, useAsync } from './util';
 import { ErrorBoundary } from './errors';
@@ -18,6 +18,8 @@ const componentCache = new Map<string, React.LazyExoticComponent<React.Component
 
 interface UserWidgetDisplayProps {
     pos: DocumentPosition
+    goals: InteractiveGoal[]
+    termGoal?: InteractiveTermGoal
     selectedLocations: GoalsLocation[]
     widget: UserWidgetInstance
 }
@@ -26,11 +28,15 @@ interface UserWidgetDisplayProps {
 export interface UserWidgetProps {
     /** Cursor position in the file at which the widget is being displayed. */
     pos: DocumentPosition
+    /** The current tactic-mode goals. */
+    goals: InteractiveGoal[]
+    /** The current term-mode goal, if any. */
+    termGoal?: InteractiveTermGoal
     /** Locations currently selected in the goal state. */
     selectedLocations: GoalsLocation[]
 }
 
-export function UserWidgetDisplay({ pos, selectedLocations, widget }: UserWidgetDisplayProps) {
+export function UserWidgetDisplay({ pos, goals, termGoal, selectedLocations, widget }: UserWidgetDisplayProps) {
     const rs = React.useContext(RpcContext);
     const hash = widget.javascriptHash
     const component = useAsync(
@@ -46,7 +52,7 @@ export function UserWidgetDisplay({ pos, selectedLocations, widget }: UserWidget
         },
         [hash])
 
-    const componentProps: UserWidgetProps = { pos, selectedLocations, ...widget.props }
+    const componentProps: UserWidgetProps = { pos, goals, termGoal, selectedLocations, ...widget.props }
 
     return (
         <React.Suspense fallback={`Loading widget: ${widget.id} ${component.state}.`}>

From 049843ae2b7b469b8aba77e5c5fd32df0446c34c Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Sun, 18 Dec 2022 17:38:01 -0500
Subject: [PATCH 07/13] feat: make names selectable

---
 lean4-infoview/src/infoview/exprContext.tsx   | 74 +++++++++++++------
 lean4-infoview/src/infoview/goals.tsx         |  1 +
 .../src/infoview/interactiveCode.tsx          | 35 +++------
 lean4-infoview/src/infoview/tooltips.tsx      | 13 +++-
 4 files changed, 71 insertions(+), 52 deletions(-)

diff --git a/lean4-infoview/src/infoview/exprContext.tsx b/lean4-infoview/src/infoview/exprContext.tsx
index 3ac5c4994..6a429d80e 100644
--- a/lean4-infoview/src/infoview/exprContext.tsx
+++ b/lean4-infoview/src/infoview/exprContext.tsx
@@ -5,6 +5,7 @@ Authors: E.W.Ayers, Wojciech Nawrocki
 */
 import { FVarId, MVarId, SubexprPos } from "@leanprover/infoview-api";
 import * as React from 'react';
+import { DetectHoverSpan, HoverState } from "./tooltips";
 
 /**
  * A location within a goal. It is either:
@@ -72,34 +73,59 @@ export interface Locations {
 export const LocationsContext = React.createContext<Locations | undefined>(undefined)
 
 type SelectableLocationProps =
-    React.PropsWithoutRef<React.DetailedHTMLProps<React.HTMLAttributes<HTMLSpanElement>, HTMLSpanElement>> &
-    { locs: Locations, loc: GoalsLocation }
+  React.PropsWithoutRef<React.DetailedHTMLProps<React.HTMLAttributes<HTMLSpanElement>, HTMLSpanElement>> &
+  { locs?: Locations, loc?: GoalsLocation, alwaysHighlight: boolean,
+    setHoverState?: React.Dispatch<React.SetStateAction<HoverState>> }
 
+/**
+ * A `<span>` with a corresponding {@link GoalsLocation} which can be (un)selected using shift-click.
+ * If `locs` or `loc` is `undefined`, selection functionality is turned off. The element is also
+ * highlighted when hovered over if `alwaysHighlight` is `true` or `locs` and `loc` are both defined.
+ * `setHoverState` is passed through to {@link DetectHoverSpan}. */
 export function SelectableLocation(props: SelectableLocationProps): JSX.Element {
-    const [isSelected, setSelected] = React.useState<boolean>(false)
+  const {locs, loc, alwaysHighlight, setHoverState: setParentHoverState} = props
+
+  const shouldHighlight: boolean = alwaysHighlight || (!!locs && !!loc)
+  const [hoverState, setHoverState] = React.useState<HoverState>('off')
+  let spanClassName: string = ''
+  if (shouldHighlight) {
+    spanClassName += 'highlightable '
+    if (hoverState != 'off') spanClassName += 'highlight '
+    if (props.className) spanClassName += props.className
+  }
 
-    const spanClassName: string = 'highlightable '
-        + (isSelected ? 'highlight-selected ' : '')
-        + (props.className ? props.className : '')
+  const [isSelected, setSelected] = React.useState<boolean>(false)
+  const innerSpanClassName: string = 'highlightable '
+    + (isSelected ? 'highlight-selected ' : '')
 
-    return <span {...props}
-        className={spanClassName}
-        onClick={e => {
-            if (e.shiftKey) {
-              setSelected(on => {
-                props.locs.setSelected(props.loc, !on)
-                return !on
-              })
-              e.stopPropagation()
-            }
-            if (props.onClick) props.onClick(e)
-        }}
-        onPointerDown={e => {
-          // Since shift-click on this component is a custom selection, when shift is held prevent
-          // the default action which on text is to start a text selection.
-          if (e.shiftKey) e.preventDefault()
-        }}
-      >
+  return <DetectHoverSpan {...props}
+      setHoverState={st => {
+        setHoverState(st)
+        if (setParentHoverState) setParentHoverState(st)
+      }}
+      className={spanClassName}
+      onClick={e => {
+          // On shift-click, if we are in a context where selecting subexpressions makes sense,
+          // (un)select the current subexpression.
+          if (e.shiftKey && locs && loc) {
+            setSelected(on => {
+              locs.setSelected(loc, !on)
+              return !on
+            })
+            e.stopPropagation()
+          }
+          if (props.onClick) props.onClick(e)
+      }}
+      onPointerDown={e => {
+        // Since shift-click on this component is a custom selection, when shift is held prevent
+        // the default action which on text is to start a text selection.
+        if (e.shiftKey) e.preventDefault()
+        if (props.onPointerDown) props.onPointerDown(e)
+      }}
+    >
+      {/* Note: we use two spans so that the two `highlight`s don't interfere. */}
+      <span className={innerSpanClassName}>
         {props.children}
       </span>
+    </DetectHoverSpan>
 }
diff --git a/lean4-infoview/src/infoview/goals.tsx b/lean4-infoview/src/infoview/goals.tsx
index 518e738eb..4f949c00f 100644
--- a/lean4-infoview/src/infoview/goals.tsx
+++ b/lean4-infoview/src/infoview/goals.tsx
@@ -78,6 +78,7 @@ function Hyp({ hyp: h, mvarId }: HypProps) {
                 <SelectableLocation
                     locs={locs}
                     loc={{ mvarId, loc: { hyp: h.fvarIds![i] }}}
+                    alwaysHighlight={false}
                 >
                     {n}
                 </SelectableLocation> :
diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx
index 395666d9b..cd7233be2 100644
--- a/lean4-infoview/src/infoview/interactiveCode.tsx
+++ b/lean4-infoview/src/infoview/interactiveCode.tsx
@@ -3,11 +3,11 @@ import * as React from 'react'
 import { EditorContext } from './contexts'
 import { useAsync, mapRpcError } from './util'
 import { SubexprInfo, CodeWithInfos, InteractiveDiagnostics_infoToInteractive, getGoToLocation, TaggedText, DiffTag } from '@leanprover/infoview-api'
-import { DetectHoverSpan, HoverState, WithTooltipOnHover } from './tooltips'
+import { HoverState, WithTooltipOnHover } from './tooltips'
 import { Location } from 'vscode-languageserver-protocol'
 import { marked } from 'marked'
 import { RpcContext } from './rpcSessions'
-import { GoalsLocation, LocationsContext } from './exprContext'
+import { GoalsLocation, LocationsContext, SelectableLocation } from './exprContext'
 
 export interface InteractiveTextComponentProps<T> {
   fmt: TaggedText<T>
@@ -156,13 +156,8 @@ function InteractiveCodeTag({tag: ct, fmt}: InteractiveTagProps<SubexprInfo>) {
   const ourLoc = locs && locs.subexprTemplate && ct.subexprPos ?
     GoalsLocation.withSubexprPos(locs.subexprTemplate, ct.subexprPos) :
     undefined
-  const [isSelected, setSelected] = React.useState<boolean>(false)
-  const innerSpanClassName: string = 'highlightable ' +
-    (isSelected ? 'highlight-selected ' : '')
 
-  let spanClassName: string = 'highlightable '
-    + (hoverState != 'off' ? 'highlight ' : '')
-    + (hoverState === 'ctrlOver' && goToLoc !== undefined ? 'underline ' : '')
+  let spanClassName: string = hoverState === 'ctrlOver' && goToLoc !== undefined ? 'underline ' : ''
   if (ct.diffStatus) {
     spanClassName += DIFF_TAG_TO_CLASS[ct.diffStatus] + ' '
   }
@@ -178,28 +173,18 @@ function InteractiveCodeTag({tag: ct, fmt}: InteractiveTagProps<SubexprInfo>) {
             if (loc === undefined) return
             void ec.revealPosition({ uri: loc.uri, ...loc.range.start })
           })
-        // On shift-click, if we are in a context where selecting subexpressions makes sense,
-        // (un)select the current subexpression.
-        } else if (e.shiftKey) {
-          if (ourLoc) {
-            setSelected(on => {
-              locs!.setSelected(ourLoc, !on)
-              return !on
-            })
-          }
-        } else next(e)
+        } else if (!e.shiftKey) next(e)
       }}
     >
-      <DetectHoverSpan
+      <SelectableLocation
         setHoverState={setHoverState}
         className={spanClassName}
+        locs={locs}
+        loc={ourLoc}
+        alwaysHighlight={true}
       >
-        {/* Note: we use two spans so that if the outer one already has a background-color,
-        the inner color still shows (with transparency). */}
-        <span className={innerSpanClassName}>
-          <InteractiveCode fmt={fmt} />
-        </span>
-      </DetectHoverSpan>
+        <InteractiveCode fmt={fmt} />
+      </SelectableLocation>
     </WithTooltipOnHover>
   )
 }
diff --git a/lean4-infoview/src/infoview/tooltips.tsx b/lean4-infoview/src/infoview/tooltips.tsx
index d72bf49c1..a54fa6d5e 100644
--- a/lean4-infoview/src/infoview/tooltips.tsx
+++ b/lean4-infoview/src/infoview/tooltips.tsx
@@ -87,7 +87,7 @@ export const DetectHoverSpan =
     {setHoverState: React.Dispatch<React.SetStateAction<HoverState>>}>((props_, ref, setRef) => {
   const {setHoverState, ...props} = props_;
 
-  const onPointerEvent = (b: boolean) => (e: React.PointerEvent<HTMLSpanElement>) => {
+  const onPointerEvent = (b: boolean, e: React.PointerEvent<HTMLSpanElement>) => {
     // It's more composable to let pointer events bubble up rather than to call `stopPropagation`,
     // but we only want to handle hovers in the innermost component. So we record that the
     // event was handled with a property.
@@ -125,13 +125,20 @@ export const DetectHoverSpan =
   return <span
       {...props}
       ref={setRef}
-      onPointerOver={onPointerEvent(true)}
-      onPointerOut={onPointerEvent(false)}
+      onPointerOver={e => {
+        onPointerEvent(true, e)
+        if (props.onPointerOver) props.onPointerOver(e)
+      }}
+      onPointerOut={e => {
+        onPointerEvent(false, e)
+        if (props.onPointerOut) props.onPointerOut(e)
+      }}
       onPointerMove={e => {
         if (e.ctrlKey || e.metaKey)
           setHoverState(st => st === 'over' ? 'ctrlOver' : st)
         else
           setHoverState(st => st === 'ctrlOver' ? 'over' : st)
+        if (props.onPointerMove) props.onPointerMove(e)
       }}
     >
       {props.children}

From 4ca3d7f6b1157d9e6f38700a2931772191e4f8df Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Sun, 18 Dec 2022 18:40:01 -0500
Subject: [PATCH 08/13] chore: lint

---
 lean4-infoview/src/infoview/exprContext.tsx |  8 +++--
 lean4-infoview/src/infoview/goals.tsx       | 28 ++++++++---------
 lean4-infoview/src/infoview/info.tsx        | 34 ++++++++++-----------
 3 files changed, 35 insertions(+), 35 deletions(-)

diff --git a/lean4-infoview/src/infoview/exprContext.tsx b/lean4-infoview/src/infoview/exprContext.tsx
index 6a429d80e..50c4136a5 100644
--- a/lean4-infoview/src/infoview/exprContext.tsx
+++ b/lean4-infoview/src/infoview/exprContext.tsx
@@ -3,9 +3,9 @@ Copyright (c) 2022 E.W.Ayers. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
 Authors: E.W.Ayers, Wojciech Nawrocki
 */
-import { FVarId, MVarId, SubexprPos } from "@leanprover/infoview-api";
+import { FVarId, MVarId, SubexprPos } from '@leanprover/infoview-api';
 import * as React from 'react';
-import { DetectHoverSpan, HoverState } from "./tooltips";
+import { DetectHoverSpan, HoverState } from './tooltips';
 
 /**
  * A location within a goal. It is either:
@@ -19,6 +19,7 @@ export type GoalLocation =
   | { hypValue: [FVarId, SubexprPos] }
   | { target: SubexprPos }
 
+// eslint-disable-next-line @typescript-eslint/no-namespace
 export namespace GoalLocation {
   export function isEqual(l1: GoalLocation, l2: GoalLocation): boolean {
     if ('hyp' in l1) return 'hyp' in l2 ? l1.hyp === l2.hyp : false
@@ -46,6 +47,7 @@ export interface GoalsLocation {
     loc: GoalLocation;
 }
 
+// eslint-disable-next-line @typescript-eslint/no-namespace
 export namespace GoalsLocation {
   export function isEqual(l1: GoalsLocation, l2: GoalsLocation): boolean {
     return l1.mvarId === l2.mvarId && GoalLocation.isEqual(l1.loc, l2.loc)
@@ -90,7 +92,7 @@ export function SelectableLocation(props: SelectableLocationProps): JSX.Element
   let spanClassName: string = ''
   if (shouldHighlight) {
     spanClassName += 'highlightable '
-    if (hoverState != 'off') spanClassName += 'highlight '
+    if (hoverState !== 'off') spanClassName += 'highlight '
     if (props.className) spanClassName += props.className
   }
 
diff --git a/lean4-infoview/src/infoview/goals.tsx b/lean4-infoview/src/infoview/goals.tsx
index 4f949c00f..663f79874 100644
--- a/lean4-infoview/src/infoview/goals.tsx
+++ b/lean4-infoview/src/infoview/goals.tsx
@@ -66,7 +66,6 @@ interface HypProps {
 
 function Hyp({ hyp: h, mvarId }: HypProps) {
     const locs = React.useContext(LocationsContext)
-    const hasLoc = locs && mvarId && h.fvarIds && h.fvarIds.length > 0
 
     const namecls: string = 'mr1 ' +
         (h.isInserted ? 'inserted-text ' : '') +
@@ -74,29 +73,28 @@ function Hyp({ hyp: h, mvarId }: HypProps) {
 
     const names = InteractiveHypothesisBundle_nonAnonymousNames(h).map((n, i) =>
         <span className={namecls + (isInaccessibleName(n) ? 'goal-inaccessible ' : '')} key={i}>
-            {hasLoc ?
-                <SelectableLocation
-                    locs={locs}
-                    loc={{ mvarId, loc: { hyp: h.fvarIds![i] }}}
-                    alwaysHighlight={false}
-                >
-                    {n}
-                </SelectableLocation> :
-                n}
+            <SelectableLocation
+                locs={locs}
+                loc={mvarId && h.fvarIds && h.fvarIds.length > i ?
+                    { mvarId, loc: { hyp: h.fvarIds[i] }} :
+                    undefined
+                }
+                alwaysHighlight={false}
+            >{n}</SelectableLocation>
         </span>)
 
     return <div>
         <strong className="goal-hyp">{names}</strong>
         :&nbsp;
-        <LocationsContext.Provider value={hasLoc ?
-            { ...locs, subexprTemplate: { mvarId, loc: { hypType: [h.fvarIds![0], ''] }}} :
+        <LocationsContext.Provider value={locs && mvarId && h.fvarIds && h.fvarIds.length > 0 ?
+            { ...locs, subexprTemplate: { mvarId, loc: { hypType: [h.fvarIds[0], ''] }}} :
             undefined
         }>
             <InteractiveCode fmt={h.type} />
         </LocationsContext.Provider>
         {h.val &&
-            <LocationsContext.Provider value={hasLoc ?
-                { ...locs, subexprTemplate: { mvarId, loc: { hypValue: [h.fvarIds![0], ''] }}} :
+            <LocationsContext.Provider value={locs && mvarId && h.fvarIds && h.fvarIds.length > 0 ?
+                { ...locs, subexprTemplate: { mvarId, loc: { hypValue: [h.fvarIds[0], ''] }}} :
                 undefined
             }>
                 &nbsp;:=&nbsp;<InteractiveCode fmt={h.val} />
@@ -185,7 +183,7 @@ export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoal
             data-id="copy-goal-to-comment"
             onClick={e => {
                 e.preventDefault();
-                if (goals) ec.copyToComment(goalsToString(goals))
+                if (goals) void ec.copyToComment(goalsToString(goals))
             }}
             title="copy state to comment" />
 
diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx
index 0ba16adb5..de0d6bcb9 100644
--- a/lean4-infoview/src/infoview/info.tsx
+++ b/lean4-infoview/src/infoview/info.tsx
@@ -48,24 +48,24 @@ const InfoStatusBar = React.memo((props: InfoStatusBarProps) => {
         {isPinned && !isPaused && ' (pinned)'}
         {!isPinned && isPaused && ' (paused)'}
         {isPinned && isPaused && ' (pinned and paused)'}
-        <span className="fr">
+        <span className='fr'>
             {isPinned &&
-                <a className="link pointer mh2 dim codicon codicon-go-to-file"
-                   data-id="reveal-file-location"
+                <a className='link pointer mh2 dim codicon codicon-go-to-file'
+                   data-id='reveal-file-location'
                    onClick={e => { e.preventDefault(); void ec.revealPosition(pos); }}
-                   title="reveal file location" />}
+                   title='reveal file location' />}
             <a className={'link pointer mh2 dim codicon ' + (isPinned ? 'codicon-pinned ' : 'codicon-pin ')}
-                data-id="toggle-pinned"
+                data-id='toggle-pinned'
                 onClick={e => { e.preventDefault(); onPin(pos); }}
                 title={isPinned ? 'unpin' : 'pin'} />
             <a className={'link pointer mh2 dim codicon ' + (isPaused ? 'codicon-debug-continue ' : 'codicon-debug-pause ')}
-               data-id="toggle-paused"
+               data-id='toggle-paused'
                onClick={e => { e.preventDefault(); setPaused(!isPaused); }}
                title={isPaused ? 'continue updating' : 'pause updating'} />
-            <a className="link pointer mh2 dim codicon codicon-refresh"
-               data-id="update"
+            <a className='link pointer mh2 dim codicon codicon-refresh'
+               data-id='update'
                onClick={e => { e.preventDefault(); void triggerUpdate(); }}
-               title="update"/>
+               title='update'/>
         </span>
     </summary>
     );
@@ -96,9 +96,9 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
     /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */
     return <>
         {hasError &&
-            <div className="error" key="errors">
+            <div className='error' key='errors'>
                 Error updating:{' '}{error}.
-                <a className="link pointer dim" onClick={e => { e.preventDefault(); void triggerUpdate(); }}>{' '}Try again.</a>
+                <a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate(); }}>{' '}Try again.</a>
             </div>}
 
         <LocationsContext.Provider value ={{
@@ -109,9 +109,9 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
             },
             subexprTemplate: undefined
         }}>
-            <FilteredGoals headerChildren={"Tactic state"} key="goals" goals={goals} />
+            <FilteredGoals headerChildren='Tactic state' key='goals' goals={goals} />
         </LocationsContext.Provider>
-        <FilteredGoals headerChildren={"Expected type"} key="term-goal"
+        <FilteredGoals headerChildren='Expected type' key='term-goal'
             goals={termGoal !== undefined ? {goals: [termGoal]} : undefined} />
         {userWidgets.map(widget =>
             <details key={`widget::${widget.id}::${widget.range?.toString()}`} open>
@@ -120,8 +120,8 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
                     selectedLocations={selectedLocs} widget={widget}/>
             </details>
         )}
-        <div style={{display: hasMessages ? 'block' : 'none'}} key="messages">
-            <details key="messages" open>
+        <div style={{display: hasMessages ? 'block' : 'none'}} key='messages'>
+            <details key='messages' open>
                 <summary className='mv2 pointer'>Messages ({messages.length})</summary>
                 <div className='ml1'>
                     <MessagesList uri={pos.uri} messages={messages} />
@@ -132,8 +132,8 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
             isPaused ?
                 /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */
                 <span>Updating is paused.{' '}
-                    <a className="link pointer dim" onClick={e => { e.preventDefault(); void triggerUpdate(); }}>Refresh</a>
-                    {' '}or <a className="link pointer dim" onClick={e => { e.preventDefault(); setPaused(false); }}>resume updating</a>
+                    <a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate(); }}>Refresh</a>
+                    {' '}or <a className='link pointer dim' onClick={e => { e.preventDefault(); setPaused(false); }}>resume updating</a>
                     {' '}to see information.
                 </span> :
                 'No info found.')}

From c43cb36d588ae387679a0dd080ce0a36d2fefb26 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Mon, 19 Dec 2022 01:14:43 -0500
Subject: [PATCH 09/13] feat: fix many bugs and memoize

---
 lean4-infoview/src/index.tsx                  |  1 +
 lean4-infoview/src/infoview/errors.tsx        |  2 +-
 .../{exprContext.tsx => goalLocation.tsx}     | 12 ++----
 lean4-infoview/src/infoview/goals.tsx         | 37 ++++++++++++-------
 lean4-infoview/src/infoview/info.tsx          | 26 ++++++++-----
 .../src/infoview/interactiveCode.tsx          |  2 +-
 lean4-infoview/src/infoview/userWidget.tsx    |  2 +-
 7 files changed, 47 insertions(+), 35 deletions(-)
 rename lean4-infoview/src/infoview/{exprContext.tsx => goalLocation.tsx} (94%)

diff --git a/lean4-infoview/src/index.tsx b/lean4-infoview/src/index.tsx
index 07f1a4f7a..08b3b7c3f 100644
--- a/lean4-infoview/src/index.tsx
+++ b/lean4-infoview/src/index.tsx
@@ -11,6 +11,7 @@ export { EditorContext, VersionContext } from './infoview/contexts';
 export { EditorConnection } from './infoview/editorConnection';
 export { RpcContext } from './infoview/rpcSessions';
 export { ServerVersion } from './infoview/serverVersion';
+export { GoalLocation, GoalsLocation } from './infoview/goalLocation';
 export { UserWidgetProps } from './infoview/userWidget';
 
 export { InteractiveCode, InteractiveCodeProps } from './infoview/interactiveCode';
diff --git a/lean4-infoview/src/infoview/errors.tsx b/lean4-infoview/src/infoview/errors.tsx
index 6db4b7ff7..ae02e3744 100644
--- a/lean4-infoview/src/infoview/errors.tsx
+++ b/lean4-infoview/src/infoview/errors.tsx
@@ -23,7 +23,7 @@ export class ErrorBoundary extends React.Component<{children?: React.ReactNode},
       // You can render any custom fallback UI
       return <div>
           <h1>Error:</h1>{this.state.error}<br/><br/>
-          <a className='pointer dim '
+          <a className='link pointer dim '
             onClick={() => this.setState({ error: undefined })}>Click to reload.</a>
         </div>;
     }
diff --git a/lean4-infoview/src/infoview/exprContext.tsx b/lean4-infoview/src/infoview/goalLocation.tsx
similarity index 94%
rename from lean4-infoview/src/infoview/exprContext.tsx
rename to lean4-infoview/src/infoview/goalLocation.tsx
index 50c4136a5..ddc37a662 100644
--- a/lean4-infoview/src/infoview/exprContext.tsx
+++ b/lean4-infoview/src/infoview/goalLocation.tsx
@@ -63,8 +63,8 @@ export namespace GoalsLocation {
  * makes sense. Currently this is only the goal state display. There, {@link GoalLocation}s can be
  * selected. */
 export interface Locations {
-  isSelected: (l: GoalsLocation) => void
-  setSelected: (l: GoalsLocation, on: boolean) => void
+  isSelected: (l: GoalsLocation) => boolean
+  setSelected: (l: GoalsLocation, fn: React.SetStateAction<boolean>) => void
   /**
    * A template for the location of the current component. It is defined if and only if the current
    * component is a subexpression of a selectable expression. We use
@@ -96,9 +96,8 @@ export function SelectableLocation(props: SelectableLocationProps): JSX.Element
     if (props.className) spanClassName += props.className
   }
 
-  const [isSelected, setSelected] = React.useState<boolean>(false)
   const innerSpanClassName: string = 'highlightable '
-    + (isSelected ? 'highlight-selected ' : '')
+    + (locs && loc && locs.isSelected(loc) ? 'highlight-selected ' : '')
 
   return <DetectHoverSpan {...props}
       setHoverState={st => {
@@ -110,10 +109,7 @@ export function SelectableLocation(props: SelectableLocationProps): JSX.Element
           // On shift-click, if we are in a context where selecting subexpressions makes sense,
           // (un)select the current subexpression.
           if (e.shiftKey && locs && loc) {
-            setSelected(on => {
-              locs.setSelected(loc, !on)
-              return !on
-            })
+            locs.setSelected(loc, on => !on)
             e.stopPropagation()
           }
           if (props.onClick) props.onClick(e)
diff --git a/lean4-infoview/src/infoview/goals.tsx b/lean4-infoview/src/infoview/goals.tsx
index 663f79874..cdfdaada2 100644
--- a/lean4-infoview/src/infoview/goals.tsx
+++ b/lean4-infoview/src/infoview/goals.tsx
@@ -3,7 +3,7 @@ import { InteractiveCode } from './interactiveCode'
 import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle, InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_stripTags } from '@leanprover/infoview-api'
 import { WithTooltipOnHover } from './tooltips';
 import { EditorContext } from './contexts';
-import { LocationsContext, SelectableLocation } from './exprContext';
+import { Locations, LocationsContext, SelectableLocation } from './goalLocation';
 
 /** Returns true if `h` is inaccessible according to Lean's default name rendering. */
 function isInaccessibleName(h: string): boolean {
@@ -83,20 +83,26 @@ function Hyp({ hyp: h, mvarId }: HypProps) {
             >{n}</SelectableLocation>
         </span>)
 
+    const typeLocs: Locations | undefined = React.useMemo(() =>
+        locs && mvarId && h.fvarIds && h.fvarIds.length > 0 ?
+            { ...locs, subexprTemplate: { mvarId, loc: { hypType: [h.fvarIds[0], ''] }}} :
+            undefined,
+        [locs, mvarId, h.fvarIds])
+
+    const valLocs: Locations | undefined = React.useMemo(() =>
+        h.val && locs && mvarId && h.fvarIds && h.fvarIds.length > 0 ?
+            { ...locs, subexprTemplate: { mvarId, loc: { hypValue: [h.fvarIds[0], ''] }}} :
+            undefined,
+        [h.val, locs, mvarId, h.fvarIds])
+
     return <div>
         <strong className="goal-hyp">{names}</strong>
         :&nbsp;
-        <LocationsContext.Provider value={locs && mvarId && h.fvarIds && h.fvarIds.length > 0 ?
-            { ...locs, subexprTemplate: { mvarId, loc: { hypType: [h.fvarIds[0], ''] }}} :
-            undefined
-        }>
+        <LocationsContext.Provider value={typeLocs}>
             <InteractiveCode fmt={h.type} />
         </LocationsContext.Provider>
         {h.val &&
-            <LocationsContext.Provider value={locs && mvarId && h.fvarIds && h.fvarIds.length > 0 ?
-                { ...locs, subexprTemplate: { mvarId, loc: { hypValue: [h.fvarIds[0], ''] }}} :
-                undefined
-            }>
+            <LocationsContext.Provider value={valLocs}>
                 &nbsp;:=&nbsp;<InteractiveCode fmt={h.val} />
             </LocationsContext.Provider>}
     </div>
@@ -112,20 +118,23 @@ interface GoalProps {
  * provided `filter`. */
 export const Goal = React.memo((props: GoalProps) => {
     const { goal, filter } = props
+
     const prefix = goal.goalPrefix ?? '⊢ '
     const filteredList = getFilteredHypotheses(goal.hyps, filter);
     const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList;
     const locs = React.useContext(LocationsContext)
+    const goalLocs = React.useMemo(() =>
+        locs && goal.mvarId ?
+            { ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} :
+            undefined,
+        [locs, goal.mvarId])
     const goalLi = <div key={'goal'}>
         <strong className="goal-vdash">{prefix}</strong>
-        <LocationsContext.Provider value={
-            locs && goal.mvarId ?
-                { ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} :
-                undefined
-        }>
+        <LocationsContext.Provider value={goalLocs}>
             <InteractiveCode fmt={goal.type} />
         </LocationsContext.Provider>
     </div>
+
     let cn = 'font-code tl pre-wrap bl bw1 pl1 b--transparent '
     if (props.goal.isInserted) cn += 'b--inserted '
     if (props.goal.isRemoved) cn += 'b--removed '
diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx
index de0d6bcb9..fc3af355d 100644
--- a/lean4-infoview/src/infoview/info.tsx
+++ b/lean4-infoview/src/infoview/info.tsx
@@ -11,7 +11,7 @@ import { getInteractiveGoals, getInteractiveTermGoal, InteractiveDiagnostic, Int
     RpcErrorCode, getInteractiveDiagnostics, InteractiveTermGoal } from '@leanprover/infoview-api';
 import { UserWidgetDisplay } from './userWidget'
 import { RpcContext, useRpcSessionAtPos } from './rpcSessions';
-import { GoalsLocation, LocationsContext } from './exprContext';
+import { GoalsLocation, Locations, LocationsContext } from './goalLocation';
 
 type InfoStatus = 'updating' | 'error' | 'ready';
 type InfoKind = 'cursor' | 'pin';
@@ -93,6 +93,20 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
     const [selectedLocs, setSelectedLocs] = React.useState<GoalsLocation[]>([])
     React.useEffect(() => setSelectedLocs([]), [pos.uri, pos.line, pos.character])
 
+    const locs: Locations = React.useMemo(() => ({
+        isSelected: (l: GoalsLocation) => selectedLocs.some(v => GoalsLocation.isEqual(v, l)),
+        setSelected: (l, act) => setSelectedLocs(ls => {
+            // We ensure that `selectedLocs` maintains its reference identity if the selection
+            // status of `l` didn't change.
+            const newLocs = ls.filter(v => !GoalsLocation.isEqual(v, l))
+            const wasSelected = newLocs.length !== ls.length
+            const isSelected = typeof act === 'function' ? act(wasSelected) : act
+            if (isSelected) newLocs.push(l)
+            return wasSelected === isSelected ? ls : newLocs
+        }),
+        subexprTemplate: undefined
+    }), [selectedLocs])
+
     /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */
     return <>
         {hasError &&
@@ -100,15 +114,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
                 Error updating:{' '}{error}.
                 <a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate(); }}>{' '}Try again.</a>
             </div>}
-
-        <LocationsContext.Provider value ={{
-            isSelected: l => selectedLocs.some(v => GoalsLocation.isEqual(v, l)),
-            setSelected: (l, on) => {
-                if (on) setSelectedLocs(ls => ls.filter(v => !GoalsLocation.isEqual(v, l)).concat([l]))
-                else setSelectedLocs(ls => ls.filter(v => !GoalsLocation.isEqual(v, l)))
-            },
-            subexprTemplate: undefined
-        }}>
+        <LocationsContext.Provider value={locs}>
             <FilteredGoals headerChildren='Tactic state' key='goals' goals={goals} />
         </LocationsContext.Provider>
         <FilteredGoals headerChildren='Expected type' key='term-goal'
diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx
index cd7233be2..c3d6672c8 100644
--- a/lean4-infoview/src/infoview/interactiveCode.tsx
+++ b/lean4-infoview/src/infoview/interactiveCode.tsx
@@ -7,7 +7,7 @@ import { HoverState, WithTooltipOnHover } from './tooltips'
 import { Location } from 'vscode-languageserver-protocol'
 import { marked } from 'marked'
 import { RpcContext } from './rpcSessions'
-import { GoalsLocation, LocationsContext, SelectableLocation } from './exprContext'
+import { GoalsLocation, LocationsContext, SelectableLocation } from './goalLocation'
 
 export interface InteractiveTextComponentProps<T> {
   fmt: TaggedText<T>
diff --git a/lean4-infoview/src/infoview/userWidget.tsx b/lean4-infoview/src/infoview/userWidget.tsx
index 56e5a0afb..30b6207bb 100644
--- a/lean4-infoview/src/infoview/userWidget.tsx
+++ b/lean4-infoview/src/infoview/userWidget.tsx
@@ -4,7 +4,7 @@ import { Widget_getWidgetSource, UserWidgetInstance, InteractiveGoal, Interactiv
 import { RpcContext } from './rpcSessions';
 import { DocumentPosition, mapRpcError, useAsync } from './util';
 import { ErrorBoundary } from './errors';
-import { GoalsLocation } from './exprContext';
+import { GoalsLocation } from './goalLocation';
 
 function dynamicallyLoadComponent(hash: string, code: string) {
     return React.lazy(async () => {

From 10932c275e347c57b72f1b46d29f1e6182f9c7ee Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Mon, 19 Dec 2022 18:03:44 -0500
Subject: [PATCH 10/13] fix: React prop

---
 lean4-infoview/src/infoview/goalLocation.tsx | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/lean4-infoview/src/infoview/goalLocation.tsx b/lean4-infoview/src/infoview/goalLocation.tsx
index ddc37a662..4f29e5db9 100644
--- a/lean4-infoview/src/infoview/goalLocation.tsx
+++ b/lean4-infoview/src/infoview/goalLocation.tsx
@@ -84,8 +84,8 @@ type SelectableLocationProps =
  * If `locs` or `loc` is `undefined`, selection functionality is turned off. The element is also
  * highlighted when hovered over if `alwaysHighlight` is `true` or `locs` and `loc` are both defined.
  * `setHoverState` is passed through to {@link DetectHoverSpan}. */
-export function SelectableLocation(props: SelectableLocationProps): JSX.Element {
-  const {locs, loc, alwaysHighlight, setHoverState: setParentHoverState} = props
+export function SelectableLocation(props_: SelectableLocationProps): JSX.Element {
+  const {locs, loc, alwaysHighlight, setHoverState: setParentHoverState, ...props} = props_
 
   const shouldHighlight: boolean = alwaysHighlight || (!!locs && !!loc)
   const [hoverState, setHoverState] = React.useState<HoverState>('off')

From b501559331417a3f5fcfa7dddbbc0e0696c4c3e5 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Mon, 9 Jan 2023 21:33:15 -0500
Subject: [PATCH 11/13] feat: export dynamic importer

---
 lean4-infoview/src/index.tsx               |  4 +-
 lean4-infoview/src/infoview/info.tsx       |  6 +-
 lean4-infoview/src/infoview/userWidget.tsx | 92 +++++++++++++---------
 3 files changed, 60 insertions(+), 42 deletions(-)

diff --git a/lean4-infoview/src/index.tsx b/lean4-infoview/src/index.tsx
index 08b3b7c3f..6f0264eb6 100644
--- a/lean4-infoview/src/index.tsx
+++ b/lean4-infoview/src/index.tsx
@@ -6,13 +6,13 @@ import { InteractiveMessage } from './infoview/traceExplorer';
 
 export * from '@leanprover/infoview-api';
 export { useAsync, useAsyncWithTrigger, useEvent, useEventResult, useServerNotificationEffect,
-useServerNotificationState, useClientNotificationEffect, useClientNotificationState, mapRpcError } from './infoview/util';
+useServerNotificationState, useClientNotificationEffect, useClientNotificationState, mapRpcError, DocumentPosition } from './infoview/util';
 export { EditorContext, VersionContext } from './infoview/contexts';
 export { EditorConnection } from './infoview/editorConnection';
 export { RpcContext } from './infoview/rpcSessions';
 export { ServerVersion } from './infoview/serverVersion';
 export { GoalLocation, GoalsLocation } from './infoview/goalLocation';
-export { UserWidgetProps } from './infoview/userWidget';
+export { importWidgetModule, DynamicComponent, DynamicComponentProps, PanelWidgetProps  } from './infoview/userWidget';
 
 export { InteractiveCode, InteractiveCodeProps } from './infoview/interactiveCode';
 export { renderInfoview } from './infoview/main';
diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx
index fc3af355d..16ea1c514 100644
--- a/lean4-infoview/src/infoview/info.tsx
+++ b/lean4-infoview/src/infoview/info.tsx
@@ -6,10 +6,10 @@ import { basename, DocumentPosition, RangeHelpers, useEvent, usePausableState, d
     mapRpcError, useAsyncWithTrigger, PausableProps } from './util';
 import { ConfigContext, EditorContext, LspDiagnosticsContext, ProgressContext } from './contexts';
 import { lspDiagToInteractive, MessagesList } from './messages';
-import { getInteractiveGoals, getInteractiveTermGoal, InteractiveDiagnostic, InteractiveGoal,
+import { getInteractiveGoals, getInteractiveTermGoal, InteractiveDiagnostic,
     InteractiveGoals, UserWidgetInstance, Widget_getWidgets, RpcSessionAtPos, isRpcError,
     RpcErrorCode, getInteractiveDiagnostics, InteractiveTermGoal } from '@leanprover/infoview-api';
-import { UserWidgetDisplay } from './userWidget'
+import { PanelWidgetDisplay } from './userWidget'
 import { RpcContext, useRpcSessionAtPos } from './rpcSessions';
 import { GoalsLocation, Locations, LocationsContext } from './goalLocation';
 
@@ -122,7 +122,7 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
         {userWidgets.map(widget =>
             <details key={`widget::${widget.id}::${widget.range?.toString()}`} open>
                 <summary className='mv2 pointer'>{widget.name}</summary>
-                <UserWidgetDisplay pos={pos} goals={goals ? goals.goals : []} termGoal={termGoal}
+                <PanelWidgetDisplay pos={pos} goals={goals ? goals.goals : []} termGoal={termGoal}
                     selectedLocations={selectedLocs} widget={widget}/>
             </details>
         )}
diff --git a/lean4-infoview/src/infoview/userWidget.tsx b/lean4-infoview/src/infoview/userWidget.tsx
index 30b6207bb..83815ea6c 100644
--- a/lean4-infoview/src/infoview/userWidget.tsx
+++ b/lean4-infoview/src/infoview/userWidget.tsx
@@ -1,22 +1,63 @@
 import * as React from 'react';
 
-import { Widget_getWidgetSource, UserWidgetInstance, InteractiveGoal, InteractiveTermGoal } from '@leanprover/infoview-api';
+import { Widget_getWidgetSource, UserWidgetInstance, InteractiveGoal, InteractiveTermGoal, RpcSessionAtPos } from '@leanprover/infoview-api';
 import { RpcContext } from './rpcSessions';
 import { DocumentPosition, mapRpcError, useAsync } from './util';
 import { ErrorBoundary } from './errors';
 import { GoalsLocation } from './goalLocation';
 
-function dynamicallyLoadComponent(hash: string, code: string) {
-    return React.lazy(async () => {
-        const file = new File([code], `widget_${hash}.js`, { type: 'text/javascript' })
-        const url = URL.createObjectURL(file)
-        return await import(url)
-    })
+async function dynamicallyLoadModule(hash: string, code: string): Promise<any> {
+    const file = new File([code], `widget_${hash}.js`, { type: 'text/javascript' })
+    const url = URL.createObjectURL(file)
+    return await import(url)
 }
 
-const componentCache = new Map<string, React.LazyExoticComponent<React.ComponentType<any>>>()
+const moduleCache = new Map<string, any>()
 
-interface UserWidgetDisplayProps {
+/**
+ * Fetch source code from Lean and dynamically import it as a JS module.
+ *
+ * The source must hash to `hash` (in Lean) and must have been annotated with `@[widget]`
+ * or `@[widget_module]` at some point before `pos`. */
+export async function importWidgetModule(rs: RpcSessionAtPos, pos: DocumentPosition, hash: string): Promise<any> {
+    const resp = await Widget_getWidgetSource(rs, pos, hash)
+    if (moduleCache.has(hash)) {
+        // eslint-disable-next-line @typescript-eslint/no-non-null-assertion
+        return moduleCache.get(hash)!
+    }
+    const mod = await dynamicallyLoadModule(hash, resp.sourcetext)
+    moduleCache.set(hash, mod)
+    return mod
+}
+
+export interface DynamicComponentProps {
+    pos: DocumentPosition
+    hash: string
+    props: any
+}
+
+/**
+ * Use {@link importWidgetModule} to import a module which must `export default` a React component,
+ * and render that with `props`. Errors in the component are caught in an error boundary. */
+export function DynamicComponent(props_: React.PropsWithChildren<DynamicComponentProps>) {
+    const { pos, hash, props, children } = props_
+    const rs = React.useContext(RpcContext)
+    const component = useAsync(async () => {
+        const mod = await importWidgetModule(rs, pos, hash)
+        return React.lazy(async () => mod)
+    }, [hash])
+
+    return (
+        <React.Suspense fallback={`Loading component ${hash}: ${component.state}.`}>
+            <ErrorBoundary>
+                {component.state === 'resolved' && React.createElement(component.value, props, children)}
+                {component.state === 'rejected' && <>Error: {mapRpcError(component.error).message}</>}
+            </ErrorBoundary>
+        </React.Suspense>
+    )
+}
+
+interface PanelWidgetDisplayProps {
     pos: DocumentPosition
     goals: InteractiveGoal[]
     termGoal?: InteractiveTermGoal
@@ -24,8 +65,8 @@ interface UserWidgetDisplayProps {
     widget: UserWidgetInstance
 }
 
-/** Props that every user widget receives as input to its `default` export. */
-export interface UserWidgetProps {
+/** Props that every infoview panel widget receives as input to its `default` export. */
+export interface PanelWidgetProps {
     /** Cursor position in the file at which the widget is being displayed. */
     pos: DocumentPosition
     /** The current tactic-mode goals. */
@@ -36,30 +77,7 @@ export interface UserWidgetProps {
     selectedLocations: GoalsLocation[]
 }
 
-export function UserWidgetDisplay({ pos, goals, termGoal, selectedLocations, widget }: UserWidgetDisplayProps) {
-    const rs = React.useContext(RpcContext);
-    const hash = widget.javascriptHash
-    const component = useAsync(
-        async () => {
-            if (componentCache.has(hash)) {
-                // eslint-disable-next-line @typescript-eslint/no-non-null-assertion
-                return componentCache.get(hash)!
-            }
-            const code = await Widget_getWidgetSource(rs, pos, hash)
-            const component = dynamicallyLoadComponent(hash, code.sourcetext)
-            componentCache.set(hash, component)
-            return component
-        },
-        [hash])
-
-    const componentProps: UserWidgetProps = { pos, goals, termGoal, selectedLocations, ...widget.props }
-
-    return (
-        <React.Suspense fallback={`Loading widget: ${widget.id} ${component.state}.`}>
-            <ErrorBoundary>
-                {component.state === 'resolved' && <div>{React.createElement(component.value, componentProps)}</div>}
-                {component.state === 'rejected' && <div>{mapRpcError(component.error).message}</div>}
-            </ErrorBoundary>
-        </React.Suspense>
-    )
+export function PanelWidgetDisplay({ pos, goals, termGoal, selectedLocations, widget }: PanelWidgetDisplayProps) {
+    const componentProps: PanelWidgetProps = { pos, goals, termGoal, selectedLocations, ...widget.props }
+    return <DynamicComponent pos={pos} hash={widget.javascriptHash} props={componentProps} />
 }

From 3c26b0abcf00dac2f51cf5d0bcd9fd107cf170ec Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Fri, 13 Jan 2023 14:36:10 -0500
Subject: [PATCH 12/13] chore: bump package versions

---
 lean4-infoview-api/package-lock.json |  16 +-
 lean4-infoview-api/package.json      |   2 +-
 lean4-infoview/package-lock.json     | 533 +++++++++------------------
 lean4-infoview/package.json          |   4 +-
 package-lock.json                    |   2 +-
 vscode-lean4/package-lock.json       | 184 ++++-----
 vscode-lean4/package.json            |   4 +-
 7 files changed, 283 insertions(+), 462 deletions(-)

diff --git a/lean4-infoview-api/package-lock.json b/lean4-infoview-api/package-lock.json
index 89db06d1f..2823eb6ac 100644
--- a/lean4-infoview-api/package-lock.json
+++ b/lean4-infoview-api/package-lock.json
@@ -1,12 +1,12 @@
 {
   "name": "@leanprover/infoview-api",
-  "version": "0.2.0",
+  "version": "0.2.1",
   "lockfileVersion": 2,
   "requires": true,
   "packages": {
     "": {
       "name": "@leanprover/infoview-api",
-      "version": "0.2.0",
+      "version": "0.2.1",
       "license": "Apache-2.0",
       "devDependencies": {
         "typescript": "^4.7.4",
@@ -14,9 +14,9 @@
       }
     },
     "node_modules/typescript": {
-      "version": "4.9.3",
-      "resolved": "https://registry.npmjs.org/typescript/-/typescript-4.9.3.tgz",
-      "integrity": "sha512-CIfGzTelbKNEnLpLdGFgdyKhG23CKdKgQPOBc+OUNrkJ2vr+KSzsSV5kq5iWhEQbok+quxgGzrAtGWCyU7tHnA==",
+      "version": "4.9.4",
+      "resolved": "https://registry.npmjs.org/typescript/-/typescript-4.9.4.tgz",
+      "integrity": "sha512-Uz+dTXYzxXXbsFpM86Wh3dKCxrQqUcVMxwU54orwlJjOpO3ao8L7j5lH+dWfTwgCwIuM9GQ2kvVotzYJMXTBZg==",
       "dev": true,
       "bin": {
         "tsc": "bin/tsc",
@@ -54,9 +54,9 @@
   },
   "dependencies": {
     "typescript": {
-      "version": "4.9.3",
-      "resolved": "https://registry.npmjs.org/typescript/-/typescript-4.9.3.tgz",
-      "integrity": "sha512-CIfGzTelbKNEnLpLdGFgdyKhG23CKdKgQPOBc+OUNrkJ2vr+KSzsSV5kq5iWhEQbok+quxgGzrAtGWCyU7tHnA==",
+      "version": "4.9.4",
+      "resolved": "https://registry.npmjs.org/typescript/-/typescript-4.9.4.tgz",
+      "integrity": "sha512-Uz+dTXYzxXXbsFpM86Wh3dKCxrQqUcVMxwU54orwlJjOpO3ao8L7j5lH+dWfTwgCwIuM9GQ2kvVotzYJMXTBZg==",
       "dev": true
     },
     "vscode-jsonrpc": {
diff --git a/lean4-infoview-api/package.json b/lean4-infoview-api/package.json
index a88a3cb5e..c80d03b66 100644
--- a/lean4-infoview-api/package.json
+++ b/lean4-infoview-api/package.json
@@ -1,6 +1,6 @@
 {
   "name": "@leanprover/infoview-api",
-  "version": "0.2.0",
+  "version": "0.2.1",
   "description": "Types and API for @leanprover/infoview.",
   "scripts": {
     "watch": "tsc --watch",
diff --git a/lean4-infoview/package-lock.json b/lean4-infoview/package-lock.json
index 2d29835ab..e7f7bbb08 100644
--- a/lean4-infoview/package-lock.json
+++ b/lean4-infoview/package-lock.json
@@ -1,12 +1,12 @@
 {
   "name": "@leanprover/infoview",
-  "version": "0.4.1",
+  "version": "0.4.2",
   "lockfileVersion": 2,
   "requires": true,
   "packages": {
     "": {
       "name": "@leanprover/infoview",
-      "version": "0.4.1",
+      "version": "0.4.2",
       "license": "Apache-2.0",
       "dependencies": {
         "@vscode/codicons": "^0.0.32",
@@ -35,11 +35,54 @@
         "typescript": "^4.8.4"
       }
     },
+    "../lean4-infoview-api": {
+      "name": "@leanprover/infoview-api",
+      "version": "0.2.1",
+      "dev": true,
+      "license": "Apache-2.0",
+      "devDependencies": {
+        "typescript": "^4.7.4",
+        "vscode-languageserver-protocol": "^3.17.2"
+      }
+    },
+    "../lean4-infoview-api/node_modules/typescript": {
+      "version": "4.9.3",
+      "dev": true,
+      "license": "Apache-2.0",
+      "bin": {
+        "tsc": "bin/tsc",
+        "tsserver": "bin/tsserver"
+      },
+      "engines": {
+        "node": ">=4.2.0"
+      }
+    },
+    "../lean4-infoview-api/node_modules/vscode-jsonrpc": {
+      "version": "8.0.2",
+      "dev": true,
+      "license": "MIT",
+      "engines": {
+        "node": ">=14.0.0"
+      }
+    },
+    "../lean4-infoview-api/node_modules/vscode-languageserver-protocol": {
+      "version": "3.17.2",
+      "dev": true,
+      "license": "MIT",
+      "dependencies": {
+        "vscode-jsonrpc": "8.0.2",
+        "vscode-languageserver-types": "3.17.2"
+      }
+    },
+    "../lean4-infoview-api/node_modules/vscode-languageserver-types": {
+      "version": "3.17.2",
+      "dev": true,
+      "license": "MIT"
+    },
     "node_modules/@jridgewell/gen-mapping": {
       "version": "0.3.2",
-      "resolved": "https://registry.npmjs.org/@jridgewell/gen-mapping/-/gen-mapping-0.3.2.tgz",
-      "integrity": "sha512-mh65xKQAzI6iBcFzwv28KVWSmCkdRBWoOh+bYQGW3+6OZvbbN3TqMGo5hqYxQniRcH9F2VZIoJCm4pa3BPDK/A==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "@jridgewell/set-array": "^1.0.1",
         "@jridgewell/sourcemap-codec": "^1.4.10",
@@ -51,27 +94,24 @@
     },
     "node_modules/@jridgewell/resolve-uri": {
       "version": "3.1.0",
-      "resolved": "https://registry.npmjs.org/@jridgewell/resolve-uri/-/resolve-uri-3.1.0.tgz",
-      "integrity": "sha512-F2msla3tad+Mfht5cJq7LSXcdudKTWCVYUgw6pLFOOHSTtZlj6SWNYAp+AhuqLmWdBO2X5hPrLcu8cVP8fy28w==",
       "dev": true,
+      "license": "MIT",
       "engines": {
         "node": ">=6.0.0"
       }
     },
     "node_modules/@jridgewell/set-array": {
       "version": "1.1.2",
-      "resolved": "https://registry.npmjs.org/@jridgewell/set-array/-/set-array-1.1.2.tgz",
-      "integrity": "sha512-xnkseuNADM0gt2bs+BvhO0p78Mk762YnZdsuzFV018NoG1Sj1SCQvpSqa7XUaTam5vAGasABV9qXASMKnFMwMw==",
       "dev": true,
+      "license": "MIT",
       "engines": {
         "node": ">=6.0.0"
       }
     },
     "node_modules/@jridgewell/source-map": {
       "version": "0.3.2",
-      "resolved": "https://registry.npmjs.org/@jridgewell/source-map/-/source-map-0.3.2.tgz",
-      "integrity": "sha512-m7O9o2uR8k2ObDysZYzdfhb08VuEml5oWGiosa1VdaPZ/A6QyPkAJuwN0Q1lhULOf6B7MtQmHENS743hWtCrgw==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "@jridgewell/gen-mapping": "^0.3.0",
         "@jridgewell/trace-mapping": "^0.3.9"
@@ -79,31 +119,26 @@
     },
     "node_modules/@jridgewell/sourcemap-codec": {
       "version": "1.4.14",
-      "resolved": "https://registry.npmjs.org/@jridgewell/sourcemap-codec/-/sourcemap-codec-1.4.14.tgz",
-      "integrity": "sha512-XPSJHWmi394fuUuzDnGz1wiKqWfo1yXecHQMRf2l6hztTO+nPru658AyDngaBe7isIxEkRsPR3FZh+s7iVa4Uw==",
-      "dev": true
+      "dev": true,
+      "license": "MIT"
     },
     "node_modules/@jridgewell/trace-mapping": {
       "version": "0.3.17",
-      "resolved": "https://registry.npmjs.org/@jridgewell/trace-mapping/-/trace-mapping-0.3.17.tgz",
-      "integrity": "sha512-MCNzAp77qzKca9+W/+I0+sEpaUnZoeasnghNeVc41VZCEKaCH73Vq3BZZ/SzWIgrqE4H4ceI+p+b6C0mHf9T4g==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "@jridgewell/resolve-uri": "3.1.0",
         "@jridgewell/sourcemap-codec": "1.4.14"
       }
     },
     "node_modules/@leanprover/infoview-api": {
-      "version": "0.2.0",
-      "resolved": "https://registry.npmjs.org/@leanprover/infoview-api/-/infoview-api-0.2.0.tgz",
-      "integrity": "sha512-HnBCg9/ijvJmQkEAlHH5E50i5uQVqdOC2sT5KzUs+Bq7woL2dPNjeDFECudye5bvbLoy+kJ/x24n0eW5PuaF3w==",
-      "dev": true
+      "resolved": "../lean4-infoview-api",
+      "link": true
     },
     "node_modules/@popperjs/core": {
       "version": "2.11.6",
-      "resolved": "https://registry.npmjs.org/@popperjs/core/-/core-2.11.6.tgz",
-      "integrity": "sha512-50/17A98tWUfQ176raKiOGXuYpLyyVMkxxG6oylzL3BPOlA6ADGdK7EYunSa4I064xerltq9TGXs8HmOk5E+vw==",
       "dev": true,
+      "license": "MIT",
       "peer": true,
       "funding": {
         "type": "opencollective",
@@ -112,9 +147,8 @@
     },
     "node_modules/@rollup/plugin-commonjs": {
       "version": "23.0.3",
-      "resolved": "https://registry.npmjs.org/@rollup/plugin-commonjs/-/plugin-commonjs-23.0.3.tgz",
-      "integrity": "sha512-31HxrT5emGfTyIfAs1lDQHj6EfYxTXcwtX5pIIhq+B/xZBNIqQ179d/CkYxlpYmFCxT78AeU4M8aL8Iv/IBxFA==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "@rollup/pluginutils": "^5.0.1",
         "commondir": "^1.0.1",
@@ -137,9 +171,8 @@
     },
     "node_modules/@rollup/plugin-node-resolve": {
       "version": "15.0.1",
-      "resolved": "https://registry.npmjs.org/@rollup/plugin-node-resolve/-/plugin-node-resolve-15.0.1.tgz",
-      "integrity": "sha512-ReY88T7JhJjeRVbfCyNj+NXAG3IIsVMsX9b5/9jC98dRP8/yxlZdz7mHZbHk5zHr24wZZICS5AcXsFZAXYUQEg==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "@rollup/pluginutils": "^5.0.1",
         "@types/resolve": "1.20.2",
@@ -162,9 +195,8 @@
     },
     "node_modules/@rollup/plugin-replace": {
       "version": "5.0.1",
-      "resolved": "https://registry.npmjs.org/@rollup/plugin-replace/-/plugin-replace-5.0.1.tgz",
-      "integrity": "sha512-Z3MfsJ4CK17BfGrZgvrcp/l6WXoKb0kokULO+zt/7bmcyayokDaQ2K3eDJcRLCTAlp5FPI4/gz9MHAsosz4Rag==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "@rollup/pluginutils": "^5.0.1",
         "magic-string": "^0.26.4"
@@ -183,9 +215,8 @@
     },
     "node_modules/@rollup/plugin-terser": {
       "version": "0.1.0",
-      "resolved": "https://registry.npmjs.org/@rollup/plugin-terser/-/plugin-terser-0.1.0.tgz",
-      "integrity": "sha512-N2KK+qUfHX2hBzVzM41UWGLrEmcjVC37spC8R3c9mt3oEDFKh3N2e12/lLp9aVSt86veR0TQiCNQXrm8C6aiUQ==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "terser": "^5.15.1"
       },
@@ -203,9 +234,8 @@
     },
     "node_modules/@rollup/plugin-typescript": {
       "version": "9.0.2",
-      "resolved": "https://registry.npmjs.org/@rollup/plugin-typescript/-/plugin-typescript-9.0.2.tgz",
-      "integrity": "sha512-/sS93vmHUMjzDUsl5scNQr1mUlNE1QjBBvOhmRwJCH8k2RRhDIm3c977B3wdu3t3Ap17W6dDeXP3hj1P1Un1bA==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "@rollup/pluginutils": "^5.0.1",
         "resolve": "^1.22.1"
@@ -229,9 +259,8 @@
     },
     "node_modules/@rollup/plugin-url": {
       "version": "8.0.1",
-      "resolved": "https://registry.npmjs.org/@rollup/plugin-url/-/plugin-url-8.0.1.tgz",
-      "integrity": "sha512-8ajztphXb5e19dk3Iwjtm2eSYJR8jFQubZ8pJ1GG2MBMM7/qUedLnZAN+Vt4jqbcT/m27jfjIBocvrzV0giNRw==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "@rollup/pluginutils": "^5.0.1",
         "make-dir": "^3.1.0",
@@ -251,9 +280,8 @@
     },
     "node_modules/@rollup/pluginutils": {
       "version": "5.0.2",
-      "resolved": "https://registry.npmjs.org/@rollup/pluginutils/-/pluginutils-5.0.2.tgz",
-      "integrity": "sha512-pTd9rIsP92h+B6wWwFbW8RkZv4hiR/xKsqre4SIuAOaOEQRxi0lqLke9k2/7WegC85GgUs9pjmOjCUi3In4vwA==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "@types/estree": "^1.0.0",
         "estree-walker": "^2.0.2",
@@ -273,27 +301,23 @@
     },
     "node_modules/@types/estree": {
       "version": "1.0.0",
-      "resolved": "https://registry.npmjs.org/@types/estree/-/estree-1.0.0.tgz",
-      "integrity": "sha512-WulqXMDUTYAXCjZnk6JtIHPigp55cVtDgDrO2gHRwhyJto21+1zbVCtOYB2L1F9w4qCQ0rOGWBnBe0FNTiEJIQ==",
-      "dev": true
+      "dev": true,
+      "license": "MIT"
     },
     "node_modules/@types/marked": {
       "version": "4.0.7",
-      "resolved": "https://registry.npmjs.org/@types/marked/-/marked-4.0.7.tgz",
-      "integrity": "sha512-eEAhnz21CwvKVW+YvRvcTuFKNU9CV1qH+opcgVK3pIMI6YZzDm6gc8o2vHjldFk6MGKt5pueSB7IOpvpx5Qekw==",
-      "dev": true
+      "dev": true,
+      "license": "MIT"
     },
     "node_modules/@types/prop-types": {
       "version": "15.7.5",
-      "resolved": "https://registry.npmjs.org/@types/prop-types/-/prop-types-15.7.5.tgz",
-      "integrity": "sha512-JCB8C6SnDoQf0cNycqd/35A7MjcnK+ZTqE7judS6o7utxUCg6imJg3QK2qzHKszlTjcj2cn+NwMB2i96ubpj7w==",
-      "dev": true
+      "dev": true,
+      "license": "MIT"
     },
     "node_modules/@types/react": {
       "version": "18.0.25",
-      "resolved": "https://registry.npmjs.org/@types/react/-/react-18.0.25.tgz",
-      "integrity": "sha512-xD6c0KDT4m7n9uD4ZHi02lzskaiqcBxf4zi+tXZY98a04wvc0hi/TcCPC2FOESZi51Nd7tlUeOJY8RofL799/g==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "@types/prop-types": "*",
         "@types/scheduler": "*",
@@ -302,35 +326,30 @@
     },
     "node_modules/@types/react-dom": {
       "version": "18.0.9",
-      "resolved": "https://registry.npmjs.org/@types/react-dom/-/react-dom-18.0.9.tgz",
-      "integrity": "sha512-qnVvHxASt/H7i+XG1U1xMiY5t+IHcPGUK7TDMDzom08xa7e86eCeKOiLZezwCKVxJn6NEiiy2ekgX8aQssjIKg==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "@types/react": "*"
       }
     },
     "node_modules/@types/resolve": {
       "version": "1.20.2",
-      "resolved": "https://registry.npmjs.org/@types/resolve/-/resolve-1.20.2.tgz",
-      "integrity": "sha512-60BCwRFOZCQhDncwQdxxeOEEkbc5dIMccYLwbxsS4TUNeVECQ/pBJ0j09mrHOl/JJvpRPGwO9SvE4nR2Nb/a4Q==",
-      "dev": true
+      "dev": true,
+      "license": "MIT"
     },
     "node_modules/@types/scheduler": {
       "version": "0.16.2",
-      "resolved": "https://registry.npmjs.org/@types/scheduler/-/scheduler-0.16.2.tgz",
-      "integrity": "sha512-hppQEBDmlwhFAXKJX2KnWLYu5yMfi91yazPb2l+lbJiwW+wdo1gNeRA+3RgNSO39WYX2euey41KEwnqesU2Jew==",
-      "dev": true
+      "dev": true,
+      "license": "MIT"
     },
     "node_modules/@vscode/codicons": {
       "version": "0.0.32",
-      "resolved": "https://registry.npmjs.org/@vscode/codicons/-/codicons-0.0.32.tgz",
-      "integrity": "sha512-3lgSTWhAzzWN/EPURoY4ZDBEA80OPmnaknNujA3qnI4Iu7AONWd9xF3iE4L+4prIe8E3TUnLQ4pxoaFTEEZNwg=="
+      "license": "CC-BY-4.0"
     },
     "node_modules/acorn": {
       "version": "8.8.1",
-      "resolved": "https://registry.npmjs.org/acorn/-/acorn-8.8.1.tgz",
-      "integrity": "sha512-7zFpHzhnqYKrkYdUjF1HI1bzd0VygEGX8lFk4k5zVMqHEoES+P+7TKI+EvLO9WVMJ8eekdO0aDEK044xTXwPPA==",
       "dev": true,
+      "license": "MIT",
       "bin": {
         "acorn": "bin/acorn"
       },
@@ -340,30 +359,26 @@
     },
     "node_modules/balanced-match": {
       "version": "1.0.2",
-      "resolved": "https://registry.npmjs.org/balanced-match/-/balanced-match-1.0.2.tgz",
-      "integrity": "sha512-3oSeUO0TMV67hN1AmbXsK4yaqU7tjiHlbxRDZOpH0KW9+CeX4bRAaX0Anxt0tx2MrpRpWwQaPwIlISEJhYU5Pw==",
-      "dev": true
+      "dev": true,
+      "license": "MIT"
     },
     "node_modules/brace-expansion": {
       "version": "2.0.1",
-      "resolved": "https://registry.npmjs.org/brace-expansion/-/brace-expansion-2.0.1.tgz",
-      "integrity": "sha512-XnAIvQ8eM+kC6aULx6wuQiwVsnzsi9d3WxzV3FpWTGA19F621kwdbsAcFKXgKUHZWsy+mY6iL1sHTxWEFCytDA==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "balanced-match": "^1.0.0"
       }
     },
     "node_modules/buffer-from": {
       "version": "1.1.2",
-      "resolved": "https://registry.npmjs.org/buffer-from/-/buffer-from-1.1.2.tgz",
-      "integrity": "sha512-E+XQCRwSbaaiChtv6k6Dwgc+bx+Bs6vuKJHHl5kox/BaKbhiXzqQOwK4cO22yElGp2OCmjwVhT3HmxgyPGnJfQ==",
-      "dev": true
+      "dev": true,
+      "license": "MIT"
     },
     "node_modules/builtin-modules": {
       "version": "3.3.0",
-      "resolved": "https://registry.npmjs.org/builtin-modules/-/builtin-modules-3.3.0.tgz",
-      "integrity": "sha512-zhaCDicdLuWN5UbN5IMnFqNMhNfo919sH85y2/ea+5Yg9TsTkeZxpL+JLbp6cgYFS4sRLp3YV4S6yDuqVWHYOw==",
       "dev": true,
+      "license": "MIT",
       "engines": {
         "node": ">=6"
       },
@@ -373,28 +388,24 @@
     },
     "node_modules/commander": {
       "version": "2.20.3",
-      "resolved": "https://registry.npmjs.org/commander/-/commander-2.20.3.tgz",
-      "integrity": "sha512-GpVkmM8vF2vQUkj2LvZmD35JxeJOLCwJ9cUkugyk2nuhbv3+mJvpLYYt+0+USMxE+oj+ey/lJEnhZw75x/OMcQ==",
-      "dev": true
+      "dev": true,
+      "license": "MIT"
     },
     "node_modules/commondir": {
       "version": "1.0.1",
-      "resolved": "https://registry.npmjs.org/commondir/-/commondir-1.0.1.tgz",
-      "integrity": "sha512-W9pAhw0ja1Edb5GVdIF1mjZw/ASI0AlShXM83UUGe2DVr5TdAPEA1OA8m/g8zWp9x6On7gqufY+FatDbC3MDQg==",
-      "dev": true
+      "dev": true,
+      "license": "MIT"
     },
     "node_modules/csstype": {
       "version": "3.1.1",
-      "resolved": "https://registry.npmjs.org/csstype/-/csstype-3.1.1.tgz",
-      "integrity": "sha512-DJR/VvkAvSZW9bTouZue2sSxDwdTN92uHjqeKVm+0dAqdfNykRzQ95tay8aXMBAAPpUiq4Qcug2L7neoRh2Egw==",
-      "dev": true
+      "dev": true,
+      "license": "MIT"
     },
     "node_modules/current-release": {
       "name": "@leanprover/infoview",
       "version": "0.4.0",
-      "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.4.0.tgz",
-      "integrity": "sha512-l053Zy+os9z53e8no6K1oYyDQrbUg+Nv/lBDQH/OqKoZukldhrsp0KQXT58+4VPhKKvxNAIor24AHfFbmDASvA==",
       "dev": true,
+      "license": "Apache-2.0",
       "dependencies": {
         "@leanprover/infoview-api": "~0.2.0",
         "@vscode/codicons": "^0.0.32",
@@ -407,55 +418,35 @@
     },
     "node_modules/deepmerge": {
       "version": "4.2.2",
-      "resolved": "https://registry.npmjs.org/deepmerge/-/deepmerge-4.2.2.tgz",
-      "integrity": "sha512-FJ3UgI4gIl+PHZm53knsuSFpE+nESMr7M4v9QcgB7S63Kj/6WqMiFQJpBBYz1Pt+66bZpP3Q7Lye0Oo9MPKEdg==",
       "dev": true,
+      "license": "MIT",
       "engines": {
         "node": ">=0.10.0"
       }
     },
     "node_modules/es-module-shims": {
       "version": "1.6.2",
-      "resolved": "https://registry.npmjs.org/es-module-shims/-/es-module-shims-1.6.2.tgz",
-      "integrity": "sha512-VISkM/sF/TlQzFY3WlyCXj3Fkv7+L3pErEFmrDHj0URx54EMY9GpSbW3CE04ZqWk6qrC/YsRDBTu9QvU2n0dZw=="
+      "license": "MIT"
     },
     "node_modules/estree-walker": {
       "version": "2.0.2",
-      "resolved": "https://registry.npmjs.org/estree-walker/-/estree-walker-2.0.2.tgz",
-      "integrity": "sha512-Rfkk/Mp/DL7JVje3u18FxFujQlTNR2q6QfMSMB7AvCBx91NGj/ba3kCfza0f6dVDbw7YlRf/nDrn7pQrCCyQ/w==",
-      "dev": true
+      "dev": true,
+      "license": "MIT"
     },
     "node_modules/fs.realpath": {
       "version": "1.0.0",
-      "resolved": "https://registry.npmjs.org/fs.realpath/-/fs.realpath-1.0.0.tgz",
-      "integrity": "sha512-OO0pH2lK6a0hZnAdau5ItzHPI6pUlvI7jMVnxUQRtw4owF2wk8lOSabtGDCTP4Ggrg2MbGnWO9X8K1t4+fGMDw==",
-      "dev": true
-    },
-    "node_modules/fsevents": {
-      "version": "2.3.2",
-      "resolved": "https://registry.npmjs.org/fsevents/-/fsevents-2.3.2.tgz",
-      "integrity": "sha512-xiqMQR4xAeHTuB9uWm+fFRcIOgKBMiOBP+eXiyT7jsgVCq1bkVygt00oASowB7EdtpOHaaPgKt812P9ab+DDKA==",
       "dev": true,
-      "hasInstallScript": true,
-      "optional": true,
-      "os": [
-        "darwin"
-      ],
-      "engines": {
-        "node": "^8.16.0 || ^10.6.0 || >=11.0.0"
-      }
+      "license": "ISC"
     },
     "node_modules/function-bind": {
       "version": "1.1.1",
-      "resolved": "https://registry.npmjs.org/function-bind/-/function-bind-1.1.1.tgz",
-      "integrity": "sha512-yIovAzMX49sF8Yl58fSCWJ5svSLuaibPxXQJFLmBObTuCr0Mf1KiPopGM9NiFjiYBCbfaa2Fh6breQ6ANVTI0A==",
-      "dev": true
+      "dev": true,
+      "license": "MIT"
     },
     "node_modules/glob": {
       "version": "8.0.3",
-      "resolved": "https://registry.npmjs.org/glob/-/glob-8.0.3.tgz",
-      "integrity": "sha512-ull455NHSHI/Y1FqGaaYFaLGkNMMJbavMrEGFXG/PGrg6y7sutWHUHrz6gy6WEBH6akM1M414dWKCNs+IhKdiQ==",
       "dev": true,
+      "license": "ISC",
       "dependencies": {
         "fs.realpath": "^1.0.0",
         "inflight": "^1.0.4",
@@ -472,9 +463,8 @@
     },
     "node_modules/has": {
       "version": "1.0.3",
-      "resolved": "https://registry.npmjs.org/has/-/has-1.0.3.tgz",
-      "integrity": "sha512-f2dvO0VU6Oej7RkWJGrehjbzMAjFp5/VKPp5tTpWIV4JHHZK1/BxbFRtf/siA2SWTe09caDmVtYYzWEIbBS4zw==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "function-bind": "^1.1.1"
       },
@@ -484,9 +474,8 @@
     },
     "node_modules/inflight": {
       "version": "1.0.6",
-      "resolved": "https://registry.npmjs.org/inflight/-/inflight-1.0.6.tgz",
-      "integrity": "sha512-k92I/b08q4wvFscXCLvqfsHCrjrF7yiXsQuIVvVE7N82W3+aqpzuUdBbfhWcy/FZR3/4IgflMgKLOsvPDrGCJA==",
       "dev": true,
+      "license": "ISC",
       "dependencies": {
         "once": "^1.3.0",
         "wrappy": "1"
@@ -494,15 +483,13 @@
     },
     "node_modules/inherits": {
       "version": "2.0.4",
-      "resolved": "https://registry.npmjs.org/inherits/-/inherits-2.0.4.tgz",
-      "integrity": "sha512-k/vGaX4/Yla3WzyMCvTQOXYeIHvqOKtnqBduzTHpzpQZzAskKMhZ2K+EnBiSM9zGSoIFeMpXKxa4dYeZIQqewQ==",
-      "dev": true
+      "dev": true,
+      "license": "ISC"
     },
     "node_modules/is-builtin-module": {
       "version": "3.2.0",
-      "resolved": "https://registry.npmjs.org/is-builtin-module/-/is-builtin-module-3.2.0.tgz",
-      "integrity": "sha512-phDA4oSGt7vl1n5tJvTWooWWAsXLY+2xCnxNqvKhGEzujg+A43wPlPOyDg3C8XQHN+6k/JTQWJ/j0dQh/qr+Hw==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "builtin-modules": "^3.3.0"
       },
@@ -515,9 +502,8 @@
     },
     "node_modules/is-core-module": {
       "version": "2.11.0",
-      "resolved": "https://registry.npmjs.org/is-core-module/-/is-core-module-2.11.0.tgz",
-      "integrity": "sha512-RRjxlvLDkD1YJwDbroBHMb+cukurkDWNyHx7D3oNB5x9rb5ogcksMC5wHCadcXoo67gVr/+3GFySh3134zi6rw==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "has": "^1.0.3"
       },
@@ -527,30 +513,26 @@
     },
     "node_modules/is-module": {
       "version": "1.0.0",
-      "resolved": "https://registry.npmjs.org/is-module/-/is-module-1.0.0.tgz",
-      "integrity": "sha512-51ypPSPCoTEIN9dy5Oy+h4pShgJmPCygKfyRCISBI+JoWT/2oJvK8QPxmwv7b/p239jXrm9M1mlQbyKJ5A152g==",
-      "dev": true
+      "dev": true,
+      "license": "MIT"
     },
     "node_modules/is-reference": {
       "version": "1.2.1",
-      "resolved": "https://registry.npmjs.org/is-reference/-/is-reference-1.2.1.tgz",
-      "integrity": "sha512-U82MsXXiFIrjCK4otLT+o2NA2Cd2g5MLoOVXUZjIOhLurrRxpEXzI8O0KZHr3IjLvlAH1kTPYSuqer5T9ZVBKQ==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "@types/estree": "*"
       }
     },
     "node_modules/js-tokens": {
       "version": "4.0.0",
-      "resolved": "https://registry.npmjs.org/js-tokens/-/js-tokens-4.0.0.tgz",
-      "integrity": "sha512-RdJUflcE3cUzKiMqQgsCu06FPu9UdIJO0beYbPhHN4k6apgJtifcoCtT9bcxOpYBtpD2kCM6Sbzg4CausW/PKQ==",
-      "dev": true
+      "dev": true,
+      "license": "MIT"
     },
     "node_modules/loose-envify": {
       "version": "1.4.0",
-      "resolved": "https://registry.npmjs.org/loose-envify/-/loose-envify-1.4.0.tgz",
-      "integrity": "sha512-lyuxPGr/Wfhrlem2CL/UcnUc1zcqKAImBDzukY7Y5F/yQiNdko6+fRLevlw1HgMySw7f611UIY408EtxRSoK3Q==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "js-tokens": "^3.0.0 || ^4.0.0"
       },
@@ -560,9 +542,8 @@
     },
     "node_modules/magic-string": {
       "version": "0.26.7",
-      "resolved": "https://registry.npmjs.org/magic-string/-/magic-string-0.26.7.tgz",
-      "integrity": "sha512-hX9XH3ziStPoPhJxLq1syWuZMxbDvGNbVchfrdCtanC7D13888bMFow61x8axrx+GfHLtVeAx2kxL7tTGRl+Ow==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "sourcemap-codec": "^1.4.8"
       },
@@ -572,9 +553,8 @@
     },
     "node_modules/make-dir": {
       "version": "3.1.0",
-      "resolved": "https://registry.npmjs.org/make-dir/-/make-dir-3.1.0.tgz",
-      "integrity": "sha512-g3FeP20LNwhALb/6Cz6Dd4F2ngze0jz7tbzrD2wAV+o9FeNHe4rL+yK2md0J/fiSf1sa1ADhXqi5+oVwOM/eGw==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "semver": "^6.0.0"
       },
@@ -587,8 +567,7 @@
     },
     "node_modules/marked": {
       "version": "4.2.3",
-      "resolved": "https://registry.npmjs.org/marked/-/marked-4.2.3.tgz",
-      "integrity": "sha512-slWRdJkbTZ+PjkyJnE30Uid64eHwbwa1Q25INCAYfZlK4o6ylagBy/Le9eWntqJFoFT93ikUKMv47GZ4gTwHkw==",
+      "license": "MIT",
       "bin": {
         "marked": "bin/marked.js"
       },
@@ -598,9 +577,8 @@
     },
     "node_modules/mime": {
       "version": "3.0.0",
-      "resolved": "https://registry.npmjs.org/mime/-/mime-3.0.0.tgz",
-      "integrity": "sha512-jSCU7/VB1loIWBZe14aEYHU/+1UMEHoaO7qxCOVJOw9GgH72VAWppxNcjU+x9a2k3GSIBXNKxXQFqRvvZ7vr3A==",
       "dev": true,
+      "license": "MIT",
       "bin": {
         "mime": "cli.js"
       },
@@ -610,9 +588,8 @@
     },
     "node_modules/minimatch": {
       "version": "5.1.1",
-      "resolved": "https://registry.npmjs.org/minimatch/-/minimatch-5.1.1.tgz",
-      "integrity": "sha512-362NP+zlprccbEt/SkxKfRMHnNY85V74mVnpUpNyr3F35covl09Kec7/sEFLt3RA4oXmewtoaanoIf67SE5Y5g==",
       "dev": true,
+      "license": "ISC",
       "dependencies": {
         "brace-expansion": "^2.0.1"
       },
@@ -622,24 +599,21 @@
     },
     "node_modules/once": {
       "version": "1.4.0",
-      "resolved": "https://registry.npmjs.org/once/-/once-1.4.0.tgz",
-      "integrity": "sha512-lNaJgI+2Q5URQBkccEKHTQOPaXdUxnZZElQTZY0MFUAuaEqe1E+Nyvgdz/aIyNi6Z9MzO5dv1H8n58/GELp3+w==",
       "dev": true,
+      "license": "ISC",
       "dependencies": {
         "wrappy": "1"
       }
     },
     "node_modules/path-parse": {
       "version": "1.0.7",
-      "resolved": "https://registry.npmjs.org/path-parse/-/path-parse-1.0.7.tgz",
-      "integrity": "sha512-LDJzPVEEEPR+y48z93A0Ed0yXb8pAByGWo/k5YYdYgpY2/2EsOsksJrq7lOHxryrVOn1ejG6oAp8ahvOIQD8sw==",
-      "dev": true
+      "dev": true,
+      "license": "MIT"
     },
     "node_modules/picomatch": {
       "version": "2.3.1",
-      "resolved": "https://registry.npmjs.org/picomatch/-/picomatch-2.3.1.tgz",
-      "integrity": "sha512-JU3teHTNjmE2VCGFzuY8EXzCDVwEqB2a8fsIvwaStHhAWJEeVd1o1QD80CU6+ZdEXXSLbSsuLwJjkCBWqRQUVA==",
       "dev": true,
+      "license": "MIT",
       "engines": {
         "node": ">=8.6"
       },
@@ -649,9 +623,8 @@
     },
     "node_modules/react": {
       "version": "18.2.0",
-      "resolved": "https://registry.npmjs.org/react/-/react-18.2.0.tgz",
-      "integrity": "sha512-/3IjMdb2L9QbBdWiW5e3P2/npwMBaU9mHCSCUzNln0ZCYbcfTsGbTJrU/kGemdH2IWmB2ioZ+zkxtmq6g09fGQ==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "loose-envify": "^1.1.0"
       },
@@ -661,9 +634,8 @@
     },
     "node_modules/react-dom": {
       "version": "18.2.0",
-      "resolved": "https://registry.npmjs.org/react-dom/-/react-dom-18.2.0.tgz",
-      "integrity": "sha512-6IMTriUmvsjHUjNtEDudZfuDQUoWXVxKHhlEGSk81n4YFS+r/Kl99wXiwlVXtPBtJenozv2P+hxDsw9eA7Xo6g==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "loose-envify": "^1.1.0",
         "scheduler": "^0.23.0"
@@ -674,14 +646,12 @@
     },
     "node_modules/react-fast-compare": {
       "version": "3.2.0",
-      "resolved": "https://registry.npmjs.org/react-fast-compare/-/react-fast-compare-3.2.0.tgz",
-      "integrity": "sha512-rtGImPZ0YyLrscKI9xTpV8psd6I8VAtjKCzQDlzyDvqJA8XOW78TXYQwNRNd8g8JZnDu8q9Fu/1v4HPAVwVdHA=="
+      "license": "MIT"
     },
     "node_modules/react-popper": {
       "version": "2.3.0",
-      "resolved": "https://registry.npmjs.org/react-popper/-/react-popper-2.3.0.tgz",
-      "integrity": "sha512-e1hj8lL3uM+sgSR4Lxzn5h1GxBlpa4CQz0XLF8kx4MDrDRWY0Ena4c97PUeSX9i5W3UAfDP0z0FXCTQkoXUl3Q==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "react-fast-compare": "^3.0.1",
         "warning": "^4.0.2"
@@ -694,9 +664,8 @@
     },
     "node_modules/resolve": {
       "version": "1.22.1",
-      "resolved": "https://registry.npmjs.org/resolve/-/resolve-1.22.1.tgz",
-      "integrity": "sha512-nBpuuYuY5jFsli/JIs1oldw6fOQCBioohqWZg/2hiaOybXOft4lonv85uDOKXdf8rhyK159cxU5cDcK/NKk8zw==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "is-core-module": "^2.9.0",
         "path-parse": "^1.0.7",
@@ -711,9 +680,8 @@
     },
     "node_modules/rollup": {
       "version": "3.5.0",
-      "resolved": "https://registry.npmjs.org/rollup/-/rollup-3.5.0.tgz",
-      "integrity": "sha512-TYu2L+TGhmNsXCtByont89u+ATQLcDy6A+++PwLXYunRtOm7XnaD+65s1pvewaOxMYR0eOkMXn9/i0saBxxpnQ==",
       "dev": true,
+      "license": "MIT",
       "bin": {
         "rollup": "dist/bin/rollup"
       },
@@ -727,9 +695,8 @@
     },
     "node_modules/rollup-plugin-css-only": {
       "version": "4.3.0",
-      "resolved": "https://registry.npmjs.org/rollup-plugin-css-only/-/rollup-plugin-css-only-4.3.0.tgz",
-      "integrity": "sha512-BsiCqJJQzZh2lQiHY5irejRoJ3I1EUFHEi5PjVqsr+EmOh54YrWVwd3YZEXnQJ2+fzlhif0YM/Kf0GuH90GAdQ==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "@rollup/pluginutils": "5"
       },
@@ -742,36 +709,32 @@
     },
     "node_modules/scheduler": {
       "version": "0.23.0",
-      "resolved": "https://registry.npmjs.org/scheduler/-/scheduler-0.23.0.tgz",
-      "integrity": "sha512-CtuThmgHNg7zIZWAXi3AsyIzA3n4xx7aNyjwC2VJldO2LMVDhFK+63xGqq6CsJH4rTAt6/M+N4GhZiDYPx9eUw==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "loose-envify": "^1.1.0"
       }
     },
     "node_modules/semver": {
       "version": "6.3.0",
-      "resolved": "https://registry.npmjs.org/semver/-/semver-6.3.0.tgz",
-      "integrity": "sha512-b39TBaTSfV6yBrapU89p5fKekE2m/NwnDocOVruQFS1/veMgdzuPcnOM34M6CwxW8jH/lxEa5rBoDeUwu5HHTw==",
       "dev": true,
+      "license": "ISC",
       "bin": {
         "semver": "bin/semver.js"
       }
     },
     "node_modules/source-map": {
       "version": "0.6.1",
-      "resolved": "https://registry.npmjs.org/source-map/-/source-map-0.6.1.tgz",
-      "integrity": "sha512-UjgapumWlbMhkBgzT7Ykc5YXUT46F0iKu8SGXq0bcwP5dz/h0Plj6enJqjz1Zbq2l5WaqYnrVbwWOWMyF3F47g==",
       "dev": true,
+      "license": "BSD-3-Clause",
       "engines": {
         "node": ">=0.10.0"
       }
     },
     "node_modules/source-map-support": {
       "version": "0.5.21",
-      "resolved": "https://registry.npmjs.org/source-map-support/-/source-map-support-0.5.21.tgz",
-      "integrity": "sha512-uBHU3L3czsIyYXKX88fdrGovxdSCoTGDRZ6SYXtSRxLZUzHg5P/66Ht6uoUlHu9EZod+inXhKo3qQgwXUT/y1w==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "buffer-from": "^1.0.0",
         "source-map": "^0.6.0"
@@ -779,15 +742,13 @@
     },
     "node_modules/sourcemap-codec": {
       "version": "1.4.8",
-      "resolved": "https://registry.npmjs.org/sourcemap-codec/-/sourcemap-codec-1.4.8.tgz",
-      "integrity": "sha512-9NykojV5Uih4lgo5So5dtw+f0JgJX30KCNI8gwhz2J9A15wD0Ml6tjHKwf6fTSa6fAdVBdZeNOs9eJ71qCk8vA==",
-      "dev": true
+      "dev": true,
+      "license": "MIT"
     },
     "node_modules/supports-preserve-symlinks-flag": {
       "version": "1.0.0",
-      "resolved": "https://registry.npmjs.org/supports-preserve-symlinks-flag/-/supports-preserve-symlinks-flag-1.0.0.tgz",
-      "integrity": "sha512-ot0WnXS9fgdkgIcePe6RHNk1WA8+muPa6cSjeR3V8K27q9BB1rTE3R1p7Hv0z1ZyAc8s6Vvv8DIyWf681MAt0w==",
       "dev": true,
+      "license": "MIT",
       "engines": {
         "node": ">= 0.4"
       },
@@ -797,14 +758,12 @@
     },
     "node_modules/tachyons": {
       "version": "4.12.0",
-      "resolved": "https://registry.npmjs.org/tachyons/-/tachyons-4.12.0.tgz",
-      "integrity": "sha512-2nA2IrYFy3raCM9fxJ2KODRGHVSZNTW3BR0YnlGsLUf1DA3pk3YfWZ/DdfbnZK6zLZS+jUenlUGJsKcA5fUiZg=="
+      "license": "MIT"
     },
     "node_modules/terser": {
       "version": "5.16.0",
-      "resolved": "https://registry.npmjs.org/terser/-/terser-5.16.0.tgz",
-      "integrity": "sha512-KjTV81QKStSfwbNiwlBXfcgMcOloyuRdb62/iLFPGBcVNF4EXjhdYBhYHmbJpiBrVxZhDvltE11j+LBQUxEEJg==",
       "dev": true,
+      "license": "BSD-2-Clause",
       "dependencies": {
         "@jridgewell/source-map": "^0.3.2",
         "acorn": "^8.5.0",
@@ -820,9 +779,8 @@
     },
     "node_modules/typescript": {
       "version": "4.9.3",
-      "resolved": "https://registry.npmjs.org/typescript/-/typescript-4.9.3.tgz",
-      "integrity": "sha512-CIfGzTelbKNEnLpLdGFgdyKhG23CKdKgQPOBc+OUNrkJ2vr+KSzsSV5kq5iWhEQbok+quxgGzrAtGWCyU7tHnA==",
       "dev": true,
+      "license": "Apache-2.0",
       "bin": {
         "tsc": "bin/tsc",
         "tsserver": "bin/tsserver"
@@ -833,16 +791,14 @@
     },
     "node_modules/vscode-jsonrpc": {
       "version": "8.0.2",
-      "resolved": "https://registry.npmjs.org/vscode-jsonrpc/-/vscode-jsonrpc-8.0.2.tgz",
-      "integrity": "sha512-RY7HwI/ydoC1Wwg4gJ3y6LpU9FJRZAUnTYMXthqhFXXu77ErDd/xkREpGuk4MyYkk4a+XDWAMqe0S3KkelYQEQ==",
+      "license": "MIT",
       "engines": {
         "node": ">=14.0.0"
       }
     },
     "node_modules/vscode-languageserver-protocol": {
       "version": "3.17.2",
-      "resolved": "https://registry.npmjs.org/vscode-languageserver-protocol/-/vscode-languageserver-protocol-3.17.2.tgz",
-      "integrity": "sha512-8kYisQ3z/SQ2kyjlNeQxbkkTNmVFoQCqkmGrzLH6A9ecPlgTbp3wDTnUNqaUxYr4vlAcloxx8zwy7G5WdguYNg==",
+      "license": "MIT",
       "dependencies": {
         "vscode-jsonrpc": "8.0.2",
         "vscode-languageserver-types": "3.17.2"
@@ -850,30 +806,25 @@
     },
     "node_modules/vscode-languageserver-types": {
       "version": "3.17.2",
-      "resolved": "https://registry.npmjs.org/vscode-languageserver-types/-/vscode-languageserver-types-3.17.2.tgz",
-      "integrity": "sha512-zHhCWatviizPIq9B7Vh9uvrH6x3sK8itC84HkamnBWoDFJtzBf7SWlpLCZUit72b3os45h6RWQNC9xHRDF8dRA=="
+      "license": "MIT"
     },
     "node_modules/warning": {
       "version": "4.0.3",
-      "resolved": "https://registry.npmjs.org/warning/-/warning-4.0.3.tgz",
-      "integrity": "sha512-rpJyN222KWIvHJ/F53XSZv0Zl/accqHR8et1kpaMTD/fLCRxtV8iX8czMzY7sVZupTI3zcUTg8eycS2kNF9l6w==",
       "dev": true,
+      "license": "MIT",
       "dependencies": {
         "loose-envify": "^1.0.0"
       }
     },
     "node_modules/wrappy": {
       "version": "1.0.2",
-      "resolved": "https://registry.npmjs.org/wrappy/-/wrappy-1.0.2.tgz",
-      "integrity": "sha512-l4Sp/DRseor9wL6EvV2+TuQn63dMkPjZ/sp9XkghTEbV9KlPS1xUsZ3u7/IQO4wxtcFB4bgpQPRcR3QCvezPcQ==",
-      "dev": true
+      "dev": true,
+      "license": "ISC"
     }
   },
   "dependencies": {
     "@jridgewell/gen-mapping": {
       "version": "0.3.2",
-      "resolved": "https://registry.npmjs.org/@jridgewell/gen-mapping/-/gen-mapping-0.3.2.tgz",
-      "integrity": "sha512-mh65xKQAzI6iBcFzwv28KVWSmCkdRBWoOh+bYQGW3+6OZvbbN3TqMGo5hqYxQniRcH9F2VZIoJCm4pa3BPDK/A==",
       "dev": true,
       "requires": {
         "@jridgewell/set-array": "^1.0.1",
@@ -883,20 +834,14 @@
     },
     "@jridgewell/resolve-uri": {
       "version": "3.1.0",
-      "resolved": "https://registry.npmjs.org/@jridgewell/resolve-uri/-/resolve-uri-3.1.0.tgz",
-      "integrity": "sha512-F2msla3tad+Mfht5cJq7LSXcdudKTWCVYUgw6pLFOOHSTtZlj6SWNYAp+AhuqLmWdBO2X5hPrLcu8cVP8fy28w==",
       "dev": true
     },
     "@jridgewell/set-array": {
       "version": "1.1.2",
-      "resolved": "https://registry.npmjs.org/@jridgewell/set-array/-/set-array-1.1.2.tgz",
-      "integrity": "sha512-xnkseuNADM0gt2bs+BvhO0p78Mk762YnZdsuzFV018NoG1Sj1SCQvpSqa7XUaTam5vAGasABV9qXASMKnFMwMw==",
       "dev": true
     },
     "@jridgewell/source-map": {
       "version": "0.3.2",
-      "resolved": "https://registry.npmjs.org/@jridgewell/source-map/-/source-map-0.3.2.tgz",
-      "integrity": "sha512-m7O9o2uR8k2ObDysZYzdfhb08VuEml5oWGiosa1VdaPZ/A6QyPkAJuwN0Q1lhULOf6B7MtQmHENS743hWtCrgw==",
       "dev": true,
       "requires": {
         "@jridgewell/gen-mapping": "^0.3.0",
@@ -905,14 +850,10 @@
     },
     "@jridgewell/sourcemap-codec": {
       "version": "1.4.14",
-      "resolved": "https://registry.npmjs.org/@jridgewell/sourcemap-codec/-/sourcemap-codec-1.4.14.tgz",
-      "integrity": "sha512-XPSJHWmi394fuUuzDnGz1wiKqWfo1yXecHQMRf2l6hztTO+nPru658AyDngaBe7isIxEkRsPR3FZh+s7iVa4Uw==",
       "dev": true
     },
     "@jridgewell/trace-mapping": {
       "version": "0.3.17",
-      "resolved": "https://registry.npmjs.org/@jridgewell/trace-mapping/-/trace-mapping-0.3.17.tgz",
-      "integrity": "sha512-MCNzAp77qzKca9+W/+I0+sEpaUnZoeasnghNeVc41VZCEKaCH73Vq3BZZ/SzWIgrqE4H4ceI+p+b6C0mHf9T4g==",
       "dev": true,
       "requires": {
         "@jridgewell/resolve-uri": "3.1.0",
@@ -920,22 +861,41 @@
       }
     },
     "@leanprover/infoview-api": {
-      "version": "0.2.0",
-      "resolved": "https://registry.npmjs.org/@leanprover/infoview-api/-/infoview-api-0.2.0.tgz",
-      "integrity": "sha512-HnBCg9/ijvJmQkEAlHH5E50i5uQVqdOC2sT5KzUs+Bq7woL2dPNjeDFECudye5bvbLoy+kJ/x24n0eW5PuaF3w==",
-      "dev": true
+      "version": "file:../lean4-infoview-api",
+      "requires": {
+        "typescript": "^4.7.4",
+        "vscode-languageserver-protocol": "^3.17.2"
+      },
+      "dependencies": {
+        "typescript": {
+          "version": "4.9.3",
+          "dev": true
+        },
+        "vscode-jsonrpc": {
+          "version": "8.0.2",
+          "dev": true
+        },
+        "vscode-languageserver-protocol": {
+          "version": "3.17.2",
+          "dev": true,
+          "requires": {
+            "vscode-jsonrpc": "8.0.2",
+            "vscode-languageserver-types": "3.17.2"
+          }
+        },
+        "vscode-languageserver-types": {
+          "version": "3.17.2",
+          "dev": true
+        }
+      }
     },
     "@popperjs/core": {
       "version": "2.11.6",
-      "resolved": "https://registry.npmjs.org/@popperjs/core/-/core-2.11.6.tgz",
-      "integrity": "sha512-50/17A98tWUfQ176raKiOGXuYpLyyVMkxxG6oylzL3BPOlA6ADGdK7EYunSa4I064xerltq9TGXs8HmOk5E+vw==",
       "dev": true,
       "peer": true
     },
     "@rollup/plugin-commonjs": {
       "version": "23.0.3",
-      "resolved": "https://registry.npmjs.org/@rollup/plugin-commonjs/-/plugin-commonjs-23.0.3.tgz",
-      "integrity": "sha512-31HxrT5emGfTyIfAs1lDQHj6EfYxTXcwtX5pIIhq+B/xZBNIqQ179d/CkYxlpYmFCxT78AeU4M8aL8Iv/IBxFA==",
       "dev": true,
       "requires": {
         "@rollup/pluginutils": "^5.0.1",
@@ -948,8 +908,6 @@
     },
     "@rollup/plugin-node-resolve": {
       "version": "15.0.1",
-      "resolved": "https://registry.npmjs.org/@rollup/plugin-node-resolve/-/plugin-node-resolve-15.0.1.tgz",
-      "integrity": "sha512-ReY88T7JhJjeRVbfCyNj+NXAG3IIsVMsX9b5/9jC98dRP8/yxlZdz7mHZbHk5zHr24wZZICS5AcXsFZAXYUQEg==",
       "dev": true,
       "requires": {
         "@rollup/pluginutils": "^5.0.1",
@@ -962,8 +920,6 @@
     },
     "@rollup/plugin-replace": {
       "version": "5.0.1",
-      "resolved": "https://registry.npmjs.org/@rollup/plugin-replace/-/plugin-replace-5.0.1.tgz",
-      "integrity": "sha512-Z3MfsJ4CK17BfGrZgvrcp/l6WXoKb0kokULO+zt/7bmcyayokDaQ2K3eDJcRLCTAlp5FPI4/gz9MHAsosz4Rag==",
       "dev": true,
       "requires": {
         "@rollup/pluginutils": "^5.0.1",
@@ -972,8 +928,6 @@
     },
     "@rollup/plugin-terser": {
       "version": "0.1.0",
-      "resolved": "https://registry.npmjs.org/@rollup/plugin-terser/-/plugin-terser-0.1.0.tgz",
-      "integrity": "sha512-N2KK+qUfHX2hBzVzM41UWGLrEmcjVC37spC8R3c9mt3oEDFKh3N2e12/lLp9aVSt86veR0TQiCNQXrm8C6aiUQ==",
       "dev": true,
       "requires": {
         "terser": "^5.15.1"
@@ -981,8 +935,6 @@
     },
     "@rollup/plugin-typescript": {
       "version": "9.0.2",
-      "resolved": "https://registry.npmjs.org/@rollup/plugin-typescript/-/plugin-typescript-9.0.2.tgz",
-      "integrity": "sha512-/sS93vmHUMjzDUsl5scNQr1mUlNE1QjBBvOhmRwJCH8k2RRhDIm3c977B3wdu3t3Ap17W6dDeXP3hj1P1Un1bA==",
       "dev": true,
       "requires": {
         "@rollup/pluginutils": "^5.0.1",
@@ -991,8 +943,6 @@
     },
     "@rollup/plugin-url": {
       "version": "8.0.1",
-      "resolved": "https://registry.npmjs.org/@rollup/plugin-url/-/plugin-url-8.0.1.tgz",
-      "integrity": "sha512-8ajztphXb5e19dk3Iwjtm2eSYJR8jFQubZ8pJ1GG2MBMM7/qUedLnZAN+Vt4jqbcT/m27jfjIBocvrzV0giNRw==",
       "dev": true,
       "requires": {
         "@rollup/pluginutils": "^5.0.1",
@@ -1002,8 +952,6 @@
     },
     "@rollup/pluginutils": {
       "version": "5.0.2",
-      "resolved": "https://registry.npmjs.org/@rollup/pluginutils/-/pluginutils-5.0.2.tgz",
-      "integrity": "sha512-pTd9rIsP92h+B6wWwFbW8RkZv4hiR/xKsqre4SIuAOaOEQRxi0lqLke9k2/7WegC85GgUs9pjmOjCUi3In4vwA==",
       "dev": true,
       "requires": {
         "@types/estree": "^1.0.0",
@@ -1013,26 +961,18 @@
     },
     "@types/estree": {
       "version": "1.0.0",
-      "resolved": "https://registry.npmjs.org/@types/estree/-/estree-1.0.0.tgz",
-      "integrity": "sha512-WulqXMDUTYAXCjZnk6JtIHPigp55cVtDgDrO2gHRwhyJto21+1zbVCtOYB2L1F9w4qCQ0rOGWBnBe0FNTiEJIQ==",
       "dev": true
     },
     "@types/marked": {
       "version": "4.0.7",
-      "resolved": "https://registry.npmjs.org/@types/marked/-/marked-4.0.7.tgz",
-      "integrity": "sha512-eEAhnz21CwvKVW+YvRvcTuFKNU9CV1qH+opcgVK3pIMI6YZzDm6gc8o2vHjldFk6MGKt5pueSB7IOpvpx5Qekw==",
       "dev": true
     },
     "@types/prop-types": {
       "version": "15.7.5",
-      "resolved": "https://registry.npmjs.org/@types/prop-types/-/prop-types-15.7.5.tgz",
-      "integrity": "sha512-JCB8C6SnDoQf0cNycqd/35A7MjcnK+ZTqE7judS6o7utxUCg6imJg3QK2qzHKszlTjcj2cn+NwMB2i96ubpj7w==",
       "dev": true
     },
     "@types/react": {
       "version": "18.0.25",
-      "resolved": "https://registry.npmjs.org/@types/react/-/react-18.0.25.tgz",
-      "integrity": "sha512-xD6c0KDT4m7n9uD4ZHi02lzskaiqcBxf4zi+tXZY98a04wvc0hi/TcCPC2FOESZi51Nd7tlUeOJY8RofL799/g==",
       "dev": true,
       "requires": {
         "@types/prop-types": "*",
@@ -1042,8 +982,6 @@
     },
     "@types/react-dom": {
       "version": "18.0.9",
-      "resolved": "https://registry.npmjs.org/@types/react-dom/-/react-dom-18.0.9.tgz",
-      "integrity": "sha512-qnVvHxASt/H7i+XG1U1xMiY5t+IHcPGUK7TDMDzom08xa7e86eCeKOiLZezwCKVxJn6NEiiy2ekgX8aQssjIKg==",
       "dev": true,
       "requires": {
         "@types/react": "*"
@@ -1051,37 +989,25 @@
     },
     "@types/resolve": {
       "version": "1.20.2",
-      "resolved": "https://registry.npmjs.org/@types/resolve/-/resolve-1.20.2.tgz",
-      "integrity": "sha512-60BCwRFOZCQhDncwQdxxeOEEkbc5dIMccYLwbxsS4TUNeVECQ/pBJ0j09mrHOl/JJvpRPGwO9SvE4nR2Nb/a4Q==",
       "dev": true
     },
     "@types/scheduler": {
       "version": "0.16.2",
-      "resolved": "https://registry.npmjs.org/@types/scheduler/-/scheduler-0.16.2.tgz",
-      "integrity": "sha512-hppQEBDmlwhFAXKJX2KnWLYu5yMfi91yazPb2l+lbJiwW+wdo1gNeRA+3RgNSO39WYX2euey41KEwnqesU2Jew==",
       "dev": true
     },
     "@vscode/codicons": {
-      "version": "0.0.32",
-      "resolved": "https://registry.npmjs.org/@vscode/codicons/-/codicons-0.0.32.tgz",
-      "integrity": "sha512-3lgSTWhAzzWN/EPURoY4ZDBEA80OPmnaknNujA3qnI4Iu7AONWd9xF3iE4L+4prIe8E3TUnLQ4pxoaFTEEZNwg=="
+      "version": "0.0.32"
     },
     "acorn": {
       "version": "8.8.1",
-      "resolved": "https://registry.npmjs.org/acorn/-/acorn-8.8.1.tgz",
-      "integrity": "sha512-7zFpHzhnqYKrkYdUjF1HI1bzd0VygEGX8lFk4k5zVMqHEoES+P+7TKI+EvLO9WVMJ8eekdO0aDEK044xTXwPPA==",
       "dev": true
     },
     "balanced-match": {
       "version": "1.0.2",
-      "resolved": "https://registry.npmjs.org/balanced-match/-/balanced-match-1.0.2.tgz",
-      "integrity": "sha512-3oSeUO0TMV67hN1AmbXsK4yaqU7tjiHlbxRDZOpH0KW9+CeX4bRAaX0Anxt0tx2MrpRpWwQaPwIlISEJhYU5Pw==",
       "dev": true
     },
     "brace-expansion": {
       "version": "2.0.1",
-      "resolved": "https://registry.npmjs.org/brace-expansion/-/brace-expansion-2.0.1.tgz",
-      "integrity": "sha512-XnAIvQ8eM+kC6aULx6wuQiwVsnzsi9d3WxzV3FpWTGA19F621kwdbsAcFKXgKUHZWsy+mY6iL1sHTxWEFCytDA==",
       "dev": true,
       "requires": {
         "balanced-match": "^1.0.0"
@@ -1089,38 +1015,26 @@
     },
     "buffer-from": {
       "version": "1.1.2",
-      "resolved": "https://registry.npmjs.org/buffer-from/-/buffer-from-1.1.2.tgz",
-      "integrity": "sha512-E+XQCRwSbaaiChtv6k6Dwgc+bx+Bs6vuKJHHl5kox/BaKbhiXzqQOwK4cO22yElGp2OCmjwVhT3HmxgyPGnJfQ==",
       "dev": true
     },
     "builtin-modules": {
       "version": "3.3.0",
-      "resolved": "https://registry.npmjs.org/builtin-modules/-/builtin-modules-3.3.0.tgz",
-      "integrity": "sha512-zhaCDicdLuWN5UbN5IMnFqNMhNfo919sH85y2/ea+5Yg9TsTkeZxpL+JLbp6cgYFS4sRLp3YV4S6yDuqVWHYOw==",
       "dev": true
     },
     "commander": {
       "version": "2.20.3",
-      "resolved": "https://registry.npmjs.org/commander/-/commander-2.20.3.tgz",
-      "integrity": "sha512-GpVkmM8vF2vQUkj2LvZmD35JxeJOLCwJ9cUkugyk2nuhbv3+mJvpLYYt+0+USMxE+oj+ey/lJEnhZw75x/OMcQ==",
       "dev": true
     },
     "commondir": {
       "version": "1.0.1",
-      "resolved": "https://registry.npmjs.org/commondir/-/commondir-1.0.1.tgz",
-      "integrity": "sha512-W9pAhw0ja1Edb5GVdIF1mjZw/ASI0AlShXM83UUGe2DVr5TdAPEA1OA8m/g8zWp9x6On7gqufY+FatDbC3MDQg==",
       "dev": true
     },
     "csstype": {
       "version": "3.1.1",
-      "resolved": "https://registry.npmjs.org/csstype/-/csstype-3.1.1.tgz",
-      "integrity": "sha512-DJR/VvkAvSZW9bTouZue2sSxDwdTN92uHjqeKVm+0dAqdfNykRzQ95tay8aXMBAAPpUiq4Qcug2L7neoRh2Egw==",
       "dev": true
     },
     "current-release": {
       "version": "npm:@leanprover/infoview@0.4.0",
-      "resolved": "https://registry.npmjs.org/@leanprover/infoview/-/infoview-0.4.0.tgz",
-      "integrity": "sha512-l053Zy+os9z53e8no6K1oYyDQrbUg+Nv/lBDQH/OqKoZukldhrsp0KQXT58+4VPhKKvxNAIor24AHfFbmDASvA==",
       "dev": true,
       "requires": {
         "@leanprover/infoview-api": "~0.2.0",
@@ -1134,44 +1048,25 @@
     },
     "deepmerge": {
       "version": "4.2.2",
-      "resolved": "https://registry.npmjs.org/deepmerge/-/deepmerge-4.2.2.tgz",
-      "integrity": "sha512-FJ3UgI4gIl+PHZm53knsuSFpE+nESMr7M4v9QcgB7S63Kj/6WqMiFQJpBBYz1Pt+66bZpP3Q7Lye0Oo9MPKEdg==",
       "dev": true
     },
     "es-module-shims": {
-      "version": "1.6.2",
-      "resolved": "https://registry.npmjs.org/es-module-shims/-/es-module-shims-1.6.2.tgz",
-      "integrity": "sha512-VISkM/sF/TlQzFY3WlyCXj3Fkv7+L3pErEFmrDHj0URx54EMY9GpSbW3CE04ZqWk6qrC/YsRDBTu9QvU2n0dZw=="
+      "version": "1.6.2"
     },
     "estree-walker": {
       "version": "2.0.2",
-      "resolved": "https://registry.npmjs.org/estree-walker/-/estree-walker-2.0.2.tgz",
-      "integrity": "sha512-Rfkk/Mp/DL7JVje3u18FxFujQlTNR2q6QfMSMB7AvCBx91NGj/ba3kCfza0f6dVDbw7YlRf/nDrn7pQrCCyQ/w==",
       "dev": true
     },
     "fs.realpath": {
       "version": "1.0.0",
-      "resolved": "https://registry.npmjs.org/fs.realpath/-/fs.realpath-1.0.0.tgz",
-      "integrity": "sha512-OO0pH2lK6a0hZnAdau5ItzHPI6pUlvI7jMVnxUQRtw4owF2wk8lOSabtGDCTP4Ggrg2MbGnWO9X8K1t4+fGMDw==",
       "dev": true
     },
-    "fsevents": {
-      "version": "2.3.2",
-      "resolved": "https://registry.npmjs.org/fsevents/-/fsevents-2.3.2.tgz",
-      "integrity": "sha512-xiqMQR4xAeHTuB9uWm+fFRcIOgKBMiOBP+eXiyT7jsgVCq1bkVygt00oASowB7EdtpOHaaPgKt812P9ab+DDKA==",
-      "dev": true,
-      "optional": true
-    },
     "function-bind": {
       "version": "1.1.1",
-      "resolved": "https://registry.npmjs.org/function-bind/-/function-bind-1.1.1.tgz",
-      "integrity": "sha512-yIovAzMX49sF8Yl58fSCWJ5svSLuaibPxXQJFLmBObTuCr0Mf1KiPopGM9NiFjiYBCbfaa2Fh6breQ6ANVTI0A==",
       "dev": true
     },
     "glob": {
       "version": "8.0.3",
-      "resolved": "https://registry.npmjs.org/glob/-/glob-8.0.3.tgz",
-      "integrity": "sha512-ull455NHSHI/Y1FqGaaYFaLGkNMMJbavMrEGFXG/PGrg6y7sutWHUHrz6gy6WEBH6akM1M414dWKCNs+IhKdiQ==",
       "dev": true,
       "requires": {
         "fs.realpath": "^1.0.0",
@@ -1183,8 +1078,6 @@
     },
     "has": {
       "version": "1.0.3",
-      "resolved": "https://registry.npmjs.org/has/-/has-1.0.3.tgz",
-      "integrity": "sha512-f2dvO0VU6Oej7RkWJGrehjbzMAjFp5/VKPp5tTpWIV4JHHZK1/BxbFRtf/siA2SWTe09caDmVtYYzWEIbBS4zw==",
       "dev": true,
       "requires": {
         "function-bind": "^1.1.1"
@@ -1192,8 +1085,6 @@
     },
     "inflight": {
       "version": "1.0.6",
-      "resolved": "https://registry.npmjs.org/inflight/-/inflight-1.0.6.tgz",
-      "integrity": "sha512-k92I/b08q4wvFscXCLvqfsHCrjrF7yiXsQuIVvVE7N82W3+aqpzuUdBbfhWcy/FZR3/4IgflMgKLOsvPDrGCJA==",
       "dev": true,
       "requires": {
         "once": "^1.3.0",
@@ -1202,14 +1093,10 @@
     },
     "inherits": {
       "version": "2.0.4",
-      "resolved": "https://registry.npmjs.org/inherits/-/inherits-2.0.4.tgz",
-      "integrity": "sha512-k/vGaX4/Yla3WzyMCvTQOXYeIHvqOKtnqBduzTHpzpQZzAskKMhZ2K+EnBiSM9zGSoIFeMpXKxa4dYeZIQqewQ==",
       "dev": true
     },
     "is-builtin-module": {
       "version": "3.2.0",
-      "resolved": "https://registry.npmjs.org/is-builtin-module/-/is-builtin-module-3.2.0.tgz",
-      "integrity": "sha512-phDA4oSGt7vl1n5tJvTWooWWAsXLY+2xCnxNqvKhGEzujg+A43wPlPOyDg3C8XQHN+6k/JTQWJ/j0dQh/qr+Hw==",
       "dev": true,
       "requires": {
         "builtin-modules": "^3.3.0"
@@ -1217,8 +1104,6 @@
     },
     "is-core-module": {
       "version": "2.11.0",
-      "resolved": "https://registry.npmjs.org/is-core-module/-/is-core-module-2.11.0.tgz",
-      "integrity": "sha512-RRjxlvLDkD1YJwDbroBHMb+cukurkDWNyHx7D3oNB5x9rb5ogcksMC5wHCadcXoo67gVr/+3GFySh3134zi6rw==",
       "dev": true,
       "requires": {
         "has": "^1.0.3"
@@ -1226,14 +1111,10 @@
     },
     "is-module": {
       "version": "1.0.0",
-      "resolved": "https://registry.npmjs.org/is-module/-/is-module-1.0.0.tgz",
-      "integrity": "sha512-51ypPSPCoTEIN9dy5Oy+h4pShgJmPCygKfyRCISBI+JoWT/2oJvK8QPxmwv7b/p239jXrm9M1mlQbyKJ5A152g==",
       "dev": true
     },
     "is-reference": {
       "version": "1.2.1",
-      "resolved": "https://registry.npmjs.org/is-reference/-/is-reference-1.2.1.tgz",
-      "integrity": "sha512-U82MsXXiFIrjCK4otLT+o2NA2Cd2g5MLoOVXUZjIOhLurrRxpEXzI8O0KZHr3IjLvlAH1kTPYSuqer5T9ZVBKQ==",
       "dev": true,
       "requires": {
         "@types/estree": "*"
@@ -1241,14 +1122,10 @@
     },
     "js-tokens": {
       "version": "4.0.0",
-      "resolved": "https://registry.npmjs.org/js-tokens/-/js-tokens-4.0.0.tgz",
-      "integrity": "sha512-RdJUflcE3cUzKiMqQgsCu06FPu9UdIJO0beYbPhHN4k6apgJtifcoCtT9bcxOpYBtpD2kCM6Sbzg4CausW/PKQ==",
       "dev": true
     },
     "loose-envify": {
       "version": "1.4.0",
-      "resolved": "https://registry.npmjs.org/loose-envify/-/loose-envify-1.4.0.tgz",
-      "integrity": "sha512-lyuxPGr/Wfhrlem2CL/UcnUc1zcqKAImBDzukY7Y5F/yQiNdko6+fRLevlw1HgMySw7f611UIY408EtxRSoK3Q==",
       "dev": true,
       "requires": {
         "js-tokens": "^3.0.0 || ^4.0.0"
@@ -1256,8 +1133,6 @@
     },
     "magic-string": {
       "version": "0.26.7",
-      "resolved": "https://registry.npmjs.org/magic-string/-/magic-string-0.26.7.tgz",
-      "integrity": "sha512-hX9XH3ziStPoPhJxLq1syWuZMxbDvGNbVchfrdCtanC7D13888bMFow61x8axrx+GfHLtVeAx2kxL7tTGRl+Ow==",
       "dev": true,
       "requires": {
         "sourcemap-codec": "^1.4.8"
@@ -1265,28 +1140,20 @@
     },
     "make-dir": {
       "version": "3.1.0",
-      "resolved": "https://registry.npmjs.org/make-dir/-/make-dir-3.1.0.tgz",
-      "integrity": "sha512-g3FeP20LNwhALb/6Cz6Dd4F2ngze0jz7tbzrD2wAV+o9FeNHe4rL+yK2md0J/fiSf1sa1ADhXqi5+oVwOM/eGw==",
       "dev": true,
       "requires": {
         "semver": "^6.0.0"
       }
     },
     "marked": {
-      "version": "4.2.3",
-      "resolved": "https://registry.npmjs.org/marked/-/marked-4.2.3.tgz",
-      "integrity": "sha512-slWRdJkbTZ+PjkyJnE30Uid64eHwbwa1Q25INCAYfZlK4o6ylagBy/Le9eWntqJFoFT93ikUKMv47GZ4gTwHkw=="
+      "version": "4.2.3"
     },
     "mime": {
       "version": "3.0.0",
-      "resolved": "https://registry.npmjs.org/mime/-/mime-3.0.0.tgz",
-      "integrity": "sha512-jSCU7/VB1loIWBZe14aEYHU/+1UMEHoaO7qxCOVJOw9GgH72VAWppxNcjU+x9a2k3GSIBXNKxXQFqRvvZ7vr3A==",
       "dev": true
     },
     "minimatch": {
       "version": "5.1.1",
-      "resolved": "https://registry.npmjs.org/minimatch/-/minimatch-5.1.1.tgz",
-      "integrity": "sha512-362NP+zlprccbEt/SkxKfRMHnNY85V74mVnpUpNyr3F35covl09Kec7/sEFLt3RA4oXmewtoaanoIf67SE5Y5g==",
       "dev": true,
       "requires": {
         "brace-expansion": "^2.0.1"
@@ -1294,8 +1161,6 @@
     },
     "once": {
       "version": "1.4.0",
-      "resolved": "https://registry.npmjs.org/once/-/once-1.4.0.tgz",
-      "integrity": "sha512-lNaJgI+2Q5URQBkccEKHTQOPaXdUxnZZElQTZY0MFUAuaEqe1E+Nyvgdz/aIyNi6Z9MzO5dv1H8n58/GELp3+w==",
       "dev": true,
       "requires": {
         "wrappy": "1"
@@ -1303,20 +1168,14 @@
     },
     "path-parse": {
       "version": "1.0.7",
-      "resolved": "https://registry.npmjs.org/path-parse/-/path-parse-1.0.7.tgz",
-      "integrity": "sha512-LDJzPVEEEPR+y48z93A0Ed0yXb8pAByGWo/k5YYdYgpY2/2EsOsksJrq7lOHxryrVOn1ejG6oAp8ahvOIQD8sw==",
       "dev": true
     },
     "picomatch": {
       "version": "2.3.1",
-      "resolved": "https://registry.npmjs.org/picomatch/-/picomatch-2.3.1.tgz",
-      "integrity": "sha512-JU3teHTNjmE2VCGFzuY8EXzCDVwEqB2a8fsIvwaStHhAWJEeVd1o1QD80CU6+ZdEXXSLbSsuLwJjkCBWqRQUVA==",
       "dev": true
     },
     "react": {
       "version": "18.2.0",
-      "resolved": "https://registry.npmjs.org/react/-/react-18.2.0.tgz",
-      "integrity": "sha512-/3IjMdb2L9QbBdWiW5e3P2/npwMBaU9mHCSCUzNln0ZCYbcfTsGbTJrU/kGemdH2IWmB2ioZ+zkxtmq6g09fGQ==",
       "dev": true,
       "requires": {
         "loose-envify": "^1.1.0"
@@ -1324,8 +1183,6 @@
     },
     "react-dom": {
       "version": "18.2.0",
-      "resolved": "https://registry.npmjs.org/react-dom/-/react-dom-18.2.0.tgz",
-      "integrity": "sha512-6IMTriUmvsjHUjNtEDudZfuDQUoWXVxKHhlEGSk81n4YFS+r/Kl99wXiwlVXtPBtJenozv2P+hxDsw9eA7Xo6g==",
       "dev": true,
       "requires": {
         "loose-envify": "^1.1.0",
@@ -1333,14 +1190,10 @@
       }
     },
     "react-fast-compare": {
-      "version": "3.2.0",
-      "resolved": "https://registry.npmjs.org/react-fast-compare/-/react-fast-compare-3.2.0.tgz",
-      "integrity": "sha512-rtGImPZ0YyLrscKI9xTpV8psd6I8VAtjKCzQDlzyDvqJA8XOW78TXYQwNRNd8g8JZnDu8q9Fu/1v4HPAVwVdHA=="
+      "version": "3.2.0"
     },
     "react-popper": {
       "version": "2.3.0",
-      "resolved": "https://registry.npmjs.org/react-popper/-/react-popper-2.3.0.tgz",
-      "integrity": "sha512-e1hj8lL3uM+sgSR4Lxzn5h1GxBlpa4CQz0XLF8kx4MDrDRWY0Ena4c97PUeSX9i5W3UAfDP0z0FXCTQkoXUl3Q==",
       "dev": true,
       "requires": {
         "react-fast-compare": "^3.0.1",
@@ -1349,8 +1202,6 @@
     },
     "resolve": {
       "version": "1.22.1",
-      "resolved": "https://registry.npmjs.org/resolve/-/resolve-1.22.1.tgz",
-      "integrity": "sha512-nBpuuYuY5jFsli/JIs1oldw6fOQCBioohqWZg/2hiaOybXOft4lonv85uDOKXdf8rhyK159cxU5cDcK/NKk8zw==",
       "dev": true,
       "requires": {
         "is-core-module": "^2.9.0",
@@ -1360,8 +1211,6 @@
     },
     "rollup": {
       "version": "3.5.0",
-      "resolved": "https://registry.npmjs.org/rollup/-/rollup-3.5.0.tgz",
-      "integrity": "sha512-TYu2L+TGhmNsXCtByont89u+ATQLcDy6A+++PwLXYunRtOm7XnaD+65s1pvewaOxMYR0eOkMXn9/i0saBxxpnQ==",
       "dev": true,
       "requires": {
         "fsevents": "~2.3.2"
@@ -1369,8 +1218,6 @@
     },
     "rollup-plugin-css-only": {
       "version": "4.3.0",
-      "resolved": "https://registry.npmjs.org/rollup-plugin-css-only/-/rollup-plugin-css-only-4.3.0.tgz",
-      "integrity": "sha512-BsiCqJJQzZh2lQiHY5irejRoJ3I1EUFHEi5PjVqsr+EmOh54YrWVwd3YZEXnQJ2+fzlhif0YM/Kf0GuH90GAdQ==",
       "dev": true,
       "requires": {
         "@rollup/pluginutils": "5"
@@ -1378,8 +1225,6 @@
     },
     "scheduler": {
       "version": "0.23.0",
-      "resolved": "https://registry.npmjs.org/scheduler/-/scheduler-0.23.0.tgz",
-      "integrity": "sha512-CtuThmgHNg7zIZWAXi3AsyIzA3n4xx7aNyjwC2VJldO2LMVDhFK+63xGqq6CsJH4rTAt6/M+N4GhZiDYPx9eUw==",
       "dev": true,
       "requires": {
         "loose-envify": "^1.1.0"
@@ -1387,20 +1232,14 @@
     },
     "semver": {
       "version": "6.3.0",
-      "resolved": "https://registry.npmjs.org/semver/-/semver-6.3.0.tgz",
-      "integrity": "sha512-b39TBaTSfV6yBrapU89p5fKekE2m/NwnDocOVruQFS1/veMgdzuPcnOM34M6CwxW8jH/lxEa5rBoDeUwu5HHTw==",
       "dev": true
     },
     "source-map": {
       "version": "0.6.1",
-      "resolved": "https://registry.npmjs.org/source-map/-/source-map-0.6.1.tgz",
-      "integrity": "sha512-UjgapumWlbMhkBgzT7Ykc5YXUT46F0iKu8SGXq0bcwP5dz/h0Plj6enJqjz1Zbq2l5WaqYnrVbwWOWMyF3F47g==",
       "dev": true
     },
     "source-map-support": {
       "version": "0.5.21",
-      "resolved": "https://registry.npmjs.org/source-map-support/-/source-map-support-0.5.21.tgz",
-      "integrity": "sha512-uBHU3L3czsIyYXKX88fdrGovxdSCoTGDRZ6SYXtSRxLZUzHg5P/66Ht6uoUlHu9EZod+inXhKo3qQgwXUT/y1w==",
       "dev": true,
       "requires": {
         "buffer-from": "^1.0.0",
@@ -1409,25 +1248,17 @@
     },
     "sourcemap-codec": {
       "version": "1.4.8",
-      "resolved": "https://registry.npmjs.org/sourcemap-codec/-/sourcemap-codec-1.4.8.tgz",
-      "integrity": "sha512-9NykojV5Uih4lgo5So5dtw+f0JgJX30KCNI8gwhz2J9A15wD0Ml6tjHKwf6fTSa6fAdVBdZeNOs9eJ71qCk8vA==",
       "dev": true
     },
     "supports-preserve-symlinks-flag": {
       "version": "1.0.0",
-      "resolved": "https://registry.npmjs.org/supports-preserve-symlinks-flag/-/supports-preserve-symlinks-flag-1.0.0.tgz",
-      "integrity": "sha512-ot0WnXS9fgdkgIcePe6RHNk1WA8+muPa6cSjeR3V8K27q9BB1rTE3R1p7Hv0z1ZyAc8s6Vvv8DIyWf681MAt0w==",
       "dev": true
     },
     "tachyons": {
-      "version": "4.12.0",
-      "resolved": "https://registry.npmjs.org/tachyons/-/tachyons-4.12.0.tgz",
-      "integrity": "sha512-2nA2IrYFy3raCM9fxJ2KODRGHVSZNTW3BR0YnlGsLUf1DA3pk3YfWZ/DdfbnZK6zLZS+jUenlUGJsKcA5fUiZg=="
+      "version": "4.12.0"
     },
     "terser": {
       "version": "5.16.0",
-      "resolved": "https://registry.npmjs.org/terser/-/terser-5.16.0.tgz",
-      "integrity": "sha512-KjTV81QKStSfwbNiwlBXfcgMcOloyuRdb62/iLFPGBcVNF4EXjhdYBhYHmbJpiBrVxZhDvltE11j+LBQUxEEJg==",
       "dev": true,
       "requires": {
         "@jridgewell/source-map": "^0.3.2",
@@ -1438,33 +1269,23 @@
     },
     "typescript": {
       "version": "4.9.3",
-      "resolved": "https://registry.npmjs.org/typescript/-/typescript-4.9.3.tgz",
-      "integrity": "sha512-CIfGzTelbKNEnLpLdGFgdyKhG23CKdKgQPOBc+OUNrkJ2vr+KSzsSV5kq5iWhEQbok+quxgGzrAtGWCyU7tHnA==",
       "dev": true
     },
     "vscode-jsonrpc": {
-      "version": "8.0.2",
-      "resolved": "https://registry.npmjs.org/vscode-jsonrpc/-/vscode-jsonrpc-8.0.2.tgz",
-      "integrity": "sha512-RY7HwI/ydoC1Wwg4gJ3y6LpU9FJRZAUnTYMXthqhFXXu77ErDd/xkREpGuk4MyYkk4a+XDWAMqe0S3KkelYQEQ=="
+      "version": "8.0.2"
     },
     "vscode-languageserver-protocol": {
       "version": "3.17.2",
-      "resolved": "https://registry.npmjs.org/vscode-languageserver-protocol/-/vscode-languageserver-protocol-3.17.2.tgz",
-      "integrity": "sha512-8kYisQ3z/SQ2kyjlNeQxbkkTNmVFoQCqkmGrzLH6A9ecPlgTbp3wDTnUNqaUxYr4vlAcloxx8zwy7G5WdguYNg==",
       "requires": {
         "vscode-jsonrpc": "8.0.2",
         "vscode-languageserver-types": "3.17.2"
       }
     },
     "vscode-languageserver-types": {
-      "version": "3.17.2",
-      "resolved": "https://registry.npmjs.org/vscode-languageserver-types/-/vscode-languageserver-types-3.17.2.tgz",
-      "integrity": "sha512-zHhCWatviizPIq9B7Vh9uvrH6x3sK8itC84HkamnBWoDFJtzBf7SWlpLCZUit72b3os45h6RWQNC9xHRDF8dRA=="
+      "version": "3.17.2"
     },
     "warning": {
       "version": "4.0.3",
-      "resolved": "https://registry.npmjs.org/warning/-/warning-4.0.3.tgz",
-      "integrity": "sha512-rpJyN222KWIvHJ/F53XSZv0Zl/accqHR8et1kpaMTD/fLCRxtV8iX8czMzY7sVZupTI3zcUTg8eycS2kNF9l6w==",
       "dev": true,
       "requires": {
         "loose-envify": "^1.0.0"
@@ -1472,8 +1293,6 @@
     },
     "wrappy": {
       "version": "1.0.2",
-      "resolved": "https://registry.npmjs.org/wrappy/-/wrappy-1.0.2.tgz",
-      "integrity": "sha512-l4Sp/DRseor9wL6EvV2+TuQn63dMkPjZ/sp9XkghTEbV9KlPS1xUsZ3u7/IQO4wxtcFB4bgpQPRcR3QCvezPcQ==",
       "dev": true
     }
   }
diff --git a/lean4-infoview/package.json b/lean4-infoview/package.json
index d5acbdee2..a17fcdf47 100644
--- a/lean4-infoview/package.json
+++ b/lean4-infoview/package.json
@@ -1,6 +1,6 @@
 {
   "name": "@leanprover/infoview",
-  "version": "0.4.1",
+  "version": "0.4.2",
   "description": "An interactive display for the Lean 4 theorem prover.",
   "scripts": {
     "watch": "rollup --config --environment NODE_ENV:development --watch",
@@ -47,7 +47,7 @@
     "typescript": "^4.8.4"
   },
   "dependencies": {
-    "@leanprover/infoview-api": "~0.2.0",
+    "@leanprover/infoview-api": "~0.2.1",
     "@vscode/codicons": "^0.0.32",
     "es-module-shims": "^1.6.2",
     "marked": "^4.2.2",
diff --git a/package-lock.json b/package-lock.json
index 3a7bbb2c7..26cdf31bc 100644
--- a/package-lock.json
+++ b/package-lock.json
@@ -10,7 +10,7 @@
         "@typescript-eslint/parser": "^5.43.0",
         "eslint": "^8.27.0",
         "lerna": "^6.0.3",
-        "typescript": "^4.9.3"
+        "typescript": "^4.8.4"
       }
     },
     "node_modules/@babel/code-frame": {
diff --git a/vscode-lean4/package-lock.json b/vscode-lean4/package-lock.json
index f6bf60362..774e10864 100644
--- a/vscode-lean4/package-lock.json
+++ b/vscode-lean4/package-lock.json
@@ -224,9 +224,9 @@
 			"dev": true
 		},
 		"node_modules/@types/node": {
-			"version": "18.11.10",
-			"resolved": "https://registry.npmjs.org/@types/node/-/node-18.11.10.tgz",
-			"integrity": "sha512-juG3RWMBOqcOuXC643OAdSA525V44cVgGV6dUDuiFtss+8Fk5x1hI93Rsld43VeJVIeqlP9I7Fn9/qaVqoEAuQ==",
+			"version": "18.11.18",
+			"resolved": "https://registry.npmjs.org/@types/node/-/node-18.11.18.tgz",
+			"integrity": "sha512-DHQpWGjyQKSHj3ebjFI/wRKcqQcdR+MoFBygntYOZytCqNfkd2ZC4ARDJ2DQqhjH5p85Nnd3jhUJIXrszFX/JA==",
 			"dev": true
 		},
 		"node_modules/@types/ps-node": {
@@ -242,15 +242,15 @@
 			"dev": true
 		},
 		"node_modules/@types/vscode": {
-			"version": "1.73.1",
-			"resolved": "https://registry.npmjs.org/@types/vscode/-/vscode-1.73.1.tgz",
-			"integrity": "sha512-eArfOrAoZVV+Ao9zQOCaFNaeXj4kTCD+bGS2gyNgIFZH9xVMuLMlRrEkhb22NyxycFWKV1UyTh03vhaVHmqVMg==",
+			"version": "1.74.0",
+			"resolved": "https://registry.npmjs.org/@types/vscode/-/vscode-1.74.0.tgz",
+			"integrity": "sha512-LyeCIU3jb9d38w0MXFwta9r0Jx23ugujkAxdwLTNCyspdZTKUc43t7ppPbCiPoQ/Ivd/pnDFZrb4hWd45wrsgA==",
 			"dev": true
 		},
 		"node_modules/@types/vscode-webview": {
-			"version": "1.57.0",
-			"resolved": "https://registry.npmjs.org/@types/vscode-webview/-/vscode-webview-1.57.0.tgz",
-			"integrity": "sha512-x3Cb/SMa1IwRHfSvKaZDZOTh4cNoG505c3NjTqGlMC082m++x/ETUmtYniDsw6SSmYzZXO8KBNhYxR0+VqymqA==",
+			"version": "1.57.1",
+			"resolved": "https://registry.npmjs.org/@types/vscode-webview/-/vscode-webview-1.57.1.tgz",
+			"integrity": "sha512-ghW5SfuDmsGDS2A4xkvGsLwDRNc3Vj5rS6rPOyPm/IryZuf3wceZKxgYaUoW+k9f0f/CB7y2c1rRsdOWZWn0PQ==",
 			"dev": true
 		},
 		"node_modules/@ungap/promise-all-settled": {
@@ -260,9 +260,9 @@
 			"dev": true
 		},
 		"node_modules/@vscode/test-electron": {
-			"version": "2.2.0",
-			"resolved": "https://registry.npmjs.org/@vscode/test-electron/-/test-electron-2.2.0.tgz",
-			"integrity": "sha512-xk2xrOTMG75/hxO8OVVZ+GErv9gmdZwOD8rEHV3ty3n1Joav2yFcfrmqD6Ukref27U13LEL8gVvSHzauGAK5nQ==",
+			"version": "2.2.2",
+			"resolved": "https://registry.npmjs.org/@vscode/test-electron/-/test-electron-2.2.2.tgz",
+			"integrity": "sha512-s5d2VtMySvff0UgqkJ0BMCr1es+qREE194EAodGIefq518W53ifvv69e80l9e2MrYJEqUUKwukE/w3H9o15YEw==",
 			"dev": true,
 			"dependencies": {
 				"http-proxy-agent": "^4.0.1",
@@ -271,7 +271,7 @@
 				"unzipper": "^0.10.11"
 			},
 			"engines": {
-				"node": ">=8.9.3"
+				"node": ">=16"
 			}
 		},
 		"node_modules/@webassemblyjs/ast": {
@@ -527,9 +527,9 @@
 			}
 		},
 		"node_modules/ajv": {
-			"version": "8.11.2",
-			"resolved": "https://registry.npmjs.org/ajv/-/ajv-8.11.2.tgz",
-			"integrity": "sha512-E4bfmKAhGiSTvMfL1Myyycaub+cUEU2/IvpylXkUu7CHBkBj1f/ikdzbD7YQ6FKUbixDxeYvB/xY4fvyroDlQg==",
+			"version": "8.12.0",
+			"resolved": "https://registry.npmjs.org/ajv/-/ajv-8.12.0.tgz",
+			"integrity": "sha512-sRu1kpcO9yLtYxBKvqfTeh9KzZEwO3STyX1HT+4CaDzC6HpTGYhIhPIzj9XuKU7KYDwnaeh5hcOwjy1QuJzBPA==",
 			"dev": true,
 			"dependencies": {
 				"fast-deep-equal": "^3.1.1",
@@ -885,9 +885,9 @@
 			}
 		},
 		"node_modules/caniuse-lite": {
-			"version": "1.0.30001435",
-			"resolved": "https://registry.npmjs.org/caniuse-lite/-/caniuse-lite-1.0.30001435.tgz",
-			"integrity": "sha512-kdCkUTjR+v4YAJelyiDTqiu82BDr4W4CP5sgTA0ZBmqn30XfS2ZghPLMowik9TPhS+psWJiUNxsqLyurDbmutA==",
+			"version": "1.0.30001444",
+			"resolved": "https://registry.npmjs.org/caniuse-lite/-/caniuse-lite-1.0.30001444.tgz",
+			"integrity": "sha512-ecER9xgJQVMqcrxThKptsW0pPxSae8R2RB87LNa+ivW9ppNWRHEplXcDzkCOP4LYWGj8hunXLqaiC41iBATNyg==",
 			"dev": true,
 			"funding": [
 				{
@@ -1604,9 +1604,9 @@
 			}
 		},
 		"node_modules/fastq": {
-			"version": "1.13.0",
-			"resolved": "https://registry.npmjs.org/fastq/-/fastq-1.13.0.tgz",
-			"integrity": "sha512-YpkpUnK8od0o1hmeSc7UUs/eB/vIPWJYjKck2QKIzAf71Vm1AAQ3EbuZB3g2JIy+pg+ERD0vqI79KyZiB2e2Nw==",
+			"version": "1.15.0",
+			"resolved": "https://registry.npmjs.org/fastq/-/fastq-1.15.0.tgz",
+			"integrity": "sha512-wBrocU2LCXXa+lWBt8RoIRD89Fi8OdABODa/kEnyeyjS5aZO5/GNvI5sEINADqP/h8M29UHTHUb53sUu5Ihqdw==",
 			"dev": true,
 			"dependencies": {
 				"reusify": "^1.0.4"
@@ -1971,9 +1971,9 @@
 			]
 		},
 		"node_modules/ignore": {
-			"version": "5.2.1",
-			"resolved": "https://registry.npmjs.org/ignore/-/ignore-5.2.1.tgz",
-			"integrity": "sha512-d2qQLzTJ9WxQftPAuEQpSPmKqzxePjzVbpAVv62AQ64NTL+wR4JkrVqR/LqFsFEUsHDAiId52mJteHDFuDkElA==",
+			"version": "5.2.4",
+			"resolved": "https://registry.npmjs.org/ignore/-/ignore-5.2.4.tgz",
+			"integrity": "sha512-MAb38BcSbH0eHNBxn7ql2NH/kX33OkB3lZ1BNdh7ENeRChHTYsTvWrMubiIAMNS2llXEEgZ1MUOBtXChP3kaFQ==",
 			"dev": true,
 			"engines": {
 				"node": ">= 4"
@@ -2663,9 +2663,9 @@
 			"peer": true
 		},
 		"node_modules/node-abi": {
-			"version": "3.30.0",
-			"resolved": "https://registry.npmjs.org/node-abi/-/node-abi-3.30.0.tgz",
-			"integrity": "sha512-qWO5l3SCqbwQavymOmtTVuCWZE23++S+rxyoHjXqUmPyzRcaoI4lA2gO55/drddGnedAyjA7sk76SfQ5lfUMnw==",
+			"version": "3.31.0",
+			"resolved": "https://registry.npmjs.org/node-abi/-/node-abi-3.31.0.tgz",
+			"integrity": "sha512-eSKV6s+APenqVh8ubJyiu/YhZgxQpGP66ntzUb3lY1xB9ukSRaGnx0AIxI+IM+1+IVYC1oWobgG5L3Lt9ARykQ==",
 			"dev": true,
 			"dependencies": {
 				"semver": "^7.3.5"
@@ -2681,9 +2681,9 @@
 			"dev": true
 		},
 		"node_modules/node-releases": {
-			"version": "2.0.6",
-			"resolved": "https://registry.npmjs.org/node-releases/-/node-releases-2.0.6.tgz",
-			"integrity": "sha512-PiVXnNuFm5+iYkLBNeq5211hvO38y63T0i2KKh2KnUs3RpzJ+JtODFjkD8yjLwnDkTYF1eKXheUwdssR+NRZdg==",
+			"version": "2.0.8",
+			"resolved": "https://registry.npmjs.org/node-releases/-/node-releases-2.0.8.tgz",
+			"integrity": "sha512-dFSmB8fFHEH/s81Xi+Y/15DQY6VHW81nXRj86EMSL3lmuTmK1e+aT4wrFCkTbm+gSwkw4KpX+rT/pMM2c1mF+A==",
 			"dev": true,
 			"peer": true
 		},
@@ -2708,9 +2708,9 @@
 			}
 		},
 		"node_modules/object-inspect": {
-			"version": "1.12.2",
-			"resolved": "https://registry.npmjs.org/object-inspect/-/object-inspect-1.12.2.tgz",
-			"integrity": "sha512-z+cPxW0QGUp0mcqcsgQyLVRDoXFQbXOwBaqyF7VIgI4TWNQsDHrBpUQslRmIfAoYWdYzs6UlKJtB2XJpTaNSpQ==",
+			"version": "1.12.3",
+			"resolved": "https://registry.npmjs.org/object-inspect/-/object-inspect-1.12.3.tgz",
+			"integrity": "sha512-geUvdk7c+eizMNUDkRpW1wJwgfOiOeHbxBR/hLXK1aT6zmVSO0jsQcs7fj6MGw89jC/cjGfLcNOrtMYtGqm81g==",
 			"dev": true,
 			"funding": {
 				"url": "https://github.com/sponsors/ljharb"
@@ -2903,6 +2903,7 @@
 			"version": "1.97.0",
 			"resolved": "https://registry.npmjs.org/vsce/-/vsce-1.97.0.tgz",
 			"integrity": "sha512-5Rxj6qO0dN4FnzVS9G94osstx8R3r1OQP39G7WYERpoO9X+OSodVVkRhFDapPNjekfUNo+d5Qn7W1EtNQVoLCg==",
+			"deprecated": "vsce has been renamed to @vscode/vsce. Install using @vscode/vsce instead.",
 			"dev": true,
 			"dependencies": {
 				"azure-devops-node-api": "^11.0.1",
@@ -3187,9 +3188,9 @@
 			}
 		},
 		"node_modules/punycode": {
-			"version": "2.1.1",
-			"resolved": "https://registry.npmjs.org/punycode/-/punycode-2.1.1.tgz",
-			"integrity": "sha512-XRsRjdf+j5ml+y/6GKHPZbrF/8p2Yga0JPtdqTIY2Xe5ohJPD9saDJJLPvp9+NSBprVvevdXZybnj2cv8OEd0A==",
+			"version": "2.2.0",
+			"resolved": "https://registry.npmjs.org/punycode/-/punycode-2.2.0.tgz",
+			"integrity": "sha512-LN6QV1IJ9ZhxWTNdktaPClrNfp8xdSAYS0Zk2ddX7XsXZAxckMHPCBcHRo0cTcEIgYPRiGEkmji3Idkh2yFtYw==",
 			"dev": true,
 			"engines": {
 				"node": ">=6"
@@ -3425,9 +3426,9 @@
 			}
 		},
 		"node_modules/rxjs": {
-			"version": "7.5.7",
-			"resolved": "https://registry.npmjs.org/rxjs/-/rxjs-7.5.7.tgz",
-			"integrity": "sha512-z9MzKh/UcOqB3i20H6rtrlaE/CgjLOvheWK/9ILrbhROGTweAi1BaFsTT9FbwZi5Trr1qNRs+MXkhmR06awzQA==",
+			"version": "7.8.0",
+			"resolved": "https://registry.npmjs.org/rxjs/-/rxjs-7.8.0.tgz",
+			"integrity": "sha512-F2+gxDshqmIub1KdvZkaEfGDwLNpPvk9Fs6LD/MyQxNgMds/WH9OdDDXOmxUZpME+iSK3rQCctkL0DYyytUqMg==",
 			"dev": true,
 			"dependencies": {
 				"tslib": "^2.1.0"
@@ -3820,9 +3821,9 @@
 			}
 		},
 		"node_modules/terser": {
-			"version": "5.16.0",
-			"resolved": "https://registry.npmjs.org/terser/-/terser-5.16.0.tgz",
-			"integrity": "sha512-KjTV81QKStSfwbNiwlBXfcgMcOloyuRdb62/iLFPGBcVNF4EXjhdYBhYHmbJpiBrVxZhDvltE11j+LBQUxEEJg==",
+			"version": "5.16.1",
+			"resolved": "https://registry.npmjs.org/terser/-/terser-5.16.1.tgz",
+			"integrity": "sha512-xvQfyfA1ayT0qdK47zskQgRZeWLoOQ8JQ6mIgRGVNwZKdQMU+5FkCBjmv4QjcrTzyZquRw2FVtlJSRUmMKQslw==",
 			"dev": true,
 			"peer": true,
 			"dependencies": {
@@ -4033,9 +4034,9 @@
 			}
 		},
 		"node_modules/typescript": {
-			"version": "4.9.3",
-			"resolved": "https://registry.npmjs.org/typescript/-/typescript-4.9.3.tgz",
-			"integrity": "sha512-CIfGzTelbKNEnLpLdGFgdyKhG23CKdKgQPOBc+OUNrkJ2vr+KSzsSV5kq5iWhEQbok+quxgGzrAtGWCyU7tHnA==",
+			"version": "4.9.4",
+			"resolved": "https://registry.npmjs.org/typescript/-/typescript-4.9.4.tgz",
+			"integrity": "sha512-Uz+dTXYzxXXbsFpM86Wh3dKCxrQqUcVMxwU54orwlJjOpO3ao8L7j5lH+dWfTwgCwIuM9GQ2kvVotzYJMXTBZg==",
 			"dev": true,
 			"bin": {
 				"tsc": "bin/tsc",
@@ -4127,6 +4128,7 @@
 			"version": "2.6.7",
 			"resolved": "https://registry.npmjs.org/vsce/-/vsce-2.6.7.tgz",
 			"integrity": "sha512-5dEtdi/yzWQbOU7JDUSOs8lmSzzkewBR5P122BUkmXE6A/DEdFsKNsg2773NGXJTwwF1MfsOgUR6QVF3cLLJNQ==",
+			"deprecated": "vsce has been renamed to @vscode/vsce. Install using @vscode/vsce instead.",
 			"dev": true,
 			"dependencies": {
 				"azure-devops-node-api": "^11.0.1",
@@ -4893,9 +4895,9 @@
 			"dev": true
 		},
 		"@types/node": {
-			"version": "18.11.10",
-			"resolved": "https://registry.npmjs.org/@types/node/-/node-18.11.10.tgz",
-			"integrity": "sha512-juG3RWMBOqcOuXC643OAdSA525V44cVgGV6dUDuiFtss+8Fk5x1hI93Rsld43VeJVIeqlP9I7Fn9/qaVqoEAuQ==",
+			"version": "18.11.18",
+			"resolved": "https://registry.npmjs.org/@types/node/-/node-18.11.18.tgz",
+			"integrity": "sha512-DHQpWGjyQKSHj3ebjFI/wRKcqQcdR+MoFBygntYOZytCqNfkd2ZC4ARDJ2DQqhjH5p85Nnd3jhUJIXrszFX/JA==",
 			"dev": true
 		},
 		"@types/ps-node": {
@@ -4911,15 +4913,15 @@
 			"dev": true
 		},
 		"@types/vscode": {
-			"version": "1.73.1",
-			"resolved": "https://registry.npmjs.org/@types/vscode/-/vscode-1.73.1.tgz",
-			"integrity": "sha512-eArfOrAoZVV+Ao9zQOCaFNaeXj4kTCD+bGS2gyNgIFZH9xVMuLMlRrEkhb22NyxycFWKV1UyTh03vhaVHmqVMg==",
+			"version": "1.74.0",
+			"resolved": "https://registry.npmjs.org/@types/vscode/-/vscode-1.74.0.tgz",
+			"integrity": "sha512-LyeCIU3jb9d38w0MXFwta9r0Jx23ugujkAxdwLTNCyspdZTKUc43t7ppPbCiPoQ/Ivd/pnDFZrb4hWd45wrsgA==",
 			"dev": true
 		},
 		"@types/vscode-webview": {
-			"version": "1.57.0",
-			"resolved": "https://registry.npmjs.org/@types/vscode-webview/-/vscode-webview-1.57.0.tgz",
-			"integrity": "sha512-x3Cb/SMa1IwRHfSvKaZDZOTh4cNoG505c3NjTqGlMC082m++x/ETUmtYniDsw6SSmYzZXO8KBNhYxR0+VqymqA==",
+			"version": "1.57.1",
+			"resolved": "https://registry.npmjs.org/@types/vscode-webview/-/vscode-webview-1.57.1.tgz",
+			"integrity": "sha512-ghW5SfuDmsGDS2A4xkvGsLwDRNc3Vj5rS6rPOyPm/IryZuf3wceZKxgYaUoW+k9f0f/CB7y2c1rRsdOWZWn0PQ==",
 			"dev": true
 		},
 		"@ungap/promise-all-settled": {
@@ -4929,9 +4931,9 @@
 			"dev": true
 		},
 		"@vscode/test-electron": {
-			"version": "2.2.0",
-			"resolved": "https://registry.npmjs.org/@vscode/test-electron/-/test-electron-2.2.0.tgz",
-			"integrity": "sha512-xk2xrOTMG75/hxO8OVVZ+GErv9gmdZwOD8rEHV3ty3n1Joav2yFcfrmqD6Ukref27U13LEL8gVvSHzauGAK5nQ==",
+			"version": "2.2.2",
+			"resolved": "https://registry.npmjs.org/@vscode/test-electron/-/test-electron-2.2.2.tgz",
+			"integrity": "sha512-s5d2VtMySvff0UgqkJ0BMCr1es+qREE194EAodGIefq518W53ifvv69e80l9e2MrYJEqUUKwukE/w3H9o15YEw==",
 			"dev": true,
 			"requires": {
 				"http-proxy-agent": "^4.0.1",
@@ -5169,9 +5171,9 @@
 			}
 		},
 		"ajv": {
-			"version": "8.11.2",
-			"resolved": "https://registry.npmjs.org/ajv/-/ajv-8.11.2.tgz",
-			"integrity": "sha512-E4bfmKAhGiSTvMfL1Myyycaub+cUEU2/IvpylXkUu7CHBkBj1f/ikdzbD7YQ6FKUbixDxeYvB/xY4fvyroDlQg==",
+			"version": "8.12.0",
+			"resolved": "https://registry.npmjs.org/ajv/-/ajv-8.12.0.tgz",
+			"integrity": "sha512-sRu1kpcO9yLtYxBKvqfTeh9KzZEwO3STyX1HT+4CaDzC6HpTGYhIhPIzj9XuKU7KYDwnaeh5hcOwjy1QuJzBPA==",
 			"dev": true,
 			"requires": {
 				"fast-deep-equal": "^3.1.1",
@@ -5416,9 +5418,9 @@
 			"dev": true
 		},
 		"caniuse-lite": {
-			"version": "1.0.30001435",
-			"resolved": "https://registry.npmjs.org/caniuse-lite/-/caniuse-lite-1.0.30001435.tgz",
-			"integrity": "sha512-kdCkUTjR+v4YAJelyiDTqiu82BDr4W4CP5sgTA0ZBmqn30XfS2ZghPLMowik9TPhS+psWJiUNxsqLyurDbmutA==",
+			"version": "1.0.30001444",
+			"resolved": "https://registry.npmjs.org/caniuse-lite/-/caniuse-lite-1.0.30001444.tgz",
+			"integrity": "sha512-ecER9xgJQVMqcrxThKptsW0pPxSae8R2RB87LNa+ivW9ppNWRHEplXcDzkCOP4LYWGj8hunXLqaiC41iBATNyg==",
 			"dev": true,
 			"peer": true
 		},
@@ -5939,9 +5941,9 @@
 			"dev": true
 		},
 		"fastq": {
-			"version": "1.13.0",
-			"resolved": "https://registry.npmjs.org/fastq/-/fastq-1.13.0.tgz",
-			"integrity": "sha512-YpkpUnK8od0o1hmeSc7UUs/eB/vIPWJYjKck2QKIzAf71Vm1AAQ3EbuZB3g2JIy+pg+ERD0vqI79KyZiB2e2Nw==",
+			"version": "1.15.0",
+			"resolved": "https://registry.npmjs.org/fastq/-/fastq-1.15.0.tgz",
+			"integrity": "sha512-wBrocU2LCXXa+lWBt8RoIRD89Fi8OdABODa/kEnyeyjS5aZO5/GNvI5sEINADqP/h8M29UHTHUb53sUu5Ihqdw==",
 			"dev": true,
 			"requires": {
 				"reusify": "^1.0.4"
@@ -6197,9 +6199,9 @@
 			"dev": true
 		},
 		"ignore": {
-			"version": "5.2.1",
-			"resolved": "https://registry.npmjs.org/ignore/-/ignore-5.2.1.tgz",
-			"integrity": "sha512-d2qQLzTJ9WxQftPAuEQpSPmKqzxePjzVbpAVv62AQ64NTL+wR4JkrVqR/LqFsFEUsHDAiId52mJteHDFuDkElA==",
+			"version": "5.2.4",
+			"resolved": "https://registry.npmjs.org/ignore/-/ignore-5.2.4.tgz",
+			"integrity": "sha512-MAb38BcSbH0eHNBxn7ql2NH/kX33OkB3lZ1BNdh7ENeRChHTYsTvWrMubiIAMNS2llXEEgZ1MUOBtXChP3kaFQ==",
 			"dev": true
 		},
 		"import-local": {
@@ -6730,9 +6732,9 @@
 			"peer": true
 		},
 		"node-abi": {
-			"version": "3.30.0",
-			"resolved": "https://registry.npmjs.org/node-abi/-/node-abi-3.30.0.tgz",
-			"integrity": "sha512-qWO5l3SCqbwQavymOmtTVuCWZE23++S+rxyoHjXqUmPyzRcaoI4lA2gO55/drddGnedAyjA7sk76SfQ5lfUMnw==",
+			"version": "3.31.0",
+			"resolved": "https://registry.npmjs.org/node-abi/-/node-abi-3.31.0.tgz",
+			"integrity": "sha512-eSKV6s+APenqVh8ubJyiu/YhZgxQpGP66ntzUb3lY1xB9ukSRaGnx0AIxI+IM+1+IVYC1oWobgG5L3Lt9ARykQ==",
 			"dev": true,
 			"requires": {
 				"semver": "^7.3.5"
@@ -6745,9 +6747,9 @@
 			"dev": true
 		},
 		"node-releases": {
-			"version": "2.0.6",
-			"resolved": "https://registry.npmjs.org/node-releases/-/node-releases-2.0.6.tgz",
-			"integrity": "sha512-PiVXnNuFm5+iYkLBNeq5211hvO38y63T0i2KKh2KnUs3RpzJ+JtODFjkD8yjLwnDkTYF1eKXheUwdssR+NRZdg==",
+			"version": "2.0.8",
+			"resolved": "https://registry.npmjs.org/node-releases/-/node-releases-2.0.8.tgz",
+			"integrity": "sha512-dFSmB8fFHEH/s81Xi+Y/15DQY6VHW81nXRj86EMSL3lmuTmK1e+aT4wrFCkTbm+gSwkw4KpX+rT/pMM2c1mF+A==",
 			"dev": true,
 			"peer": true
 		},
@@ -6766,9 +6768,9 @@
 			}
 		},
 		"object-inspect": {
-			"version": "1.12.2",
-			"resolved": "https://registry.npmjs.org/object-inspect/-/object-inspect-1.12.2.tgz",
-			"integrity": "sha512-z+cPxW0QGUp0mcqcsgQyLVRDoXFQbXOwBaqyF7VIgI4TWNQsDHrBpUQslRmIfAoYWdYzs6UlKJtB2XJpTaNSpQ==",
+			"version": "1.12.3",
+			"resolved": "https://registry.npmjs.org/object-inspect/-/object-inspect-1.12.3.tgz",
+			"integrity": "sha512-geUvdk7c+eizMNUDkRpW1wJwgfOiOeHbxBR/hLXK1aT6zmVSO0jsQcs7fj6MGw89jC/cjGfLcNOrtMYtGqm81g==",
 			"dev": true
 		},
 		"once": {
@@ -7143,9 +7145,9 @@
 			}
 		},
 		"punycode": {
-			"version": "2.1.1",
-			"resolved": "https://registry.npmjs.org/punycode/-/punycode-2.1.1.tgz",
-			"integrity": "sha512-XRsRjdf+j5ml+y/6GKHPZbrF/8p2Yga0JPtdqTIY2Xe5ohJPD9saDJJLPvp9+NSBprVvevdXZybnj2cv8OEd0A==",
+			"version": "2.2.0",
+			"resolved": "https://registry.npmjs.org/punycode/-/punycode-2.2.0.tgz",
+			"integrity": "sha512-LN6QV1IJ9ZhxWTNdktaPClrNfp8xdSAYS0Zk2ddX7XsXZAxckMHPCBcHRo0cTcEIgYPRiGEkmji3Idkh2yFtYw==",
 			"dev": true
 		},
 		"qs": {
@@ -7305,9 +7307,9 @@
 			}
 		},
 		"rxjs": {
-			"version": "7.5.7",
-			"resolved": "https://registry.npmjs.org/rxjs/-/rxjs-7.5.7.tgz",
-			"integrity": "sha512-z9MzKh/UcOqB3i20H6rtrlaE/CgjLOvheWK/9ILrbhROGTweAi1BaFsTT9FbwZi5Trr1qNRs+MXkhmR06awzQA==",
+			"version": "7.8.0",
+			"resolved": "https://registry.npmjs.org/rxjs/-/rxjs-7.8.0.tgz",
+			"integrity": "sha512-F2+gxDshqmIub1KdvZkaEfGDwLNpPvk9Fs6LD/MyQxNgMds/WH9OdDDXOmxUZpME+iSK3rQCctkL0DYyytUqMg==",
 			"dev": true,
 			"requires": {
 				"tslib": "^2.1.0"
@@ -7579,9 +7581,9 @@
 			}
 		},
 		"terser": {
-			"version": "5.16.0",
-			"resolved": "https://registry.npmjs.org/terser/-/terser-5.16.0.tgz",
-			"integrity": "sha512-KjTV81QKStSfwbNiwlBXfcgMcOloyuRdb62/iLFPGBcVNF4EXjhdYBhYHmbJpiBrVxZhDvltE11j+LBQUxEEJg==",
+			"version": "5.16.1",
+			"resolved": "https://registry.npmjs.org/terser/-/terser-5.16.1.tgz",
+			"integrity": "sha512-xvQfyfA1ayT0qdK47zskQgRZeWLoOQ8JQ6mIgRGVNwZKdQMU+5FkCBjmv4QjcrTzyZquRw2FVtlJSRUmMKQslw==",
 			"dev": true,
 			"peer": true,
 			"requires": {
@@ -7731,9 +7733,9 @@
 			}
 		},
 		"typescript": {
-			"version": "4.9.3",
-			"resolved": "https://registry.npmjs.org/typescript/-/typescript-4.9.3.tgz",
-			"integrity": "sha512-CIfGzTelbKNEnLpLdGFgdyKhG23CKdKgQPOBc+OUNrkJ2vr+KSzsSV5kq5iWhEQbok+quxgGzrAtGWCyU7tHnA==",
+			"version": "4.9.4",
+			"resolved": "https://registry.npmjs.org/typescript/-/typescript-4.9.4.tgz",
+			"integrity": "sha512-Uz+dTXYzxXXbsFpM86Wh3dKCxrQqUcVMxwU54orwlJjOpO3ao8L7j5lH+dWfTwgCwIuM9GQ2kvVotzYJMXTBZg==",
 			"dev": true
 		},
 		"uc.micro": {
diff --git a/vscode-lean4/package.json b/vscode-lean4/package.json
index e9b1e06e8..9a6956b8a 100644
--- a/vscode-lean4/package.json
+++ b/vscode-lean4/package.json
@@ -404,8 +404,8 @@
 		"test": "node ./out/test/suite/runTest.js"
 	},
 	"dependencies": {
-		"@leanprover/infoview": "~0.4.0",
-		"@leanprover/infoview-api": "~0.2.0",
+		"@leanprover/infoview": "~0.4.2",
+		"@leanprover/infoview-api": "~0.2.1",
 		"axios": "~0.24.0",
 		"cheerio": "^1.0.0-rc.10",
 		"mobx": "5.15.7",

From f63862ed3941cc6bbb190e9be2dde3bb32693c1e Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Sat, 14 Jan 2023 17:07:39 -0500
Subject: [PATCH 13/13] fix: ensure InteractiveCode uses code font

---
 lean4-infoview/src/infoview/interactiveCode.tsx | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx
index c3d6672c8..f719b074f 100644
--- a/lean4-infoview/src/infoview/interactiveCode.tsx
+++ b/lean4-infoview/src/infoview/interactiveCode.tsx
@@ -193,5 +193,7 @@ export type InteractiveCodeProps = InteractiveTextComponentProps<SubexprInfo>
 
 /** Displays a {@link CodeWithInfos} obtained via RPC from the Lean server. */
 export function InteractiveCode(props: InteractiveCodeProps) {
-  return InteractiveTaggedText({...props, InnerTagUi: InteractiveCodeTag})
+  return <span className='font-code'>
+    <InteractiveTaggedText {...props} InnerTagUi={InteractiveCodeTag} />
+  </span>
 }