From 6e0469d3bf8a60a6fc29c55b5777163414233200 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Thu, 19 Jan 2023 17:43:36 +0100
Subject: [PATCH] world titles

---
 client/src/components/Welcome.tsx               | 17 +++++++++++------
 server/leanserver/GameServer/EnvExtensions.lean |  8 ++++++--
 .../testgame/TestGame/Levels/Implication.lean   |  4 ++++
 server/testgame/TestGame/Levels/Predicate.lean  |  4 ++++
 .../testgame/TestGame/Levels/Proposition.lean   |  4 ++++
 5 files changed, 29 insertions(+), 8 deletions(-)

diff --git a/client/src/components/Welcome.tsx b/client/src/components/Welcome.tsx
index 2caafd5..6b64871 100644
--- a/client/src/components/Welcome.tsx
+++ b/client/src/components/Welcome.tsx
@@ -40,7 +40,7 @@ function Welcome() {
     if (gameInfo.data?.title) window.document.title = gameInfo.data.title
   }, [gameInfo.data?.title])
 
-  const padding = 10
+  const padding = 20
 
   const svgElements = []
 
@@ -48,16 +48,18 @@ function Welcome() {
     for (let i in gameInfo.data.worlds.edges) {
       const edge = gameInfo.data.worlds.edges[i]
       svgElements.push(
-        <line key={`pathway${i}`} x1={nodes[edge[0]].x} y1={nodes[edge[0]].y} x2={nodes[edge[1]].x} y2={nodes[edge[1]].y} stroke="#1976d2" strokeWidth="1"/>
+        <line key={`pathway${i}`} x1={nodes[edge[0]].position.x} y1={nodes[edge[0]].position.y}
+          x2={nodes[edge[1]].position.x} y2={nodes[edge[1]].position.y} stroke="#1976d2" strokeWidth="1"/>
       )
     }
     for (let id in nodes) {
-      let position: cytoscape.Position = nodes[id]
+      let position: cytoscape.Position = nodes[id].position
 
       svgElements.push(
         <Link key={`world${id}`} to={`/world/${id}/level/1`}>
           <circle fill="#61DAFB" cx={position.x} cy={position.y} r="8" />
-          <text style={{font: "italic 2px sans-serif",  textAnchor: "middle", dominantBaseline: "middle"} as any} x={position.x} y={position.y}>{id}</text>
+          <text style={{font: "italic 2px sans-serif",  textAnchor: "middle", dominantBaseline: "middle"} as any}
+            x={position.x} y={position.y}>{nodes[id].data.title ? nodes[id].data.title : id}</text>
         </Link>
       )
 
@@ -97,7 +99,7 @@ function computeWorldLayout(worlds) {
 
   let elements = []
   for (let node of worlds.nodes) {
-    elements.push({ data: { id: node } })
+    elements.push({ data: { id: node.name, title: node.title } })
   }
   for (let edge of worlds.edges) {
     elements.push({
@@ -119,7 +121,10 @@ function computeWorldLayout(worlds) {
   const layout = cy.layout({name: "klay", klay: {direction: "DOWN"}} as LayoutOptions).run()
   let nodes = {}
   cy.nodes().forEach((node, id) => {
-    nodes[node.id()] = node.position()
+    nodes[node.id()] = {
+      position: node.position(),
+      data: node.data()
+    }
   })
   const bounds = cy.nodes().boundingBox()
   return { nodes, bounds }
diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean
index 295ce60..83ca77a 100644
--- a/server/leanserver/GameServer/EnvExtensions.lean
+++ b/server/leanserver/GameServer/EnvExtensions.lean
@@ -114,9 +114,9 @@ structure Graph (α β : Type) [inst : BEq α] [inst : Hashable α] where
   edges: Array (α × α) := {}
 deriving Inhabited
 
-instance [inst : BEq α] [inst : Hashable α] [ToJson α] : ToJson (Graph α β) := {
+instance [inst : BEq α] [inst : Hashable α] [ToJson α] [ToJson β] : ToJson (Graph α β) := {
   toJson := fun graph => Json.mkObj [
-    ("nodes", toJson (graph.nodes.toArray.map Prod.fst)),
+    ("nodes", toJson (graph.nodes.toArray.map Prod.snd)),
     ("edges", toJson graph.edges)
   ]
 }
@@ -216,6 +216,10 @@ structure World where
   levels: HashMap Nat GameLevel := {}
 deriving Inhabited
 
+instance : ToJson World := ⟨
+  fun world => Json.mkObj [("name", toJson world.name), ("title", world.title)]
+⟩
+
 /-! ## Game -/
 
 structure Game where
diff --git a/server/testgame/TestGame/Levels/Implication.lean b/server/testgame/TestGame/Levels/Implication.lean
index bb0f73c..d88d75a 100644
--- a/server/testgame/TestGame/Levels/Implication.lean
+++ b/server/testgame/TestGame/Levels/Implication.lean
@@ -10,3 +10,7 @@ import TestGame.Levels.Implication.L09_Iff
 import TestGame.Levels.Implication.L10_Apply
 import TestGame.Levels.Implication.L11_Rw
 import TestGame.Levels.Implication.L12_Summary
+
+Game "TestGame"
+World "Implication"
+Title "Meer der Implikationen"
diff --git a/server/testgame/TestGame/Levels/Predicate.lean b/server/testgame/TestGame/Levels/Predicate.lean
index 85d84b1..43bcc35 100644
--- a/server/testgame/TestGame/Levels/Predicate.lean
+++ b/server/testgame/TestGame/Levels/Predicate.lean
@@ -7,3 +7,7 @@ import TestGame.Levels.Predicate.L06_Exists
 import TestGame.Levels.Predicate.L07_Forall
 import TestGame.Levels.Predicate.L08_PushNeg
 import TestGame.Levels.Predicate.L09_Summary
+
+Game "TestGame"
+World "Predicate"
+Title "Reich der Prädikate"
diff --git a/server/testgame/TestGame/Levels/Proposition.lean b/server/testgame/TestGame/Levels/Proposition.lean
index 5c39d04..b458a31 100644
--- a/server/testgame/TestGame/Levels/Proposition.lean
+++ b/server/testgame/TestGame/Levels/Proposition.lean
@@ -11,3 +11,7 @@ import TestGame.Levels.Proposition.L10_And
 import TestGame.Levels.Proposition.L11_Or
 import TestGame.Levels.Proposition.L12_Or
 import TestGame.Levels.Proposition.L13_Summary
+
+Game "TestGame"
+World "Proposition"
+Title "Land der Proposititionen"