diff --git a/client/src/components/hints.tsx b/client/src/components/hints.tsx index f9e1371..39c5513 100644 --- a/client/src/components/hints.tsx +++ b/client/src/components/hints.tsx @@ -32,7 +32,7 @@ export function DeletedHint({hint} : {hint: GameHint}) { } -export function DeletedHints({hints, showHidden} : {hints: GameHint[], showHidden: boolean}) { +export function DeletedHints({hints} : {hints: GameHint[]}) { const openHints = hints.filter(hint => !hint.hidden) const hiddenHints = hints.filter(hint => hint.hidden) @@ -40,6 +40,6 @@ export function DeletedHints({hints, showHidden} : {hints: GameHint[], showHidde // TODO: Should not use index as key. return <> {openHints.map((hint, i) => )} - {showHidden && hiddenHints.map((hint, i) => )} + {hiddenHints.map((hint, i) => )} } diff --git a/client/src/components/infoview/command_line.tsx b/client/src/components/infoview/command_line.tsx index 3991e40..caaf0d3 100644 --- a/client/src/components/infoview/command_line.tsx +++ b/client/src/components/infoview/command_line.tsx @@ -19,7 +19,7 @@ import { DocumentPosition } from '../../../../node_modules/lean4-infoview/src/in import { useRpcSessionAtPos } from '../../../../node_modules/lean4-infoview/src/infoview/rpcSessions'; import { DeletedChatContext, InputModeContext, MonacoEditorContext, ProofContext, ProofStep } from './context' import { goalsToString } from './goals' -import { InteractiveGoals } from './rpc_api' +import { GameHint, InteractiveGoals } from './rpc_api' /* We register a new language `leancmd` that looks like lean4, but does not use the lsp server. */ @@ -155,14 +155,14 @@ export function CommandLine({proofPanelRef}: {proofPanelRef: React.MutableRefObj } goalCount = goals.goals.length + // with no goals there will be no hints. + let hints : GameHint[] = goals.goals.length ? goals.goals[0].hints : [] + console.debug(`Command (${i}): `, i ? model.getLineContent(i) : '') console.debug(`Goals: (${i}): `, goalsToString(goals)) // - console.debug(`Hints: (${i}): `, goals.goals[0]?.hints) + console.debug(`Hints: (${i}): `, hints) console.debug(`Errors: (${i}): `, messages) - // with no goals there will be no hints - let hints = goals.goals.length ? goals.goals[0].hints : [] - tmpProof.push({ // the command of the line above. Note that `getLineContent` starts counting // at `1` instead of `zero`. The first ProofStep will have an empty command. diff --git a/client/src/components/infoview/context.ts b/client/src/components/infoview/context.ts index dfc570a..4549e04 100644 --- a/client/src/components/infoview/context.ts +++ b/client/src/components/infoview/context.ts @@ -75,9 +75,13 @@ export const SelectionContext = React.createContext<{ export const DeletedChatContext = React.createContext<{ deletedChat : GameHint[], setDeletedChat: React.Dispatch>> + showHelp : Set, + setShowHelp: React.Dispatch>> }>({ deletedChat: undefined, - setDeletedChat: () => {} + setDeletedChat: () => {}, + showHelp: undefined, + setShowHelp: () => {} }) export const InputModeContext = React.createContext<{ diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index f83fa9c..433b7ed 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -276,7 +276,7 @@ export function CommandLineInterface(props: {world: string, level: number, data: const gameId = React.useContext(GameIdContext) const {proof} = React.useContext(ProofContext) const {selectedStep, setSelectedStep} = React.useContext(SelectionContext) - const {setDeletedChat} = React.useContext(DeletedChatContext) + const {setDeletedChat, showHelp} = React.useContext(DeletedChatContext) const proofPanelRef = React.useRef(null) @@ -305,8 +305,9 @@ export function CommandLineInterface(props: {world: string, level: number, data: function deleteProof(line: number) { return (ev) => { let deletedChat: Array = [] - proof.slice(line).map(step => { - deletedChat = [...deletedChat, ...step.hints] + proof.slice(line).map((step, i) => { + // Only add these hidden hints to the deletion stack which were visible + deletedChat = [...deletedChat, ...step.hints.filter(hint => (!hint.hidden || showHelp.has(line+i)))] }) setDeletedChat(deletedChat) diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 2a043ab..4aa15e8 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -72,6 +72,9 @@ function PlayableLevel({worldId, levelId}) { // a new proof has been entered. e.g. to consult messages coming from dead ends const [deletedChat, setDeletedChat] = useState>([]) + // A set of row numbers where help is displayed + const [showHelp, setShowHelp] = useState>(new Set()) + const initialCode = useAppSelector(selectCode(gameId, worldId, levelId)) const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId)) @@ -98,7 +101,7 @@ function PlayableLevel({worldId, levelId}) { // TODO: For some reason this is always called twice console.debug('scroll chat') chatRef.current!.lastElementChild?.scrollIntoView() //scrollTo(0,0) - }, [proof, showHiddenHints]) + }, [proof, showHelp]) React.useEffect(() => { if (!commandLineMode) { @@ -121,6 +124,11 @@ function PlayableLevel({worldId, levelId}) { } }, [selectedStep]) + React.useEffect(() => { + // Forget whether hidden hints are displayed for steps that don't exist yet + setShowHelp(new Set(Array.from(showHelp).filter(i => (i < proof.length)))) + }, [proof]) + /** Unused. Was implementing an undo button, which has been replaced by `deleteProof` inside * `CommandLineInterface`. */ @@ -221,7 +229,7 @@ function PlayableLevel({worldId, levelId}) { return <>
- + @@ -240,11 +248,11 @@ function PlayableLevel({worldId, levelId}) { if (!(i == proof.length - 1 && hasInteractiveErrors(step.errors))) { // TODO: Should not use index as key. return } })} - + {completed && <>
@@ -264,7 +272,21 @@ function PlayableLevel({worldId, levelId}) {
setShowHiddenHints((prev) => !prev)} />} + control={ { + console.debug(proof.length) + if (!(proof.length)) {return} + + let k = proof.length - 1 + // state must not be mutated, therefore we need to clone the set + let tmp = new Set(showHelp) + if (tmp.has(k)) { + tmp.delete(k) + } else { + tmp.add(k) + } + setShowHelp(tmp) + console.debug(`help: ${Array.from(tmp.values())}`) + }} />} label="Show more help!" />
diff --git a/client/src/state/progress.ts b/client/src/state/progress.ts index b82fd5b..476d3ca 100644 --- a/client/src/state/progress.ts +++ b/client/src/state/progress.ts @@ -14,7 +14,8 @@ interface Selection { interface LevelProgressState { code: string, selections: Selection[], - completed: boolean + completed: boolean, + help: number[], // A set of rows where hidden hints have been displayed } export interface GameProgressState { @@ -29,7 +30,7 @@ interface ProgressState { const initialProgressState: ProgressState = loadState() ?? { games: {} } // TODO: There was some weird unreproducible bug with removing `as LevelProgressState` here... -const initalLevelProgressState: LevelProgressState = {code: "", completed: false, selections: []} +const initalLevelProgressState: LevelProgressState = {code: "", completed: false, selections: [], help: []} /** Add an empty skeleton with progress for the current level */ function addLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) { @@ -54,7 +55,7 @@ export const progressSlice = createSlice({ state.games[action.payload.game][action.payload.world][action.payload.level].code = action.payload.code state.games[action.payload.game][action.payload.world][action.payload.level].completed = false }, - /** TODO: ? */ + /** TODO: docstring */ changedSelection(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, selections: Selection[]}>) { addLevelProgress(state, action) state.games[action.payload.game][action.payload.world][action.payload.level].selections = action.payload.selections @@ -64,6 +65,10 @@ export const progressSlice = createSlice({ addLevelProgress(state, action) state.games[action.payload.game][action.payload.world][action.payload.level].completed = true }, + /** Set the list of rows where help is displayed */ + helpEdited(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, help: number[]}>) { + state.games[action.payload.game][action.payload.world][action.payload.level].help = action.payload.help + }, /** delete all progress for this game */ deleteProgress(state: ProgressState, action: PayloadAction<{game: string}>) { state.games[action.payload.game] = {}