Pantograph/Frontend/Elab.lean

@@ -148,10 +148,15 @@ structure AnnotatedGoalState where
 Since we cannot directly merge `MetavarContext`s, we have to get creative. This
 function duplicates frozen mvars in term and tactic info nodes, and add them to
 the current `MetavarContext`.
+
+WARNING: Behaviour is unstable when there are multiple `sorry`s. Consider using
+the draft tactic instead.
 -/
 @[export pantograph_frontend_sorrys_to_goal_state_m]
 def sorrysToGoalState (sorrys : List InfoWithContext) : MetaM AnnotatedGoalState := do
+  let env := sorrys.head? >>= (·.context?) |>.map (·.env) |>.getD (← getEnv)
   assert! !sorrys.isEmpty
+  withEnv env do
     let goalsM := sorrys.mapM λ i => do
       match i.info with
       | .ofTermInfo termInfo  => do

Repl.lean

@@ -44,8 +44,6 @@ structure CompilationUnit where
   messages : Array String
   newConstants : List Name
 
-
-
 def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol.FrontendProcessResult) := do
   let options := (← get).options
   let (fileName, file) ← match args.fileName?, args.file? with
@@ -78,7 +76,7 @@ def frontend_process_inner (args: Protocol.FrontendProcess): MainM (CR Protocol.
       else
         pure []
     return {
-      env := step.after,
+      env := step.before,
       boundary,
       invocations,
       sorrys,