fix: refactor userwidget api

To satisfy leanprover/lean4#1238 (comment)
Vtec234 · Jul 20, 2022 · d1eef2d · d1eef2d
1 parent 9501eba
commit d1eef2d
Show file tree

Hide file tree

Showing 3 changed files with 23 additions and 19 deletions.
diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx
@@ -205,10 +205,10 @@ export function InfoDisplay(props0: InfoDisplayProps) {
             </div>
             {widgets && widgets.map(widget =>
                 <div style={{display: hasWidget ? 'block' : 'none'}}
-                     key={`widget::${widget.widgetSourceId}::${widget.range?.toString()}`}>
+                     key={`widget::${widget.id}::${widget.range?.toString()}`}>
                     <Details initiallyOpen>
                         <summary className="mv2 pointer">
-                            Widget: {widget.widgetSourceId}
+                            {widget.name}
                         </summary>
                         <div className="ml1">
                              <UserWidget pos={pos} widget={widget}/>

diff --git a/lean4-infoview/src/infoview/rpcInterface.ts b/lean4-infoview/src/infoview/rpcInterface.ts
@@ -185,24 +185,28 @@ export async function getGoToLocation(rs: RpcSessions, pos: DocumentPosition, ki
     return rs.call<LocationLink[]>(pos, 'Lean.Widget.getGoToLocation', args)
 }
 
-/** Represents an instance of a user widget that can be rendered.
- * This is used as the input to the `UserWidget` component.
- */
 export interface UserWidget {
-    /** The identifier of the type of widget to dynamically load. */
-    widgetSourceId: string
+    id: string;
+    /** Pretty user name. */
+    name: string;
     /** A hash (provided by Lean) of the widgetSource's sourcetext.
      * This is used to look up the WidgetSource object.
      */
-    hash : string
+    javascriptHash: string;
+}
+
+/** Represents an instance of a user widget that can be rendered.
+ * This is used as the input to the `UserWidget` component.
+ */
+export interface UserWidgetInstance extends UserWidget {
     /** JSON object to be passed as props to the component */
     props : any
     range?: Range
 }
 
 /** The response type for the RPC call `Widget_getWidgets`. */
 export interface UserWidgets {
-    widgets : UserWidget[]
+    widgets : UserWidgetInstance[]
 }
 
 /** Given a position, returns all of the user-widgets on the infotree at this position. */
@@ -216,7 +220,6 @@ export interface WidgetSource {
      * the component to render.
      */
     sourcetext: string
-    hash: string
 }
 
 /** Gets the static code for a given widget.

diff --git a/lean4-infoview/src/infoview/userWidget.tsx b/lean4-infoview/src/infoview/userWidget.tsx
@@ -3,7 +3,7 @@ import * as React from 'react';
 import { RpcContext } from './contexts';
 import { DocumentPosition, mapRpcError, useAsync } from './util';
 import { ErrorBoundary } from './errors';
-import { Widget_getWidgetSource, UserWidget } from './rpcInterface';
+import { Widget_getWidgetSource, UserWidget, UserWidgetInstance } from './rpcInterface';
 
 function dynamicallyLoadComponent(hash: string, code: string) {
     return React.lazy(async () => {
@@ -17,31 +17,32 @@ const componentCache = new Map<string,  React.LazyExoticComponent<React.Componen
 
 interface UserWidgetProps {
     pos: DocumentPosition
-    widget: UserWidget
+    widget: UserWidgetInstance
 }
 
 export function UserWidget({ pos, widget }: UserWidgetProps) {
     const rs = React.useContext(RpcContext);
+    const hash = widget.javascriptHash
     const [status, component, error] = useAsync(
         async () => {
-            if (componentCache.has(widget.hash)) {
-                return componentCache.get(widget.hash)
+            if (componentCache.has(hash)) {
+                return componentCache.get(hash)
             }
-            const code = await Widget_getWidgetSource(rs, pos, widget.hash)
+            const code = await Widget_getWidgetSource(rs, pos, hash)
             if (!code) {
                 // This case happens when the relevant RPC session is not connected, a react rerender will be triggered.
                 throw new Error('Expected RPC session to be connected.')
             }
-            const component = dynamicallyLoadComponent(widget.hash, code.sourcetext)
-            componentCache.set(widget.hash, component)
+            const component = dynamicallyLoadComponent(hash, code.sourcetext)
+            componentCache.set(hash, component)
             return component
         },
-        [widget.hash])
+        [hash])
 
     const componentProps = { pos, ...widget.props }
 
     return (
-        <React.Suspense fallback={`Loading widget: ${ widget.widgetSourceId} ${status}.`}>
+        <React.Suspense fallback={`Loading widget: ${widget.id} ${status}.`}>
             <ErrorBoundary>
                 {component && <div>{React.createElement(component, componentProps)}</div>}
                 {error && <div>{mapRpcError(error).message}</div>}