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

fix ts warnings

Browse Source
This commit is contained in:
Jon Eugster
2024-03-11 12:18:30 +01:00
parent 68f84a3426
commit edf1085310
2 changed files with 4 additions and 3 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/level.tsx
+2 -2
View File
@@ -127,7 +127,7 @@ function ChatPanel({lastLevel, visible = true}) {
{introText?.filter(t => t.trim()).map(((t, i) => {introText?.filter(t => t.trim()).map(((t, i) =>
// Show the level's intro text as hints, too // Show the level's intro text as hints, too
<Hint key={`intro-p-${i}`} <Hint key={`intro-p-${i}`}
hint={{text: t, hidden: false}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} /> hint={{text: t, hidden: false, rawText: t, varNames: []}} step={0} selected={selectedStep} toggleSelection={toggleSelection(0)} />
))} ))}
{proof.steps.map((step, i) => { {proof.steps.map((step, i) => {
let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints) let filteredHints = filterHints(step.goals[0]?.hints, proof?.steps[i-1]?.goals[0]?.hints)
@@ -427,7 +427,7 @@ function IntroductionPanel({gameInfo}) {
<div className="chat"> <div className="chat">
{text?.filter(t => t.trim()).map(((t, i) => {text?.filter(t => t.trim()).map(((t, i) =>
<Hint key={`intro-p-${i}`} <Hint key={`intro-p-${i}`}
hint={{text: t, hidden: false}} step={0} selected={null} toggleSelection={undefined} /> hint={{text: t, hidden: false, rawText: t, varNames: []}} step={0} selected={null} toggleSelection={undefined} />
))} ))}
</div> </div>
<div className={`button-row${mobile ? ' mobile' : ''}`}> <div className={`button-row${mobile ? ' mobile' : ''}`}>
tsconfig.json
+2 -1
View File
@@ -12,7 +12,8 @@
"experimentalDecorators": true, "experimentalDecorators": true,
"allowSyntheticDefaultImports": true, "allowSyntheticDefaultImports": true,
"lib": [ "lib": [
"ES2021.String" "ES2021.String",
"DOM"
] ]
}, },
"exclude": ["server", "relay"] "exclude": ["server", "relay"]