Pantograph/Goal.lean

@@ -113,11 +113,14 @@ 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_parent]
+@[export pantograph_goal_state_immediate_resume]
 protected def GoalState.immediateResume (state: GoalState) (parent: GoalState): GoalState :=
   -- Prune parents solved goals
   let mctx := state.mctx
-  let parentGoals := parent.goals.filter $ λ goal => mctx.eAssignment.contains goal
+  let parentGoals := parent.goals.filter λ goal =>
+    let isDuplicate := state.goals.contains goal
+    let isSolved := mctx.eAssignment.contains goal || mctx.dAssignment.contains goal
+    (¬ isDuplicate) && (¬ isSolved)
   {
     state with
     savedState := {
@@ -127,19 +130,19 @@ protected def GoalState.immediateResume (state: GoalState) (parent: GoalState):
   }
 
 /--
-Brings into scope a list of goals
+Brings into scope a list of goals. User must ensure `goals` is distinct.
 -/
 @[export pantograph_goal_state_resume]
-protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState :=
+protected def GoalState.resume (state: GoalState) (goals: List MVarId): Except String GoalState := do
   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"
-  else
   -- Set goals to the goals that have not been assigned yet, similar to the `focus` tactic.
-    let unassigned := goals.filter (λ goal =>
-      let mctx := state.mctx
-      ¬(mctx.eAssignment.contains goal || mctx.dAssignment.contains goal))
-    .ok {
+  let unassigned := goals.filter λ goal =>
+    let isSolved := state.mctx.eAssignment.contains goal || state.mctx.dAssignment.contains goal
+    let isDuplicate := state.goals.contains goal
+    (¬ isDuplicate) && (¬ isSolved)
+  return {
     state with
     savedState := {
       term := state.savedState.term,

Repl.lean

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