From 719b8d29645e61371608dd0439a04f3e3d981702 Mon Sep 17 00:00:00 2001
From: Alexander Bentkamp <bentkamp@gmail.com>
Date: Fri, 20 Jan 2023 11:36:44 +0100
Subject: [PATCH] World names

Closes #7
---
 client/src/components/Level.tsx                 |  4 ++--
 client/src/components/Welcome.tsx               | 12 +++++++++---
 client/src/state/api.ts                         |  2 +-
 server/leanserver/GameServer/EnvExtensions.lean |  4 ++--
 4 files changed, 14 insertions(+), 8 deletions(-)

diff --git a/client/src/components/Level.tsx b/client/src/components/Level.tsx
index 9876e42..d66b1ed 100644
--- a/client/src/components/Level.tsx
+++ b/client/src/components/Level.tsx
@@ -136,8 +136,8 @@ function Level() {
   const {setTitle, setSubtitle} = React.useContext(SetTitleContext);
 
   useEffect(() => {
-    setTitle(`World: ${worldId}`)
-  }, [worldId])
+    setTitle(`World: ${gameInfo.data?.worlds.nodes[worldId].title}`)
+  }, [gameInfo.data?.worlds.nodes[worldId].title])
 
   useEffect(() => {
     if (level?.data?.title) {
diff --git a/client/src/components/Welcome.tsx b/client/src/components/Welcome.tsx
index 6b64871..3406d95 100644
--- a/client/src/components/Welcome.tsx
+++ b/client/src/components/Welcome.tsx
@@ -17,6 +17,7 @@ import { useGetGameInfoQuery } from '../state/api';
 import { Link } from 'react-router-dom';
 import Markdown from './Markdown';
 import { selectCompleted } from '../state/progress';
+import { SetTitleContext } from '../App';
 
 
 function LevelIcon({ worldId, levelId, position }) {
@@ -36,8 +37,13 @@ function Welcome() {
 
   const { nodes, bounds }: any = gameInfo.data ? computeWorldLayout(gameInfo.data?.worlds) : {nodes: []}
 
+  const {setTitle, setSubtitle} = React.useContext(SetTitleContext);
+
   useEffect(() => {
-    if (gameInfo.data?.title) window.document.title = gameInfo.data.title
+    if (gameInfo.data?.title) {
+      window.document.title = gameInfo.data.title
+      setTitle(gameInfo.data.title)
+    }
   }, [gameInfo.data?.title])
 
   const padding = 20
@@ -98,8 +104,8 @@ export default Welcome
 function computeWorldLayout(worlds) {
 
   let elements = []
-  for (let node of worlds.nodes) {
-    elements.push({ data: { id: node.name, title: node.title } })
+  for (let id in worlds.nodes) {
+    elements.push({ data: { id: id, title: worlds.nodes[id].title } })
   }
   for (let edge of worlds.edges) {
     elements.push({
diff --git a/client/src/state/api.ts b/client/src/state/api.ts
index e66921b..082fe53 100644
--- a/client/src/state/api.ts
+++ b/client/src/state/api.ts
@@ -4,7 +4,7 @@ import { Connection } from '../connection'
 interface GameInfo {
   title: null|string,
   introduction: null|string,
-  worlds: null|{nodes: string[], edges: string[][]},
+  worlds: null|{nodes: {[id:string]: {id: string, title: string}}, edges: string[][]},
   worldSize: null|{[key: string]: number},
   authors: null|string[],
   conclusion: null|string,
diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean
index 83ca77a..1f755a0 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 β] : ToJson (Graph α β) := {
+instance [ToJson β] : ToJson (Graph Name β) := {
   toJson := fun graph => Json.mkObj [
-    ("nodes", toJson (graph.nodes.toArray.map Prod.snd)),
+    ("nodes", Json.mkObj (graph.nodes.toList.map fun (a,b) => (a.toString, toJson b))),
     ("edges", toJson graph.edges)
   ]
 }