Pantograph/Goal.lean

@@ -113,14 +113,11 @@ protected def GoalState.focus (state: GoalState) (goalId: Nat): Option GoalState
   }
 
 /-- Immediately bring all parent goals back into scope. Used in automatic mode -/
-@[export pantograph_goal_state_immediate_resume]
+@[export pantograph_goal_state_immediate_resume_parent]
 protected def GoalState.immediateResume (state: GoalState) (parent: GoalState): GoalState :=
   -- Prune parents solved goals
   let mctx := state.mctx
-  let parentGoals := parent.goals.filter λ goal =>
+  let parentGoals := parent.goals.filter $ λ goal => mctx.eAssignment.contains goal
-    let isDuplicate := state.goals.contains goal
-    let isSolved := mctx.eAssignment.contains goal || mctx.dAssignment.contains goal
-    (¬ isDuplicate) && (¬ isSolved)
   {
     state with
     savedState := {
@@ -130,25 +127,25 @@ protected def GoalState.immediateResume (state: GoalState) (parent: GoalState):
   }
 
 /--
-Brings into scope a list of goals. User must ensure `goals` is distinct.
+Brings into scope a list of goals
 -/
 @[export pantograph_goal_state_resume]
-protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState := do
+protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
   if ¬ (goals.all (λ goal => state.mvars.contains goal)) then
     let invalid_goals := goals.filter (λ goal => ¬ state.mvars.contains goal) |>.map (·.name.toString)
     .error s!"Goals {invalid_goals} are not in scope"
-  -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
+  else
-  let unassigned := goals.filter λ goal =>
+    -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
-    let isSolved := state.mctx.eAssignment.contains goal || state.mctx.dAssignment.contains goal
+    let unassigned := goals.filter (λ goal =>
-    let isDuplicate := state.goals.contains goal
+      let mctx := state.mctx
-    (¬ isDuplicate) && (¬ isSolved)
+      ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
-  return {
+    .ok {
-    state with
+      state with
-    savedState := {
+      savedState := {
-      term := state.savedState.term,
+        term := state.savedState.term,
-      tactic := { goals := unassigned },
+        tactic := { goals := unassigned },
-    },
+      },
-  }
+    }
 /--
 Brings into scope all goals from `branch`
 -/

Repl.lean

@@ -321,7 +321,9 @@ def execute (command: Protocol.Command): MainM Json := do
     | .ok (.success nextGoalState) => do
       let nextGoalState ← match state.options.automaticMode, args.conv? with
         | true, .none => do
-          pure $ nextGoalState.immediateResume goalState
+          let .ok result := nextGoalState.resume (nextGoalState.goals ++ goalState.goals) |
+            Protocol.throw $ errorIO "Resuming known goals"
+          pure result
         | true, .some true => pure nextGoalState
         | true, .some false => do
           let .some (_, _, dormantGoals) := goalState.convMVar? |