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

selecting hints and proof steps

Browse Source
This commit is contained in:
Jon Eugster
2023-07-14 18:14:21 +02:00
parent d0316b734a
commit d40fd1d6cb
5 changed files with 72 additions and 15 deletions
Download Patch File Download Diff File Expand all files Collapse all files
client/src/components/hints.tsx
+11 -7
View File
@@ -2,21 +2,25 @@ import { GameHint } from "./infoview/rpc_api";
import * as React from 'react';
import Markdown from './markdown';
export function Hint({hint} : {hint: GameHint}) {
return <div className="message information"><Markdown>{hint.text}</Markdown></div>
export function Hint({hint, selected, toggleSelection} : {hint: GameHint, selected: boolean, toggleSelection: any}) {
return <div className={"message information" + (selected ? ' selected' : '')} onClick={toggleSelection}>
<Markdown>{hint.text}</Markdown>
</div>
}
export function AdditionalHint({hint} : {hint: GameHint}) {
return <div className="message warning"><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}>
<Markdown>{hint.text}</Markdown>
</div>
}
export function Hints({hints, showHidden} : {hints: GameHint[], showHidden: boolean}) {
export function Hints({hints, showHidden, selected, toggleSelection} : {hints: GameHint[], showHidden: boolean, selected: boolean, toggleSelection: any}) {
const openHints = hints.filter(hint => !hint.hidden)
const hiddenHints = hints.filter(hint => hint.hidden)
return <>
{openHints.map(hint => <Hint hint={hint} />)}
{showHidden && hiddenHints.map(hint => <AdditionalHint hint={hint}/>)}
{openHints.map(hint => <Hint hint={hint} selected={selected} toggleSelection={toggleSelection}/>)}
{showHidden && hiddenHints.map(hint => <AdditionalHint hint={hint} selected={selected} toggleSelection={toggleSelection}/>)}
</>
}
client/src/components/infoview/context.ts
+10
View File
@@ -62,6 +62,16 @@ export const ProofStateContext = React.createContext<{
setProofState: () => {},
});
/** Context to keep highlight selected proof step and corresponding chat messages. */
export const SelectionContext = React.createContext<{
selectedStep : number,
setSelectedStep: React.Dispatch<React.SetStateAction<number>>
}>({
selectedStep : undefined,
setSelectedStep: () => {}
})
export const InputModeContext = React.createContext<{
commandLineMode: boolean,
setCommandLineMode: React.Dispatch<React.SetStateAction<boolean>>,
client/src/components/infoview/main.tsx
+18 -3
View File
@@ -27,7 +27,7 @@ import Markdown from '../markdown';
import { Infos } from './infos';
import { AllMessages, Errors, WithLspDiagnosticsContext } from './messages';
import { Goal } from './goals';
import { InputModeContext, MonacoEditorContext, ProofContext, ProofStep } from './context';
import { InputModeContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext } from './context';
import { CommandLine, hasErrors, hasInteractiveErrors } from './command_line';
import { InteractiveDiagnostic } from '@leanprover/infoview/*';
import { Button } from '../button';
@@ -255,7 +255,7 @@ function GoalsTab({proofStep} : {proofStep: ProofStep}) {
return <div>
<div className="tab-bar">
{proofStep.goals.map((goal, i) => (
<div className={`tab ${i == (selectedGoal) ? "active": ""}`} onClick={() => { setSelectedGoal(i) }}>
<div className={`tab ${i == (selectedGoal) ? "active": ""}`} onClick={(ev) => { setSelectedGoal(i); ev.stopPropagation() }}>
{i ? `Goal ${i+1}` : "Active Goal"}
</div>
))}
@@ -273,6 +273,7 @@ export function CommandLineInterface(props: {world: string, level: number, data:
const editor = React.useContext(MonacoEditorContext)
const gameId = React.useContext(GameIdContext)
const {proof} = React.useContext(ProofContext)
const {selectedStep, setSelectedStep} = React.useContext(SelectionContext)
const proofPanelRef = React.useRef<HTMLDivElement>(null)
@@ -308,6 +309,20 @@ export function CommandLineInterface(props: {world: string, level: number, data:
text: '',
forceMoveMarkers: false
}])
setSelectedStep(undefined)
ev.stopPropagation()
}
}
function selectStep(line: number) {
return (ev) => {
if (selectedStep == line) {
setSelectedStep(undefined)
console.debug(`unselected step`)
} else {
setSelectedStep(line)
console.debug(`step ${line} selected`)
}
}
}
@@ -363,7 +378,7 @@ export function CommandLineInterface(props: {world: string, level: number, data:
</div>
} else {
return <>
<div className="step">
<div className={'step' + (selectedStep == i ? ' selected' : '')} onClick={selectStep(i)}>
<Command command={step.command} deleteProof={deleteProof(i)}/>
<Errors errors={step.errors} commandLineMode={true}/>
<GoalsTab proofStep={step}/>
client/src/components/level.css
+15 -3
View File
@@ -35,8 +35,8 @@
}
.chat-panel, .infoview, .exercise-statement {
padding-left: 1em;
padding-right: 1em;
padding-left: .5em;
padding-right: .5em;
}
.conclusion {
@@ -209,7 +209,7 @@ td code {
.commandline-interface .content {
flex: 1 1 auto;
overflow-y: scroll;
padding: 1em;
padding: .5em;
}
/* TODO: Create a nice style and move this to a better place */
@@ -227,5 +227,17 @@ td code {
/* background-color: #e6f0f4; */
margin-top: 5px;
margin-bottom: 5px;
border-radius: 0.5em;
padding: 0.5em;
/* border: 3px dotted rgb(88, 131, 24); */
}
.chat .message {
margin-left: .5em;
margin-right: .5em;
}
.exercise .step.selected, .chat .selected {
/* border: 3px solid #5191d1; */
box-shadow: .0em .0em .4em .1em var(--clr-primary);
}
client/src/components/level.tsx
+18 -2
View File
@@ -39,7 +39,7 @@ import { useGetGameInfoQuery, useLoadLevelQuery } from '../state/api';
import { changedSelection, codeEdited, selectCode, selectSelections, progressSlice, selectCompleted } from '../state/progress';
import { DualEditor } from './infoview/main'
import { Hints } from './hints';
import { InputModeContext, MonacoEditorContext, ProofContext, ProofStep } from './infoview/context';
import { InputModeContext, MonacoEditorContext, ProofContext, ProofStep, SelectionContext } from './infoview/context';
function Level() {
@@ -58,6 +58,7 @@ function Level() {
function PlayableLevel({worldId, levelId}) {
const codeviewRef = useRef<HTMLDivElement>(null)
const chatRef = useRef<HTMLDivElement>(null)
const gameId = React.useContext(GameIdContext)
@@ -74,6 +75,8 @@ function PlayableLevel({worldId, levelId}) {
const [showHiddenHints, setShowHiddenHints] = useState(false)
const [selectedStep, setSelectedStep] = useState<number>()
const theme = useTheme();
useEffect(() => {
@@ -188,8 +191,20 @@ function PlayableLevel({worldId, levelId}) {
// TODO: with the new design, there is no difference between the introduction and
// a hint at the beginning of the proof...
function toggleSelection(line: number) {
return (ev) => {
console.debug('toggled selection')
if (selectedStep == line) {
setSelectedStep(undefined)
} else {
setSelectedStep(line)
}
}
}
return <>
<div style={level.isLoading ? null : {display: "none"}} className="app-content loading"><CircularProgress /></div>
<SelectionContext.Provider value={{selectedStep, setSelectedStep}}>
<InputModeContext.Provider value={{commandLineMode, setCommandLineMode, commandLineInput, setCommandLineInput}}>
<ProofContext.Provider value={{proof, setProof}}>
<LevelAppBar isLoading={level.isLoading} levelTitle={levelTitle} worldId={worldId} levelId={levelId} />
@@ -202,7 +217,7 @@ function PlayableLevel({worldId, levelId}) {
</div>
}
{proof.map((step, i) => {
return <Hints hints={step.hints} showHidden={showHiddenHints}/>
return <Hints hints={step.hints} showHidden={showHiddenHints} selected={i == selectedStep} toggleSelection={toggleSelection(i)}/>
})}
{completed &&
<>
@@ -249,6 +264,7 @@ function PlayableLevel({worldId, levelId}) {
</Split>
</ProofContext.Provider>
</InputModeContext.Provider>
</SelectionContext.Provider>
</>
}