From 95480a752d4985d31a90a4820875376d2a00e93f Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sun, 16 Jul 2023 18:51:59 +0200 Subject: [PATCH] fix loading issue --- client/src/components/infoview/command_line.tsx | 6 ++++++ client/src/components/infoview/main.tsx | 1 - 2 files changed, 6 insertions(+), 1 deletion(-) diff --git a/client/src/components/infoview/command_line.tsx b/client/src/components/infoview/command_line.tsx index d9fc2f3..f1f037c 100644 --- a/client/src/components/infoview/command_line.tsx +++ b/client/src/components/infoview/command_line.tsx @@ -285,6 +285,12 @@ export function CommandLine({proofPanelRef}: {proofPanelRef: React.MutableRefObj return () => { l.dispose() } }, [oneLineEditor, runCommand]) + //TODO: Intention is to run once when loading, does that work? + useEffect(() => { + console.debug('time to update') + loadAllGoals(proofPanelRef) + }, []) + /** Process the entered command */ const handleSubmit : React.FormEventHandler = (ev) => { ev.preventDefault() diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index f31541f..3c3f21e 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -335,7 +335,6 @@ export function CommandLineInterface(props: {world: string, level: number, data: } }, [selectedStep]) - const completed = useAppSelector(selectCompleted(gameId, props.world, props.level)) /* Set up updates to the global infoview seither you solved the level with warnings or your last command contains a syntax error Lean can't parseate on editor events. */