From 1c3fa815dabad2e93f6d21448f57efc1da9e8f5d Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Tue, 7 Mar 2023 08:59:23 +0100 Subject: [PATCH 1/2] fix bug: level completed on reload --- client/src/components/infoview/main.tsx | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index bde2910..dcb0ec7 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -33,9 +33,8 @@ export function Main(props: {world: string, level: number}) { if (ec.events.changedCursorLocation.current && ec.events.changedCursorLocation.current.uri === params.uri) { - dispatch(codeEdited) + dispatch(levelCompleted({world: props.world, level: props.level})) } - dispatch(levelCompleted({world: props.world, level: props.level})) }, [] ); From d71f43b8547e2f85dad1b1fb5a0e940cd2566105 Mon Sep 17 00:00:00 2001 From: Alexander Bentkamp Date: Tue, 7 Mar 2023 09:25:57 +0100 Subject: [PATCH 2/2] hide hidden hints again when goal changes --- client/src/components/infoview/goals.tsx | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/client/src/components/infoview/goals.tsx b/client/src/components/infoview/goals.tsx index 6393c0c..2e20c6a 100644 --- a/client/src/components/infoview/goals.tsx +++ b/client/src/components/infoview/goals.tsx @@ -146,7 +146,7 @@ export const Goal = React.memo((props: GoalProps) => { // if (props.goal.isInserted) cn += 'b--inserted ' // if (props.goal.isRemoved) cn += 'b--removed ' - const hints = + const hints = const objectHyps = hyps.filter(hyp => !hyp.isAssumption) const assumptionHyps = hyps.filter(hyp => hyp.isAssumption) const {commandLineMode} = React.useContext(InputModeContext)