bug fix: no goals

client/src/components/infoview/command_line.tsx

@@ -121,6 +121,17 @@ export function CommandLine({proofPanelRef}: {proofPanelRef: React.MutableRefObj
               msg.message.append[0].text === "unsolved goals")
           })
 
+          if (typeof goals == 'undefined') {
+            tmpProof.push({
+              command: i ? model.getLineContent(i) : '',
+              goals: [],
+              hints: [],
+              errors: messages
+            } as ProofStep)
+            console.debug('goals is undefined')
+            return
+          }
+
           // If the number of goals reduce, show a message
           if (goals.goals.length && goalCount > goals.goals.length) {
             messages.unshift({
@@ -141,36 +152,26 @@ export function CommandLine({proofPanelRef}: {proofPanelRef: React.MutableRefObj
           }
           goalCount = goals.goals.length
 
-          // TODO: Check what happens if the code gets into a bad state and no goals are available
+          console.debug(`Command (${i}): `, i ? model.getLineContent(i) : '')
-          if (!goals) {
+          console.debug(`Goals: (${i}): `, goalsToString(goals)) //
-            tmpProof.push({
+          console.debug(`Hints: (${i}): `, goals.goals[0]?.hints)
-              command: i ? model.getLineContent(i) : '',
+          console.debug(`Errors: (${i}): `, messages)
-              goals: [],
+
-              hints: [],
+          // with no goals there will be no hints
-              errors: messages
+          let hints = goals.goals.length ? goals.goals[0].hints : []
-            } as ProofStep)
+
-          } else {
+          tmpProof.push({
-
+            // the command of the line above. Note that `getLineContent` starts counting
-            console.debug(`Command (${i}): `, i ? model.getLineContent(i) : '')
+            // at `1` instead of `zero`. The first ProofStep will have an empty command.
-            console.debug(`Goals: (${i}): `, goalsToString(goals)) //
+            command: i ? model.getLineContent(i) : '',
-            console.debug(`Hints: (${i}): `, goals.goals[0]?.hints)
+            // TODO: store correct data
-            console.debug(`Errors: (${i}): `, messages)
+            goals: goals.goals,
-
+            // only need the hints of the active goals in chat
-            // with no goals there will be no hints
+            hints: hints,
-            let hints = goals.goals.length ? goals.goals[0].hints : []
+            // errors and messages from the server
+            errors: messages
+          } as ProofStep)
 
-            tmpProof.push({
-              // the command of the line above. Note that `getLineContent` starts counting
-              // at `1` instead of `zero`. The first ProofStep will have an empty command.
-              command: i ? model.getLineContent(i) : '',
-              // TODO: store correct data
-              goals: goals.goals || [],
-              // only need the hints of the active goals in chat
-              hints: hints,
-              // errors and messages from the server
-              errors: messages
-            } as ProofStep)
-          }
         })
         // Save the proof to the context
         setProof(tmpProof)

client/src/components/infoview/main.tsx

@@ -338,7 +338,6 @@ export function CommandLineInterface(props: {world: string, level: number, data:
 
   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. */
   const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig;
 
   const [allProgress, _1] = useServerNotificationState(
@@ -399,7 +398,7 @@ export function CommandLineInterface(props: {world: string, level: number, data:
                   <p>Level completed! 🎉</p> :
                   <p>
                     <b>no goals left</b><br />
-                    <i>This probably means you solved the level with warnings</i>
+                    <i>This probably means you solved the level with warnings or Lean encountered a parsing error.</i>
                   </p>
                 }
               </div>

client/src/components/level.tsx

@@ -212,6 +212,8 @@ function PlayableLevel({worldId, levelId}) {
     }
   }
 
+  let k = proof.length - 1
+
   return <>
     <div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
     <SelectionContext.Provider value={{selectedStep, setSelectedStep}}>
@@ -238,11 +240,11 @@ function PlayableLevel({worldId, levelId}) {
             })}
             {completed &&
               <>
-                <div className="message information">
+                <div className={`message information step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
                   Level completed! 🎉
                 </div>
                 {level?.data?.conclusion?.trim() &&
-                  <div className="message information">
+                  <div className={`message information step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
                     <Markdown>{level?.data?.conclusion}</Markdown>
                   </div>
                 }