add unlocked inventory items to local storage

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,6 +33,7 @@ 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.
@@ -42,7 +43,7 @@ export function DualEditor({level, codeviewRef, levelId, worldId}) {
   const { commandLineMode } = React.useContext(InputModeContext)
   return <>
     <div className={commandLineMode ? 'hidden' : ''}>
-      <ExerciseStatement data={level?.data} />
+      <ExerciseStatement data={level} />
       <div ref={codeviewRef} className={'codeview'}></div>
     </div>
     {ec ?
@@ -57,11 +58,37 @@ 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)
 
+  // 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;
 
@@ -81,7 +108,7 @@ function DualEditorMain({worldId, levelId, level}) {
           <WithLspDiagnosticsContext>
             <ProgressContext.Provider value={allProgress}>
               {commandLineMode ?
-              <CommandLineInterface world={worldId} level={levelId} data={level?.data}/>
+                <CommandLineInterface world={worldId} level={levelId} data={level} />
                 :
                 <Main key={`${worldId}/${levelId}`} world={worldId} level={levelId} />
               }
@@ -112,21 +139,6 @@ 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. */
@@ -280,20 +292,6 @@ export function CommandLineInterface(props: {world: string, level: number, data:
 
   const proofPanelRef = React.useRef<HTMLDivElement>(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)
@@ -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<DocumentUri, LeanFileProgressProcessingInfo[]>(),
-    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(
@@ -378,10 +367,12 @@ export function CommandLineInterface(props: {world: string, level: number, data:
   // that we want to persist.
 
   if (!serverVersion) { return <p>Waiting for Lean server to start...</p> }
-  if (serverStoppedResult) {return <div>
+  if (serverStoppedResult) {
+    return <div>
       <p>{serverStoppedResult.message}</p>
       <p className="error">{serverStoppedResult.reason}</p>
-  </div>}
+    </div>
+  }
 
   return <div className="commandline-interface">
     <div className="content" ref={proofPanelRef}>

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<string>()
   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}</div>)}
       </div>}
     <div className="inventory-list">
-      {[...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)

client/src/components/level.tsx

@@ -324,7 +324,7 @@ function PlayableLevel({worldId, levelId}) {
           <EditorContext.Provider value={editorConnection}>
             <MonacoEditorContext.Provider value={editor}>
               <div className="exercise">
-                <DualEditor level={level} codeviewRef={codeviewRef} levelId={levelId} worldId={worldId} />
+                <DualEditor level={level?.data} codeviewRef={codeviewRef} levelId={levelId} worldId={worldId} />
               </div>
             </MonacoEditorContext.Provider>
           </EditorContext.Provider>

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 */
+/** Add an empty skeleton with progress for the current game */
-function addLevelProgress(state: ProgressState, action: PayloadAction<{game: string, world: string, level: number}>) {
+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] = {}
 }
-  if (!state.games[action.payload.game][action.payload.world][action.payload.level]) {
+
-    state.games[action.payload.game][action.payload.world][action.payload.level] = {...initalLevelProgressState}
+/** 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].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].data[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].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].data[world]) { return initalLevelProgressState }
-    if (!state.progress.games[game][world][level]) { return initalLevelProgressState }
+    if (!state.progress.games[game].data[world][level]) { return initalLevelProgressState }
-    return state.progress.games[game][world][level]
+    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