diff --git a/server/leanserver/GameServer/Commands.lean b/server/leanserver/GameServer/Commands.lean
index 3fc828e..5ac3717 100644
--- a/server/leanserver/GameServer/Commands.lean
+++ b/server/leanserver/GameServer/Commands.lean
@@ -1,32 +1,28 @@
 import Lean
-
 import GameServer.EnvExtensions
 
-open Lean Meta
+open Lean Meta Elab Command
 
 set_option autoImplicit false
 
-/-! ## Easy metadata -/
-
-section metadata
-
-open Lean Meta Elab Command Term
+/-! # Game metadata -/
 
-/-- Create a game with the given identifier as name. -/
+/-- Switch to the specified `Game` (and create it if non-existent). Example: `Game "NNG"` -/
 elab "Game" n:str : command => do
   let name := n.getString
   setCurGameId name
   if (← getGame? name).isNone then
     insertGame name {name}
 
-/-- Create a World -/
+/-- Create a new world in the active game. Example: `World "Addition"` -/
 elab "World" n:str : command => do
   let name := n.getString
   setCurWorldId name
   if ¬ (← getCurGame).worlds.nodes.contains name then
     addWorld {name}
 
-/-- Define the current level number. -/
+/-- Define the current level number. Levels inside a world must be
+numbered consecutive starting with `1`. Example: `Level 1` -/
 elab "Level" level:num : command => do
   let level := level.getNat
   setCurLevelIdx level
@@ -46,99 +42,6 @@ elab "Introduction" t:str : command => do
   | .World => modifyCurWorld  fun world => pure {world with introduction := t.getString}
   | .Game => modifyCurGame  fun game => pure {game with introduction := t.getString}
 
--- TODO: Instead of this, it would be nice to have a proper syntax parser that enables
--- us highlighting on the client side.
-partial def reprintCore : Syntax → Option Format
-  | Syntax.missing => none
-  | Syntax.atom _ val => val.trim
-  | Syntax.ident _ rawVal _ _ => rawVal.toString
-  | Syntax.node _ kind args =>
-    match args.toList.filterMap reprintCore with
-    | [] => none
-    | [arg] => arg
-    | args => Format.group <| Format.nest 2 <| Format.joinSep args " "
-
-def reprint (stx : Syntax) : Format :=
-  reprintCore stx |>.getD ""
-
-syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
-
-/-- Remove any spaces at the beginning of a new line -/
-partial def removeIndentation (s : String) : String :=
-  let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
-    let c := s.get i
-    let i := s.next i
-    if s.atEnd i then
-      acc.push c
-    else if removeSpaces && c == ' ' then
-      loop i acc (removeSpaces := true)
-    else if c == '\n' then
-      loop i (acc.push c) (removeSpaces := true)
-    else
-      loop i (acc.push c)
-  loop ⟨0⟩ ""
-
-/-- A tactic that can be used inside `Statement`s to indicate in which proof states players should
-see hints. The tactic does not affect the goal state. -/
-elab "Hint" args:hintArg* msg:interpolatedStr(term) : tactic => do
-  let mut strict := false
-  let mut hidden := false
-
-  -- remove spaces at the beginngng of new lines
-  let msg := TSyntax.mk $ msg.raw.setArgs $ ← msg.raw.getArgs.mapM fun m => do
-    match m with
-    | Syntax.node info k args =>
-      logInfo k
-      if k == interpolatedStrLitKind && args.size == 1 then
-        match args.get! 0 with
-        | (Syntax.atom info' val) =>
-          let val := removeIndentation val
-          return Syntax.node info k #[Syntax.atom info' val]
-        | _ => return m
-      else
-        return m
-    | _ => return m
-
-  for arg in args do
-    match arg with
-    | `(hintArg| (strict := true)) => strict := true
-    | `(hintArg| (strict := false)) => strict := false
-    | `(hintArg| (hidden := true)) => hidden := true
-    | `(hintArg| (hidden := false)) => hidden := false
-    | _ => throwUnsupportedSyntax
-
-  let goal ← Tactic.getMainGoal
-  goal.withContext do
-    -- We construct an expression that can produce the hint text. The difficulty is that we
-    -- want the text to possibly contain quotation of the local variables which might have been
-    -- named differently by the player.
-    let varsName := `vars
-    let text ← withLocalDeclD varsName (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr)) fun vars => do
-      let mut text ← `(m! $msg)
-      let goalDecl ← goal.getDecl
-      let decls := goalDecl.lctx.decls.toArray.filterMap id
-      for i in [:decls.size] do
-        text ← `(let $(mkIdent decls[i]!.userName) := $(mkIdent varsName)[$(quote i)]!; $text)
-      return ← mkLambdaFVars #[vars] $ ← elabTermAndSynthesize text none
-    let textmvar ← mkFreshExprMVar none
-    guard $ ← isDefEq textmvar text -- Store the text in a mvar.
-    -- The information about the hint is logged as a message using `logInfo` to transfer it to the
-    -- `Statement` command defined below:
-    logInfo $
-      .tagged `Hint $
-      .nest (if strict then 1 else 0) $
-      .nest (if hidden then 1 else 0) $
-      .compose (.ofGoal textmvar.mvarId!) (.ofGoal goal)
-
-/-- This tactic allows us to execute an alternative sequence of tactics, but without affecting the
-proof state. We use it to define Hints for alternative proof methods or dead ends. -/
-elab "Branch" t:tacticSeq : tactic => do
-  let b ← saveState
-  Tactic.evalTactic t
-  let msgs ← Core.getMessageLog
-  b.restore
-  Core.setMessageLog msgs
-
 /-- Define the conclusion of the current game or current level if some
 building a level. -/
 elab "Conclusion" t:str : command => do
@@ -147,20 +50,14 @@ elab "Conclusion" t:str : command => do
   | .World => modifyCurWorld  fun world => pure {world with conclusion := t.getString}
   | .Game => modifyCurGame  fun game => pure {game with conclusion := t.getString}
 
--- /-- Print current game for debugging purposes. -/
--- elab "PrintCurGame" : command => do
---   logInfo (toJson (← getCurGame))
-
-/-- Print current level for debugging purposes. -/
-elab "PrintCurLevel" : command => do
-  logInfo (repr (← getCurLevel))
-
--- /-- Print levels for debugging purposes. -/
-elab "PrintLevels" : command => do
-  logInfo $ repr $ (← getCurWorld).levels.toArray
+/-! ## World Paths -/
 
+/-- The worlds of a game are joint by paths. These are defined with the syntax
+`Path World₁ → World₂ → World₃`. -/
 def Parser.path := Parser.sepBy1Indent Parser.ident "→"
 
+/-- The worlds of a game are joint by paths. These are defined with the syntax
+`Path World₁ → World₂ → World₃`. -/
 elab "Path" s:Parser.path : command => do
   let mut last : Option Name := none
   for stx in s.raw.getArgs.getEvenElems do
@@ -172,71 +69,21 @@ elab "Path" s:Parser.path : command => do
       pure {game with worlds := {game.worlds with edges := game.worlds.edges.push (l, stx.getId)}}
     last := some stx.getId
 
-end metadata
-
-/-! ## Hints -/
-
-open Lean Meta Elab Command Term
-
-/-- From a term `s` and a list of pairs `(i, t) ; Ident × Term`, create the syntax
-where `s` is preceded with universal quantifiers `∀ i : t`. -/
-def mkGoalSyntax (s : Term) : List (Ident × Term) → MacroM Term
-| (n, t)::tail => do return (← `(∀ $n : $t, $(← mkGoalSyntax s tail)))
-| [] => return s
-
--- def elabHint (hidden : Bool) (binders : TSyntaxArray `Lean.Parser.Term.bracketedBinder)
---   (goal : TSyntax `term) (msg : TSyntax `interpolatedStrKind) :=
--- liftTermElabM do withOptions (fun options => options.setBool `linter.unusedVariables false) do
---   let (g, decls) ← elabBinders binders fun xs => do
---     let g ← mkForallFVars xs $ ← elabTermAndSynthesize goal none
---     synthesizeSyntheticMVarsNoPostponing false
---     return (← instantiateMVars g, ← xs.mapM (fun x => x.fvarId!.getDecl))
---   let varsName := `vars
---   let msg ← withLocalDeclD varsName (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr)) fun vars => do
---     let mut msg ← `(m! $msg)
---     for i in [:decls.size] do
---       msg ← `(let $(mkIdent decls[i]!.userName) := $(mkIdent varsName)[$(quote i)]!; $msg)
---     return ← mkLambdaFVars #[vars] $ ← elabTermAndSynthesize msg none
-
---   if g.hasMVar then throwError m!"Goal contains metavariables: {g}"
-
-  -- modifyCurLevel fun level => pure {level with hints := level.hints.push {
-  --   goal := g,
-  --   intros := decls.size,
-  --   hidden := hidden,
-  --   text := msg }}
-
-/-- Declare a hint. This version doesn't prevent the unused linter variable from running. -/
-local elab "Hint'" binders:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command =>
-  -- elabHint false binders goal msg
-  pure ()
-
-/--
-Declare a hint. This version doesn't prevent the unused linter variable from running.
-A hidden hint is only displayed if explicitly requested by the user.
--/
-local elab "HiddenHint'" binders:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command => do
-  -- elabHint true binders goal msg
-  pure ()
 
-/-- Declare a hint in reaction to a given tactic state in the current level. -/
-macro "Hint" decls:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command => do
-  `(set_option linter.unusedVariables false in Hint' $decls* : $goal => $msg)
 
-/-- Declare a hidden hint in reaction to a given tactic state in the current level. -/
-macro "HiddenHint" decls:bracketedBinder* ":" goal:term "=>" msg:interpolatedStr(term) : command => do
-  `(set_option linter.unusedVariables false in HiddenHint' $decls* : $goal => $msg)
+/-! # Inventory
 
+The inventory contains docs for tactics, lemmas, and definitions. These are all disabled
+in the first level and get enabled during the game.
+-/
 
-/-! ## Inventory -/
+/-! ## Doc entries -/
 
 /-- Throw an error if inventory doc does not exist -/
 def checkInventoryDoc (type : InventoryType) (name : Name) : CommandElabM Unit := do
   let some _ := (inventoryDocExt.getState (← getEnv)).find?
       (fun x => x.name == name && x.type == type)
-    | throwError "Missing {type} Documentation: {name}"
-
-/-! ### Tactics -/
+    | throwError "Missing {type} Documentation: {name} (add `{type}Doc {name}` in your game's docs section)"
 
 /-- Documentation entry of a tactic. Example:
 
@@ -255,26 +102,25 @@ elab "TacticDoc" name:ident content:str : command =>
     displayName := name.getId.toString,
     content := content.getString })
 
-/-- Declare tactics that are introduced by this level. -/
-elab "NewTactic" args:ident* : command => do
-  let names := args.map (·.getId)
-  for name in names do checkInventoryDoc .Tactic name
-  modifyCurLevel fun level => pure {level with tactics := {level.tactics with new := names}}
-
-/-- Declare tactics that are temporarily disabled in this level.
-This is ignored if `OnlyTactic` is set. -/
-elab "DisabledTactic" args:ident* : command => do
-  let names := args.map (·.getId)
-  -- for name in names do checkInventoryDoc .Tactic name
-  modifyCurLevel fun level => pure {level with tactics := {level.tactics with disabled := names}}
+/-- Documentation entry of a lemma. Example:
 
-/-- Temporarily disable all tactics except the ones declared here -/
-elab "OnlyTactic" args:ident* : command => do
-  let names := args.map (·.getId)
-  for name in names do checkInventoryDoc .Tactic name
-  modifyCurLevel fun level => pure {level with tactics := {level.tactics with only := names}}
+```
+LemmaDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
+```
 
-/-! ### Definitions -/
+* The first identifier is used in the commands `[New/Only/Disabled]Lemma`.
+  It is preferably the true name of the lemma. However, this is not required.
+* The string following `as` is the displayed name (in the Inventory).
+* The identifier after `in` is the category to group lemmas by (in the Inventory).
+* The description is a string supporting Markdown.
+ -/
+elab "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str : command =>
+  modifyEnv (inventoryDocExt.addEntry · {
+    name := name.getId,
+    type := .Lemma
+    displayName := displayName.getString,
+    category := category.getString,
+    content := content.getString })
 
 /-- Documentation entry of a definition. Example:
 
@@ -295,18 +141,58 @@ elab "DefinitionDoc" name:ident "as" displayName:str content:str : command =>
     displayName := displayName.getString,
     content := content.getString })
 
+/-! ## Add inventory items -/
+
+/-- Declare tactics that are introduced by this level. -/
+elab "NewTactic" args:ident* : command => do
+  let names := args.map (·.getId)
+  for name in names do checkInventoryDoc .Tactic name
+  modifyCurLevel fun level => pure {level with tactics := {level.tactics with new := names}}
+
+/-- Declare lemmas that are introduced by this level. -/
+elab "NewLemma" args:ident* : command => do
+  let names := args.map (·.getId)
+  for name in names do checkInventoryDoc .Lemma name
+  modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with new := names}}
+
 /-- Declare definitions that are introduced by this level. -/
 elab "NewDefinition" args:ident* : command => do
   let names := args.map (·.getId)
   for name in names do checkInventoryDoc .Definition name
   modifyCurLevel fun level => pure {level with definitions := {level.definitions with new := names}}
 
+/-- Declare tactics that are temporarily disabled in this level.
+This is ignored if `OnlyTactic` is set. -/
+elab "DisabledTactic" args:ident* : command => do
+  let names := args.map (·.getId)
+  -- for name in names do checkInventoryDoc .Tactic name
+  modifyCurLevel fun level => pure {level with tactics := {level.tactics with disabled := names}}
+
+/-- Declare lemmas that are temporarily disabled in this level.
+This is ignored if `OnlyLemma` is set. -/
+elab "DisabledLemma" args:ident* : command => do
+  let names := args.map (·.getId)
+  -- for name in names do checkInventoryDoc .Lemma name
+  modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with disabled := names}}
+
 /-- Declare definitions that are temporarily disabled in this level -/
 elab "DisabledDefinition" args:ident* : command => do
   let names := args.map (·.getId)
   -- for name in names do checkInventoryDoc .Definition name
   modifyCurLevel fun level => pure {level with definitions := {level.definitions with disabled := names}}
 
+/-- Temporarily disable all tactics except the ones declared here -/
+elab "OnlyTactic" args:ident* : command => do
+  let names := args.map (·.getId)
+  for name in names do checkInventoryDoc .Tactic name
+  modifyCurLevel fun level => pure {level with tactics := {level.tactics with only := names}}
+
+/-- Temporarily disable all lemmas except the ones declared here -/
+elab "OnlyLemma" args:ident* : command => do
+  let names := args.map (·.getId)
+  for name in names do checkInventoryDoc .Lemma name
+  modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with only := names}}
+
 /-- Temporarily disable all definitions except the ones declared here.
 This is ignored if `OnlyDefinition` is set. -/
 elab "OnlyDefinition" args:ident* : command => do
@@ -314,16 +200,32 @@ elab "OnlyDefinition" args:ident* : command => do
   for name in names do checkInventoryDoc .Definition name
   modifyCurLevel fun level => pure {level with definitions := {level.definitions with only := names}}
 
+/-- Define which tab of Lemmas is opened by default. Usage: `LemmaTab "Nat"`.
+If omitted, the current tab will remain open. -/
+elab "LemmaTab"  category:str : command =>
+  modifyCurLevel fun level => pure {level with lemmaTab := category.getString}
+
+
 
-/-! ### Lemmas -/
+/-! # Exercise Statement -/
 
+-- TODO: Instead of this, it would be nice to have a proper syntax parser that enables
+-- us highlighting on the client side.
+partial def reprintCore : Syntax → Option Format
+  | Syntax.missing => none
+  | Syntax.atom _ val => val.trim
+  | Syntax.ident _ rawVal _ _ => rawVal.toString
+  | Syntax.node _ _ args =>
+    match args.toList.filterMap reprintCore with
+    | [] => none
+    | [arg] => arg
+    | args => Format.group <| Format.nest 2 <| Format.joinSep args " "
 
-/-- Define the statement of the current level.
+/-- `reprint` is used to display the Lean-statement to the user-/
+def reprint (stx : Syntax) : Format :=
+  reprintCore stx |>.getD ""
 
-Arguments:
-- ident: (Optional) The name of the statemtent.
-- descr: (Optional) The human-readable version of the lemma as string. Accepts Markdown and Mathjax.
--/
+/-- Define the statement of the current level. -/
 elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : command => do
 
   -- Check that the statement name is a lemma in the doc
@@ -389,71 +291,118 @@ elab "Statement" statementName:ident ? descr:str ? sig:declSig val:declVal : com
   } -- Format.pretty <| format thmStatement.raw }
 
 
-/-- Documentation entry of a lemma. Example:
 
-```
-LemmaDoc Nat.succ_pos as "succ_pos" in "Nat" "says `0 < n.succ`, etc."
-```
+/-! # Hints -/
 
-* The first identifier is used in the commands `[New/Only/Disabled]Lemma`.
-  It is preferably the true name of the lemma. However, this is not required.
-* The string following `as` is the displayed name (in the Inventory).
-* The identifier after `in` is the category to group lemmas by (in the Inventory).
-* The description is a string supporting Markdown.
- -/
-elab "LemmaDoc" name:ident "as" displayName:str "in" category:str content:str : command =>
-  modifyEnv (inventoryDocExt.addEntry · {
-    name := name.getId,
-    type := .Lemma
-    displayName := displayName.getString,
-    category := category.getString,
-    content := content.getString })
+syntax hintArg := atomic(" (" (&"strict" <|> &"hidden") " := " withoutPosition(term) ")")
 
-/-- Define which tab of Lemmas is opened by default. Usage: `LemmaTab "Nat"`.
+/-- Remove any spaces at the beginning of a new line -/
+partial def removeIndentation (s : String) : String :=
+  let rec loop (i : String.Pos) (acc : String) (removeSpaces := false) : String :=
+    let c := s.get i
+    let i := s.next i
+    if s.atEnd i then
+      acc.push c
+    else if removeSpaces && c == ' ' then
+      loop i acc (removeSpaces := true)
+    else if c == '\n' then
+      loop i (acc.push c) (removeSpaces := true)
+    else
+      loop i (acc.push c)
+  loop ⟨0⟩ ""
 
-If omitted, the first tab will be open by default. -/
-elab "LemmaTab"  category:str : command =>
-  modifyCurLevel fun level => pure {level with lemmaTab := category.getString}
+/-- A tactic that can be used inside `Statement`s to indicate in which proof states players should
+see hints. The tactic does not affect the goal state.
+-/
+elab "Hint" args:hintArg* msg:interpolatedStr(term) : tactic => do
+  let mut strict := false
+  let mut hidden := false
 
-/-- Declare lemmas that are introduced by this level. -/
-elab "NewLemma" args:ident* : command => do
-  let names := args.map (·.getId)
-  for name in names do checkInventoryDoc .Lemma name
-  modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with new := names}}
+  -- remove spaces at the beginngng of new lines
+  let msg := TSyntax.mk $ msg.raw.setArgs $ ← msg.raw.getArgs.mapM fun m => do
+    match m with
+    | Syntax.node info k args =>
+      if k == interpolatedStrLitKind && args.size == 1 then
+        match args.get! 0 with
+        | (Syntax.atom info' val) =>
+          let val := removeIndentation val
+          return Syntax.node info k #[Syntax.atom info' val]
+        | _ => return m
+      else
+        return m
+    | _ => return m
 
-/-- Declare lemmas that are temporarily disabled in this level.
-This is ignored if `OnlyLemma` is set. -/
-elab "DisabledLemma" args:ident* : command => do
-  let names := args.map (·.getId)
-  -- for name in names do checkInventoryDoc .Lemma name
-  modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with disabled := names}}
+  for arg in args do
+    match arg with
+    | `(hintArg| (strict := true)) => strict := true
+    | `(hintArg| (strict := false)) => strict := false
+    | `(hintArg| (hidden := true)) => hidden := true
+    | `(hintArg| (hidden := false)) => hidden := false
+    | _ => throwUnsupportedSyntax
 
-/-- Temporarily disable all lemmas except the ones declared here -/
-elab "OnlyLemma" args:ident* : command => do
-  let names := args.map (·.getId)
-  for name in names do checkInventoryDoc .Lemma name
-  modifyCurLevel fun level => pure {level with lemmas := {level.lemmas with only := names}}
+  let goal ← Tactic.getMainGoal
+  goal.withContext do
+    -- We construct an expression that can produce the hint text. The difficulty is that we
+    -- want the text to possibly contain quotation of the local variables which might have been
+    -- named differently by the player.
+    let varsName := `vars
+    let text ← withLocalDeclD varsName (mkApp (mkConst ``Array [levelZero]) (mkConst ``Expr)) fun vars => do
+      let mut text ← `(m! $msg)
+      let goalDecl ← goal.getDecl
+      let decls := goalDecl.lctx.decls.toArray.filterMap id
+      for i in [:decls.size] do
+        text ← `(let $(mkIdent decls[i]!.userName) := $(mkIdent varsName)[$(quote i)]!; $text)
+      return ← mkLambdaFVars #[vars] $ ← Term.elabTermAndSynthesize text none
+    let textmvar ← mkFreshExprMVar none
+    guard $ ← isDefEq textmvar text -- Store the text in a mvar.
+    -- The information about the hint is logged as a message using `logInfo` to transfer it to the
+    -- `Statement` command:
+    logInfo $
+      .tagged `Hint $
+      .nest (if strict then 1 else 0) $
+      .nest (if hidden then 1 else 0) $
+      .compose (.ofGoal textmvar.mvarId!) (.ofGoal goal)
+
+/-- This tactic allows us to execute an alternative sequence of tactics, but without affecting the
+proof state. We use it to define Hints for alternative proof methods or dead ends. -/
+elab "Branch" t:tacticSeq : tactic => do
+  let b ← saveState
+  Tactic.evalTactic t
 
-/-! ## Make Game -/
+  -- Show an info whether the branch proofs all remaining goals.
+  let gs ← Tactic.getUnsolvedGoals
+  if gs.isEmpty then
+    logInfo "This branch finishes the proof."
+  else
+    logInfo "This branch leaves open goals."
+
+  let msgs ← Core.getMessageLog
+  b.restore
+  Core.setMessageLog msgs
+
+
+
+/-! # Make Game -/
 
 def GameLevel.getInventory (level : GameLevel) : InventoryType → InventoryInfo
 | .Tactic => level.tactics
 | .Definition => level.definitions
 | .Lemma => level.lemmas
 
-def GameLevel.setComputedInventory (level : GameLevel) : InventoryType → Array ComputedInventoryItem → GameLevel
+def GameLevel.setComputedInventory (level : GameLevel) :
+    InventoryType → Array ComputedInventoryItem → GameLevel
 | .Tactic, v =>     {level with tactics     := {level.tactics     with computed := v}}
 | .Definition, v => {level with definitions := {level.definitions with computed := v}}
 | .Lemma, v =>      {level with lemmas      := {level.lemmas      with computed := v}}
 
-/-- Make the final Game. This command will precompute various things about the game, such as which
+/-- Build the game. This command will precompute various things about the game, such as which
 tactics are available in each level etc. -/
 elab "MakeGame" : command => do
   let game ← getCurGame
 
   -- Check for loops in world graph
   if game.worlds.hasLoops then
-    throwError "World graph has loops!"
+    throwError "World graph must not contain loops! Check your `Path` declarations."
 
   -- Compute which inventory items are available in which level:
   for inventoryType in open InventoryType in #[Tactic, Definition, Lemma] do
@@ -523,3 +472,19 @@ elab "MakeGame" : command => do
 
         modifyLevel ⟨← getCurGameId, worldId, levelId⟩ fun level => do
           return level.setComputedInventory inventoryType itemsArray
+
+
+
+/-! # Debugging tools -/
+
+-- /-- Print current game for debugging purposes. -/
+-- elab "PrintCurGame" : command => do
+--   logInfo (toJson (← getCurGame))
+
+/-- Print current level for debugging purposes. -/
+elab "PrintCurLevel" : command => do
+  logInfo (repr (← getCurLevel))
+
+/-- Print levels for debugging purposes. -/
+elab "PrintLevels" : command => do
+  logInfo $ repr $ (← getCurWorld).levels.toArray
diff --git a/server/leanserver/GameServer/EnvExtensions.lean b/server/leanserver/GameServer/EnvExtensions.lean
index be1e032..200082c 100644
--- a/server/leanserver/GameServer/EnvExtensions.lean
+++ b/server/leanserver/GameServer/EnvExtensions.lean
@@ -8,7 +8,6 @@ The game framework stores almost all its game building data in environment exten
 defined in this file.
 -/
 
-
 open Lean
 
 /-! ## Hints -/
@@ -20,9 +19,9 @@ structure GoalHintEntry where
   goal : AbstractCtxResult
   /-- Text of the hint as an expression of type `Array Expr → MessageData` -/
   text : Expr
-  /--  If true, then hint should be hidden and only be shown on player's request -/
+  /-- If true, then hint should be hidden and only be shown on player's request -/
   hidden : Bool := false
-  /--  If true, then the goal must contain only the assumptions specified in `goal` and no others -/
+  /-- If true, then the goal must contain only the assumptions specified in `goal` and no others -/
   strict : Bool := false
 
 instance : Repr GoalHintEntry := {
@@ -40,14 +39,45 @@ instance : ToString InventoryType := ⟨fun t => match t with
 | .Definition => "Definition"
 ⟩
 
+/-- An inventory item represents the documentation of a tactic/lemma/definitions. -/
 structure InventoryDocEntry where
+  /--
+  The name of the item. The restrictions are:
+
+  * for Tactics: The name of the tactic.
+  * for Lemmas: *Fully qualified* lemma name.
+  * for Definitions: no restrictions.
+  -/
   name : Name
+  /-- One of `Tactic`, `Lemma` and `Definition`. -/
   type : InventoryType
+  /-- The display name shown in the inventory. This can be free-text. -/
   displayName : String
+  /-- Category to group inventory items by. (currently only used for lemmas) -/
   category : String
+  /-- The description (doc) of the item. (free-text) -/
   content : String
   deriving ToJson, Repr, Inhabited
 
+structure ComputedInventoryItem where
+  /--
+  The name of the item. The restrictions are:
+
+  * for Tactics: The name of the tactic.
+  * for Lemmas: *Fully qualified* lemma name.
+  * for Definitions: no restrictions.
+  -/
+  name : Name
+  /-- The display name shown in the inventory. This can be free-text. -/
+  displayName : String
+  /-- Category to group inventory items by (currently only used for lemmas). -/
+  category : String
+  /-- If `true` then the item only gets unlocked in a later level. -/
+  locked : Bool
+  /-- If `true` then the item is blocked for this level. -/
+  disabled : Bool := false
+deriving ToJson, FromJson, Repr, Inhabited
+
 /-- Environment extension for inventory documentation. -/
 initialize inventoryDocExt : SimplePersistentEnvExtension InventoryDocEntry (Array InventoryDocEntry) ←
   registerSimplePersistentEnvExtension {
@@ -120,15 +150,6 @@ structure LevelId where
   level : Nat
 deriving Inhabited
 
-structure ComputedInventoryItem where
-  name : Name
-  displayName : String
-  category : String
-  locked : Bool
-  -- items that are temporarily blocked in this level.
-  disabled : Bool := false
-deriving ToJson, FromJson, Repr, Inhabited
-
 structure InventoryInfo where
   -- new inventory items introduced by this level:
   new : Array Name
@@ -148,35 +169,41 @@ instance : Repr Elab.Command.Scope := ⟨fun s _ => repr s.currNamespace⟩
 
 structure GameLevel where
   index: Nat
+  /-- The title of the level. -/
   title: String := default
-  /-- introduction: Theory block shown all the time -/
+  /-- Introduction text shown all the time. (markdown) -/
   introduction: String := default
-  /-- The mathematical statemtent in mathematician-readable form -/
-  description: String := default
-  /-- conclusion displayed when level is completed. -/
   conclusion: String := default
-  tactics: InventoryInfo := default
-  definitions: InventoryInfo := default
-  lemmas: InventoryInfo := default
-  lemmaTab: Option String := none
   hints: Array GoalHintEntry := default
   /-- The statement in Lean. -/
   goal : TSyntax `Lean.Parser.Command.declSig := default
   scope : Elab.Command.Scope := default
+  /-- The mathematical statement in mathematician-readable form. (markdown) -/
   descrText: String := default
   descrFormat : String := default
-  -- The module to be imported when playing this level:
+  /-- The `category` of lemmas to be open by default -/
+  lemmaTab: Option String := none
+  /-- The module to be imported when playing this level -/
   module : Name := default
+  tactics: InventoryInfo := default
+  definitions: InventoryInfo := default
+  lemmas: InventoryInfo := default
   deriving Inhabited, Repr
 
 /-! ## World -/
 
+/-- A world is a collection of levels, like a chapter. -/
 structure World where
+  /- Internal name of the world. Not visible to the player. -/
   name: Name
-  title: String := ""
-  introduction: String := ""
-  conclusion : String := ""
-  levels: HashMap Nat GameLevel := {}
+  /-- Display title of the world. -/
+  title: String := default
+  /-- World introduction to be shown before the first level is loaded. (markdown) -/
+  introduction: String := default
+  /-- TODO: This is currently unused. -/
+  conclusion : String := default
+  /-- The levels of the world. -/
+  levels: HashMap Nat GameLevel := default
 deriving Inhabited
 
 instance : ToJson World := ⟨
@@ -189,12 +216,17 @@ instance : ToJson World := ⟨
 /-! ## Game -/
 
 structure Game where
+  /-- Internal name of the game. -/
   name : Name
-  title : String := ""
-  introduction : String := ""
-  conclusion : String := ""
-  authors : List String := []
-  worlds : Graph Name World := {}
+  /-- TODO: currently unused. -/
+  title : String := default
+  /-- Text displayed on the main landing page of the game. -/
+  introduction : String := default
+  /-- TODO: currently unused. -/
+  conclusion : String := default
+  /-- TODO: currently unused. -/
+  authors : List String := default
+  worlds : Graph Name World := default
 deriving Inhabited, ToJson
 
 /-! ## Game environment extension -/