diff --git a/server/GameServer/EnvExtensions.lean b/server/GameServer/EnvExtensions.lean index c4174cc..6e54609 100644 --- a/server/GameServer/EnvExtensions.lean +++ b/server/GameServer/EnvExtensions.lean @@ -65,6 +65,13 @@ structure InventoryDocEntry where content : String deriving ToJson, Repr, Inhabited +/-- The reduced version of `InventoryDocEntry` which is sent to the client -/ +structure Doc where + name: String + displayName: String + text: String -- TODO: rename to `content` +deriving ToJson + /-- Another reduced version of `InventoryDocEntry` which is used for the tiles in the doc -/ structure ComputedInventoryItem where /-- diff --git a/server/GameServer/Game.lean b/server/GameServer/Game.lean index 230f818..f418d22 100644 --- a/server/GameServer/Game.lean +++ b/server/GameServer/Game.lean @@ -65,12 +65,6 @@ structure DidOpenLevelParams where definitions : Array ComputedInventoryItem deriving ToJson, FromJson -structure Doc where - name: String - displayName: String - text: String -deriving ToJson - structure LoadDocParams where name : Name type : InventoryType