define paths

server/leanserver/GameServer/Commands.lean

@@ -70,10 +70,25 @@ elab "Conclusion" t:str : command => do
 elab "PrintCurLevel" : command => do
   logInfo (repr (← getCurLevel))
 
+#check Syntax.SepArray
+
 -- /-- Print levels for debugging purposes. -/
 elab "PrintLevels" : command => do
   logInfo $ repr $ (← getCurWorld).levels.toArray
 
+def Parser.path := Parser.sepBy1Indent Parser.ident "→"
+
+elab "Path" s:Parser.path : command => do
+  let mut last : Option Name := none
+  for stx in s.raw.getArgs.getEvenElems do
+    let some l := last
+      | do
+          last := some stx.getId
+          continue
+    modifyCurGame fun game =>
+      pure {game with worlds := {game.worlds with edges := game.worlds.edges.push (l, stx.getId)}}
+    last := some stx.getId
+
 end metadata
 
 /-! ## Messages -/

server/leanserver/GameServer/EnvExtensions.lean

@@ -217,7 +217,7 @@ new.fold (fun acc a b =>
   else acc.insert a b) old
 
 def GameLevel.merge (old : GameLevel) (new : GameLevel) : GameLevel :=
-  new
+  new -- simply override old level
 
 def World.merge (old : World) (new : World) : World :=
 { new with
@@ -227,7 +227,12 @@ def Game.merge (old : Game) (new : Game) : Game :=
 { new with
   worlds := {
     nodes := HashMap.merge old.worlds.nodes new.worlds.nodes World.merge
-    edges := old.worlds.edges ++ new.worlds.edges
+    edges := Id.run do
+      let mut res := old.worlds.edges
+      for e in new.worlds.edges do
+        if ¬ res.contains e then
+          res := res.push e
+      return res
   } }
 
 initialize gameExt : PersistentEnvExtension (Name × Game) (Name × Game) (HashMap Name Game) ←