diff --git a/client/src/components/hints.tsx b/client/src/components/hints.tsx
index 39c5513..2692a7d 100644
--- a/client/src/components/hints.tsx
+++ b/client/src/components/hints.tsx
@@ -2,27 +2,27 @@ import { GameHint } from "./infoview/rpc_api";
import * as React from 'react';
import Markdown from './markdown';
-export function Hint({hint, step, selected, toggleSelection} : {hint: GameHint, step: number, selected: number, toggleSelection: any}) {
- return
+export function Hint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
+ return
{hint.text}
}
-export function HiddenHint({hint, step, selected, toggleSelection} : {hint: GameHint, step: number, selected: number, toggleSelection: any}) {
- return
+export function HiddenHint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
+ return
{hint.text}
}
-export function Hints({hints, showHidden, step, selected, toggleSelection} : {hints: GameHint[], showHidden: boolean, step: number, selected: number, toggleSelection: any}) {
+export function Hints({hints, showHidden, step, selected, toggleSelection, lastLevel} : {hints: GameHint[], showHidden: boolean, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
const openHints = hints.filter(hint => !hint.hidden)
const hiddenHints = hints.filter(hint => hint.hidden)
// TODO: Should not use index as key.
return <>
- {openHints.map((hint, j) =>
)}
- {showHidden && hiddenHints.map((hint, j) => )}
+ {openHints.map((hint, j) => )}
+ {showHidden && hiddenHints.map((hint, j) => )}
>
}
diff --git a/client/src/components/infoview/command_line.tsx b/client/src/components/infoview/command_line.tsx
index c93a1ec..100d54b 100644
--- a/client/src/components/infoview/command_line.tsx
+++ b/client/src/components/infoview/command_line.tsx
@@ -64,7 +64,7 @@ config.autoClosingPairs = config.autoClosingPairs.map(
monaco.languages.setLanguageConfiguration('lean4cmd', config);
/** The input field */
-export function CommandLine({proofPanelRef}: {proofPanelRef: React.MutableRefObject}) {
+export function CommandLine({proofPanelRef, hidden}: {proofPanelRef: React.MutableRefObject, hidden?: boolean}) {
/** Reference to the hidden multi-line editor */
const editor = React.useContext(MonacoEditorContext)
@@ -311,7 +311,7 @@ export function CommandLine({proofPanelRef}: {proofPanelRef: React.MutableRefObj
runCommand()
}
- return
+ return
}
diff --git a/client/src/components/level.css b/client/src/components/level.css
index 3d39dfb..103921b 100644
--- a/client/src/components/level.css
+++ b/client/src/components/level.css
@@ -258,6 +258,10 @@ td code {
margin-right: .5em;
}
+.chat .recent {
+ box-shadow: .0em .0em .4em .1em #8cbbe9;
+}
+
.exercise .step.selected, .chat .selected {
/* border: 3px solid #5191d1; */
box-shadow: .0em .0em .4em .1em var(--clr-primary);
diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx
index 8be5b71..074154b 100644
--- a/client/src/components/level.tsx
+++ b/client/src/components/level.tsx
@@ -140,17 +140,17 @@ function ChatPanel({lastLevel}) {
// TODO: Should not use index as key.
return
+ selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.length - 1}/>
}
})}
{completed &&
<>
-
+
Level completed! 🎉
{level?.data?.conclusion?.trim() &&
-
+
{level?.data?.conclusion}
}
@@ -439,6 +439,7 @@ function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber = undef
return
{mobile ?
<>
+ {/* MOBILE VERSION */}
{levelTitle}
@@ -492,6 +493,7 @@ function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber = undef
>
:
<>
+ {/* DESKTOP VERSION */}
>}
- {levelId < gameInfo.data?.worldSize[worldId] &&
+ {levelId < gameInfo.data?.worldSize[worldId] ?
+ :
+
}