diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx index 3cb8b54..42c1b38 100644 --- a/client/src/components/Level.tsx +++ b/client/src/components/Level.tsx @@ -13,6 +13,8 @@ import Grid from '@mui/material/Unstable_Grid2'; import LeftPanel from './LeftPanel'; import { LeanTaskGutter } from 'lean4web/client/src/editor/taskgutter'; import { AbbreviationProvider } from 'lean4web/client/src/editor/abbreviation/AbbreviationProvider'; +import 'lean4web/client/src/editor/vscode.css'; +import 'lean4web/client/src/editor/infoview.css'; import { AbbreviationRewriter } from 'lean4web/client/src/editor/abbreviation/rewriter/AbbreviationRewriter'; import { InfoProvider } from 'lean4web/client/src/editor/infoview'; import 'lean4web/client/src/editor/infoview.css' diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx new file mode 100644 index 0000000..d40fbb1 --- /dev/null +++ b/client/src/components/infoview/goals.tsx @@ -0,0 +1,241 @@ +/* Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/goals.tsx */ + +import * as React from 'react' +import { InteractiveCode } from '../../../../node_modules/lean4-infoview/src/infoview/interactiveCode' +import { InteractiveGoal, InteractiveGoals, InteractiveHypothesisBundle, InteractiveHypothesisBundle_nonAnonymousNames, MVarId, TaggedText_stripTags } from '@leanprover/infoview-api' +import { WithTooltipOnHover } from '../../../../node_modules/lean4-infoview/src/infoview/tooltips'; +import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'; +import { Locations, LocationsContext, SelectableLocation } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation'; + +/** Returns true if `h` is inaccessible according to Lean's default name rendering. */ +function isInaccessibleName(h: string): boolean { + return h.indexOf('✝') >= 0; +} + +function goalToString(g: InteractiveGoal): string { + let ret = '' + + if (g.userName) { + ret += `case ${g.userName}\n` + } + + for (const h of g.hyps) { + const names = InteractiveHypothesisBundle_nonAnonymousNames(h).join(' ') + ret += `${names} : ${TaggedText_stripTags(h.type)}` + if (h.val) { + ret += ` := ${TaggedText_stripTags(h.val)}` + } + ret += '\n' + } + + ret += `⊢ ${TaggedText_stripTags(g.type)}` + + return ret +} + +export function goalsToString(goals: InteractiveGoals): string { + return goals.goals.map(goalToString).join('\n\n') +} + +interface GoalFilterState { + /** If true reverse the list of hypotheses, if false present the order received from LSP. */ + reverse: boolean, + /** If true show hypotheses that have isType=True, otherwise hide them. */ + showType: boolean, + /** If true show hypotheses that have isInstance=True, otherwise hide them. */ + showInstance: boolean, + /** If true show hypotheses that contain a dagger in the name, otherwise hide them. */ + showHiddenAssumption: boolean + /** If true show the bodies of let-values, otherwise hide them. */ + showLetValue: boolean; +} + +function getFilteredHypotheses(hyps: InteractiveHypothesisBundle[], filter: GoalFilterState): InteractiveHypothesisBundle[] { + return hyps.reduce((acc: InteractiveHypothesisBundle[], h) => { + if (h.isInstance && !filter.showInstance) return acc + if (h.isType && !filter.showType) return acc + const names = filter.showHiddenAssumption ? h.names : h.names.filter(n => !isInaccessibleName(n)) + const hNew: InteractiveHypothesisBundle = filter.showLetValue ? { ...h, names } : { ...h, names, val: undefined } + if (names.length !== 0) acc.push(hNew) + return acc + }, []) +} + +interface HypProps { + hyp: InteractiveHypothesisBundle + mvarId?: MVarId +} + +function Hyp({ hyp: h, mvarId }: HypProps) { + const locs = React.useContext(LocationsContext) + + const namecls: string = 'mr1 ' + + (h.isInserted ? 'inserted-text ' : '') + + (h.isRemoved ? 'removed-text ' : '') + + const names = InteractiveHypothesisBundle_nonAnonymousNames(h).map((n, i) => + + i ? + { mvarId, loc: { hyp: h.fvarIds[i] }} : + undefined + } + alwaysHighlight={false} + >{n} + ) + + const typeLocs: Locations | undefined = React.useMemo(() => + locs && mvarId && h.fvarIds && h.fvarIds.length > 0 ? + { ...locs, subexprTemplate: { mvarId, loc: { hypType: [h.fvarIds[0], ''] }}} : + undefined, + [locs, mvarId, h.fvarIds]) + + const valLocs: Locations | undefined = React.useMemo(() => + h.val && locs && mvarId && h.fvarIds && h.fvarIds.length > 0 ? + { ...locs, subexprTemplate: { mvarId, loc: { hypValue: [h.fvarIds[0], ''] }}} : + undefined, + [h.val, locs, mvarId, h.fvarIds]) + + return
+ {names} + :  + + + + {h.val && + +  :=  + } +
+} + +interface GoalProps { + goal: InteractiveGoal + filter: GoalFilterState +} + +/** + * Displays the hypotheses, target type and optional case label of a goal according to the + * provided `filter`. */ +export const Goal = React.memo((props: GoalProps) => { + const { goal, filter } = props + + const prefix = goal.goalPrefix ?? 'Prove: ' + const filteredList = getFilteredHypotheses(goal.hyps, filter); + const hyps = filter.reverse ? filteredList.slice().reverse() : filteredList; + const locs = React.useContext(LocationsContext) + const goalLocs = React.useMemo(() => + locs && goal.mvarId ? + { ...locs, subexprTemplate: { mvarId: goal.mvarId, loc: { target: '' }}} : + undefined, + [locs, goal.mvarId]) + const goalLi =
+ Prove: + + + +
+ + let cn = 'font-code tl pre-wrap bl bw1 pl1 b--transparent ' + if (props.goal.isInserted) cn += 'b--inserted ' + if (props.goal.isRemoved) cn += 'b--removed ' + + if (goal.userName) { + return
+ + case {goal.userName} + + {filter.reverse && goalLi} + {hyps.map((h, i) => )} + {!filter.reverse && goalLi} +
+ } else return
+ {filter.reverse && goalLi} + {hyps.map((h, i) => )} + {!filter.reverse && goalLi} +
+}) + +interface GoalsProps { + goals: InteractiveGoals + filter: GoalFilterState +} + +export function Goals({ goals, filter }: GoalsProps) { + if (goals.goals.length === 0) { + return <>No goals + } else { + return <> + {goals.goals.map((g, i) => )} + + } +} + +interface FilteredGoalsProps { + /** Components to render in the header. */ + headerChildren: React.ReactNode + /** + * When this is `undefined`, the component will not appear at all but will remember its state + * by virtue of still being mounted in the React tree. When it does appear again, the filter + * settings and collapsed state will be as before. */ + goals?: InteractiveGoals +} + +/** + * Display goals together with a header containing the provided children as well as buttons + * to control how the goals are displayed. + */ +export const FilteredGoals = React.memo(({ headerChildren, goals }: FilteredGoalsProps) => { + const ec = React.useContext(EditorContext) + + const copyToCommentButton = + { + e.preventDefault(); + if (goals) void ec.copyToComment(goalsToString(goals)) + }} + title="copy state to comment" /> + + const [goalFilters, setGoalFilters] = React.useState( + { reverse: false, showType: true, showInstance: true, showHiddenAssumption: true, showLetValue: true }); + + const sortClasses = 'link pointer mh2 dim codicon ' + (goalFilters.reverse ? 'codicon-arrow-up ' : 'codicon-arrow-down '); + const sortButton = + setGoalFilters(s => ({ ...s, reverse: !s.reverse }))} /> + + const mkFilterButton = (filterFn: React.SetStateAction, filledFn: (_: GoalFilterState) => boolean, name: string) => + { setGoalFilters(filterFn) }}> +   + {name} + + const filterMenu = + {mkFilterButton(s => ({ ...s, showType: !s.showType }), gf => gf.showType, 'types')} +
+ {mkFilterButton(s => ({ ...s, showInstance: !s.showInstance }), gf => gf.showInstance, 'instances')} +
+ {mkFilterButton(s => ({ ...s, showHiddenAssumption: !s.showHiddenAssumption }), gf => gf.showHiddenAssumption, 'hidden assumptions')} +
+ {mkFilterButton(s => ({ ...s, showLetValue: !s.showLetValue }), gf => gf.showLetValue, 'let-values')} + + + const isFiltered = !goalFilters.showInstance || !goalFilters.showType || !goalFilters.showHiddenAssumption || !goalFilters.showLetValue + const filterButton = + filterMenu}> + + + + return
+
+ + {headerChildren} + {copyToCommentButton}{sortButton}{filterButton} + +
+ {goals && } +
+
+
+}) diff --git a/client/src/components/infoview/info.tsx b/client/src/components/infoview/info.tsx new file mode 100644 index 0000000..b344be4 --- /dev/null +++ b/client/src/components/infoview/info.tsx @@ -0,0 +1,399 @@ +/* Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/info.tsx */ + +import * as React from 'react'; +import type { Location, Diagnostic } from 'vscode-languageserver-protocol'; + +import { goalsToString, Goals, FilteredGoals } from './goals' +import { basename, DocumentPosition, RangeHelpers, useEvent, usePausableState, discardMethodNotFound, + mapRpcError, useAsyncWithTrigger, PausableProps } from '../../../../node_modules/lean4-infoview/src/infoview/util'; +import { ConfigContext, EditorContext, LspDiagnosticsContext, ProgressContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'; +import { lspDiagToInteractive, MessagesList } from './messages'; +import { getInteractiveGoals, getInteractiveTermGoal, InteractiveDiagnostic, + InteractiveGoals, UserWidgetInstance, Widget_getWidgets, RpcSessionAtPos, isRpcError, + RpcErrorCode, getInteractiveDiagnostics, InteractiveTermGoal } from '@leanprover/infoview-api'; +import { PanelWidgetDisplay } from '../../../../node_modules/lean4-infoview/src/infoview/userWidget' +import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions'; +import { GoalsLocation, Locations, LocationsContext } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation'; + +type InfoStatus = 'updating' | 'error' | 'ready'; +type InfoKind = 'cursor' | 'pin'; + +interface InfoPinnable { + kind: InfoKind; + /** Takes an argument for caching reasons, but should only ever (un)pin itself. */ + onPin: (pos: DocumentPosition) => void; +} + +interface InfoStatusBarProps extends InfoPinnable, PausableProps { + pos: DocumentPosition; + status: InfoStatus; + triggerUpdate: () => Promise; +} + +const InfoStatusBar = React.memo((props: InfoStatusBarProps) => { + const { kind, onPin, status, pos, isPaused, setPaused, triggerUpdate } = props; + + const ec = React.useContext(EditorContext); + + const statusColTable: {[T in InfoStatus]: string} = { + 'updating': 'gold ', + 'error': 'dark-red ', + 'ready': '', + } + const statusColor = statusColTable[status]; + const locationString = `${basename(pos.uri)}:${pos.line+1}:${pos.character}`; + const isPinned = kind === 'pin'; + + return ( + + {locationString} + {isPinned && !isPaused && ' (pinned)'} + {!isPinned && isPaused && ' (paused)'} + {isPinned && isPaused && ' (pinned and paused)'} + + {isPinned && + { e.preventDefault(); void ec.revealPosition(pos); }} + title='reveal file location' />} + { e.preventDefault(); onPin(pos); }} + title={isPinned ? 'unpin' : 'pin'} /> + { e.preventDefault(); setPaused(!isPaused); }} + title={isPaused ? 'continue updating' : 'pause updating'} /> + { e.preventDefault(); void triggerUpdate(); }} + title='update'/> + + + ); +}) + +interface InfoDisplayContentProps extends PausableProps { + pos: DocumentPosition; + messages: InteractiveDiagnostic[]; + goals?: InteractiveGoals; + termGoal?: InteractiveTermGoal; + error?: string; + userWidgets: UserWidgetInstance[]; + triggerUpdate: () => Promise; +} + +const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => { + const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused} = props; + + const hasWidget = userWidgets.length > 0; + const hasError = !!error; + const hasMessages = messages.length !== 0; + + const nothingToShow = !hasError && !goals && !termGoal && !hasMessages && !hasWidget; + + const [selectedLocs, setSelectedLocs] = React.useState([]) + React.useEffect(() => setSelectedLocs([]), [pos.uri, pos.line, pos.character]) + + const locs: Locations = React.useMemo(() => ({ + isSelected: (l: GoalsLocation) => selectedLocs.some(v => GoalsLocation.isEqual(v, l)), + setSelected: (l, act) => setSelectedLocs(ls => { + // We ensure that `selectedLocs` maintains its reference identity if the selection + // status of `l` didn't change. + const newLocs = ls.filter(v => !GoalsLocation.isEqual(v, l)) + const wasSelected = newLocs.length !== ls.length + const isSelected = typeof act === 'function' ? act(wasSelected) : act + if (isSelected) newLocs.push(l) + return wasSelected === isSelected ? ls : newLocs + }), + subexprTemplate: undefined + }), [selectedLocs]) + + /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */ + return <> + {hasError && +
+ Error updating:{' '}{error}. + { e.preventDefault(); void triggerUpdate(); }}>{' '}Try again. +
} + + {goals && } + + + {userWidgets.map(widget => +
+ {widget.name} + +
+ )} +
+ {/*
+ Messages ({messages.length}) */} +
+ +
+ {/*
*/} +
+ {nothingToShow && ( + isPaused ? + /* Adding {' '} to manage string literals properly: https://reactjs.org/docs/jsx-in-depth.html#string-literals-1 */ + Updating is paused.{' '} + { e.preventDefault(); void triggerUpdate(); }}>Refresh + {' '}or { e.preventDefault(); setPaused(false); }}>resume updating + {' '}to see information. + : + 'No info found.')} + +}) + +interface InfoDisplayProps { + pos: DocumentPosition; + status: InfoStatus; + messages: InteractiveDiagnostic[]; + goals?: InteractiveGoals; + termGoal?: InteractiveTermGoal; + error?: string; + userWidgets: UserWidgetInstance[]; + rpcSess: RpcSessionAtPos; + triggerUpdate: () => Promise; +} + +/** Displays goal state and messages. Can be paused. */ +function InfoDisplay(props0: InfoDisplayProps & InfoPinnable) { + // Used to update the paused state *just once* if it is paused, + // but a display update is triggered + const [shouldRefresh, setShouldRefresh] = React.useState(false); + const [{ isPaused, setPaused }, props, propsRef] = usePausableState(false, props0); + if (shouldRefresh) { + propsRef.current = props0; + setShouldRefresh(false); + } + const triggerDisplayUpdate = async () => { + await props0.triggerUpdate(); + setShouldRefresh(true); + }; + + const {kind, goals, rpcSess} = props; + + const ec = React.useContext(EditorContext); + + // If we are the cursor infoview, then we should subscribe to + // some commands from the editor extension + const isCursor = kind === 'cursor'; + useEvent(ec.events.requestedAction, act => { + if (!isCursor) return; + if (act.kind !== 'copyToComment') return; + if (goals) void ec.copyToComment(goalsToString(goals)); + }, [goals]); + useEvent(ec.events.requestedAction, act => { + if (!isCursor) return; + if (act.kind !== 'togglePaused') return; + setPaused(isPaused => !isPaused); + }); + + return ( + + {/*
*/} + {/* */} +
+ +
+ {/*
*/} + + ); +} + +/** + * Note: in the cursor view, we have to keep the cursor position as part of the component state + * to avoid flickering when the cursor moved. Otherwise, the component is re-initialised and the + * goal states reset to `undefined` on cursor moves. + */ +export type InfoProps = InfoPinnable & { pos?: DocumentPosition }; + +/** Fetches info from the server and renders an {@link InfoDisplay}. */ +export function Info(props: InfoProps) { + if (props.kind === 'cursor') return + else return +} + +function InfoAtCursor(props: InfoProps) { + const ec = React.useContext(EditorContext); + // eslint-disable-next-line @typescript-eslint/no-non-null-assertion + const [curLoc, setCurLoc] = React.useState(ec.events.changedCursorLocation.current!); + useEvent(ec.events.changedCursorLocation, loc => loc && setCurLoc(loc), []); + const pos = { uri: curLoc.uri, ...curLoc.range.start }; + return +} + +function useIsProcessingAt(p: DocumentPosition): boolean { + const allProgress = React.useContext(ProgressContext); + const processing = allProgress.get(p.uri); + if (!processing) return false; + return processing.some(i => RangeHelpers.contains(i.range, p)); +} + +function InfoAux(props: InfoProps) { + const config = React.useContext(ConfigContext) + + // eslint-disable-next-line @typescript-eslint/no-non-null-assertion + const pos = props.pos! + const rpcSess = useRpcSessionAtPos(pos) + + // Compute the LSP diagnostics at this info's position. We try to ensure that if these remain + // the same, then so does the identity of `lspDiagsHere` so that it can be used as a dep. + const lspDiags = React.useContext(LspDiagnosticsContext) + const [lspDiagsHere, setLspDiagsHere] = React.useState([]) + React.useEffect(() => { + // Note: the curly braces are important. https://medium.com/geekculture/react-uncaught-typeerror-destroy-is-not-a-function-192738a6e79b + setLspDiagsHere(diags0 => { + const diagPred = (d: Diagnostic) => + RangeHelpers.contains(d.range, pos, config.allErrorsOnLine) + const newDiags = (lspDiags.get(pos.uri) || []).filter(diagPred) + if (newDiags.length === diags0.length && newDiags.every((d, i) => d === diags0[i])) return diags0 + return newDiags + }) + }, [lspDiags, pos.uri, pos.line, pos.character, config.allErrorsOnLine]) + + const serverIsProcessing = useIsProcessingAt(pos) + + // This is a virtual dep of the info-requesting function. It is bumped whenever the Lean server + // indicates that another request should be made. Bumping it dirties the dep state of + // `useAsyncWithTrigger` below, causing the `useEffect` lower down in this component to + // make the request. We cannot simply call `triggerUpdateCore` because `useAsyncWithTrigger` + // does not support reentrancy like that. + const [updaterTick, setUpdaterTick] = React.useState(0) + + // For atomicity, we use a single update function that fetches all the info at `pos` at once. + // Besides what the server replies with, we also include the inputs (deps) in this type so + // that the displayed state cannot ever get out of sync by showing an old reply together + // with e.g. a new `pos`. + type InfoRequestResult = Omit + const [state, triggerUpdateCore] = useAsyncWithTrigger(() => new Promise((resolve, reject) => { + const goalsReq = getInteractiveGoals(rpcSess, DocumentPosition.toTdpp(pos)); + const termGoalReq = getInteractiveTermGoal(rpcSess, DocumentPosition.toTdpp(pos)) + const widgetsReq = Widget_getWidgets(rpcSess, pos).catch(discardMethodNotFound) + const messagesReq = getInteractiveDiagnostics(rpcSess, {start: pos.line, end: pos.line+1}) + // fall back to non-interactive diagnostics when lake fails + // (see https://github.com/leanprover/vscode-lean4/issues/90) + .then(diags => diags.length === 0 ? lspDiagsHere.map(lspDiagToInteractive) : diags) + + // While `lake print-paths` is running, the output of Lake is shown as + // info diagnostics on line 1. However, all RPC requests block until + // Lake is finished, so we don't see these diagnostics while Lake is + // building. Therefore we show the LSP diagnostics on line 1 if the + // server does not respond within half a second. + if (pos.line === 0 && lspDiagsHere.length) { + setTimeout(() => resolve({ + pos, + status: 'updating', + messages: lspDiagsHere.map(lspDiagToInteractive), + goals: undefined, + termGoal: undefined, + error: undefined, + userWidgets: [], + rpcSess + }), 500) + } + + // NB: it is important to await await reqs at once, otherwise + // if both throw then one exception becomes unhandled. + Promise.all([goalsReq, termGoalReq, widgetsReq, messagesReq]).then( + ([goals, termGoal, userWidgets, messages]) => resolve({ + pos, + status: 'ready', + messages, + goals, + termGoal, + error: undefined, + userWidgets: userWidgets?.widgets ?? [], + rpcSess + }), + ex => { + if (ex?.code === RpcErrorCode.ContentModified || + ex?.code === RpcErrorCode.RpcNeedsReconnect) { + // Document has been changed since we made the request, or we need to reconnect + // to the RPC sessions. Try again. + setUpdaterTick(t => t + 1) + reject('retry') + } + + let errorString = '' + if (typeof ex === 'string') { + errorString = ex + } else if (isRpcError(ex)) { + errorString = mapRpcError(ex).message + } else if (ex instanceof Error) { + errorString = ex.toString() + } else { + errorString = `Unrecognized error: ${JSON.stringify(ex)}` + } + + resolve({ + pos, + status: 'error', + messages: lspDiagsHere.map(lspDiagToInteractive), + goals: undefined, + termGoal: undefined, + error: `Error fetching goals: ${errorString}`, + userWidgets: [], + rpcSess + }) + } + ) + }), [updaterTick, pos.uri, pos.line, pos.character, rpcSess, serverIsProcessing, lspDiagsHere]) + + // We use a timeout to debounce info requests. Whenever a request is already scheduled + // but something happens that warrants a request for newer info, we cancel the old request + // and schedule just the new one. + const updaterTimeout = React.useRef() + const clearUpdaterTimeout = () => { + if (updaterTimeout.current) { + window.clearTimeout(updaterTimeout.current) + updaterTimeout.current = undefined + } + } + const triggerUpdate = React.useCallback(() => new Promise(resolve => { + clearUpdaterTimeout() + const tm = window.setTimeout(() => { + void triggerUpdateCore().then(resolve) + updaterTimeout.current = undefined + }, config.debounceTime) + // Hack: even if the request is cancelled, the promise should resolve so that no `await` + // is left waiting forever. We ensure this happens in a simple way. + window.setTimeout(resolve, config.debounceTime) + updaterTimeout.current = tm + }), [triggerUpdateCore, config.debounceTime]) + + const [displayProps, setDisplayProps] = React.useState({ + pos, + status: 'updating', + messages: [], + goals: undefined, + termGoal: undefined, + error: undefined, + userWidgets: [], + rpcSess, + triggerUpdate + }) + + // Propagates changes in the state of async info requests to the display props, + // and re-requests info if needed. + // This effect triggers new requests for info whenever need. It also propagates changes + // in the state of the `useAsyncWithTrigger` to the displayed props. + React.useEffect(() => { + if (state.state === 'notStarted') + void triggerUpdate() + else if (state.state === 'loading') + setDisplayProps(dp => ({ ...dp, status: 'updating' })) + else if (state.state === 'resolved') { + setDisplayProps({ ...state.value, triggerUpdate }) + } else if (state.state === 'rejected' && state.error !== 'retry') { + // The code inside `useAsyncWithTrigger` may only ever reject with a `retry` exception. + console.warn('Unreachable code reached with error: ', state.error) + } + }, [state]) + + return +} diff --git a/client/src/components/infoview/infos.tsx b/client/src/components/infoview/infos.tsx new file mode 100644 index 0000000..b077150 --- /dev/null +++ b/client/src/components/infoview/infos.tsx @@ -0,0 +1,131 @@ +/* Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/infos.tsx */ + +import * as React from 'react'; +import { DidChangeTextDocumentParams, DidCloseTextDocumentParams, TextDocumentContentChangeEvent } from 'vscode-languageserver-protocol'; + +import { EditorContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'; +import { DocumentPosition, Keyed, PositionHelpers, useClientNotificationEffect, useClientNotificationState, useEvent, useEventResult } from '../../../../node_modules/lean4-infoview/src/infoview/util'; +import { Info, InfoProps } from './info'; + +/** Manages and displays pinned infos, as well as info for the current location. */ +export function Infos() { + const ec = React.useContext(EditorContext); + + // Update pins when the document changes. In particular, when edits are made + // earlier in the text such that a pin has to move up or down. + const [pinnedPositions, setPinnedPositions] = useClientNotificationState( + 'textDocument/didChange', + new Array>(), + (pinnedPositions, params: DidChangeTextDocumentParams) => { + if (pinnedPositions.length === 0) return pinnedPositions; + + let changed: boolean = false; + const newPins = pinnedPositions.map(pin => { + if (pin.uri !== params.textDocument.uri) return pin; + // NOTE(WN): It's important to make a clone here, otherwise this + // actually mutates the pin. React state updates must be pure. + // See https://github.com/facebook/react/issues/12856 + const newPin: Keyed = { ...pin }; + for (const chg of params.contentChanges) { + if (!TextDocumentContentChangeEvent.isIncremental(chg)) { + changed = true; + return null; + } + if (PositionHelpers.isLessThanOrEqual(newPin, chg.range.start)) continue; + // We can assume chg.range.start < pin + + // If the pinned position is replaced with new text, just delete the pin. + if (PositionHelpers.isLessThanOrEqual(newPin, chg.range.end)) { + changed = true; + return null; + } + + const oldPin = { ...newPin }; + + // How many lines before the pin position were added by the change. + // Can be negative when more lines are removed than added. + let additionalLines = 0; + let lastLineLen = chg.range.start.character; + for (const c of chg.text) + if (c === '\n') { + additionalLines++; + lastLineLen = 0; + } else lastLineLen++; + + // Subtract lines that were already present + additionalLines -= (chg.range.end.line - chg.range.start.line) + newPin.line += additionalLines; + + if (oldPin.line < chg.range.end.line) { + // Should never execute by the <= check above. + throw new Error('unreachable code reached') + } else if (oldPin.line === chg.range.end.line) { + newPin.character = lastLineLen + (oldPin.character - chg.range.end.character); + } + } + if (!DocumentPosition.isEqual(newPin, pin)) changed = true; + + // NOTE(WN): We maintain the `key` when a pin is moved around to maintain + // its component identity and minimise flickering. + return newPin; + }); + + if (changed) return newPins.filter(p => p !== null) as Keyed[]; + return pinnedPositions; + }, + [] + ); + + // Remove pins for closed documents + useClientNotificationEffect( + 'textDocument/didClose', + (params: DidCloseTextDocumentParams) => { + setPinnedPositions(pinnedPositions => pinnedPositions.filter(p => p.uri !== params.textDocument.uri)); + }, + [] + ); + + const curPos: DocumentPosition | undefined = + useEventResult(ec.events.changedCursorLocation, loc => loc ? { uri: loc.uri, ...loc.range.start } : undefined) + + // Update pins on UI actions + const pinKey = React.useRef(0); + const isPinned = (pinnedPositions: DocumentPosition[], pos: DocumentPosition) => { + return pinnedPositions.some(p => DocumentPosition.isEqual(p, pos)); + } + const pin = React.useCallback((pos: DocumentPosition) => { + setPinnedPositions(pinnedPositions => { + if (isPinned(pinnedPositions, pos)) return pinnedPositions; + pinKey.current += 1; + return [ ...pinnedPositions, { ...pos, key: pinKey.current.toString() } ]; + }); + }, []); + const unpin = React.useCallback((pos: DocumentPosition) => { + setPinnedPositions(pinnedPositions => { + if (!isPinned(pinnedPositions, pos)) return pinnedPositions; + return pinnedPositions.filter(p => !DocumentPosition.isEqual(p, pos)); + }); + }, []); + + // Toggle pin at current position when the editor requests it + useEvent(ec.events.requestedAction, act => { + if (act.kind !== 'togglePin') return + if (!curPos) return + setPinnedPositions(pinnedPositions => { + if (isPinned(pinnedPositions, curPos)) { + return pinnedPositions.filter(p => !DocumentPosition.isEqual(p, curPos)); + } else { + pinKey.current += 1; + return [ ...pinnedPositions, { ...curPos, key: pinKey.current.toString() } ]; + } + }); + }, [curPos?.uri, curPos?.line, curPos?.character]); + + const infoProps: Keyed[] = pinnedPositions.map(pos => ({ kind: 'pin', onPin: unpin, pos, key: pos.key })); + if (curPos) infoProps.push({ kind: 'cursor', onPin: pin, key: 'cursor' }); + + return
+ {infoProps.map (ps => )} + {!curPos &&

Click somewhere in the Lean file to enable the infoview.

} +
; +} diff --git a/client/src/components/infoview/infoview.css b/client/src/components/infoview/infoview.css new file mode 100644 index 0000000..52a35f4 --- /dev/null +++ b/client/src/components/infoview/infoview.css @@ -0,0 +1,18 @@ + +.message { + margin: 10px 0; + padding: 5px 10px; + border-radius: 3px 3px 3px 3px; +} +.message.info { + color: #059; + background-color: #BEF; +} +.message.warning { + color: #9F6000; + background-color: #FEEFB3; +} +.message.error { + color: #D8000C; + background-color: #FFBABA; +} diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index 54f62db..892d584 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -8,10 +8,11 @@ import 'tachyons/css/tachyons.css'; // import '@vscode/codicons/dist/codicon.ttf'; import '@vscode/codicons/dist/codicon.css'; import '../../../../node_modules/lean4-infoview/src/infoview/index.css'; +import './infoview.css' import { LeanFileProgressParams, LeanFileProgressProcessingInfo, defaultInfoviewConfig, EditorApi, InfoviewApi } from '@leanprover/infoview-api'; -import { Infos } from '../../../../node_modules/lean4-infoview/src/infoview/infos'; +import { Infos } from './infos'; import { AllMessages, WithLspDiagnosticsContext } from '../../../../node_modules/lean4-infoview/src/infoview/messages'; import { useClientNotificationEffect, useEventResult, useServerNotificationState } from '../../../../node_modules/lean4-infoview/src/infoview/util'; import { EditorContext, ConfigContext, ProgressContext, VersionContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'; diff --git a/client/src/components/infoview/messages.tsx b/client/src/components/infoview/messages.tsx new file mode 100644 index 0000000..f64b495 --- /dev/null +++ b/client/src/components/infoview/messages.tsx @@ -0,0 +1,176 @@ +import * as React from 'react'; +import fastIsEqual from 'react-fast-compare'; +import { Location, DocumentUri, Diagnostic, DiagnosticSeverity, PublishDiagnosticsParams } from 'vscode-languageserver-protocol'; + +import { LeanDiagnostic, RpcErrorCode } from '@leanprover/infoview-api'; + +import { basename, escapeHtml, usePausableState, useEvent, addUniqueKeys, DocumentPosition, useServerNotificationState } from '../../../../node_modules/lean4-infoview/src/infoview/util'; +import { ConfigContext, EditorContext, LspDiagnosticsContext, VersionContext } from '../../../../node_modules/lean4-infoview/src/infoview/contexts'; +import { Details } from '../../../../node_modules/lean4-infoview/src/infoview/collapsing'; +import { InteractiveMessage } from '../../../../node_modules/lean4-infoview/src/infoview/traceExplorer'; +import { getInteractiveDiagnostics, InteractiveDiagnostic, TaggedText_stripTags } from '@leanprover/infoview-api'; +import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions'; + +interface MessageViewProps { + uri: DocumentUri; + diag: InteractiveDiagnostic; +} + +const MessageView = React.memo(({uri, diag}: MessageViewProps) => { + const ec = React.useContext(EditorContext); + const fname = escapeHtml(basename(uri)); + const {line, character} = diag.range.start; + const loc: Location = { uri, range: diag.range }; + const text = TaggedText_stripTags(diag.message); + const severityClass = diag.severity ? { + [DiagnosticSeverity.Error]: 'error', + [DiagnosticSeverity.Warning]: 'warning', + [DiagnosticSeverity.Information]: 'information', + [DiagnosticSeverity.Hint]: 'hint', + }[diag.severity] : ''; + const title = `${fname}:${line+1}:${character}`; + return ( + //
+ // {title} + // + // { e.preventDefault(); void ec.revealLocation(loc); }} + // title="reveal file location"> + // {e.preventDefault(); void ec.copyToComment(text)}} + // title="copy message to comment"> + // {e.preventDefault(); void ec.api.copyToClipboard(text)}} + // title="copy message to clipboard"> + // + // +
+

{title}

+ 
+                
+
+
+ //
+ ) +}, fastIsEqual) + +function mkMessageViewProps(uri: DocumentUri, messages: InteractiveDiagnostic[]): MessageViewProps[] { + const views: MessageViewProps[] = messages + .sort((msga, msgb) => { + const a = msga.fullRange?.end || msga.range.end; + const b = msgb.fullRange?.end || msgb.range.end; + return a.line === b.line ? a.character - b.character : a.line - b.line + }).map(m => { + return { uri, diag: m }; + }); + + return addUniqueKeys(views, v => DocumentPosition.toString({uri: v.uri, ...v.diag.range.start})); +} + +/** Shows the given messages assuming they are for the given file. */ +export const MessagesList = React.memo(({uri, messages}: {uri: DocumentUri, messages: InteractiveDiagnostic[]}) => { + const should_hide = messages.length === 0; + if (should_hide) { return <>No messages. } + + return ( +
+ {mkMessageViewProps(uri, messages).map(m => )} +
+ ); +}) + +function lazy(f: () => T): () => T { + let state: {t: T} | undefined + return () => { + if (!state) state = {t: f()} + return state.t + } +} + +/** Displays all messages for the specified file. Can be paused. */ +export function AllMessages({uri: uri0}: { uri: DocumentUri }) { + const ec = React.useContext(EditorContext); + const sv = React.useContext(VersionContext); + const rs0 = useRpcSessionAtPos({ uri: uri0, line: 0, character: 0 }); + const dc = React.useContext(LspDiagnosticsContext); + const config = React.useContext(ConfigContext); + const diags0 = dc.get(uri0) || []; + + const iDiags0 = React.useMemo(() => lazy(async () => { + try { + const diags = await getInteractiveDiagnostics(rs0); + if (diags.length > 0) { + return diags + } + } catch (err: any) { + if (err?.code === RpcErrorCode.ContentModified) { + // Document has been changed since we made the request. This can happen + // while typing quickly. When the server catches up on next edit, it will + // send new diagnostics to which the infoview responds by calling + // `getInteractiveDiagnostics` again. + } else { + console.log('getInteractiveDiagnostics error ', err) + } + } + return diags0.map(d => ({ ...(d as LeanDiagnostic), message: { text: d.message } })); + }), [sv, rs0, uri0, diags0]); + const [{ isPaused, setPaused }, [uri, rs, diags, iDiags], _] = usePausableState(false, [uri0, rs0, diags0, iDiags0]); + + // Fetch interactive diagnostics when we're entering the paused state + // (if they haven't already been fetched before) + React.useEffect(() => { if (isPaused) { void iDiags() } }, [iDiags, isPaused]); + + const setOpenRef = React.useRef>>(); + useEvent(ec.events.requestedAction, act => { + if (act.kind === 'toggleAllMessages' && setOpenRef.current !== undefined) { + setOpenRef.current(t => !t); + } + }); + + return ( + +
+ + All Messages ({diags.length}) + + { e.preventDefault(); setPaused(p => !p); }} + title={isPaused ? 'continue updating' : 'pause updating'}> + + + + +
+ + ) +} + +/** We factor out the body of {@link AllMessages} which lazily fetches its contents only when expanded. */ +function AllMessagesBody({uri, messages}: {uri: DocumentUri, messages: () => Promise}) { + const [msgs, setMsgs] = React.useState(undefined) + React.useEffect(() => { void messages().then(setMsgs) }, [messages]) + if (msgs === undefined) return <>Loading messages... + else return +} + +/** + * Provides a `LspDiagnosticsContext` which stores the latest version of the + * diagnostics as sent by the publishDiagnostics notification. + */ +export function WithLspDiagnosticsContext({children}: React.PropsWithChildren<{}>) { + const [allDiags, _0] = useServerNotificationState( + 'textDocument/publishDiagnostics', + new Map(), + async (params: PublishDiagnosticsParams) => diags => + new Map(diags).set(params.uri, params.diagnostics), + [] + ) + + return {children} +} + +/** Embeds a non-interactive diagnostic into the type `InteractiveDiagnostic`. */ +export function lspDiagToInteractive(diag: Diagnostic): InteractiveDiagnostic { + return { ...(diag as LeanDiagnostic), message: { text: diag.message } }; +}