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

small improvements to the client

Browse Source
This commit is contained in:
Jon Eugster
2023-08-11 18:25:52 +02:00
parent d00a2337d4
commit 735f58be95
5 changed files with 24 additions and 14 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/hints.tsx
+7 -7
View File
@@ -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 <div className={`message information step-${step}` + (step == selected ? ' selected' : '')} onClick={toggleSelection}>
export function Hint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
return <div className={`message information step-${step}` + (step == selected ? ' selected' : '') + (lastLevel ? ' recent' : '')} onClick={toggleSelection}>
<Markdown>{hint.text}</Markdown>
</div>
}
export function HiddenHint({hint, step, selected, toggleSelection} : {hint: GameHint, step: number, selected: number, toggleSelection: any}) {
return <div className={`message warning step-${step}` + (step == selected ? ' selected' : '')} onClick={toggleSelection}>
export function HiddenHint({hint, step, selected, toggleSelection, lastLevel} : {hint: GameHint, step: number, selected: number, toggleSelection: any, lastLevel?: boolean}) {
return <div className={`message warning step-${step}` + (step == selected ? ' selected' : '') + (lastLevel ? ' recent' : '')} onClick={toggleSelection}>
<Markdown>{hint.text}</Markdown>
</div>
}
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) => <Hint key={`hint-${step}-${j}`} hint={hint} step={step} selected={selected} toggleSelection={toggleSelection}/>)}
{showHidden && hiddenHints.map((hint, j) => <HiddenHint key={`hidden-hint-${step}-${j}`} hint={hint} step={step} selected={selected} toggleSelection={toggleSelection}/>)}
{openHints.map((hint, j) => <Hint key={`hint-${step}-${j}`} hint={hint} step={step} selected={selected} toggleSelection={toggleSelection} lastLevel={lastLevel} />)}
{showHidden && hiddenHints.map((hint, j) => <HiddenHint key={`hidden-hint-${step}-${j}`} hint={hint} step={step} selected={selected} toggleSelection={toggleSelection} lastLevel={lastLevel} />)}
</>
}
client/src/components/infoview/command_line.tsx
+2 -2
View File
@@ -64,7 +64,7 @@ config.autoClosingPairs = config.autoClosingPairs.map(
monaco.languages.setLanguageConfiguration('lean4cmd', config);
/** The input field */
export function CommandLine({proofPanelRef}: {proofPanelRef: React.MutableRefObject<HTMLDivElement>}) {
export function CommandLine({proofPanelRef, hidden}: {proofPanelRef: React.MutableRefObject<HTMLDivElement>, 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 <div className="command-line">
return <div className={`command-line${hidden ? ' hidden' : ''}`}>
<form onSubmit={handleSubmit}>
<div className="command-line-input-wrapper">
<div ref={inputRef} className="command-line-input" />
client/src/components/infoview/main.tsx
+1 -1
View File
@@ -475,6 +475,6 @@ export function CommandLineInterface(props: { world: string, level: number, data
</>
: <CircularProgress />}
</div>
<CommandLine proofPanelRef={proofPanelRef} />
<CommandLine proofPanelRef={proofPanelRef} hidden={proof[proof.length - 1]?.goals.length == 0}/>
</div>
}
client/src/components/level.css
+4
View File
@@ -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);
client/src/components/level.tsx
+10 -4
View File
@@ -140,17 +140,17 @@ function ChatPanel({lastLevel}) {
// TODO: Should not use index as key.
return <Hints key={`hints-${i}`}
hints={step.hints} showHidden={showHelp.has(i)} step={i}
selected={selectedStep} toggleSelection={toggleSelection(i)}/>
selected={selectedStep} toggleSelection={toggleSelection(i)} lastLevel={i == proof.length - 1}/>
}
})}
<DeletedHints hints={deletedChat}/>
{completed &&
<>
<div className={`message information step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
<div className={`message information recent step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
Level completed! 🎉
</div>
{level?.data?.conclusion?.trim() &&
<div className={`message information step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
<div className={`message information recent step-${k}${selectedStep == k ? ' selected' : ''}`} onClick={toggleSelection(k)}>
<Markdown>{level?.data?.conclusion}</Markdown>
</div>
}
@@ -439,6 +439,7 @@ function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber = undef
return <div className="app-bar" style={isLoading ? {display: "none"} : null} >
{mobile ?
<>
{/* MOBILE VERSION */}
<div>
<span className="app-bar-title">
{levelTitle}
@@ -492,6 +493,7 @@ function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber = undef
</>
:
<>
{/* DESKTOP VERSION */}
<div>
<Button to={`/${gameId}`} inverted="true" title="back to world selection" id="home-btn">
<FontAwesomeIcon icon={faHome} />
@@ -514,13 +516,17 @@ function LevelAppBar({isLoading, levelTitle, toggleImpressum, pageNumber = undef
<FontAwesomeIcon icon={faArrowLeft} />&nbsp;Previous
</Button>
</>}
{levelId < gameInfo.data?.worldSize[worldId] &&
{levelId < gameInfo.data?.worldSize[worldId] ?
<Button inverted="true"
to={`/${gameId}/world/${worldId}/level/${levelId + 1}`} title="next level"
disabled={difficulty >= 2 && !(completed || levelId == 0)}
onClick={() => setNavOpen(false)}>
<FontAwesomeIcon icon={faArrowRight} />&nbsp;{levelId ? "Next" : "Start"}
</Button>
:
<Button to={`/${gameId}`} inverted="true" title="back to world selection" id="home-btn">
<FontAwesomeIcon icon={faHome} />&nbsp;Leave World
</Button>
}
<Button disabled={levelId <= 0} inverted="true" to=""
onClick={(ev) => { setCommandLineMode(!commandLineMode); setNavOpen(false) }}