Use local scope from level file in game

Fixes #31

server/leanserver/GameServer/Commands.lean

@@ -79,9 +79,12 @@ elab "Statement" statementName:ident ? descr:str sig:declSig val:declVal : comma
   -- | none => `(lemma $(mkIdent "XX") $sig $val) -- TODO: Make it into an `example`
   -- | some name => `(lemma $name $sig $val)
 
+  let scope ← getScope
+
   elabCommand thmStatement
   modifyCurLevel fun level => pure {level with
     goal := sig,
+    scope := scope,
     descrText := descr.getString,
     descrFormat := match statementName with
     | none => "example " ++ (toString <| reprint sig.raw) ++ " := by"

server/leanserver/GameServer/EnvExtensions.lean

@@ -161,9 +161,10 @@ deriving ToJson, FromJson, Repr
 def getCurLevelId [MonadError m] : m LevelId := do
   return { game := ← getCurGameId, world := ← getCurWorldId, level := ← getCurLevelIdx}
 
-/--
+/-- Instance to make GameLevel Repr work -/
-
+instance : Repr Elab.Command.Scope := ⟨fun s _ => repr s.currNamespace⟩
 
+/--
 Fields:
 - TODO
 - introduction: Theory block shown all the time.
@@ -195,6 +196,7 @@ structure GameLevel where
   lemmas: Array Availability := default
   hints: Array GoalHintEntry := default
   goal : TSyntax `Lean.Parser.Command.declSig := default
+  scope : Elab.Command.Scope := default
   descrText: String := default
   descrFormat : String := default
   deriving Inhabited, Repr

server/leanserver/GameServer/FileWorker.lean

@@ -153,6 +153,8 @@ def compileProof (inputCtx : Parser.InputContext) (snap : Snapshot) (hasWidgets
           let cmdStx ← `(command|
             set_option tactic.hygienic false in
             theorem the_theorem $(level.goal) := by {$(⟨tacticStx⟩)} )
+
+          Elab.Command.withScope (fun _ => level.scope) do -- use open namespaces and options as in the file
             Elab.Command.elabCommandTopLevel cmdStx)
         cmdCtx cmdStateRef
     let postNew := (← tacticCacheNew.get).post