From aed2899fb6193c8ffd2b2b0165abfe86404a0424 Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Tue, 11 Jun 2024 23:08:05 +0200 Subject: [PATCH] do not display any errors before the first step #209 --- client/src/components/infoview/main.tsx | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index 45a8d18..f9d4c62 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -339,7 +339,7 @@ function Command({ proof, i, deleteProof }: { proof: ProofState, i: number, dele // ) // }, 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 }) { let { t } = useTranslation() const [selectedGoal, setSelectedGoal] = React.useState(0) @@ -555,8 +555,10 @@ export function TypewriterInterface({props}) { // // } else { return
- - + {i > 0 && <> + + + } {mobile && i == 0 && props.data?.introduction &&
{props.data?.introduction}