Merge branch 'main' of github.com:leanprover-community/lean4game

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) {

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({

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,

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)
   ]
 }