feat: user widgets

lean4-infoview-api/src/rpcApi.ts

@@ -5,7 +5,7 @@
  * @module
  */
 
-import type { LocationLink, TextDocumentPositionParams } from 'vscode-languageserver-protocol'
+import type { LocationLink, Position, Range, TextDocumentPositionParams } from 'vscode-languageserver-protocol'
 import { LeanDiagnostic, RpcPtr } from './lspTypes'
 import { RpcSessionAtPos } from './rpcSessions'
 
@@ -22,6 +22,7 @@ export interface SubexprInfo {
     subexprPos?: number
 }
 
+/** A piece of code pretty-printed with subexpression information by the Lean server. */
 export type CodeWithInfos = TaggedText<SubexprInfo>
 
 /** Information that should appear in a popup when clicking on a subexpression. */
@@ -105,3 +106,52 @@ export function getGoToLocation(rs: RpcSessionAtPos, kind: GoToKind, info: InfoW
     }
     return rs.call<GetGoToLocationParams, LocationLink[]>('Lean.Widget.getGoToLocation', { kind, info });
 }
+
+export interface UserWidget {
+    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.
+     */
+    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 : UserWidgetInstance[]
+}
+
+/** Given a position, returns all of the user-widgets on the infotree at this position. */
+export function Widget_getWidgets(rs: RpcSessionAtPos, pos: Position): Promise<UserWidgets> {
+    return rs.call<Position, UserWidgets>('Lean.Widget.getWidgets', pos)
+}
+
+/** Code that should be dynamically loaded by the UserWidget component. */
+export interface WidgetSource {
+    /** JavaScript sourcecode. Should be a plain JavaScript ESModule whose default export is
+     * the component to render.
+     */
+    sourcetext: string
+}
+
+/** Gets the static 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 function Widget_getWidgetSource(rs: RpcSessionAtPos, pos: Position, hash: string): Promise<WidgetSource> {
+    interface GetWidgetSourceParams {
+        hash: string
+        pos: Position
+    }
+    return rs.call<GetWidgetSourceParams, WidgetSource>('Lean.Widget.getWidgetSource', { pos, hash })
+}

lean4-infoview/src/components.tsx

@@ -1,9 +1,19 @@
 import * as React from 'react';
 
+import { InteractiveDiagnostics_msgToInteractive, MessageData } from '@lean4/infoview-api';
 import { InteractiveMessage } from './infoview/traceExplorer';
 import { useAsync, mapRpcError } from './infoview/util';
 import { RpcContext } from './infoview/rpcSessions';
-import { InteractiveDiagnostics_msgToInteractive, MessageData } from '@lean4/infoview-api';
+
+export * from '@lean4/infoview-api';
+export * 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 { InteractiveCode, InteractiveCodeProps } from './infoview/interactiveCode';
+
 
 /** Display the given message data as interactive, pretty-printed text. */
 export function InteractiveMessageData({ msg }: { msg: MessageData }) {

lean4-infoview/src/infoview/collapsing.tsx

@@ -37,8 +37,9 @@ export function Details({initiallyOpen, children: [summary, ...children], setOpe
         }
     }, []);
     if (setOpenRef) setOpenRef.current = setOpen;
-    return <details ref={setupEventListener} open={isOpen}>
+    /* HACK: `as any` works around a bug in `@types/react` */
+    return <details ref={setupEventListener as any} open={isOpen}>
         {summary}
         { isOpen && children }
     </details>;
-}
+}

lean4-infoview/src/infoview/info.tsx

@@ -2,13 +2,15 @@ import * as React from 'react';
 import type { Location } from 'vscode-languageserver-protocol';
 
 import { Goals as GoalsUi, Goal as GoalUi, goalsToString, GoalFilterState } from './goals';
-import { basename, DocumentPosition, RangeHelpers, useEvent, usePausableState } from './util';
+import { basename, DocumentPosition, RangeHelpers, useEvent, usePausableState, useClientNotificationEffect, discardMethodNotFound, mapRpcError } from './util';
 import { Details } from './collapsing';
 import { EditorContext, ProgressContext, VersionContext } from './contexts';
 import { MessagesList, useMessagesFor } from './messages';
-import { getInteractiveGoals, getInteractiveTermGoal, InteractiveDiagnostic, InteractiveGoal, InteractiveGoals, RpcSessionAtPos } from '@lean4/infoview-api';
+import { getInteractiveGoals, getInteractiveTermGoal, InteractiveDiagnostic, InteractiveGoal,
+    InteractiveGoals, UserWidgets, Widget_getWidgets, RpcSessionAtPos, isRpcError, RpcErrorCode } from '@lean4/infoview-api';
 import { updatePlainGoals, updateTermGoal } from './goalCompat';
 import { WithTooltipOnHover } from './tooltips'
+import { UserWidget } from './userWidget'
 import { RpcContext, useRpcSessionAtPos } from './rpcSessions';
 
 type InfoStatus = 'loading' | 'updating' | 'error' | 'ready';
@@ -85,6 +87,7 @@ interface InfoDisplayProps extends InfoPinnable {
     goals?: InteractiveGoals;
     termGoal?: InteractiveGoal;
     error?: string;
+    userWidgets?: UserWidgets;
     rpcSess: RpcSessionAtPos;
     messagesRpcSess: RpcSessionAtPos;
     triggerUpdate: () => Promise<void>;
@@ -103,9 +106,10 @@ export function InfoDisplay(props0: InfoDisplayProps) {
         await props0.triggerUpdate();
         setShouldRefresh(true);
     };
-    const [goalFilters, setGoalFilters] = React.useState<GoalFilterState>({ reverse: false, isType: true, isInstance: true, isHiddenAssumption: true});
+    const [goalFilters, setGoalFilters] = React.useState<GoalFilterState>(
+        { reverse: false, isType: true, isInstance: true, isHiddenAssumption: true});
 
-    const {kind, pos, status, messages, goals, termGoal, error, rpcSess, messagesRpcSess} = props;
+    const {kind, pos, status, messages, goals, termGoal, error, userWidgets, rpcSess, messagesRpcSess} = props;
 
     const ec = React.useContext(EditorContext);
     let copyGoalToComment: (() => void) | undefined
@@ -125,7 +129,12 @@ export function InfoDisplay(props0: InfoDisplayProps) {
         setPaused(isPaused => !isPaused);
     });
 
-    const nothingToShow = !error && !goals && !termGoal && messages.length === 0;
+    const rs = React.useContext(RpcContext);
+
+    const widgets = userWidgets && userWidgets.widgets
+    const hasWidget = (widgets !== undefined) && (widgets.length > 0)
+
+    const nothingToShow = !error && !goals && !termGoal && messages.length === 0 && !hasWidget;
 
     const hasError = status === 'error' && error;
     const hasGoals = status !== 'error' && goals;
@@ -174,11 +183,11 @@ export function InfoDisplay(props0: InfoDisplayProps) {
         <InfoStatusBar {...props} triggerUpdate={triggerDisplayUpdate} isPaused={isPaused} setPaused={setPaused} copyGoalToComment={copyGoalToComment} />
         <div className="ml1">
             {hasError &&
-                <div className="error">
+                <div className="error" key="errors">
                     Error updating:{' '}{error}.
                     <a className="link pointer dim" onClick={e => { e.preventDefault(); void triggerDisplayUpdate(); }}>{' '}Try again.</a>
                 </div>}
-            <div style={{display: hasGoals ? 'block' : 'none'}}>
+            <div style={{display: hasGoals ? 'block' : 'none'}} key="goals">
                 <Details initiallyOpen>
                     <summary className="mv2 pointer">
                         Tactic state {sortButton} {filterButton}
@@ -188,7 +197,7 @@ export function InfoDisplay(props0: InfoDisplayProps) {
                     </div>
                 </Details>
             </div>
-            <div style={{display: hasTermGoal ? 'block' : 'none'}}>
+            <div style={{display: hasTermGoal ? 'block' : 'none'}} key="term-goal">
                 <Details initiallyOpen>
                     <summary className="mv2 pointer">
                         Expected type {sortButton} {filterButton}
@@ -198,8 +207,21 @@ export function InfoDisplay(props0: InfoDisplayProps) {
                     </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">
+                             <UserWidget pos={pos} widget={widget}/>
+                        </div>
+                    </Details>
+                </div>
+            )}
             <RpcContext.Provider value={messagesRpcSess}>
-            <div style={{display: hasMessages ? 'block' : 'none'}}>
+            <div style={{display: hasMessages ? 'block' : 'none'}} key="messages">
                 <Details initiallyOpen>
                     <summary className="mv2 pointer">
                         Messages ({messages.length})
@@ -292,6 +314,7 @@ function InfoAux(props: InfoProps) {
     const [status, setStatus] = React.useState<InfoStatus>('loading');
     const [goals, setGoals] = React.useState<InteractiveGoals>();
     const [termGoal, setTermGoal] = React.useState<InteractiveGoal>();
+    const [userWidgets, setUserWidgets] = React.useState<UserWidgets>();
     const [error, setError] = React.useState<string>();
 
     // RPC session used for the update
@@ -304,7 +327,7 @@ function InfoAux(props: InfoProps) {
 
     // We encapsulate `InfoDisplay` props in a single piece of state for atomicity, in particular
     // to avoid displaying a new position before the server has sent us all the goal state there.
-    const mkDisplayProps = () => ({ ...props, pos, goals, termGoal, error, rpcSess });
+    const mkDisplayProps = () => ({ ...props, pos, goals, termGoal, error, rpcSess, userWidgets });
     const [displayProps, setDisplayProps] = React.useState(mkDisplayProps());
     const [shouldUpdateDisplay, setShouldUpdateDisplay] = React.useState(false);
     if (shouldUpdateDisplay) {
@@ -315,12 +338,17 @@ function InfoAux(props: InfoProps) {
     const triggerUpdate = useDelayedThrottled(serverIsProcessing ? 500 : 50, async () => {
         setStatus('updating');
 
-        let allReq
+        let allReq : Promise<[
+            InteractiveGoals | undefined,
+            InteractiveGoal | undefined,
+            UserWidgets | undefined
+        ]>
         if (sv?.hasWidgetsV1()) {
-            // Start both goal requests before awaiting them.
+            // Start all requests before awaiting them.
             const goalsReq = getInteractiveGoals(rpcSess0, DocumentPosition.toTdpp(pos));
             const termGoalReq = getInteractiveTermGoal(rpcSess0, DocumentPosition.toTdpp(pos));
-            allReq = Promise.all([goalsReq, termGoalReq]);
+            const userWidgets = Widget_getWidgets(rpcSess0, pos).catch(discardMethodNotFound);
+            allReq = Promise.all([goalsReq, termGoalReq, userWidgets]);
         } else {
             const goalsReq = ec.requestPlainGoal(pos).then(gs => {
                 if (gs) return updatePlainGoals(gs)
@@ -330,36 +358,47 @@ function InfoAux(props: InfoProps) {
                 if (g) return updateTermGoal(g)
                 else return undefined
             }).catch(() => undefined) // ignore error on Lean version that don't support term goals yet
-            allReq = Promise.all([goalsReq, termGoalReq]);
-        }
-
-        function onError(err: any) {
-            const errS = typeof err === 'string' ? err : JSON.stringify(err);
-            // we need to check if this value is empty or not, because maybe we are assigning
-            // a message error with an empty error
-            if (errS === '{}' || errS === undefined) {
-                setError(undefined);
-            }
-            else {
-                setError(`Error fetching goals: ${errS}`);
-                setStatus('error');
-            }
+            allReq = Promise.all([
+                goalsReq,
+                termGoalReq,
+                undefined
+            ]);
         }
 
         try {
             // NB: it is important to await both reqs at once, otherwise
             // if both throw then one exception becomes unhandled.
-            const [goals, termGoal] = await allReq;
+            const [goals, termGoal, userWidgets] = await allReq;
             setGoals(goals);
             setTermGoal(termGoal);
+            setUserWidgets(userWidgets);
             setRpcSess(rpcSess0);
             setStatus('ready');
         } catch (err: any) {
-            if (err?.code === -32801) {
+            if (isRpcError(err) && err.code === RpcErrorCode.ContentModified) {
                 // Document has been changed since we made the request, try again
                 void triggerUpdate();
                 return;
-            } else { onError(err); }
+            }
+            let errorString : string;
+            if (typeof error === 'string') {
+                errorString = error
+            } else if (isRpcError(err)) {
+                errorString = mapRpcError(err).message
+            } else if (err instanceof Error) {
+                errorString = err.toString()
+            } else if (err === undefined || JSON.stringify(err) === '{}')  {
+                // we need to check if this value is empty or not, because maybe we are assigning
+                // a message error with an empty error
+                setError(undefined);
+                return;
+            } else {
+                // unrecognised error
+                errorString = `Unrecognised error: ${JSON.stringify(err)}`
+            }
+
+            setError(`Error fetching goals: ${errorString}`);
+            setStatus('error');
         }
         setShouldUpdateDisplay(true);
     });

lean4-infoview/src/infoview/interactiveCode.tsx

@@ -146,10 +146,11 @@ function InteractiveCodeTag({tag: ct, fmt}: InteractiveTagProps<SubexprInfo>) {
   )
 }
 
-interface InteractiveCodeProps {
+export interface InteractiveCodeProps {
   fmt: CodeWithInfos
 }
 
+/** Displays a {@link CodeWithInfos} obtained via RPC from the Lean server. */
 export function InteractiveCode({fmt}: InteractiveCodeProps) {
   return <InteractiveTaggedText InnerTagUi={InteractiveCodeTag} fmt={fmt} />
 }

lean4-infoview/src/infoview/userWidget.tsx

@@ -0,0 +1,48 @@
+import * as React from 'react';
+
+import { Widget_getWidgetSource, UserWidget, UserWidgetInstance } from '@lean4/infoview-api';
+import { RpcContext } from './rpcSessions';
+import { DocumentPosition, mapRpcError, useAsync } from './util';
+import { ErrorBoundary } from './errors';
+
+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)
+    })
+}
+
+const componentCache = new Map<string, React.LazyExoticComponent<React.ComponentType<any>>>()
+
+interface UserWidgetProps {
+    pos: DocumentPosition
+    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(hash)) {
+                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 = { pos, ...widget.props }
+
+    return (
+        <React.Suspense fallback={`Loading widget: ${widget.id} ${status}.`}>
+            <ErrorBoundary>
+                {component && <div>{React.createElement(component, componentProps)}</div>}
+                {error && <div>{mapRpcError(error).message}</div>}
+            </ErrorBoundary>
+        </React.Suspense>
+    )
+}

lean4-infoview/src/infoview/util.ts

@@ -279,6 +279,17 @@ export function mapRpcError(err : unknown) : Error {
     }
 }
 
+/** Catch handler for RPC methods that just returns undefined if the method is not found.
+ * This is useful for compatibility with versions of Lean that do not yet have the given RPC method.
+*/
+ export function discardMethodNotFound(e: unknown) : undefined {
+  if (isRpcError(e) && (e.code === RpcErrorCode.MethodNotFound)) {
+    return undefined
+  } else {
+      throw mapRpcError(e)
+  }
+}
+
 type Status = 'pending' | 'fulfilled' | 'rejected'