From 60876b4a7764b79c0f8b2ebef30df1f3ef538ece Mon Sep 17 00:00:00 2001
From: Jon Eugster <eugster.jon@gmail.com>
Date: Fri, 19 May 2023 13:03:23 +0200
Subject: [PATCH] move Doc class

---
 server/GameServer/EnvExtensions.lean | 7 +++++++
 server/GameServer/Game.lean          | 6 ------
 2 files changed, 7 insertions(+), 6 deletions(-)

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