doc: docstrings for rpc

leanprover · Jun 23, 2022 · 45e21a0 · 45e21a0
1 parent 61ac5fd
commit 45e21a0
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 8 deletions.
diff --git a/lean4-infoview/src/infoview/rpcInterface.ts b/lean4-infoview/src/infoview/rpcInterface.ts
@@ -185,22 +185,36 @@ 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
+    /** A hash (provided by Lean) of the widgetSource's sourcetext.
+     * This is used to look up the WidgetSource object.
+     */
     hash : string
+    /** 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 GetWidgetsResponse {
     widgets : UserWidget[]
 }
 
+/** Given a position, returns all of the user-widgets on the infotree at this position. */
 export function Widget_getWidgets(rs: RpcSessions, pos: DocumentPosition): Promise<GetWidgetsResponse | undefined> {
     return rs.call(pos, 'Lean.Widget.getWidgets', DocumentPosition.toTdpp(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
     hash: string
 }

diff --git a/lean4-infoview/src/infoview/userWidget.tsx b/lean4-infoview/src/infoview/userWidget.tsx
@@ -1,13 +1,9 @@
 import * as React from 'react';
-import type { Location } from 'vscode-languageserver-protocol';
 
-import { EditorContext, RpcContext } from './contexts';
-import { Details } from './collapsing';
-import { DocumentPosition, mapRpcError, useAsync, useEventResult } from './util';
+import { RpcContext } from './contexts';
+import { DocumentPosition, mapRpcError, useAsync } from './util';
 import { ErrorBoundary } from './errors';
-import { RpcSessions } from './rpcSessions';
-import { isRpcError, RpcErrorCode } from '@lean4/infoview-api';
-import { Widget_getWidgetSource, UserWidget, WidgetSource, Widget_getWidgets } from './rpcInterface';
+import { Widget_getWidgetSource, UserWidget } from './rpcInterface';
 
 function dynamicallyLoadComponent(hash: string, code: string,) {
     return React.lazy(async () => {
@@ -24,7 +20,6 @@ interface UserWidgetProps {
     widget: UserWidget
 }
 
-
 export function UserWidget({ pos, widget }: UserWidgetProps) {
     const rs = React.useContext(RpcContext);
     if (!pos) {