avoid unknown free variable error in messages

2022-12-06 09:58:45 +01:00
parent c6cd627eec
commit 9f5fdbe35b
1 changed files with 8 additions and 7 deletions
@@ -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