refactor: preparing for user-widgets and context suggestions

lean4-infoview-api/src/lspTypes.ts

@@ -44,19 +44,24 @@ export interface LeanFileProgressParams {
 
 // https://stackoverflow.com/a/56749647
 declare const tag: unique symbol;
+/** An RPC pointer is a reference to an object on the lean server.
+ * An example where you need this is passing the Environment object,
+ * which we need to be able to reference but which would be too large to
+ * send over directly.
+ */
 export type RpcPtr<T> = { readonly [tag]: T, p: string }
 
 // eslint-disable-next-line @typescript-eslint/no-namespace
 export namespace RpcPtr {
 
-export function copy<T>(p: RpcPtr<T>): RpcPtr<T> {
-    return { p: p.p } as RpcPtr<T>;
-}
+    export function copy<T>(p: RpcPtr<T>): RpcPtr<T> {
+        return { p: p.p } as RpcPtr<T>;
+    }
 
-/** Turns a reference into a unique string. Useful for React `key`s. */
-export function toKey(p: RpcPtr<any>): string {
-    return p.p;
-}
+    /** Turns a reference into a unique string. Useful for React `key`s. */
+    export function toKey(p: RpcPtr<any>): string {
+        return p.p;
+    }
 
 }
 
@@ -85,4 +90,27 @@ export interface RpcReleaseParams {
     refs: RpcPtr<any>[]
 }
 
-export const RpcNeedsReconnect = -32900
+export enum RpcErrorCode {
+    ParseError = -32700,
+    InvalidRequest = -32600,
+    MethodNotFound = -32601,
+    InvalidParams = -32602,
+    InternalError = -32603,
+    ServerNotInitialized = -32002,
+    UnknownErrorCode = -32001,
+    ContentModified = -32801,
+    RequestCancelled = -32800,
+    RpcNeedsReconnect = -32900,
+    WorkerExited = -32901,
+    WorkerCrashed = -32902,
+}
+
+export interface RpcError {
+    code: RpcErrorCode
+    message: string
+}
+
+export function isRpcError(x : any) : x is RpcError {
+    return !!(x?.code && x?.message)
+}
+

lean4-infoview/src/components.tsx

@@ -0,0 +1,32 @@
+import * as React from 'react';
+
+import { InteractiveDiagnostics_msgToInteractive, MessageData } from './infoview/rpcInterface';
+import { InteractiveMessage } from './infoview/traceExplorer';
+import { DocumentPosition, useAsync, mapRpcError } from './infoview/util';
+import { RpcContext } from './infoview/contexts';
+
+export { DocumentPosition };
+export { EditorContext, RpcContext, VersionContext } from './infoview/contexts';
+export { EditorConnection } from './infoview/editorConnection';
+export { RpcSessions } from './infoview/rpcSessions';
+export { ServerVersion } from './infoview/serverVersion';
+
+/** Display the given message data as interactive, pretty-printed text. */
+export function InteractiveMessageData({ pos, msg }: { pos: DocumentPosition, msg: MessageData }) {
+    const rs = React.useContext(RpcContext)
+
+    const [status, tt, error] = useAsync(
+        () => InteractiveDiagnostics_msgToInteractive(rs, pos, msg, 0),
+        [pos.character, pos.line, pos.uri, msg]
+    )
+
+    if (tt) {
+        return <InteractiveMessage pos={pos} fmt={tt} />
+    } else if (status === 'pending') {
+        return <>...</>
+    } else {
+        return <div>Failed to display message:
+            {error && <span>{mapRpcError(error).message}</span>}
+        </div>
+    }
+}

lean4-infoview/src/infoview/editorConnection.ts

@@ -7,6 +7,8 @@ import { DocumentPosition } from './util';
 
 export type EditorEvents = Eventify<InfoviewApi>;
 
+/** Provides higher-level wrappers around functionality provided by the editor,
+ * e.g. to insert a comment. See also {@link EditorApi}. */
 export class EditorConnection {
   constructor(readonly api: EditorApi, readonly events: EditorEvents) {}
 

lean4-infoview/src/infoview/errors.tsx

@@ -0,0 +1,33 @@
+import React from 'react';
+
+
+/** Error boundary as described in https://reactjs.org/docs/error-boundaries.html */
+export class ErrorBoundary extends React.Component<{}, {error: string | undefined}> {
+  constructor(props: {}) {
+    super(props);
+    this.state = { error: undefined };
+  }
+
+  static getDerivedStateFromError(error: any) {
+    // Update state so the next render will show the fallback UI.
+    return { error: error.toString() };
+  }
+
+  componentDidCatch(error : any, errorInfo : any) {
+    // You can also log the error to an error reporting service
+    return
+  }
+
+  render() {
+    if (this.state.error) {
+      // You can render any custom fallback UI
+      return <div>
+          <h1>Error:</h1>{this.state.error}<br/>
+          <a onClick={() => this.setState({ error: undefined })}>Click to reload.</a>
+        </div>;
+    }
+
+    return this.props.children;
+  }
+}
+

lean4-infoview/src/infoview/goalCompat.ts

@@ -1,5 +1,5 @@
 import { PlainGoal, PlainTermGoal } from '@lean4/infoview-api';
-import { InteractiveGoal, InteractiveGoals, InteractiveHypothesis } from './rpcInterface';
+import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle } from './rpcInterface';
 
 function getGoals(plainGoals: PlainGoal): string[] {
     if (plainGoals.goals) return plainGoals.goals
@@ -21,7 +21,7 @@ function transformGoalToInteractive(g: string): InteractiveGoal {
     // by keeping indented lines with the most recent non-indented line
     const parts = (g.match(/(^(?!  ).*\n?(  .*\n?)*)/mg) ?? []).map(line => line.trim())
     let userName
-    const hyps: InteractiveHypothesis[] = []
+    const hyps: InteractiveHypothesisBundle[] = []
     let type = ''
     for (const p of parts) {
         if (p.match(/^(⊢) /mg)) {
@@ -30,7 +30,7 @@ function transformGoalToInteractive(g: string): InteractiveGoal {
             userName = p.slice(5)
         } else if (p.match(/^([^:\n< ][^:\n⊢{[(⦃]*) :/mg)) {
             const ss = p.split(':')
-            const hyp: InteractiveHypothesis = {
+            const hyp: InteractiveHypothesisBundle = {
                 isType: false,
                 isInstance: false,
                 names: ss[0].split(' ')

lean4-infoview/src/infoview/goals.tsx

@@ -1,8 +1,27 @@
 import * as React from 'react'
 import { DocumentPosition } from './util'
-import { ConfigContext } from './contexts'
 import { InteractiveCode } from './interactiveCode'
-import { InteractiveGoal, InteractiveGoals, InteractiveHypothesis, TaggedText_stripTags } from './rpcInterface'
+import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle, InteractiveHypothesisBundle_accessibleNames, TaggedText_stripTags } from './rpcInterface'
+
+interface HypProps {
+    pos: DocumentPosition
+    hyp: InteractiveHypothesisBundle
+    index: number
+}
+
+export function Hyp({ pos, hyp : h, index }: HypProps) {
+    const names = InteractiveHypothesisBundle_accessibleNames(h).map((n, i) =>
+            <span className="mr1">{n}</span>
+        )
+    return <li>
+        <strong className="goal-hyp">{names}</strong>
+        :&nbsp;
+        <InteractiveCode pos={pos} fmt={h.type} />
+        {h.val && <>
+            := <InteractiveCode pos={pos} fmt={h.val} />
+        </>}
+    </li>
+}
 
 function goalToString(g: InteractiveGoal): string {
     let ret = ''
@@ -12,7 +31,7 @@ function goalToString(g: InteractiveGoal): string {
     }
 
     for (const h of g.hyps) {
-        const names = h.names.join(' ')
+        const names = InteractiveHypothesisBundle_accessibleNames(h).join(' ')
         ret += `${names} : ${TaggedText_stripTags(h.type)}`
         if (h.val) {
             ret += ` := ${TaggedText_stripTags(h.val)}`
@@ -30,56 +49,66 @@ export function goalsToString(goals: InteractiveGoals): string {
 }
 
 export interface GoalFilterState {
-    /** If true reverse the list of InteractiveHypothesis, if false present the order received from LSP */
+    /** If true reverse the list of hypotheses, if false present the order received from LSP */
     reverse: boolean,
-    /** If true show InteractiveHypothesis that have isType=True, if false, hide InteractiveHypothesis that have isType=True. */
+    /** If true show hypotheses that have isType=True, if false, hide hypotheses that have isType=True. */
     isType: boolean,
-    /** If true show InteractiveHypothesis that have isInstance=True, if false, hide InteractiveHypothesis that have isInstance=True. */
+    /** If true show hypotheses that have isInstance=True, if false, hide hypotheses that have isInstance=True. */
     isInstance: boolean,
-    /** If true show InteractiveHypothesis that contain a dagger in the name, if false, hide InteractiveHypothesis that contain a dagger in the name. */
+    /** If true show hypotheses that contain a dagger in the name, if false, hide hypotheses that contain a dagger in the name. */
     isHiddenAssumption: boolean
 }
 
-function isHiddenAssumption(h: InteractiveHypothesis){
+function isHiddenAssumption(h: InteractiveHypothesisBundle) {
     return h.names.every(n => n.indexOf('✝') >= 0);
 }
 
-function getFilteredHypotheses(hyps: InteractiveHypothesis[], filter: GoalFilterState): InteractiveHypothesis[] {
+function getFilteredHypotheses(hyps: InteractiveHypothesisBundle[], filter: GoalFilterState): InteractiveHypothesisBundle[] {
     return hyps.filter(h =>
         (!h.isInstance || filter.isInstance) &&
         (!h.isType || filter.isType) &&
         (filter.isHiddenAssumption || !isHiddenAssumption(h)));
 }
 
-export function Goal({pos, goal, filter}: {pos: DocumentPosition, goal: InteractiveGoal, filter: GoalFilterState}) {
+interface GoalProps {
+    pos: DocumentPosition
+    goal: InteractiveGoal
+    filter: GoalFilterState
+    /** Where the goal appears in the goal list. Or none if not present. */
+    index?: number
+}
+
+
+export function Goal({ pos, goal, filter }: GoalProps) {
     const prefix = goal.goalPrefix ?? '⊢ '
     const filteredList = getFilteredHypotheses(goal.hyps, filter);
-    const hyps = filter.reverse  ? filteredList.slice().reverse() : filteredList;
-    const goalLi  = <li key={'goal'}>
-                        <strong className="goal-vdash">{prefix}</strong><InteractiveCode pos={pos} fmt={goal.type} />
-                     </li>
+    const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList;
+    const goalLi = <li key={'goal'}>
+        <strong className="goal-vdash">{prefix}</strong>
+        <InteractiveCode pos={pos} fmt={goal.type} />
+    </li>
     return <div className="font-code tl pre-wrap">
         <ul className="list pl0">
             {goal.userName && <li key={'case'}><strong className="goal-case">case </strong>{goal.userName}</li>}
-            {filter.reverse && goalLi }
-            {hyps.map ((h, i) => {
-                const names = h.names.reduce((acc, n) => acc + ' ' + n, '').slice(1)
-                return <li key={`hyp-${i}`}>
-                    <strong className="goal-hyp">{names}</strong> : <InteractiveCode pos={pos} fmt={h.type} />{h.val && <> := <InteractiveCode pos={pos} fmt={h.val}/></>}
-                </li>
-            })}
-            {!filter.reverse && goalLi }
+            {filter.reverse && goalLi}
+            {hyps.map((h, i) => <Hyp pos={pos} index={i} hyp={h} key={i}/>)}
+            {!filter.reverse && goalLi}
         </ul>
     </div>
 }
 
-export function Goals({pos, goals, filter}: {pos: DocumentPosition, goals: InteractiveGoals, filter: GoalFilterState}) {
-    const config = React.useContext(ConfigContext)
+interface GoalsProps {
+    pos: DocumentPosition
+    goals: InteractiveGoals
+    filter: GoalFilterState
+}
+
+export function Goals({ pos, goals, filter }: GoalsProps) {
     if (goals.goals.length === 0) {
         return <>Goals accomplished 🎉</>
     } else {
         return <>
-            {goals.goals.map ((g, i) => <Goal key={i} pos={pos} goal={g} filter={filter}/>)}
+            {goals.goals.map((g, i) => <Goal key={i} pos={pos} goal={g} filter={filter} index={i} />)}
         </>
     }
 }

lean4-infoview/src/infoview/interactiveCode.tsx

@@ -1,8 +1,8 @@
 import * as React from 'react'
 
 import { EditorContext, RpcContext } from './contexts'
-import { DocumentPosition } from './util'
-import { SubexprInfo, CodeWithInfos, InfoPopup, InfoWithCtx, InteractiveDiagnostics_infoToInteractive, getGoToLocation, TaggedText } from './rpcInterface'
+import { DocumentPosition, useAsync, mapRpcError } from './util'
+import { SubexprInfo, CodeWithInfos, InteractiveDiagnostics_infoToInteractive, getGoToLocation, TaggedText } from './rpcInterface'
 import { DetectHoverSpan, HoverState, WithTooltipOnHover } from './tooltips'
 import { Location } from 'vscode-languageserver-protocol'
 
@@ -32,48 +32,41 @@ export function InteractiveTaggedText<T>({pos, fmt, InnerTagUi}: InteractiveTagg
   else throw new Error(`malformed 'TaggedText': '${fmt}'`)
 }
 
+interface TypePopupContentsProps {
+  pos: DocumentPosition
+  info: SubexprInfo
+  redrawTooltip: () => void
+}
+
 /** Shows `explicitValue : itsType` and a docstring if there is one. */
-function TypePopupContents({pos, info, redrawTooltip}: {pos: DocumentPosition, info: InfoWithCtx, redrawTooltip: () => void}) {
+function TypePopupContents({ pos, info, redrawTooltip }: TypePopupContentsProps) {
   const rs = React.useContext(RpcContext)
   // When `err` is defined we show the error,
   // otherwise if `ip` is defined we show its contents,
   // otherwise a 'loading' message.
-  const [ip, setIp] = React.useState<InfoPopup>()
-  const [err, setErr] = React.useState<string>()
-
-  React.useEffect(() => {
-    InteractiveDiagnostics_infoToInteractive(rs, pos, info).then(val => {
-      if (val) {
-        setErr(undefined)
-        setIp(val)
-      }
-    }).catch(ex => {
-      if ('message' in ex) setErr('' + ex.message)
-      else if ('code' in ex) setErr(`RPC error (${ex.code})`)
-      else setErr(JSON.stringify(ex))
-    })
-  }, [rs, pos.uri, pos.line, pos.character, info])
+  const [_, ip, err] = useAsync(
+    () => InteractiveDiagnostics_infoToInteractive(rs, pos, info.info),
+    [rs, pos.uri, pos.line, pos.character, info.info, info.subexprPos])
 
   // We let the tooltip know to redo its layout whenever our contents change.
   React.useEffect(() => redrawTooltip(), [ip, err, redrawTooltip])
 
-  if (err)
-    return <>Error: {err}</>
-
-  if (ip) {
-    return <>
+  return <>
+    {ip && <>
       {ip.exprExplicit && <InteractiveCode pos={pos} fmt={ip.exprExplicit} />} : {ip.type && <InteractiveCode pos={pos} fmt={ip.type} />}
       {ip.doc && <hr />}
       {ip.doc && ip.doc} {/* TODO markdown */}
-    </>
-  } else return <>Loading..</>
+    </>}
+    {err && <>Error: {mapRpcError(err).message}</>}
+    {(!ip && !err) && <>Loading..</>}
+  </>
 }
 
 /** Tagged spans can be hovered over to display extra info stored in the associated `SubexprInfo`. */
 function InteractiveCodeTag({pos, tag: ct, fmt}: InteractiveTagProps<SubexprInfo>) {
   const mkTooltip = React.useCallback((redrawTooltip: () => void) =>
     <div className="font-code tl pre-wrap">
-      <TypePopupContents pos={pos} info={ct.info}
+      <TypePopupContents pos={pos} info={ct}
         redrawTooltip={redrawTooltip} />
     </div>, [pos.uri, pos.line, pos.character, ct.info])
 
@@ -126,6 +119,11 @@ function InteractiveCodeTag({pos, tag: ct, fmt}: InteractiveTagProps<SubexprInfo
   )
 }
 
-export function InteractiveCode({pos, fmt}: {pos: DocumentPosition, fmt: CodeWithInfos}) {
-  return InteractiveTaggedText({pos, fmt, InnerTagUi: InteractiveCodeTag})
+interface InteractiveCodeProps {
+  pos: DocumentPosition
+  fmt: CodeWithInfos
+}
+
+export function InteractiveCode(props: InteractiveCodeProps) {
+  return <InteractiveTaggedText InnerTagUi={InteractiveCodeTag} fmt={props.fmt} pos={props.pos} />
 }