feat: Capture environment in drafting

2024-10-12 16:46:44 -07:00 · 2024-10-12 16:46:44 -07:00 · 5a2ae880f4
parent e0ba65a7cd
commit 5a2ae880f4
1 changed files with 2 additions and 2 deletions
--- a/Repl.lean
+++ b/Repl.lean
@ -233,9 +233,9 @@ def execute (command: Protocol.Command): MainM Lean.Json := do
          else
            []
        let messages ← step.messageStrings
-        return (boundary, invocations?, sorrys, messages)
+        return (step.before, boundary, invocations?, sorrys, messages)
      let li ← frontendM.run context |>.run' state
-      let units ← li.mapM λ (boundary, invocations?, sorrys, messages) => do
+      let units ← li.mapM λ (env, boundary, invocations?, sorrys, messages) => Lean.withEnv env do
        let (goalStateId?, goals) ← if sorrys.isEmpty then do
            pure (.none, #[])
          else do