diff --git a/server/leanserver/GameServer/RpcHandlers.lean b/server/leanserver/GameServer/RpcHandlers.lean
index 6fb41d8..02544c5 100644
--- a/server/leanserver/GameServer/RpcHandlers.lean
+++ b/server/leanserver/GameServer/RpcHandlers.lean
@@ -76,13 +76,14 @@ def getLevelByFileName [Monad m] [MonadError m] [MonadEnv m] (fileName : String)
 open Meta in
 /-- Find all messages whose trigger matches the current goal -/
 def findMessages (goal : MVarId) (doc : FileWorker.EditableDocument) : MetaM (Array String) := do
-  let level ← getLevelByFileName doc.meta.mkInputContext.fileName
-  let messages ← level.messages.filterMapM fun message => do
-    let (declMvars, binderInfo, messageGoal) ← forallMetaBoundedTelescope message.goal message.intros
-    if ← isDefEq messageGoal (← inferType $ mkMVar goal) -- TODO: also check assumptions
-    then return some message.message
-    else return none
-  return messages
+  goal.withContext do
+    let level ← getLevelByFileName doc.meta.mkInputContext.fileName
+    let messages ← level.messages.filterMapM fun message => do
+      let (declMvars, binderInfo, messageGoal) ← forallMetaBoundedTelescope message.goal message.intros
+      if ← isDefEq messageGoal (← inferType $ mkMVar goal) -- TODO: also check assumptions
+      then return some message.message
+      else return none
+    return messages
 
 /-- Get goals and messages at a given position -/
 def getGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option PlainGoal)) := do