phc/lean4game
6
1
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

show other goals only for more than 1 goal

Browse Source
This commit is contained in:
Alexander Bentkamp
2023-01-25 16:22:45 +01:00
parent e3c67a06b8
commit 5bfae3a1c2
1 changed files with 9 additions and 9 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/infoview/info.tsx
+9 -9
View File
@@ -121,10 +121,10 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
<a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate(); }}>{' '}Try again.</a> <a className='link pointer dim' onClick={e => { e.preventDefault(); void triggerUpdate(); }}>{' '}Try again.</a>
</div>} </div>}
<LocationsContext.Provider value={locs}> <LocationsContext.Provider value={locs}>
<div className="goals-section"> {goals && goals.goals.length > 0 && <div className="goals-section">
<div className="goals-section-title">Main Goal</div> <div className="goals-section-title">Main Goal</div>
{goals && goals.goals.length > 0 && <Goal filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} />} <Goal filter={goalFilter} key='mainGoal' goal={goals.goals[0]} showHints={true} />
</div> </div>}
</LocationsContext.Provider> </LocationsContext.Provider>
{/* <FilteredGoals headerChildren='Expected type' key='term-goal' {/* <FilteredGoals headerChildren='Expected type' key='term-goal'
goals={termGoal !== undefined ? {goals: [{...termGoal, hints: []}]} : undefined} /> */} goals={termGoal !== undefined ? {goals: [{...termGoal, hints: []}]} : undefined} /> */}
@@ -154,12 +154,12 @@ const InfoDisplayContent = React.memo((props: InfoDisplayContentProps) => {
<div>Loading goal...</div>)} <div>Loading goal...</div>)}
<AllMessages /> <AllMessages />
<LocationsContext.Provider value={locs}> <LocationsContext.Provider value={locs}>
<div className="goals-section"> {goals && goals.goals.length > 1 && <div className="goals-section">
<div className="goals-section-title">Other Goals</div> <div className="goals-section-title">Other Goals</div>
{goals && goals.goals.slice(1).map((goal, i) => {goals.goals.slice(1).map((goal, i) =>
<details key={i}><summary><InteractiveCode fmt={goal.type} /></summary> <Goal filter={goalFilter} goal={goal} /></details>)} <details key={i}><summary><InteractiveCode fmt={goal.type} /></summary> <Goal filter={goalFilter} goal={goal} /></details>)}
</div> </div>}
</LocationsContext.Provider> </LocationsContext.Provider>
</> </>
}) })