feat: use api from RFC

leanprover/lean4#1225

lean4-infoview/src/infoview/info.tsx

@@ -9,7 +9,7 @@ import { MessagesList, useMessagesFor } from './messages';
 import { getInteractiveGoals, getInteractiveTermGoal, InteractiveDiagnostic, InteractiveGoal, InteractiveGoals } from './rpcInterface';
 import { updatePlainGoals, updateTermGoal } from './goalCompat';
 import { WithTooltipOnHover } from './tooltips'
-import { isGetWidgetResponse, UserWidget, useWidget, Widget_getWidget} from './userWidget'
+import { UserWidget, Widget_getWidgetInfos} from './userWidget'
 
 type InfoStatus = 'loading' | 'updating' | 'error' | 'ready';
 type InfoKind = 'cursor' | 'pin';
@@ -125,9 +125,11 @@ export function InfoDisplay(props0: InfoDisplayProps) {
     });
 
     const rs = React.useContext(RpcContext);
-    const [widgetStatus, widget, widgetError] = useAsync(
-        () => Widget_getWidget(rs, pos),
+    const [widgetStatus, widgets, widgetError] = useAsync(
+        () => Widget_getWidgetInfos(rs, pos),
         [pos.uri, pos.line, pos.character])
+    // [todo] for now just show the first widget.
+    const widget = (widgets !== undefined) && (widgets.infos.length > 0) && widgets.infos[0]
     const hasWidget = (widget !== undefined)
 
     const nothingToShow = !error && !goals && !termGoal && messages.length === 0 && !hasWidget;
@@ -215,7 +217,7 @@ export function InfoDisplay(props0: InfoDisplayProps) {
             <div style={{display: hasWidget ? 'block' : 'none'}}>
                 <Details initiallyOpen>
                     <summary className="mv2 pointer">
-                    Widget: {widget && widget.id}
+                    Widget: {widget && widget.widgetSourceId}
                       {widgetStatus === 'pending' && ' (pending)'}
                       {widgetStatus === 'rejected' && ' (errored)'}
                     </summary>

lean4-infoview/src/infoview/userWidget.tsx

@@ -8,12 +8,6 @@ import { ErrorBoundary } from './errors';
 import { RpcSessions } from './rpcSessions';
 import { isRpcError, RpcErrorCode } from '@lean4/infoview-api';
 
-export interface GetWidgetResponse {
-    id: string
-    hash: number
-    props: any
-}
-
 function handleWidgetRpcError(e: unknown): undefined {
     if (isRpcError(e)) {
         if (e.code === RpcErrorCode.MethodNotFound || e.code === RpcErrorCode.InvalidParams) {
@@ -28,29 +22,41 @@ function handleWidgetRpcError(e: unknown): undefined {
     }
 }
 
-export function Widget_getWidget(rs: RpcSessions, pos: DocumentPosition): Promise<GetWidgetResponse | undefined> {
-    return rs.call<GetWidgetResponse | undefined>(pos, 'Lean.Widget.getWidget', DocumentPosition.toTdpp(pos))
+export interface UserWidgetInfo {
+    widgetSourceId: string
+    hash : string
+    props : any
+    range?: Range
+}
+
+export interface GetWidgetInfosResponse {
+    infos : UserWidgetInfo[]
+}
+
+export function Widget_getWidgetInfos(rs: RpcSessions, pos: DocumentPosition): Promise<GetWidgetInfosResponse | undefined> {
+    return rs.call<GetWidgetInfosResponse | undefined>(pos, 'Lean.Widget.getWidgetInfos', DocumentPosition.toTdpp(pos))
         .catch<undefined>(handleWidgetRpcError);
 }
 
-export interface StaticJS {
-    javascript: string
-    hash: number
+export interface WidgetSource {
+    widgetSourceId : string
+    sourcetext : string
+    hash: string
 }
 
 /** Gets the static JS code for a given widget.
  *
  * We make the assumption that either the code doesn't exist, or it exists and does not change for the lifetime of the widget.
  */
-export async function Widget_getStaticJS(rs: RpcSessions, pos: DocumentPosition, widgetId: string): Promise<StaticJS | undefined> {
+export async function Widget_getWidgetSource(rs: RpcSessions, pos: DocumentPosition, widgetSourceId: string): Promise<WidgetSource | undefined> {
     try {
-        return await rs.call(pos, 'Lean.Widget.getStaticJS', { 'pos': DocumentPosition.toTdpp(pos), widgetId })
+        return await rs.call(pos, 'Lean.Widget.getWidgetSource', { 'pos': DocumentPosition.toTdpp(pos), widgetSourceId })
     } catch (e) {
         return handleWidgetRpcError(e)
     }
 }
 
-function dynamicallyLoadComponent(hash: number, code: string,) {
+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)
@@ -62,7 +68,7 @@ const componentCache = new Map()
 
 interface UserWidgetProps {
     pos: DocumentPosition
-    widget: GetWidgetResponse
+    widget: UserWidgetInfo
 }
 
 export function UserWidget({ pos, widget }: UserWidgetProps) {
@@ -75,21 +81,20 @@ export function UserWidget({ pos, widget }: UserWidgetProps) {
             if (componentCache.has(widget.hash)) {
                 return componentCache.get(widget.hash)
             }
-            const code = await Widget_getStaticJS(rs, pos, widget.id)
+            const code = await Widget_getWidgetSource(rs, pos, widget.widgetSourceId)
             if (!code) {
-                throw Error(`No widget static javascript found for ${widget.id}.`)
+                throw Error(`No widget static javascript found for ${widget.widgetSourceId}.`)
             }
-            const component = dynamicallyLoadComponent(widget.hash, code.javascript)
+            const component = dynamicallyLoadComponent(widget.hash, code.sourcetext)
             componentCache.set(widget.hash, component)
             return component
         },
         [pos.uri, pos.line, pos.character, widget.hash])
 
-    const widgetId = widget.id
     const componentProps = { pos, ...widget.props }
 
     return (
-        <React.Suspense fallback={`Loading widget: ${widgetId} ${status}.`}>
+        <React.Suspense fallback={`Loading widget: ${ widget.widgetSourceId} ${status}.`}>
             <ErrorBoundary>
                 {component && <div>{React.createElement(component, componentProps)}</div>}
                 {error && <div>{mapRpcError(error).message}</div>}