|
|
|
|
@ -413,63 +413,67 @@ export function CommandLineInterface(props: { world: string, level: number, data
|
|
|
|
|
<div className="content" ref={proofPanelRef}>
|
|
|
|
|
<ExerciseStatement data={props.data} />
|
|
|
|
|
<div className="tmp-pusher"></div>
|
|
|
|
|
{proof.length ? proof.map((step, i) => {
|
|
|
|
|
if (i == proof.length - 1 && hasInteractiveErrors(step.errors)) {
|
|
|
|
|
// 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.
|
|
|
|
|
// TODO: Should not use index as key.
|
|
|
|
|
return <div key={`proof-step-${i}`}>
|
|
|
|
|
<Errors errors={step.errors} commandLineMode={true} />
|
|
|
|
|
</div>
|
|
|
|
|
} else {
|
|
|
|
|
return <div key={`proof-step-${i}`} className={`step step-${i}` + (selectedStep == i ? ' selected' : '')} onClick={toggleSelectStep(i)}>
|
|
|
|
|
<Command command={step.command} deleteProof={deleteProof(i)} />
|
|
|
|
|
<Errors errors={step.errors} commandLineMode={true} />
|
|
|
|
|
{mobile && i == 0 && props.data?.introduction &&
|
|
|
|
|
<div className={`message information step-0${selectedStep === 0 ? ' selected' : ''}`} onClick={toggleSelectStep(0)}>
|
|
|
|
|
<Markdown>{props.data?.introduction}</Markdown>
|
|
|
|
|
{proof.length ?
|
|
|
|
|
<>
|
|
|
|
|
{proof.map((step, i) => {
|
|
|
|
|
if (i == proof.length - 1 && hasInteractiveErrors(step.errors)) {
|
|
|
|
|
// 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.
|
|
|
|
|
// TODO: Should not use index as key.
|
|
|
|
|
return <div key={`proof-step-${i}`}>
|
|
|
|
|
<Errors errors={step.errors} commandLineMode={true} />
|
|
|
|
|
</div>
|
|
|
|
|
}
|
|
|
|
|
{mobile && <>
|
|
|
|
|
<Hints key={`hints-${i}`}
|
|
|
|
|
hints={step.hints} showHidden={showHelp.has(i)} step={i}
|
|
|
|
|
selected={selectedStep} toggleSelection={toggleSelectStep(i)}/>
|
|
|
|
|
{i == proof.length - 1 && hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
|
|
|
|
|
<Button className="btn btn-help" to="" onClick={activateHiddenHints}>
|
|
|
|
|
Show more help!
|
|
|
|
|
</Button>
|
|
|
|
|
}
|
|
|
|
|
</>
|
|
|
|
|
}
|
|
|
|
|
<GoalsTab proofStep={step} />
|
|
|
|
|
{/* Show a message that there are no goals left */}
|
|
|
|
|
{!step.goals.length && (
|
|
|
|
|
<div className="message information">
|
|
|
|
|
{completed ?
|
|
|
|
|
<p>Level completed! 🎉</p> :
|
|
|
|
|
<p>
|
|
|
|
|
<b>no goals left</b><br />
|
|
|
|
|
<i>This probably means you solved the level with warnings or Lean encountered a parsing error.</i>
|
|
|
|
|
</p>
|
|
|
|
|
} else {
|
|
|
|
|
return <div key={`proof-step-${i}`} className={`step step-${i}` + (selectedStep == i ? ' selected' : '')} onClick={toggleSelectStep(i)}>
|
|
|
|
|
<Command command={step.command} deleteProof={deleteProof(i)} />
|
|
|
|
|
<Errors errors={step.errors} commandLineMode={true} />
|
|
|
|
|
{mobile && i == 0 && props.data?.introduction &&
|
|
|
|
|
<div className={`message information step-0${selectedStep === 0 ? ' selected' : ''}`} onClick={toggleSelectStep(0)}>
|
|
|
|
|
<Markdown>{props.data?.introduction}</Markdown>
|
|
|
|
|
</div>
|
|
|
|
|
}
|
|
|
|
|
</div>
|
|
|
|
|
)}
|
|
|
|
|
{completed && i == proof.length - 1 &&
|
|
|
|
|
<div className="button-row">
|
|
|
|
|
{props.level >= props.worldSize ?
|
|
|
|
|
<Button to={`/${gameId}`}>
|
|
|
|
|
<FontAwesomeIcon icon={faHome} /> Leave World
|
|
|
|
|
</Button>
|
|
|
|
|
:
|
|
|
|
|
<Button to={`/${gameId}/world/${props.world}/level/${props.level + 1}`}>
|
|
|
|
|
Next <FontAwesomeIcon icon={faArrowRight} />
|
|
|
|
|
</Button>
|
|
|
|
|
{mobile && <>
|
|
|
|
|
<Hints key={`hints-${i}`}
|
|
|
|
|
hints={step.hints} showHidden={showHelp.has(i)} step={i}
|
|
|
|
|
selected={selectedStep} toggleSelection={toggleSelectStep(i)}/>
|
|
|
|
|
{i == proof.length - 1 && hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) &&
|
|
|
|
|
<Button className="btn btn-help" to="" onClick={activateHiddenHints}>
|
|
|
|
|
Show more help!
|
|
|
|
|
</Button>
|
|
|
|
|
}
|
|
|
|
|
</>
|
|
|
|
|
}
|
|
|
|
|
<GoalsTab proofStep={step} />
|
|
|
|
|
{/* Show a message that there are no goals left */}
|
|
|
|
|
{!step.goals.length && (
|
|
|
|
|
<div className="message information">
|
|
|
|
|
{completed ?
|
|
|
|
|
<p>Level completed! 🎉</p> :
|
|
|
|
|
<p>
|
|
|
|
|
<b>no goals left</b><br />
|
|
|
|
|
<i>This probably means you solved the level with warnings or Lean encountered a parsing error.</i>
|
|
|
|
|
</p>
|
|
|
|
|
}
|
|
|
|
|
</div>
|
|
|
|
|
)}
|
|
|
|
|
</div>
|
|
|
|
|
}
|
|
|
|
|
</div>
|
|
|
|
|
}
|
|
|
|
|
}) : <CircularProgress />}
|
|
|
|
|
})}
|
|
|
|
|
{mobile && completed &&
|
|
|
|
|
<div className="button-row">
|
|
|
|
|
{props.level >= props.worldSize ?
|
|
|
|
|
<Button to={`/${gameId}`}>
|
|
|
|
|
<FontAwesomeIcon icon={faHome} /> Leave World
|
|
|
|
|
</Button>
|
|
|
|
|
:
|
|
|
|
|
<Button to={`/${gameId}/world/${props.world}/level/${props.level + 1}`}>
|
|
|
|
|
Next <FontAwesomeIcon icon={faArrowRight} />
|
|
|
|
|
</Button>
|
|
|
|
|
}
|
|
|
|
|
</div>
|
|
|
|
|
}
|
|
|
|
|
</>
|
|
|
|
|
: <CircularProgress />}
|
|
|
|
|
</div>
|
|
|
|
|
<CommandLine proofPanelRef={proofPanelRef} />
|
|
|
|
|
</div>
|
|
|
|
|
|