fix loading issue
This commit is contained in:
@@ -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<HTMLFormElement> = (ev) => {
|
||||
ev.preventDefault()
|
||||
|
||||
@@ -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. */
|
||||
|
||||
Reference in New Issue
Block a user