diff --git a/client/src/components/infoview/main.tsx b/client/src/components/infoview/main.tsx index 433b7ed..2fd15ca 100644 --- a/client/src/components/infoview/main.tsx +++ b/client/src/components/infoview/main.tsx @@ -21,7 +21,7 @@ import * as monaco from 'monaco-editor/esm/vs/editor/editor.api.js' import { GameIdContext } from '../../app'; import { useAppDispatch, useAppSelector } from '../../hooks'; import { LevelInfo } from '../../state/api'; -import { levelCompleted, selectCompleted } from '../../state/progress'; +import { changedInventory, levelCompleted, selectCompleted, selectInventory } from '../../state/progress'; import Markdown from '../markdown'; import { Infos } from './infos'; @@ -33,16 +33,17 @@ import { InteractiveDiagnostic } from '@leanprover/infoview/*'; import { Button } from '../button'; import { CircularProgress } from '@mui/material'; import { GameHint } from './rpc_api'; +import { store } from '../../state/store'; /** Wrapper for the two editors. It is important that the `div` with `codeViewRef` is * always present, or the monaco editor cannot start. */ -export function DualEditor({level, codeviewRef, levelId, worldId}) { +export function DualEditor({ level, codeviewRef, levelId, worldId }) { const ec = React.useContext(EditorContext) - const {commandLineMode} = React.useContext(InputModeContext) + const { commandLineMode } = React.useContext(InputModeContext) return <>
- +
{ec ? @@ -57,10 +58,36 @@ export function DualEditor({level, codeviewRef, levelId, worldId}) { } /** The part of the two editors that needs the editor connection first */ -function DualEditorMain({worldId, levelId, level}) { +function DualEditorMain({ worldId, levelId, level }: { worldId: string, levelId: number, level: LevelInfo }) { const ec = React.useContext(EditorContext) const gameId = React.useContext(GameIdContext) - const {commandLineMode} = React.useContext(InputModeContext) + const { commandLineMode } = React.useContext(InputModeContext) + + // Mark level as completed when server gives notification + const dispatch = useAppDispatch() + useServerNotificationEffect( + '$/game/completed', + (params: any) => { + if (ec.events.changedCursorLocation.current && + ec.events.changedCursorLocation.current.uri === params.uri) { + dispatch(levelCompleted({ game: gameId, world: worldId, level: levelId })) + + // On completion, add the names of all new items to the local storage + let newTiles = [ + ...level?.tactics, + ...level?.lemmas, + ...level?.definitions + ].filter((tile) => tile.new).map((tile) => tile.name) + + let inv: string[] = selectInventory(gameId)(store.getState()) + + // add new items and remove duplicates + let newInv = [...inv, ...newTiles].filter((item, i, array) => array.indexOf(item) == i) + + dispatch(changedInventory({ game: gameId, inventory: newInv })) + } + }, [level] + ) /* Set up updates to the global infoview state on editor events. */ const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig; @@ -75,22 +102,22 @@ function DualEditorMain({worldId, levelId, level}) { const serverVersion = useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? '')) return <> - - - - - - {commandLineMode ? - - : -
- } - - - - - - + + + + + + {commandLineMode ? + + : +
+ } + + + + + + } /** The mathematical formulation of the statement, supporting e.g. Latex @@ -99,81 +126,66 @@ function DualEditorMain({worldId, levelId, level}) { * - Theorem xyz * - Exercises: description */ -function ExerciseStatement({data}) { +function ExerciseStatement({ data }) { if (!data?.descrText) { return <> } return
- {(data?.statementName ? `**Theorem** \`${data?.statementName}\`: ` : data?.descrText && "**Exercise**: ") + `${data?.descrText}` } + {(data?.statementName ? `**Theorem** \`${data?.statementName}\`: ` : data?.descrText && "**Exercise**: ") + `${data?.descrText}`}
} // TODO: This is only used in `EditorInterface` // while `CommandLineInterface` has this copy-pasted in. -export function Main(props: {world: string, level: number}) { - const ec = React.useContext(EditorContext); - const gameId = React.useContext(GameIdContext) - - const dispatch = useAppDispatch() - - // Mark level as completed when server gives notification - useServerNotificationEffect( - '$/game/completed', - (params: any) => { - - if (ec.events.changedCursorLocation.current && - ec.events.changedCursorLocation.current.uri === params.uri) { - dispatch(levelCompleted({game: gameId, world: props.world, level: props.level})) - } - }, - [] - ); - - const completed = useAppSelector(selectCompleted(gameId, props.world, props.level)) - - /* Set up updates to the global infoview state on editor events. */ - const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig; - - const [allProgress, _1] = useServerNotificationState( - '$/lean/fileProgress', - new Map(), - async (params: LeanFileProgressParams) => (allProgress) => { - const newProgress = new Map(allProgress); - return newProgress.set(params.textDocument.uri, params.processing); - }, - [] - ); - - const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri); - - useClientNotificationEffect( - 'textDocument/didClose', - (params: DidCloseTextDocumentParams) => { - if (ec.events.changedCursorLocation.current && - ec.events.changedCursorLocation.current.uri === params.textDocument.uri) { - ec.events.changedCursorLocation.fire(undefined) - } - }, - [] - ); - - const serverVersion = - useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? '')) - const serverStoppedResult = useEventResult(ec.events.serverStopped); - // NB: the cursor may temporarily become `undefined` when a file is closed. In this case - // it's important not to reconstruct the `WithBlah` wrappers below since they contain state - // that we want to persist. - let ret - if (!serverVersion) { - ret =

Waiting for Lean server to start...

- } else if (serverStoppedResult){ - ret =

{serverStoppedResult.message}

{serverStoppedResult.reason}

- } else { - ret =
- {completed &&
Level completed! 🎉
} - -
- } +export function Main(props: { world: string, level: number }) { + const ec = React.useContext(EditorContext); + const gameId = React.useContext(GameIdContext) + + const completed = useAppSelector(selectCompleted(gameId, props.world, props.level)) + + /* Set up updates to the global infoview state on editor events. */ + const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig; + + const [allProgress, _1] = useServerNotificationState( + '$/lean/fileProgress', + new Map(), + async (params: LeanFileProgressParams) => (allProgress) => { + const newProgress = new Map(allProgress); + return newProgress.set(params.textDocument.uri, params.processing); + }, + [] + ); + + const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri); + + useClientNotificationEffect( + 'textDocument/didClose', + (params: DidCloseTextDocumentParams) => { + if (ec.events.changedCursorLocation.current && + ec.events.changedCursorLocation.current.uri === params.textDocument.uri) { + ec.events.changedCursorLocation.fire(undefined) + } + }, + [] + ); + + const serverVersion = + useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? '')) + const serverStoppedResult = useEventResult(ec.events.serverStopped); + // NB: the cursor may temporarily become `undefined` when a file is closed. In this case + // it's important not to reconstruct the `WithBlah` wrappers below since they contain state + // that we want to persist. + let ret + if (!serverVersion) { + ret =

Waiting for Lean server to start...

+ } else if (serverStoppedResult) { + ret =

{serverStoppedResult.message}

{serverStoppedResult.reason}

+ } else { + ret =
+ {completed &&
Level completed! 🎉
} + +
+ } - return ret + return ret } const goalFilter = { @@ -185,9 +197,9 @@ const goalFilter = { } /** The display of a single entered lean command */ -function Command({command, deleteProof} : {command: string, deleteProof: any}) { +function Command({ command, deleteProof }: { command: string, deleteProof: any }) { // The first step will always have an empty command - if (!command) {return <>} + if (!command) { return <> } return
{command}
@@ -248,17 +260,17 @@ function Command({command, deleteProof} : {command: string, deleteProof: any}) { // }, fastIsEqual) /** The tabs of goals that lean ahs after the command of this step has been processed */ -function GoalsTab({proofStep} : {proofStep: ProofStep}) { +function GoalsTab({ proofStep }: { proofStep: ProofStep }) { const [selectedGoal, setSelectedGoal] = React.useState(0) - if (!proofStep.goals.length) {return <>} + if (!proofStep.goals.length) { return <> } return
{proofStep.goals.map((goal, i) => ( // TODO: Should not use index as key. -
{ setSelectedGoal(i); ev.stopPropagation() }}> - {i ? `Goal ${i+1}` : "Active Goal"} +
{ setSelectedGoal(i); ev.stopPropagation() }}> + {i ? `Goal ${i + 1}` : "Active Goal"}
))}
@@ -269,31 +281,17 @@ function GoalsTab({proofStep} : {proofStep: ProofStep}) { } /** The interface in command line mode */ -export function CommandLineInterface(props: {world: string, level: number, data: LevelInfo}) { +export function CommandLineInterface(props: { world: string, level: number, data: LevelInfo }) { const ec = React.useContext(EditorContext) const editor = React.useContext(MonacoEditorContext) const gameId = React.useContext(GameIdContext) - const {proof} = React.useContext(ProofContext) - const {selectedStep, setSelectedStep} = React.useContext(SelectionContext) - const {setDeletedChat, showHelp} = React.useContext(DeletedChatContext) + const { proof } = React.useContext(ProofContext) + const { selectedStep, setSelectedStep } = React.useContext(SelectionContext) + const { setDeletedChat, showHelp } = React.useContext(DeletedChatContext) const proofPanelRef = React.useRef(null) - const dispatch = useAppDispatch() - - // Mark level as completed when server gives notification - useServerNotificationEffect( - '$/game/completed', - (params: any) => { - - if (ec.events.changedCursorLocation.current && - ec.events.changedCursorLocation.current.uri === params.uri) { - dispatch(levelCompleted({game: gameId, world: props.world, level: props.level})) - } - }, [] - ) - // React.useEffect(() => { // console.debug('updated proof') // // proofPanelRef.current?.lastElementChild?.scrollIntoView() //scrollTo(0,0) @@ -307,13 +305,13 @@ export function CommandLineInterface(props: {world: string, level: number, data: let deletedChat: Array = [] 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)))] + deletedChat = [...deletedChat, ...step.hints.filter(hint => (!hint.hidden || showHelp.has(line + i)))] }) setDeletedChat(deletedChat) editor.executeEdits("command-line", [{ range: monaco.Selection.fromPositions( - {lineNumber: line, column: 1}, + { lineNumber: line, column: 1 }, editor.getModel().getFullModelRange().getEndPosition() ), text: '', @@ -340,7 +338,7 @@ export function CommandLineInterface(props: {world: string, level: number, data: React.useEffect(() => { if (typeof selectedStep !== 'undefined') { Array.from(proofPanelRef.current?.getElementsByClassName(`step-${selectedStep}`)).map((elem) => { - elem.scrollIntoView({block: "center"}) + elem.scrollIntoView({ block: "center" }) }) } }, [selectedStep]) @@ -349,15 +347,6 @@ export function CommandLineInterface(props: {world: string, level: number, data: const config = useEventResult(ec.events.changedInfoviewConfig) ?? defaultInfoviewConfig; - const [allProgress, _1] = useServerNotificationState( - '$/lean/fileProgress', - new Map(), - async (params: LeanFileProgressParams) => (allProgress) => { - const newProgress = new Map(allProgress); - return newProgress.set(params.textDocument.uri, params.processing); - }, [] - ) - const curUri = useEventResult(ec.events.changedCursorLocation, loc => loc?.uri); useClientNotificationEffect( @@ -371,17 +360,19 @@ export function CommandLineInterface(props: {world: string, level: number, data: ) const serverVersion = - useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? '')) + useEventResult(ec.events.serverRestarted, result => new ServerVersion(result.serverInfo?.version ?? '')) const serverStoppedResult = useEventResult(ec.events.serverStopped); // NB: the cursor may temporarily become `undefined` when a file is closed. In this case // it's important not to reconstruct the `WithBlah` wrappers below since they contain state // that we want to persist. - if (!serverVersion) {return

Waiting for Lean server to start...

} - if (serverStoppedResult) {return
-

{serverStoppedResult.message}

-

{serverStoppedResult.reason}

-
} + if (!serverVersion) { return

Waiting for Lean server to start...

} + if (serverStoppedResult) { + return
+

{serverStoppedResult.message}

+

{serverStoppedResult.reason}

+
+ } return
@@ -393,13 +384,13 @@ export function CommandLineInterface(props: {world: string, level: number, data: // entered command as it is still present in the command line. // TODO: Should not use index as key. return
- +
} else { return
- - - + + + {/* Show a message that there are no goals left */} {!step.goals.length && (
@@ -416,6 +407,6 @@ export function CommandLineInterface(props: {world: string, level: number, data: } }) : }
- +
} diff --git a/client/src/components/inventory.tsx b/client/src/components/inventory.tsx index 3d085dd..cff2c1b 100644 --- a/client/src/components/inventory.tsx +++ b/client/src/components/inventory.tsx @@ -6,6 +6,8 @@ import { faLock, faLockOpen, faBook, faHammer, faBan } from '@fortawesome/free-s import { GameIdContext } from '../app'; import Markdown from './markdown'; import { useLoadDocQuery, InventoryTile, LevelInfo, InventoryOverview } from '../state/api'; +import { selectInventory } from '../state/progress'; +import { store } from '../state/store'; export function Inventory({levelInfo, openDoc, enableAll=false} : { @@ -46,13 +48,22 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine // TODO: `level` is only used in the `useEffect` below to check if a new level has // been loaded. Is there a better way to observe this? + const gameId = React.useContext(GameIdContext) + const categorySet = new Set() for (let item of items) { categorySet.add(item.category) } const categories = Array.from(categorySet).sort() - const [tab, setTab] = useState(defaultTab); + const [tab, setTab] = useState(defaultTab) + + // Add inventory items from local store as unlocked. + // Items are unlocked if they are in the local store, or if the server says they should be + // given the dependency graph. (OR-connection) (TODO: maybe add different logic for different + // modi) + let inv: string[] = selectInventory(gameId)(store.getState()) + let modifiedItems : InventoryTile[] = items.map(tile => inv.includes(tile.name) ? {...tile, locked: false} : tile) useEffect(() => { // If the level specifies `LemmaTab "Nat"`, we switch to this tab on loading. @@ -69,7 +80,7 @@ function InventoryList({items, docType, openDoc, defaultTab=null, level=undefine onClick={() => { setTab(cat) }}>{cat}
)}
}
- {[...items].sort( + {[...modifiedItems].sort( // For lemas, sort entries `available > disabled > locked` // otherwise alphabetically (x, y) => +(docType == "Lemma") * (+x.locked - +y.locked || +x.disabled - +y.disabled) diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 7314a51..117b0ab 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -324,7 +324,7 @@ function PlayableLevel({worldId, levelId}) {
- +
diff --git a/client/src/state/progress.ts b/client/src/state/progress.ts index d87b098..396fc69 100644 --- a/client/src/state/progress.ts +++ b/client/src/state/progress.ts @@ -4,6 +4,7 @@ import { createSlice } from '@reduxjs/toolkit' import type { PayloadAction } from '@reduxjs/toolkit' import { loadState } from "./local_storage"; +import { WorkDoneProgressBegin } from 'vscode-languageserver-protocol'; interface Selection { selectionStartLineNumber: number, @@ -17,9 +18,13 @@ interface LevelProgressState { completed: boolean, help: number[], // A set of rows where hidden hints have been displayed } +interface WorldProgressState { + [world: string] : {[level: number]: LevelProgressState}, +} export interface GameProgressState { - [world: string] : {[level: number]: LevelProgressState} + inventory: string[], + data: WorldProgressState } /** The progress made on all lean4-games */ @@ -32,16 +37,21 @@ const initialProgressState: ProgressState = loadState() ?? { games: {} } // TODO: There was some weird unreproducible bug with removing `as LevelProgressState` here... 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}>) { +/** Add an empty skeleton with progress for the current game */ +function addGameProgress (state: ProgressState, action: PayloadAction<{game: string}>) { if (!state.games[action.payload.game]) { - state.games[action.payload.game] = {} + state.games[action.payload.game] = {inventory: [], data: {}} } - if (!state.games[action.payload.game][action.payload.world]) { - state.games[action.payload.game][action.payload.world] = {} +} + +/** Add an empty skeleton with progress for the current level */ +function addLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) { + addGameProgress(state, action) + if (!state.games[action.payload.game].data[action.payload.world]) { + state.games[action.payload.game].data[action.payload.world] = {} } - if (!state.games[action.payload.game][action.payload.world][action.payload.level]) { - state.games[action.payload.game][action.payload.world][action.payload.level] = {...initalLevelProgressState} + if (!state.games[action.payload.game].data[action.payload.world][action.payload.level]) { + state.games[action.payload.game].data[action.payload.world][action.payload.level] = {...initalLevelProgressState} } } @@ -52,39 +62,44 @@ export const progressSlice = createSlice({ /** put edited code in the state and set completed to false */ codeEdited(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number, code: string}>) { addLevelProgress(state, action) - 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 + state.games[action.payload.game].data[action.payload.world][action.payload.level].code = action.payload.code + state.games[action.payload.game].data[action.payload.world][action.payload.level].completed = false }, /** 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 + state.games[action.payload.game].data[action.payload.world][action.payload.level].selections = action.payload.selections }, /** mark level as completed */ levelCompleted(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) { addLevelProgress(state, action) - state.games[action.payload.game][action.payload.world][action.payload.level].completed = true + state.games[action.payload.game].data[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[]}>) { addLevelProgress(state, action) console.debug(`!setting help to: ${action.payload.help}`) - state.games[action.payload.game][action.payload.world][action.payload.level].help = action.payload.help + state.games[action.payload.game].data[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] = {} + state.games[action.payload.game] = {inventory: [], data: {}} }, /** delete progress for this level */ deleteLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) { addLevelProgress(state, action) - state.games[action.payload.game][action.payload.world][action.payload.level] = initalLevelProgressState + state.games[action.payload.game].data[action.payload.world][action.payload.level] = initalLevelProgressState }, /** load progress, e.g. from external import */ loadProgress(state: ProgressState, action: PayloadAction<{game: string, data:GameProgressState}>) { console.debug(`setting data to:\n ${action.payload.data}`) state.games[action.payload.game] = action.payload.data }, + /** set the current inventory */ + changedInventory(state: ProgressState, action: PayloadAction<{game: string, inventory: string[]}>) { + addGameProgress(state, action) + state.games[action.payload.game].inventory = action.payload.inventory + }, } }) @@ -92,9 +107,9 @@ export const progressSlice = createSlice({ export function selectLevel(game: string, world: string, level: number) { return (state) =>{ if (!state.progress.games[game]) { return initalLevelProgressState } - if (!state.progress.games[game][world]) { return initalLevelProgressState } - if (!state.progress.games[game][world][level]) { return initalLevelProgressState } - return state.progress.games[game][world][level] + if (!state.progress.games[game].data[world]) { return initalLevelProgressState } + if (!state.progress.games[game].data[world][level]) { return initalLevelProgressState } + return state.progress.games[game].data[world][level] } } @@ -105,6 +120,14 @@ export function selectCode(game: string, world: string, level: number) { } } +/** return the current inventory */ +export function selectInventory(game: string) { + return (state) => { + if (!state.progress.games[game]) { return [] } + return state.progress.games[game].inventory + } +} + /** return the code of the current level */ export function selectHelp(game: string, world: string, level: number) { return (state) => { @@ -135,4 +158,4 @@ export function selectProgress(game: string) { /** Export actions to modify the progress */ export const { changedSelection, codeEdited, levelCompleted, deleteProgress, - deleteLevelProgress, loadProgress, helpEdited } = progressSlice.actions + deleteLevelProgress, loadProgress, helpEdited, changedInventory } = progressSlice.actions