From 44f7b6703e96a256048ad1708bede720578d7144 Mon Sep 17 00:00:00 2001
From: joneugster <eugster.jon@gmail.com>
Date: Thu, 30 Nov 2023 12:16:06 +0100
Subject: [PATCH] Revert "fix variables in hints"

This reverts commit 8851cd8b1f795e7701179d9b3568e52fc6729824.
---
 server/GameServer/RpcHandlers.lean | 35 +++++++++++++++---------------
 1 file changed, 18 insertions(+), 17 deletions(-)

diff --git a/server/GameServer/RpcHandlers.lean b/server/GameServer/RpcHandlers.lean
index 28b4829..ae71a25 100644
--- a/server/GameServer/RpcHandlers.lean
+++ b/server/GameServer/RpcHandlers.lean
@@ -114,24 +114,25 @@ def evalHintMessage : Expr → MetaM (Array Expr → MessageData) := fun _ => pu
 open Meta in
 /-- Find all hints whose trigger matches the current goal -/
 def findHints (goal : MVarId) (doc : FileWorker.EditableDocument) (initParams : Lsp.InitializeParams) : MetaM (Array GameHint) := do
-  let some level ← getLevelByFileName? initParams doc.meta.mkInputContext.fileName
-    | throwError "Level not found: {doc.meta.mkInputContext.fileName}"
-  let hints ← level.hints.filterMapM fun hint => do
-    openAbstractCtxResult hint.goal fun hintFVars hintGoal => goal.withContext do
-      if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
-      then
-        let lctx := (← goal.getDecl).lctx
-        if let some bij ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
+  goal.withContext do
+    let some level ← getLevelByFileName? initParams doc.meta.mkInputContext.fileName
+      | throwError "Level not found: {doc.meta.mkInputContext.fileName}"
+    let hints ← level.hints.filterMapM fun hint => do
+      openAbstractCtxResult hint.goal fun hintFVars hintGoal => do
+        if let some fvarBij := matchExpr (← instantiateMVars $ hintGoal) (← instantiateMVars $ ← inferType $ mkMVar goal)
         then
-          let userFVars := hintFVars.map fun v => bij.forward.findD v.fvarId! v.fvarId!
-          let text := (← evalHintMessage hint.text) (userFVars.map Expr.fvar)
-          let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
-          let text ← (MessageData.withContext ctx text).toString
-          return some { text := text, hidden := hint.hidden }
-        else return none
-      else
-        return none
-  return hints
+          let lctx := (← goal.getDecl).lctx
+          if let some bij ← matchDecls hintFVars lctx.getFVars (strict := hint.strict) (initBij := fvarBij)
+          then
+            let userFVars := hintFVars.map fun v => bij.forward.findD v.fvarId! v.fvarId!
+            let text := (← evalHintMessage hint.text) (userFVars.map Expr.fvar)
+            let ctx := {env := ← getEnv, mctx := ← getMCtx, lctx := ← getLCtx, opts := {}}
+            let text ← (MessageData.withContext ctx text).toString
+            return some { text := text, hidden := hint.hidden }
+          else return none
+        else
+          return none
+    return hints
 
 open RequestM in
 def getInteractiveGoals (p : Lsp.PlainGoalParams) : RequestM (RequestTask (Option InteractiveGoals)) := do