phc
/
lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

cleanup

Browse Source
pull/118/head
Jon Eugster 3 years ago
parent bd7dc02e70
commit 805b0b94c1
5 changed files with 97 additions and 115 deletions
Show Stats Download Patch File Download Diff File

9
client/src/components/infoview/context.ts
Unescape Escape View File

@ -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<React.SetStateAction<boolean>>
}>({
showHiddenHints: true,
setShowHiddenHints: () => {},
});
export interface ProofStateProps {
// pos: DocumentPosition;
status: InfoStatus;

181
client/src/components/infoview/info.tsx
Unescape Escape View File

@ -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<void>;
pos: DocumentPosition
status: InfoStatus
triggerUpdate: () => Promise<void>
}
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 (
<summary style={{transition: 'color 0.5s ease'}} className={'mv2 pointer ' + statusColor}>
@ -68,36 +64,36 @@ const InfoStatusBar = React.memo((props: InfoStatusBarProps) => {
title={isPinned ? 'unpin' : 'pin'} />
<a className={'link pointer mh2 dim codicon ' + (isPaused ? 'codicon-debug-continue ' : 'codicon-debug-pause ')}
data-id='toggle-paused'
onClick={e => { e.preventDefault(); setPaused(!isPaused); }}
onClick={e => { e.preventDefault(); setPaused(!isPaused) }}
title={isPaused ? 'continue updating' : 'pause updating'} />
<a className='link pointer mh2 dim codicon codicon-refresh'
data-id='update'
onClick={e => { e.preventDefault(); void triggerUpdate(); }}
onClick={e => { e.preventDefault(); void triggerUpdate() }}
title='update'/>
</span>
</summary>
);
)
})
interface InfoDisplayContentProps extends PausableProps {
pos: DocumentPosition;
messages: InteractiveDiagnostic[];
goals?: InteractiveGoals;
termGoal?: InteractiveTermGoal;
error?: string;
userWidgets: UserWidgetInstance[];
triggerUpdate: () => Promise<void>;
proof? : string;
pos: DocumentPosition
messages: InteractiveDiagnostic[]
goals?: InteractiveGoals
termGoal?: InteractiveTermGoal
error?: string
userWidgets: UserWidgetInstance[]
triggerUpdate: () => Promise<void>
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<GoalsLocation[]>([])
React.useEffect(() => setSelectedLocs([]), [pos.uri, pos.line, pos.character])
@ -122,12 +118,13 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
{hasError &&
<div className='error' key='errors'>
Error updating:{' '}{error}.
<a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate(); }}>{' '}Try again.</a>
<a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate() }}>{' '}Try again.</a>
</div>}
<LocationsContext.Provider value={locs}>
<div className="goals-section">
{ goals && goals.goals.length > 0 && <>
<MainAssumptions filter={goalFilter} key='mainGoal' goals={goals.goals} />
<ProofDisplay proof={proof}/>
<OtherGoals filter={goalFilter} goals={goals.goals} />
</>}
</div>
@ -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 */
<span>Updating is paused.{' '}
<a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate(); }}>Refresh</a>
{' '}or <a className='link pointer dim' onClick={e => { e.preventDefault(); setPaused(false); }}>resume updating</a>
<a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate() }}>Refresh</a>
{' '}or <a className='link pointer dim' onClick={e => { e.preventDefault(); setPaused(false) }}>resume updating</a>
{' '}to see information.
</span> :
<><CircularProgress /><div>Loading goal...</div></>)}
@ -167,44 +164,49 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
})
interface InfoDisplayProps {
pos: DocumentPosition;
userWidgets: UserWidgetInstance[];
rpcSess: RpcSessionAtPos;
triggerUpdate: () => Promise<void>;
pos: DocumentPosition,
status: InfoStatus,
messages: InteractiveDiagnostic[],
goals?: InteractiveGoals,
termGoal?: InteractiveTermGoal,
error?: string,
userWidgets: UserWidgetInstance[],
rpcSess: RpcSessionAtPos,
triggerUpdate: () => Promise<void>,
}
/** 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<boolean>(false);
const [{ isPaused, setPaused }, props, propsRef] = usePausableState(false, props0);
const [shouldRefresh, setShouldRefresh] = React.useState<boolean>(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)
</div>
{/* </details> */}
</RpcContext.Provider>
);
)
}
/**
@ -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<Location>(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<Location>(ec.events.changedCursorLocation.current!)
useEvent(ec.events.changedCursorLocation, loc => loc && setCurLoc(loc), [])
const pos = { uri: curLoc.uri, ...curLoc.range.start }
return <InfoAux {...props} pos={pos} />
}
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<ProofStateProps & InfoDisplayProps, 'triggerUpdate'>
type InfoRequestResult = Omit<InfoDisplayProps, 'triggerUpdate'>
const [state, triggerUpdateCore] = useAsyncWithTrigger(() => new Promise<InfoRequestResult>((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<InfoDisplayProps>({
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 <InfoDisplay kind={props.kind} onPin={props.onPin} {...proofStateContext.proofState} {...displayProps} />
return <InfoDisplay kind={props.kind} onPin={props.onPin} {...displayProps} />
}

2
client/src/components/infoview/main.tsx
Unescape Escape View File

@ -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';

2
client/src/components/level.css
Unescape Escape View File

@ -220,7 +220,7 @@ td code {
background-color: #eee;
padding: .5rem;
border-radius: .5rem;
margin-top: 1rem;
margin-top: 2rem;
}
.exercise .step {

18
client/src/components/level.tsx
Unescape Escape View File

@ -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<ProofStateProps>({
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 <>
<div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
<ProofStateContext.Provider value={{proofState, setProofState}}>
<InputModeContext.Provider value={{commandLineMode, setCommandLineMode, commandLineInput, setCommandLineInput}}>
<ProofContext.Provider value={{proof, setProof}}>
<HintContext.Provider value={{showHiddenHints, setShowHiddenHints}}>
<LevelAppBar isLoading={level.isLoading} levelTitle={levelTitle} worldId={worldId} levelId={levelId} />
<Split minSize={0} snapOffset={200} sizes={[25, 50, 25]} className={`app-content level ${level.isLoading ? 'hidden' : ''}`}>
<div ref={chatPanelRef} className="chat-panel">
@ -248,10 +240,8 @@ function PlayableLevel({worldId, levelId}) {
}
</div>
</Split>
</HintContext.Provider>
</ProofContext.Provider>
</InputModeContext.Provider>
</ProofStateContext.Provider>
</>
}

Write Preview
Loading…
Cancel
Save