Merge branch 'main' of github.com:leanprover-community/lean4game

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 = <Hints hints={goal.hints} />
+    const hints = <Hints hints={goal.hints} key={goal.mvarId} />
     const objectHyps = hyps.filter(hyp => !hyp.isAssumption)
     const assumptionHyps = hyps.filter(hyp => hyp.isAssumption)
     const {commandLineMode} = React.useContext(InputModeContext)

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}))
         },
         []
     );