diff --git a/lean4-infoview-api/src/rpcApi.ts b/lean4-infoview-api/src/rpcApi.ts index a1358d001..f76777dc9 100644 --- a/lean4-infoview-api/src/rpcApi.ts +++ b/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 /** 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('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 { + return rs.call('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 { + interface GetWidgetSourceParams { + hash: string + pos: Position + } + return rs.call('Lean.Widget.getWidgetSource', { pos, hash }) +} diff --git a/lean4-infoview/src/components.tsx b/lean4-infoview/src/components.tsx index 9b78533af..0356423f7 100644 --- a/lean4-infoview/src/components.tsx +++ b/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 }) { diff --git a/lean4-infoview/src/infoview/collapsing.tsx b/lean4-infoview/src/infoview/collapsing.tsx index 17e7838dd..ded9ffdf6 100644 --- a/lean4-infoview/src/infoview/collapsing.tsx +++ b/lean4-infoview/src/infoview/collapsing.tsx @@ -37,8 +37,9 @@ export function Details({initiallyOpen, children: [summary, ...children], setOpe } }, []); if (setOpenRef) setOpenRef.current = setOpen; - return
+ /* HACK: `as any` works around a bug in `@types/react` */ + return
{summary} { isOpen && children }
; -} \ No newline at end of file +} diff --git a/lean4-infoview/src/infoview/info.tsx b/lean4-infoview/src/infoview/info.tsx index ec78f5ffe..82ae82bf7 100644 --- a/lean4-infoview/src/infoview/info.tsx +++ b/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; @@ -103,9 +106,10 @@ export function InfoDisplay(props0: InfoDisplayProps) { await props0.triggerUpdate(); setShouldRefresh(true); }; - const [goalFilters, setGoalFilters] = React.useState({ reverse: false, isType: true, isInstance: true, isHiddenAssumption: true}); + const [goalFilters, setGoalFilters] = React.useState( + { 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) {
{hasError && -
+ } -
+
Tactic state {sortButton} {filterButton} @@ -188,7 +197,7 @@ export function InfoDisplay(props0: InfoDisplayProps) {
-
+
Expected type {sortButton} {filterButton} @@ -198,8 +207,21 @@ export function InfoDisplay(props0: InfoDisplayProps) {
+ {widgets && widgets.map(widget => +
+
+ + {widget.name} + +
+ +
+
+
+ )} -
+
Messages ({messages.length}) @@ -292,6 +314,7 @@ function InfoAux(props: InfoProps) { const [status, setStatus] = React.useState('loading'); const [goals, setGoals] = React.useState(); const [termGoal, setTermGoal] = React.useState(); + const [userWidgets, setUserWidgets] = React.useState(); const [error, setError] = React.useState(); // 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); }); diff --git a/lean4-infoview/src/infoview/interactiveCode.tsx b/lean4-infoview/src/infoview/interactiveCode.tsx index 5830cb444..6f700ed9d 100644 --- a/lean4-infoview/src/infoview/interactiveCode.tsx +++ b/lean4-infoview/src/infoview/interactiveCode.tsx @@ -146,10 +146,11 @@ function InteractiveCodeTag({tag: ct, fmt}: InteractiveTagProps) { ) } -interface InteractiveCodeProps { +export interface InteractiveCodeProps { fmt: CodeWithInfos } +/** Displays a {@link CodeWithInfos} obtained via RPC from the Lean server. */ export function InteractiveCode({fmt}: InteractiveCodeProps) { return } diff --git a/lean4-infoview/src/infoview/userWidget.tsx b/lean4-infoview/src/infoview/userWidget.tsx new file mode 100644 index 000000000..fb4aeda73 --- /dev/null +++ b/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>>() + +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 ( + + + {component &&
{React.createElement(component, componentProps)}
} + {error &&
{mapRpcError(error).message}
} + + + ) +} diff --git a/lean4-infoview/src/infoview/util.ts b/lean4-infoview/src/infoview/util.ts index f8657f1ee..c1815e664 100644 --- a/lean4-infoview/src/infoview/util.ts +++ b/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'