$/game/setInventory no longer needed
This commit is contained in:
@@ -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
|
||||
|
||||
@@ -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
|
||||
|
||||
Reference in New Issue
Block a user