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

show exercise name even if no text present

Browse Source
This commit is contained in:
Jon Eugster
2024-04-25 15:10:51 +02:00
parent 06cc52bb7e
commit 1daef0d80f
1 changed files with 4 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/infoview/main.tsx
+4 -1
View File
@@ -142,9 +142,12 @@ function ExerciseStatement({ data, showLeanStatement = false }) {
if (!(data?.descrText || data?.descrFormat)) { return <></> } if (!(data?.descrText || data?.descrFormat)) { return <></> }
return <> return <>
<div className="exercise-statement"> <div className="exercise-statement">
{data?.descrText && {data?.descrText ?
<Markdown> <Markdown>
{(data?.displayName ? `**${t("Theorem")}** \`${data?.displayName}\`: ` : '') + t(data?.descrText, {ns: gameId})} {(data?.displayName ? `**${t("Theorem")}** \`${data?.displayName}\`: ` : '') + t(data?.descrText, {ns: gameId})}
</Markdown> : data?.displayName &&
<Markdown>
{`**${t("Theorem")}** \`${data?.displayName}\``}
</Markdown> </Markdown>
} }
{data?.descrFormat && showLeanStatement && {data?.descrFormat && showLeanStatement &&