diff --git a/client/src/components/level.tsx b/client/src/components/level.tsx index 7541752..4b5a53d 100644 --- a/client/src/components/level.tsx +++ b/client/src/components/level.tsx @@ -219,10 +219,8 @@ function PlayableLevel({impressum, setImpressum}) { const dispatch = useAppDispatch() - const difficulty = useSelector(selectDifficulty(gameId)) const initialCode = useAppSelector(selectCode(gameId, worldId, levelId)) const initialSelections = useAppSelector(selectSelections(gameId, worldId, levelId)) - const inventory: Array = useSelector(selectInventory(gameId)) const typewriterMode = useSelector(selectTypewriterMode(gameId)) const setTypewriterMode = (newTypewriterMode: boolean) => dispatch(changeTypewriterMode({game: gameId, typewriterMode: newTypewriterMode})) @@ -301,12 +299,6 @@ function PlayableLevel({impressum, setImpressum}) { // a hint at the beginning of the proof... const [selectedStep, setSelectedStep] = useState() - // TODO: if the user inventory changes, notify the server - // useEffect(() => { - // let leanClient = connection.getLeanClient(gameId) - // leanClient.sendNotification('$/game/setInventory', {inventory: inventory, difficulty: difficulty}) - // }, [inventory]) - useEffect (() => { // Lock editor mode if (level?.data?.template) { diff --git a/server/GameServer/FileWorker.lean b/server/GameServer/FileWorker.lean index d66c2a2..30829d8 100644 --- a/server/GameServer/FileWorker.lean +++ b/server/GameServer/FileWorker.lean @@ -562,13 +562,6 @@ section MainLoop | Message.request id "shutdown" none => ctx.hOut.writeLspResponse ⟨id, Json.null⟩ mainLoop - | Message.notification "$/game/setInventory" params => - let p := (← parseParams Game.SetInventoryParams (toJson params)) - let s ← get - set {s with - inventory := p.inventory, - difficulty := p.difficulty} - mainLoop | Message.notification method (some params) => handleNotification method (toJson params) mainLoop diff --git a/server/GameServer/Game.lean b/server/GameServer/Game.lean index ae20e01..c64d424 100644 --- a/server/GameServer/Game.lean +++ b/server/GameServer/Game.lean @@ -77,9 +77,4 @@ def InitializeParams.toLeanInternal (p : InitializeParams) : Lean.Lsp.Initialize workspaceFolders? := p.workspaceFolders? } -structure SetInventoryParams where - inventory : Array String - difficulty : Nat -deriving ToJson, FromJson - end Game