feat: optional user widget names (#376)

* feat: optional user widget names * chore: fix doc
leanprover · Dec 21, 2023 · a09d19a · a09d19a
1 parent 23c9571
commit a09d19a
Show file tree

Hide file tree

Showing 2 changed files with 19 additions and 9 deletions.
diff --git a/lean4-infoview-api/src/rpcApi.ts b/lean4-infoview-api/src/rpcApi.ts
@@ -153,8 +153,9 @@ export function getGoToLocation(rs: RpcSessionAtPos, kind: GoToKind, info: InfoW
 
 export interface UserWidget {
     id: string;
-    /** Pretty user name. */
-    name: string;
+    /** Newer widget APIs do not send this.
+     * In previous versions, it used to be a user-readable name to show in a title bar. */
+    name?: string;
     /** A hash (provided by Lean) of the widgetSource's sourcetext.
      * This is used to look up the WidgetSource object.
      */

diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx
@@ -130,13 +130,22 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
             initiallyOpen={config.showExpectedType}
             displayCount={false}
             togglingAction='toggleExpectedType' />
-        {userWidgets.map(widget =>
-            <details key={`widget::${widget.id}::${widget.range?.toString()}`} open>
-                <summary className='mv2 pointer'>{widget.name}</summary>
-                <PanelWidgetDisplay pos={pos} goals={goals ? goals.goals : []} termGoal={termGoal}
-                    selectedLocations={selectedLocs} widget={widget}/>
-            </details>
-        )}
+        {userWidgets.map(widget => {
+            const inner =
+                <PanelWidgetDisplay key={`widget::${widget.id}::${widget.range?.toString()}`}
+                    pos={pos}
+                    goals={goals ? goals.goals : []}
+                    termGoal={termGoal}
+                    selectedLocations={selectedLocs}
+                    widget={widget} />
+            if (widget.name)
+                return <details key={`widget::${widget.id}::${widget.range?.toString()}`} open>
+                    <summary className='mv2 pointer'>{widget.name}</summary>
+                    {inner}
+                </details>
+            else
+                return inner
+        })}
         <div style={{display: hasMessages ? 'block' : 'none'}} key='messages'>
             <details key='messages' open>
                 <summary className='mv2 pointer'>Messages ({messages.length})</summary>