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

fix client breaking if server timed out.

Browse Source
pull/204/head
Jon Eugster 2 years ago
parent edf1085310
commit f3f077741d
4 changed files with 42 additions and 40 deletions
Show Stats Download Patch File Download Diff File

8
client/src/components/hints.tsx
Unescape Escape View File

@ -91,12 +91,14 @@ export function MoreHelpButton({selected=null} : {selected?: number}) {
const {proof, setProof} = React.useContext(ProofContext) const {proof, setProof} = React.useContext(ProofContext)
const {deletedChat, setDeletedChat, showHelp, setShowHelp} = React.useContext(DeletedChatContext) const {deletedChat, setDeletedChat, showHelp, setShowHelp} = React.useContext(DeletedChatContext)
let k = (selected === null) ? (proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected let k = proof?.steps.length ?
((selected === null) ? (proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)) : selected)
: 0
const activateHiddenHints = (ev) => { const activateHiddenHints = (ev) => {
// If the last step (`k`) has errors, we want the hidden hints from the // If the last step (`k`) has errors, we want the hidden hints from the
// second-to-last step to be affected // second-to-last step to be affected
if (!(proof.steps.length)) {return} if (!(proof?.steps.length)) {return}
// state must not be mutated, therefore we need to clone the set // state must not be mutated, therefore we need to clone the set
let tmp = new Set(showHelp) let tmp = new Set(showHelp)
@ -109,7 +111,7 @@ export function MoreHelpButton({selected=null} : {selected?: number}) {
console.debug(`help: ${Array.from(tmp.values())}`) console.debug(`help: ${Array.from(tmp.values())}`)
} }
if (hasHiddenHints(proof.steps[k]) && !showHelp.has(k)) { if (hasHiddenHints(proof?.steps[k]) && !showHelp.has(k)) {
return <Button to="" onClick={activateHiddenHints}> return <Button to="" onClick={activateHiddenHints}>
Show more help! Show more help!
</Button> </Button>

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

@ -67,7 +67,7 @@ function DualEditorMain({ worldId, levelId, level, worldSize }: { worldId: strin
const dispatch = useAppDispatch() const dispatch = useAppDispatch()
React.useEffect(() => { React.useEffect(() => {
if (proof.completed) { if (proof?.completed) {
dispatch(levelCompleted({ game: gameId, world: worldId, level: levelId })) dispatch(levelCompleted({ game: gameId, world: worldId, level: levelId }))
// On completion, add the names of all new items to the local storage // On completion, add the names of all new items to the local storage
@ -232,16 +232,16 @@ export function Main(props: { world: string, level: number, data: LevelInfo}) {
ret = <div><p>{serverStoppedResult.message}</p><p className="error">{serverStoppedResult.reason}</p></div> ret = <div><p>{serverStoppedResult.message}</p><p className="error">{serverStoppedResult.reason}</p></div>
} else { } else {
ret = <div className="infoview vscode-light"> ret = <div className="infoview vscode-light">
{proof.completedWithWarnings && {proof?.completedWithWarnings &&
<div className="level-completed"> <div className="level-completed">
{proof.completed ? "Level completed! 🎉" : "Level completed with warnings 🎭"} {proof?.completed ? "Level completed! 🎉" : "Level completed with warnings 🎭"}
</div> </div>
} }
<Infos /> <Infos />
<Hints hints={proof.steps[curPos?.line]?.goals[0]?.hints} <Hints hints={proof?.steps[curPos?.line]?.goals[0]?.hints}
showHidden={showHelp.has(curPos?.line)} step={curPos?.line} showHidden={showHelp.has(curPos?.line)} step={curPos?.line}
selected={selectedStep} toggleSelection={toggleSelection(curPos?.line)} selected={selectedStep} toggleSelection={toggleSelection(curPos?.line)}
lastLevel={curPos?.line == proof.steps.length - 1}/> lastLevel={curPos?.line == proof?.steps.length - 1}/>
<MoreHelpButton selected={curPos?.line}/> <MoreHelpButton selected={curPos?.line}/>
</div> </div>
} }
@ -266,11 +266,11 @@ function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, dele
// If the last step has errors, we display the command in a different style // If the last step has errors, we display the command in a different style
// indicating that it will be removed on the next try. // indicating that it will be removed on the next try.
return <div className="failed-command"> return <div className="failed-command">
<i>Failed command</i>: {proof.steps[i].command} <i>Failed command</i>: {proof?.steps[i].command}
</div> </div>
} else { } else {
return <div className="command"> return <div className="command">
<div className="command-text">{proof.steps[i].command}</div> <div className="command-text">{proof?.steps[i].command}</div>
<Button to="" className="undo-button btn btn-inverted" title="Retry proof from here" onClick={deleteProof}> <Button to="" className="undo-button btn btn-inverted" title="Retry proof from here" onClick={deleteProof}>
<FontAwesomeIcon icon={faDeleteLeft} />&nbsp;Retry <FontAwesomeIcon icon={faDeleteLeft} />&nbsp;Retry
</Button> </Button>
@ -414,7 +414,7 @@ export function TypewriterInterface({props}) {
function deleteProof(line: number) { function deleteProof(line: number) {
return (ev) => { return (ev) => {
let deletedChat: Array<GameHint> = [] let deletedChat: Array<GameHint> = []
proof.steps.slice(line).map((step, i) => { proof?.steps.slice(line).map((step, i) => {
let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints) let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
// Only add these hidden hints to the deletion stack which were visible // Only add these hidden hints to the deletion stack which were visible
@ -431,7 +431,7 @@ export function TypewriterInterface({props}) {
forceMoveMarkers: false forceMoveMarkers: false
}]) }])
setSelectedStep(undefined) setSelectedStep(undefined)
setTypewriterInput(proof.steps[line].command) setTypewriterInput(proof?.steps[line].command)
// Reload proof on deleting // Reload proof on deleting
loadGoals(rpcSess, uri, setProof) loadGoals(rpcSess, uri, setProof)
ev.stopPropagation() ev.stopPropagation()
@ -453,7 +453,7 @@ export function TypewriterInterface({props}) {
// Scroll to the end of the proof if it is updated. // Scroll to the end of the proof if it is updated.
React.useEffect(() => { React.useEffect(() => {
if (proof.steps.length > 1) { if (proof?.steps.length > 1) {
proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0) proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0)
} else { } else {
proofPanelRef.current?.scrollTo(0,0) proofPanelRef.current?.scrollTo(0,0)
@ -475,7 +475,7 @@ export function TypewriterInterface({props}) {
}, [selectedStep]) }, [selectedStep])
// TODO: superfluous, can be replaced with `withErr` from above // TODO: superfluous, can be replaced with `withErr` from above
let lastStepErrors = proof.steps.length ? hasInteractiveErrors(getInteractiveDiagsAt(proof, proof.steps.length)) : false let lastStepErrors = proof?.steps.length ? hasInteractiveErrors(getInteractiveDiagsAt(proof, proof?.steps.length)) : false
useServerNotificationEffect("$/game/loading", (params : any) => { useServerNotificationEffect("$/game/loading", (params : any) => {
@ -495,12 +495,12 @@ export function TypewriterInterface({props}) {
</div> </div>
<div className='proof' ref={proofPanelRef}> <div className='proof' ref={proofPanelRef}>
<ExerciseStatement data={props.data} /> <ExerciseStatement data={props.data} />
{proof.steps.length ? {proof?.steps.length ?
<> <>
{proof.steps.map((step, i) => { {proof?.steps.map((step, i) => {
let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints) let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
// if (i == proof.steps.length - 1 && hasInteractiveErrors(step.diags)) { // if (i == proof?.steps.length - 1 && hasInteractiveErrors(step.diags)) {
// // if the last command contains an error, we only display the errors but not the // // if the last command contains an error, we only display the errors but not the
// // entered command as it is still present in the command line. // // entered command as it is still present in the command line.
// // TODO: Should not use index as key. // // TODO: Should not use index as key.
@ -521,18 +521,18 @@ export function TypewriterInterface({props}) {
hints={filteredHints} showHidden={showHelp.has(i)} step={i} hints={filteredHints} showHidden={showHelp.has(i)} step={i}
selected={selectedStep} toggleSelection={toggleSelectStep(i)}/> selected={selectedStep} toggleSelection={toggleSelectStep(i)}/>
} }
{/* <GoalsTabs proofStep={step} last={i == proof.steps.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.steps.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/> */} {/* <GoalsTabs proofStep={step} last={i == proof?.steps.length - (lastStepErrors ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof?.steps.length - 1 - withErr ? (n) => setDisableInput(n > 0) : (n) => {}}/> */}
{!(isLastStepWithErrors(proof, i)) && {!(isLastStepWithErrors(proof, i)) &&
<GoalsTabs proofStep={step} last={i == proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1) ? (n) => setDisableInput(n > 0) : (n) => {}}/> <GoalsTabs proofStep={step} last={i == proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1)} onClick={toggleSelectStep(i)} onGoalChange={i == proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) ? (n) => setDisableInput(n > 0) : (n) => {}}/>
} }
{mobile && i == proof.steps.length - 1 && {mobile && i == proof?.steps.length - 1 &&
<MoreHelpButton /> <MoreHelpButton />
} }
{/* Show a message that there are no goals left */} {/* Show a message that there are no goals left */}
{/* {!step.goals.length && ( {/* {!step.goals.length && (
<div className="message information"> <div className="message information">
{proof.completed ? {proof?.completed ?
<p>Level completed! 🎉</p> : <p>Level completed! 🎉</p> :
<p> <p>
<b>no goals left</b><br /> <b>no goals left</b><br />
@ -545,12 +545,12 @@ export function TypewriterInterface({props}) {
} }
//} //}
)} )}
{proof.diagnostics.length > 0 && {proof?.diagnostics.length > 0 &&
<div key={`proof-step-remaining`} className="step step-remaining"> <div key={`proof-step-remaining`} className="step step-remaining">
<Errors errors={proof.diagnostics} typewriterMode={true} /> <Errors errors={proof?.diagnostics} typewriterMode={true} />
</div> </div>
} }
{mobile && proof.completed && {mobile && proof?.completed &&
<div className="button-row mobile"> <div className="button-row mobile">
{props.level >= props.worldSize ? {props.level >= props.worldSize ?
<Button to={`/${gameId}`}> <Button to={`/${gameId}`}>
@ -567,7 +567,7 @@ export function TypewriterInterface({props}) {
} }
</div> </div>
</div> </div>
<Typewriter disabled={disableInput || !proof.steps.length}/> <Typewriter disabled={disableInput || !proof?.steps.length}/>
</RpcContext.Provider> </RpcContext.Provider>
</div> </div>
} }

10
client/src/components/infoview/typewriter.tsx
Unescape Escape View File

@ -230,7 +230,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
/** If the last step has an error, add the command to the typewriter. */ /** If the last step has an error, add the command to the typewriter. */
useEffect(() => { useEffect(() => {
if (lastStepHasErrors(proof)) { if (lastStepHasErrors(proof)) {
setTypewriterInput(proof.steps[proof.steps.length - 1].command) setTypewriterInput(proof?.steps[proof?.steps.length - 1].command)
} }
}, [proof]) }, [proof])
@ -344,7 +344,7 @@ export function Typewriter({disabled}: {disabled?: boolean}) {
} }
// do not display if the proof is completed (with potential warnings still present) // do not display if the proof is completed (with potential warnings still present)
return <div className={`typewriter${proof.completedWithWarnings ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}> return <div className={`typewriter${proof?.completedWithWarnings ? ' hidden' : ''}${disabled ? ' disabled' : ''}`}>
<form onSubmit={handleSubmit}> <form onSubmit={handleSubmit}>
<div className="typewriter-input-wrapper"> <div className="typewriter-input-wrapper">
<div ref={inputRef} className="typewriter-input" /> <div ref={inputRef} className="typewriter-input" />
@ -376,10 +376,10 @@ export function hasInteractiveErrors (diags: InteractiveDiagnostic[]) {
export function getInteractiveDiagsAt (proof: ProofState, k : number) { export function getInteractiveDiagsAt (proof: ProofState, k : number) {
if (k == 0) { if (k == 0) {
return [] return []
} else if (k >= proof.steps.length-1) { } else if (k >= proof?.steps.length-1) {
// TODO: Do we need that? // TODO: Do we need that?
return proof.diagnostics.filter(msg => msg.range.start.line >= proof.steps.length-1) return proof?.diagnostics.filter(msg => msg.range.start.line >= proof?.steps.length-1)
} else { } else {
return proof.diagnostics.filter(msg => msg.range.start.line == k-1) return proof?.diagnostics.filter(msg => msg.range.start.line == k-1)
} }
} }

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

@ -84,7 +84,7 @@ function ChatPanel({lastLevel, visible = true}) {
const {selectedStep, setSelectedStep} = useContext(SelectionContext) const {selectedStep, setSelectedStep} = useContext(SelectionContext)
const completed = useAppSelector(selectCompleted(gameId, worldId, levelId)) const completed = useAppSelector(selectCompleted(gameId, worldId, levelId))
let k = proof.steps.length - (lastStepHasErrors(proof) ? 2 : 1) let k = proof?.steps.length ? proof?.steps.length - (lastStepHasErrors(proof) ? 2 : 1) : 0
function toggleSelection(line: number) { function toggleSelection(line: number) {
return (ev) => { return (ev) => {
@ -129,27 +129,27 @@ function ChatPanel({lastLevel, visible = true}) {
<Hint key={`intro-p-${i}`} <Hint key={`intro-p-${i}`}
hint={{text: t, hidden: false, rawText: t, varNames: []}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} /> hint={{text: t, hidden: false, rawText: t, varNames: []}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
))} ))}
{proof.steps.map((step, i) => { {proof?.steps.map((step, i) => {
let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints) let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
if (step.goals.length > 0 && !isLastStepWithErrors(proof, i)) { if (step.goals.length > 0 && !isLastStepWithErrors(proof, i)) {
return <Hints key={`hints-${i}`} return <Hints key={`hints-${i}`}
hints={filteredHints} showHidden={showHelp.has(i)} step={i} hints={filteredHints} showHidden={showHelp.has(i)} step={i}
selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.steps.length - 1}/> selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof?.steps.length - 1}/>
} }
})} })}
{/* {modifiedHints.map((step, i) => { {/* {modifiedHints.map((step, i) => {
// It the last step has errors, it will have the same hints // It the last step has errors, it will have the same hints
// as the second-to-last step. Therefore we should not display them. // as the second-to-last step. Therefore we should not display them.
if (!(i == proof.steps.length - 1 && withErr)) { if (!(i == proof?.steps.length - 1 && withErr)) {
// TODO: Should not use index as key. // TODO: Should not use index as key.
return <Hints key={`hints-${i}`} return <Hints key={`hints-${i}`}
hints={step} showHidden={showHelp.has(i)} step={i} hints={step} showHidden={showHelp.has(i)} step={i}
selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.steps.length - 1}/> selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof?.steps.length - 1}/>
} }
})} */} })} */}
<DeletedHints hints={deletedChat}/> <DeletedHints hints={deletedChat}/>
{proof.completed && {proof?.completed &&
<> <>
<div className={`message information recent step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}> <div className={`message information recent step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
Level completed! 🎉 Level completed! 🎉
@ -163,7 +163,7 @@ function ChatPanel({lastLevel, visible = true}) {
} }
</div> </div>
<div className="button-row"> <div className="button-row">
{proof.completed && (lastLevel ? {proof?.completed && (lastLevel ?
<Button to={`/${gameId}`}> <Button to={`/${gameId}`}>
<FontAwesomeIcon icon={faHome} />&nbsp;Leave World <FontAwesomeIcon icon={faHome} />&nbsp;Leave World
</Button> : </Button> :
@ -334,15 +334,15 @@ function PlayableLevel({impressum, setImpressum}) {
useEffect(() => { useEffect(() => {
// Forget whether hidden hints are displayed for steps that don't exist yet // Forget whether hidden hints are displayed for steps that don't exist yet
if (proof.steps.length) { if (proof?.steps.length) {
console.debug(Array.from(showHelp)) console.debug(Array.from(showHelp))
setShowHelp(new Set(Array.from(showHelp).filter(i => (i < proof.steps.length)))) setShowHelp(new Set(Array.from(showHelp).filter(i => (i < proof?.steps.length))))
} }
}, [proof]) }, [proof])
// save showed help in store // save showed help in store
useEffect(() => { useEffect(() => {
if (proof.steps.length) { if (proof?.steps.length) {
console.debug(`showHelp:\n ${showHelp}`) console.debug(`showHelp:\n ${showHelp}`)
dispatch(helpEdited({game: gameId, world: worldId, level: levelId, help: Array.from(showHelp)})) dispatch(helpEdited({game: gameId, world: worldId, level: levelId, help: Array.from(showHelp)}))
} }

Write Preview
Loading…
Cancel
Save