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

scroll to selected step

Browse Source
This commit is contained in:
Jon Eugster
2023-07-16 23:01:55 +02:00
parent 0a2c4552bf
commit 446a33e5e8
5 changed files with 36 additions and 12 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/hints.tsx
+7 -7
View File
@@ -2,25 +2,25 @@ import { GameHint } from "./infoview/rpc_api";
import * as React from 'react';
import Markdown from './markdown';
export function Hint({hint, selected, toggleSelection} : {hint: GameHint, selected: boolean, toggleSelection: any}) {
return <div className={"message information" + (selected ? ' selected' : '')} onClick={toggleSelection}>
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}>
<Markdown>{hint.text}</Markdown>
</div>
}
export function AdditionalHint({hint, selected, toggleSelection} : {hint: GameHint, selected: boolean, toggleSelection: any}) {
return <div className={"message warning" + (selected ? ' selected' : '')} onClick={toggleSelection}>
export function AdditionalHint({hint, step, selected, toggleSelection} : {hint: GameHint, step: number, selected: number, toggleSelection: any}) {
return <div className={`message warning step-${step}` + (step == selected ? ' selected' : '')} onClick={toggleSelection}>
<Markdown>{hint.text}</Markdown>
</div>
}
export function Hints({hints, showHidden, selected, toggleSelection} : {hints: GameHint[], showHidden: boolean, selected: boolean, toggleSelection: any}) {
export function Hints({hints, showHidden, step, selected, toggleSelection} : {hints: GameHint[], showHidden: boolean, step: number, selected: number, toggleSelection: any}) {
const openHints = hints.filter(hint => !hint.hidden)
const hiddenHints = hints.filter(hint => hint.hidden)
return <>
{openHints.map(hint => <Hint hint={hint} selected={selected} toggleSelection={toggleSelection}/>)}
{showHidden && hiddenHints.map(hint => <AdditionalHint hint={hint} selected={selected} toggleSelection={toggleSelection}/>)}
{openHints.map(hint => <Hint hint={hint} step={step} selected={selected} toggleSelection={toggleSelection}/>)}
{showHidden && hiddenHints.map(hint => <AdditionalHint hint={hint} step={step} selected={selected} toggleSelection={toggleSelection}/>)}
</>
}