From a09d19a78fd3d1c9409505164b610cf36edff7e7 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <wjnawrocki@protonmail.com>
Date: Thu, 21 Dec 2023 14:23:46 +0100
Subject: [PATCH] feat: optional user widget names (#376)

* feat: optional user widget names

* chore: fix doc
---
 lean4-infoview-api/src/rpcApi.ts     |  5 +++--
 lean4-infoview/src/infoview/info.tsx | 23 ++++++++++++++++-------
 2 files changed, 19 insertions(+), 9 deletions(-)

diff --git a/lean4-infoview-api/src/rpcApi.ts b/lean4-infoview-api/src/rpcApi.ts
index 61f602a26..55835eb1c 100644
--- 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
index 1b577a5df..0c797e9d8 100644
--- 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>