From 805b0b94c100508d5c6391a6b3a66bbd19d13530 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Fri, 14 Jul 2023 13:34:57 +0200 Subject: [PATCH] cleanup --- client/src/components/infoview/context.ts | 9 -- client/src/components/infoview/info.tsx | 181 +++++++++++----------- client/src/components/infoview/main.tsx | 2 +- client/src/components/level.css | 2 +- client/src/components/level.tsx | 18 +-- 5 files changed, 97 insertions(+), 115 deletions(-) diff --git a/client/src/components/infoview/context.ts b/client/src/components/infoview/context.ts index 719b022..f5751aa 100644 --- a/client/src/components/infoview/context.ts +++ b/client/src/components/infoview/context.ts @@ -37,15 +37,6 @@ export const ProofContext = React.createContext<{ setProof: () => {} // TODO: implement me }) -// TODO: Is this still used? -export const HintContext = React.createContext<{ - showHiddenHints : boolean, - setShowHiddenHints: React.Dispatch> -}>({ - showHiddenHints: true, - setShowHiddenHints: () => {}, -}); - export interface ProofStateProps { // pos: DocumentPosition; status: InfoStatus; diff --git a/client/src/components/infoview/info.tsx b/client/src/components/infoview/info.tsx index 9085eeb..e65a56e 100644 --- a/client/src/components/infoview/info.tsx +++ b/client/src/components/infoview/info.tsx @@ -1,54 +1,50 @@ /* Mostly copied from https://github.com/leanprover/vscode-lean4/blob/master/lean4-infoview/src/infoview/info.tsx */ -import * as React from 'react'; -import { CircularProgress } from '@mui/material'; - - -import type { Location, Diagnostic } from 'vscode-languageserver-protocol'; - -import { getInteractiveTermGoal, InteractiveDiagnostic, - UserWidgetInstance, Widget_getWidgets, RpcSessionAtPos, isRpcError, - RpcErrorCode, getInteractiveDiagnostics, InteractiveTermGoal } from '@leanprover/infoview-api'; +import * as React from 'react' +import { CircularProgress } from '@mui/material' +import type { Location, Diagnostic } from 'vscode-languageserver-protocol' +import { getInteractiveTermGoal, InteractiveDiagnostic, UserWidgetInstance, Widget_getWidgets, RpcSessionAtPos, isRpcError, + RpcErrorCode, getInteractiveDiagnostics, InteractiveTermGoal } from '@leanprover/infoview-api' 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'; + 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 { 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'; +import { RpcContext, useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions' +import { GoalsLocation, Locations, LocationsContext } from '../../../../node_modules/lean4-infoview/src/infoview/goalLocation' -import { AllMessages, lspDiagToInteractive, MessagesList } from './messages'; -import { goalsToString, Goal, MainAssumptions, OtherGoals, FilteredGoals, ProofDisplay } from './goals' -import { InteractiveGoal, InteractiveGoals } from './rpc_api'; -import { InputModeContext, MonacoEditorContext, HintContext, ProofStateProps, InfoStatus, ProofStateContext } from './context' +import { AllMessages, lspDiagToInteractive } from './messages' +import { goalsToString, Goal, MainAssumptions, OtherGoals, ProofDisplay } from './goals' +import { InteractiveGoals } from './rpc_api' +import { MonacoEditorContext, ProofStateProps, InfoStatus, ProofContext } from './context' - -type InfoKind = 'cursor' | 'pin'; +// TODO: All about pinning could probably be removed +type InfoKind = 'cursor' | 'pin' interface InfoPinnable { - kind: InfoKind; + kind: InfoKind /** Takes an argument for caching reasons, but should only ever (un)pin itself. */ - onPin: (pos: DocumentPosition) => void; + onPin: (pos: DocumentPosition) => void } interface InfoStatusBarProps extends InfoPinnable, PausableProps { - pos: DocumentPosition; - status: InfoStatus; - triggerUpdate: () => Promise; + pos: DocumentPosition + status: InfoStatus + triggerUpdate: () => Promise } const InfoStatusBar = React.memo((props: InfoStatusBarProps) => { - const { kind, onPin, status, pos, isPaused, setPaused, triggerUpdate } = props; + const { kind, onPin, status, pos, isPaused, setPaused, triggerUpdate } = props - const ec = React.useContext(EditorContext); + 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'; + const statusColor = statusColTable[status] + const locationString = `${basename(pos.uri)}:${pos.line+1}:${pos.character}` + const isPinned = kind === 'pin' return ( @@ -68,36 +64,36 @@ const InfoStatusBar = React.memo((props: InfoStatusBarProps) => { title={isPinned ? 'unpin' : 'pin'} /> { e.preventDefault(); setPaused(!isPaused); }} + onClick={e => { e.preventDefault(); setPaused(!isPaused) }} title={isPaused ? 'continue updating' : 'pause updating'} /> { e.preventDefault(); void triggerUpdate(); }} + onClick={e => { e.preventDefault(); void triggerUpdate() }} title='update'/> - ); + ) }) interface InfoDisplayContentProps extends PausableProps { - pos: DocumentPosition; - messages: InteractiveDiagnostic[]; - goals?: InteractiveGoals; - termGoal?: InteractiveTermGoal; - error?: string; - userWidgets: UserWidgetInstance[]; - triggerUpdate: () => Promise; - proof? : string; + pos: DocumentPosition + messages: InteractiveDiagnostic[] + goals?: InteractiveGoals + termGoal?: InteractiveTermGoal + error?: string + userWidgets: UserWidgetInstance[] + triggerUpdate: () => Promise + proof? : string } const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => { - const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused, proof} = props; + const {pos, messages, goals, termGoal, error, userWidgets, triggerUpdate, isPaused, setPaused, proof} = props - const hasWidget = userWidgets.length > 0; - const hasError = !!error; - const hasMessages = messages.length !== 0; + const hasWidget = userWidgets.length > 0 + const hasError = !!error + const hasMessages = messages.length !== 0 - const nothingToShow = !hasError && !goals && !termGoal && !hasMessages && !hasWidget; + const nothingToShow = !hasError && !goals && !termGoal && !hasMessages && !hasWidget const [selectedLocs, setSelectedLocs] = React.useState([]) React.useEffect(() => setSelectedLocs([]), [pos.uri, pos.line, pos.character]) @@ -122,12 +118,13 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => { {hasError &&
Error updating:{' '}{error}. - { e.preventDefault(); void triggerUpdate(); }}>{' '}Try again. + { e.preventDefault(); void triggerUpdate() }}>{' '}Try again.
}
{ goals && goals.goals.length > 0 && <> + }
@@ -149,8 +146,8 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => { 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 + { e.preventDefault(); void triggerUpdate() }}>Refresh + {' '}or { e.preventDefault(); setPaused(false) }}>resume updating {' '}to see information. : <>
Loading goal...
)} @@ -167,44 +164,49 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => { }) interface InfoDisplayProps { - pos: DocumentPosition; - userWidgets: UserWidgetInstance[]; - rpcSess: RpcSessionAtPos; - triggerUpdate: () => Promise; + 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: ProofStateProps & 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); + const [shouldRefresh, setShouldRefresh] = React.useState(false) + const [{ isPaused, setPaused }, props, propsRef] = usePausableState(false, props0) if (shouldRefresh) { - propsRef.current = props0; - setShouldRefresh(false); + propsRef.current = props0 + setShouldRefresh(false) } const triggerDisplayUpdate = async () => { - await props0.triggerUpdate(); - setShouldRefresh(true); - }; + await props0.triggerUpdate() + setShouldRefresh(true) + } - const {kind, goals, rpcSess} = props; + const {kind, goals, rpcSess} = props - const ec = React.useContext(EditorContext); + 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'; + 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]); + 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); - }); + if (!isCursor) return + if (act.kind !== 'togglePaused') return + setPaused(isPaused => !isPaused) + }) const editor = React.useContext(MonacoEditorContext) @@ -217,7 +219,7 @@ function InfoDisplay(props0: ProofStateProps & InfoDisplayProps & InfoPinnable) {/* */} - ); + ) } /** @@ -225,7 +227,7 @@ function InfoDisplay(props0: ProofStateProps & InfoDisplayProps & InfoPinnable) * 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 }; +export type InfoProps = InfoPinnable & { pos?: DocumentPosition } /** Fetches info from the server and renders an {@link InfoDisplay}. */ export function Info(props: InfoProps) { @@ -234,28 +236,24 @@ export function Info(props: InfoProps) { } function InfoAtCursor(props: InfoProps) { - const ec = React.useContext(EditorContext); + 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 }; + 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)); + 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) { - // TODO: proofStateContext is not quite implemented correctly yet. - // i.e. there is an asynchronous state in this file that seems to partally overlap - // search for `const [state, triggerUpdateCore]` - const hintContext = React.useContext(HintContext) - const proofStateContext = React.useContext(ProofStateContext) + const proofContext = React.useContext(ProofContext) const config = React.useContext(ConfigContext) @@ -291,9 +289,9 @@ function InfoAux(props: InfoProps) { // 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 + type InfoRequestResult = Omit const [state, triggerUpdateCore] = useAsyncWithTrigger(() => new Promise((resolve, reject) => { - const goalsReq = rpcSess.call('Game.getInteractiveGoals', DocumentPosition.toTdpp(pos)); + const goalsReq = rpcSess.call('Game.getInteractiveGoals', 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}) @@ -390,6 +388,11 @@ function InfoAux(props: InfoProps) { const [displayProps, setDisplayProps] = React.useState({ pos, + status: 'updating', + messages: [], + goals: undefined, + termGoal: undefined, + error: undefined, userWidgets: [], rpcSess, triggerUpdate @@ -403,14 +406,12 @@ function InfoAux(props: InfoProps) { if (state.state === 'notStarted') void triggerUpdate() else if (state.state === 'loading') { - proofStateContext.setProofState(dp => ({ ...dp, status: 'updating' })) setDisplayProps(dp => ({ ...dp, status: 'updating' })) } else if (state.state === 'resolved') { // if (state.value.goals?.goals?.length) { // hintContext.setHints(state.value.goals.goals[0].hints) // } - proofStateContext.setProofState({ ...state.value }) setDisplayProps({ ...state.value, triggerUpdate }) } else if (state.state === 'rejected' && state.error !== 'retry') { // The code inside `useAsyncWithTrigger` may only ever reject with a `retry` exception. @@ -418,5 +419,5 @@ function InfoAux(props: InfoProps) { } }, [state]) - return + return } diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index 7a8fa23..626d4fe 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -27,7 +27,7 @@ import Markdown from '../markdown'; import { Infos } from './infos'; import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages'; import { Goal } from './goals'; -import { InputModeContext, MonacoEditorContext, ProofContext, ProofStateContext, ProofStep } from './context'; +import { InputModeContext, MonacoEditorContext, ProofContext, ProofStep } from './context'; import { CommandLine, hasErrors, hasInteractiveErrors } from './command_line'; import { InteractiveDiagnostic } from '@leanprover/infoview/*'; import { Button } from '../button'; diff --git a/client/src/components/level.css b/client/src/components/level.css index d62f284..cfb3d86 100644 --- a/client/src/components/level.css +++ b/client/src/components/level.css @@ -220,7 +220,7 @@ td code { background-color: #eee; padding: .5rem; border-radius: .5rem; - margin-top: 1rem; + margin-top: 2rem; } .exercise .step { diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index dd8ea40..338bdca 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -39,7 +39,7 @@ import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api'; import { changedSelection, codeEdited, selectCode, selectSelections, progressSlice, selectCompleted } from '../state/progress'; import { DualEditor } from './infoview/main' import { Hints } from './hints'; -import { HintContext, InputModeContext, MonacoEditorContext, ProofContext, ProofStateContext, ProofStateProps, ProofStep } from './infoview/context'; +import { InputModeContext, MonacoEditorContext, ProofContext, ProofStep } from './infoview/context'; function Level() { @@ -74,15 +74,6 @@ function PlayableLevel({worldId, levelId}) { const [showHiddenHints, setShowHiddenHints] = useState(false) - - const [proofState, setProofState] = React.useState({ - status: 'updating', - messages: [], - goals: undefined, - termGoal: undefined, - error: undefined, - }) - const theme = useTheme(); useEffect(() => { @@ -105,6 +96,9 @@ function PlayableLevel({worldId, levelId}) { } }, [commandLineMode]) + /** Unused. Was implementing an undo button, which has been replaced by `deleteProof` inside + * `CommandLineInterface`. + */ const handleUndo = () => { const endPos = editor.getModel().getFullModelRange().getEndPosition() let range @@ -189,10 +183,8 @@ function PlayableLevel({worldId, levelId}) { return <>
- -
@@ -248,10 +240,8 @@ function PlayableLevel({worldId, levelId}) { }
- - }