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

do not display any errors before the first step #209

Browse Source
This commit is contained in:
Jon Eugster
2024-06-11 23:08:05 +02:00
parent 1f14ad185f
commit aed2899fb6
1 changed files with 5 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/infoview/main.tsx
+5 -3
View File
@@ -339,7 +339,7 @@ function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, dele
// ) // )
// }, fastIsEqual) // }, fastIsEqual)
/** The tabs of goals that lean ahs after the command of this step has been processed */ /** The tabs of goals that lean has after the command of this step has been processed */
function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofStep: InteractiveGoalsWithHints, last : boolean, onClick? : any, onGoalChange?: (n?: number) => void }) { function GoalsTabs({ proofStep, last, onClick, onGoalChange=(n)=>{}}: { proofStep: InteractiveGoalsWithHints, last : boolean, onClick? : any, onGoalChange?: (n?: number) => void }) {
let { t } = useTranslation() let { t } = useTranslation()
const [selectedGoal, setSelectedGoal] = React.useState<number>(0) const [selectedGoal, setSelectedGoal] = React.useState<number>(0)
@@ -555,8 +555,10 @@ export function TypewriterInterface({props}) {
// </div> // </div>
// } else { // } else {
return <div key={`proof-step-${i}`} className={`step step-${i}` + (selectedStep == i ? ' selected' : '')}> return <div key={`proof-step-${i}`} className={`step step-${i}` + (selectedStep == i ? ' selected' : '')}>
<Command proof={proof} i={i} deleteProof={deleteProof(i)} /> {i > 0 && <>
<Errors errors={step.diags} typewriterMode={true} /> <Command proof={proof} i={i} deleteProof={deleteProof(i)} />
<Errors errors={step.diags} typewriterMode={true} />
</>}
{mobile && i == 0 && props.data?.introduction && {mobile && i == 0 && props.data?.introduction &&
<div className={`message information step-0${selectedStep === 0 ? ' selected' : ''}`} onClick={toggleSelectStep(0)}> <div className={`message information step-0${selectedStep === 0 ? ' selected' : ''}`} onClick={toggleSelectStep(0)}>
<Markdown>{props.data?.introduction}</Markdown> <Markdown>{props.data?.introduction}</Markdown>