From 5e4a959c8a31aafb6a5aae0362365df217e89d6e Mon Sep 17 00:00:00 2001 From: Jon Eugster Date: Sat, 29 Jul 2023 16:41:59 +0200 Subject: [PATCH] move next-level-buttons on mobile --- client/src/components/infoview/main.tsx | 108 ++++++++++++------------ 1 file changed, 56 insertions(+), 52 deletions(-) diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index a230f45..6316e89 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -413,63 +413,67 @@ export function CommandLineInterface(props: { world: string, level: number, data
- {proof.length ? proof.map((step, i) => { - if (i == proof.length - 1 && hasInteractiveErrors(step.errors)) { - // if the last command contains an error, we only display the errors but not the - // entered command as it is still present in the command line. - // TODO: Should not use index as key. - return
- -
- } else { - return
- - - {mobile && i == 0 && props.data?.introduction && -
- {props.data?.introduction} + {proof.length ? + <> + {proof.map((step, i) => { + if (i == proof.length - 1 && hasInteractiveErrors(step.errors)) { + // if the last command contains an error, we only display the errors but not the + // entered command as it is still present in the command line. + // TODO: Should not use index as key. + return
+
- } - {mobile && <> - - {i == proof.length - 1 && hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) && - - } - - } - - {/* Show a message that there are no goals left */} - {!step.goals.length && ( -
- {completed ? -

Level completed! 🎉

: -

- no goals left
- This probably means you solved the level with warnings or Lean encountered a parsing error. -

+ } else { + return
+ + + {mobile && i == 0 && props.data?.introduction && +
+ {props.data?.introduction} +
} -
- )} - {completed && i == proof.length - 1 && -
- {props.level >= props.worldSize ? - - : - + {mobile && <> + + {i == proof.length - 1 && hasHiddenHints(proof.length - 1) && !showHelp.has(k - withErr) && + + } + } + + {/* Show a message that there are no goals left */} + {!step.goals.length && ( +
+ {completed ? +

Level completed! 🎉

: +

+ no goals left
+ This probably means you solved the level with warnings or Lean encountered a parsing error. +

+ } +
+ )}
} -
- } - }) : } + })} + {mobile && completed && +
+ {props.level >= props.worldSize ? + + : + + } +
+ } + + : }