diff --git a/README.md b/README.md
index fb7fe1bb..3455eef2 100644
--- a/README.md
+++ b/README.md
@@ -44,7 +44,8 @@ Example output:
 {"sorries":
  [{"pos": {"line": 1, "column": 18},
    "endPos": {"line": 1, "column": 23},
-   "goal": "⊢ Nat",
+   "parentDecl": "h",
+   "goals": ["⊢ Nat"],
    "proofState": 0}],
  "messages":
  [{"severity": "error",
@@ -92,12 +93,13 @@ and then use the `proofState` index returned for each `sorry`.
 
 Example usage:
 ```json
-{"cmd" : "def f (x : Unit) : Nat := by sorry"}
+{"cmd" : "def f (x : Unit) : Nat := by sorry", "sorries": "individual"}
 
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 29},
-   "goal": "x : Unit\n⊢ Nat",
+   "parentDecl": "f",
+   "goals": ["x : Unit\n⊢ Nat"],
    "endPos": {"line": 1, "column": 34}}],
  "messages":
  [{"severity": "warning",
diff --git a/REPL/JSON.lean b/REPL/JSON.lean
index ebec4c56..492bbe75 100644
--- a/REPL/JSON.lean
+++ b/REPL/JSON.lean
@@ -13,7 +13,8 @@ namespace REPL
 
 structure CommandOptions where
   allTactics : Option Bool := none
-  rootGoals : Option Bool := none
+  -- Should be "individual", "grouped", or "rootGoals".
+  sorries : Option String := none
   /--
   Should be "full", "tactics", "original", or "substantive".
   Anything else is ignored.
@@ -76,28 +77,32 @@ def Message.of (m : Lean.Message) : IO Message := do pure <|
 structure Sorry where
   pos : Pos
   endPos : Pos
-  goal : String
+  goals : List String
   /--
   The index of the proof state at the sorry.
   You can use the `ProofStep` instruction to run a tactic at this state.
   -/
   proofState : Option Nat
+  parentDecl: Option Name := none
 deriving FromJson
 
 instance : ToJson Sorry where
   toJson r := Json.mkObj <| .flatten [
-    [("goal", r.goal)],
+    [("goals", toJson r.goals)],
     [("proofState", toJson r.proofState)],
     if r.pos.line ≠ 0 then [("pos", toJson r.pos)] else [],
     if r.endPos.line ≠ 0 then [("endPos", toJson r.endPos)] else [],
+    if r.parentDecl.isSome then [("parentDecl", toJson r.parentDecl)] else []
   ]
 
 /-- Construct the JSON representation of a Lean sorry. -/
-def Sorry.of (goal : String) (pos endPos : Lean.Position) (proofState : Option Nat) : Sorry :=
+def Sorry.of (goals : List String) (pos endPos : Lean.Position) (proofState : Option Nat)
+(parentDecl : Option Name): Sorry :=
   { pos := ⟨pos.line, pos.column⟩,
     endPos := ⟨endPos.line, endPos.column⟩,
-    goal,
-    proofState }
+    goals,
+    proofState,
+    parentDecl }
 
 structure Tactic where
   pos : Pos
@@ -106,16 +111,19 @@ structure Tactic where
   tactic : String
   proofState : Option Nat
   usedConstants : Array Name
+  parentDecl : Option Name := none
 deriving ToJson, FromJson
 
 /-- Construct the JSON representation of a Lean tactic. -/
-def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState : Option Nat) (usedConstants : Array Name) : Tactic :=
+def Tactic.of (goals tactic : String) (pos endPos : Lean.Position) (proofState : Option Nat)
+(usedConstants : Array Name) (parentDecl : Option Name) : Tactic :=
   { pos := ⟨pos.line, pos.column⟩,
     endPos := ⟨endPos.line, endPos.column⟩,
     goals,
     tactic,
     proofState,
-    usedConstants }
+    usedConstants,
+    parentDecl }
 
 /--
 A response to a Lean command.
@@ -150,7 +158,6 @@ structure ProofStepResponse where
   proofState : Nat
   goals : List String
   messages : List Message := []
-  sorries : List Sorry := []
   traces : List String
   proofStatus : String
 deriving ToJson, FromJson
@@ -160,7 +167,6 @@ instance : ToJson ProofStepResponse where
     [("proofState", r.proofState)],
     [("goals", toJson r.goals)],
     Json.nonemptyList "messages" r.messages,
-    Json.nonemptyList "sorries" r.sorries,
     Json.nonemptyList "traces" r.traces,
     [("proofStatus", r.proofStatus)]
   ]
diff --git a/REPL/Lean/InfoTree.lean b/REPL/Lean/InfoTree.lean
index a3f68165..ba1687e4 100644
--- a/REPL/Lean/InfoTree.lean
+++ b/REPL/Lean/InfoTree.lean
@@ -195,18 +195,18 @@ def findTacticNodes (t : InfoTree) : List (TacticInfo × ContextInfo × List MVa
   | (.ofTacticInfo i, some ctx, rootGoals) => (i, ctx, rootGoals)
   | _ => none
 
-/-- Returns the root goals for a given `InfoTree`. -/
-partial def findRootGoals (t : InfoTree) (ctx? : Option ContextInfo := none) :
-  List (TacticInfo × ContextInfo × List MVarId) :=
+/-- Returns the root and last goals for a given `InfoTree`. -/
+partial def findRootAndLastGoals (t : InfoTree) (ctx? : Option ContextInfo := none) :
+    List (TacticInfo × ContextInfo × List MVarId × List MVarId) :=
   match t with
-  | .context ctx t => t.findRootGoals (ctx.mergeIntoOuter? ctx?)
+  | .context ctx t => t.findRootAndLastGoals (ctx.mergeIntoOuter? ctx?)
   | .node info ts =>
     match info with
     | .ofTacticInfo i =>
       match ctx? with
-      | some ctx => [(i, ctx, i.goalsBefore)]
+      | some ctx => [(i, ctx, i.goalsBefore, i.goalsAfter)]
       | _ => []
-    | _ => ts.toList.flatMap (fun t => t.findRootGoals ctx?)
+    | _ => ts.toList.flatMap (fun t => t.findRootAndLastGoals ctx?)
   | _ => []
 
 /-- Return all `TacticInfo` nodes in an `InfoTree`
@@ -264,12 +264,21 @@ def tactics (t : InfoTree) : List (ContextInfo × Syntax × List MVarId × List
       i.getUsedConstantsAsSet.toArray )
 
 def rootGoals (t : InfoTree) : List (ContextInfo × List MVarId × Position) :=
-  t.findRootGoals.map fun ⟨i, ctx, rootGoals⟩ =>
+  t.findRootAndLastGoals.map fun ⟨i, ctx, rootGoals, _⟩ =>
     let range := stxRange ctx.fileMap i.stx
     ( { ctx with mctx := i.mctxBefore, ngen := ctx.ngen.mkChild.1 },
       rootGoals,
       range.fst )
 
+def rootAndLastGoals (t : InfoTree) : List (ContextInfo × List MVarId × List MVarId × Position × Position) :=
+  t.findRootAndLastGoals.map fun ⟨i, ctx, rootGoals, lastGoals⟩ =>
+    let range := stxRange ctx.fileMap i.stx
+    ( { ctx with mctx := i.mctxAfter, ngen := ctx.ngen.mkChild.1 },
+      rootGoals,
+      lastGoals,
+      range.fst,
+      range.snd )
+
 end Lean.Elab.InfoTree
 
 namespace Lean.Elab.TacticInfo
diff --git a/REPL/Main.lean b/REPL/Main.lean
index d181080f..0a1ce54c 100644
--- a/REPL/Main.lean
+++ b/REPL/Main.lean
@@ -100,20 +100,33 @@ def sorries (trees : List InfoTree) (env? : Option Environment) (rootGoals? : Op
     | .term _ none => false
     | _ => true ) |>.mapM
       fun ⟨ctx, g, pos, endPos⟩ => do
-        let (goal, proofState) ← match g with
+        let (goals, proofState) ← match g with
         | .tactic g => do
           let lctx ← ctx.runMetaM {} do
               match ctx.mctx.findDecl? g with
               | some decl => return decl.lctx
               | none => throwError "unknown metavariable '{g}'"
           let s ← ProofSnapshot.create ctx lctx env? [g] rootGoals?
-          pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
+          pure ((← s.ppGoals).map (s!"{·}"), some s)
         | .term lctx (some t) => do
           let s ← ProofSnapshot.create ctx lctx env? [] rootGoals? [t]
-          pure ("\n".intercalate <| (← s.ppGoals).map fun s => s!"{s}", some s)
+          pure ((← s.ppGoals).map (s!"{·}"), some s)
         | .term _ none => unreachable!
         let proofStateId ← proofState.mapM recordProofSnapshot
-        return Sorry.of goal pos endPos proofStateId
+        return Sorry.of goals pos endPos proofStateId ctx.parentDecl?
+
+def groupedSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do
+  let a ← trees.flatMap InfoTree.rootAndLastGoals |>.mapM
+    fun ⟨ctx, rootGoals, lastGoals, startPos, endPos⟩ => do
+      let proofState ← ProofSnapshot.create ctx none env? lastGoals rootGoals
+      let proofState' ← proofState.runString "skip" -- Trick to get the sorries
+      let goals := (← proofState'.ppGoals).map (s!"{·}")
+      if goals.isEmpty then
+        return []
+      else
+        let proofStateId ← recordProofSnapshot proofState'
+        return [Sorry.of goals startPos endPos proofStateId ctx.parentDecl?]
+  return a.flatten
 
 def ppTactic (ctx : ContextInfo) (stx : Syntax) : IO Format :=
   ctx.runMetaM {} try
@@ -128,15 +141,15 @@ def tactics (trees : List InfoTree) (env? : Option Environment) : M m (List Tact
       let goals := s!"{(← ctx.ppGoals goals)}".trim
       let tactic := Format.pretty (← ppTactic ctx stx)
       let proofStateId ← proofState.mapM recordProofSnapshot
-      return Tactic.of goals tactic pos endPos proofStateId ns
+      return Tactic.of goals tactic pos endPos proofStateId ns ctx.parentDecl?
 
 def collectRootGoalsAsSorries (trees : List InfoTree) (env? : Option Environment) : M m (List Sorry) := do
   trees.flatMap InfoTree.rootGoals |>.mapM
     fun ⟨ctx, goals, pos⟩ => do
       let proofState := some (← ProofSnapshot.create ctx none env? goals goals)
-      let goals := s!"{(← ctx.ppGoals goals)}".trim
+      let goals ← goals.mapM (fun g => do pure s!"{(← ctx.ppGoals [g])}".trim)
       let proofStateId ← proofState.mapM recordProofSnapshot
-      return Sorry.of goals pos pos proofStateId
+      return Sorry.of goals pos ⟨0,0⟩ proofStateId ctx.parentDecl?
 
 
 private def collectFVarsAux : Expr → NameSet
@@ -200,6 +213,8 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do
             let pf ← abstractAllLambdaFVars pf
             let pft ← Meta.inferType pf >>= instantiateMVars
 
+            if pf.hasSorry then
+              return "Incomplete: contains sorry"
             if pf.hasExprMVar then
               return "Incomplete: contains metavariable(s)"
 
@@ -220,9 +235,6 @@ def getProofStatus (proofState : ProofSnapshot) : M m String := do
               let _ ← addDecl decl
             catch ex =>
               return s!"Error: kernel type check failed: {← ex.toMessageData.toString}"
-
-            if pf.hasSorry then
-              return "Incomplete: contains sorry"
             return "Completed"
 
         | _ => return "Not verified: more than one initial goal"
@@ -236,22 +248,11 @@ def createProofStepReponse (proofState : ProofSnapshot) (old? : Option ProofSnap
   let messages := proofState.newMessages old?
   let messages ← messages.mapM fun m => Message.of m
   let traces ← proofState.newTraces old?
-  let trees := proofState.newInfoTrees old?
-  let trees ← match old? with
-  | some old => do
-    let (ctx, _) ← old.runMetaM do return { ← CommandContextInfo.save with }
-    let ctx := PartialContextInfo.commandCtx ctx
-    pure <| trees.map fun t => InfoTree.context ctx t
-  | none => pure trees
-  -- For debugging purposes, sometimes we print out the trees here:
-  -- trees.forM fun t => do IO.println (← t.format)
-  let sorries ← sorries trees none (some proofState.rootGoals)
   let id ← recordProofSnapshot proofState
   return {
     proofState := id
-    goals := (← proofState.ppGoals).map fun s => s!"{s}"
+    goals := (← proofState.ppGoals).map (s!"{·}")
     messages
-    sorries
     traces
     proofStatus := (← getProofStatus proofState) }
 
@@ -309,10 +310,11 @@ def runCommand (s : Command) : M IO (CommandResponse ⊕ Error) := do
   let messages ← messages.mapM fun m => Message.of m
   -- For debugging purposes, sometimes we print out the trees here:
   -- trees.forM fun t => do IO.println (← t.format)
-  let sorries ← sorries trees initialCmdState.env none
-  let sorries ← match s.rootGoals with
-  | some true => pure (sorries ++ (← collectRootGoalsAsSorries trees initialCmdState.env))
-  | _ => pure sorries
+  let sorries ← match s.sorries with
+  | some "individual" => sorries trees initialCmdState.env none
+  | some "grouped" => groupedSorries trees initialCmdState.env
+  | some "rootGoals" => collectRootGoalsAsSorries trees initialCmdState.env
+  | _ => pure []
   let tactics ← match s.allTactics with
   | some true => tactics trees initialCmdState.env
   | _ => pure []
@@ -350,8 +352,10 @@ def processFile (s : File) : M IO (CommandResponse ⊕ Error) := do
 
 /--
 Run a single tactic, returning the id of the new proof statement, and the new goals.
+This implementation supports branching in tactic proofs.
+When a tactic generates new goals, each goal is properly tracked to allow subsequent tactics to be
+applied.
 -/
--- TODO detect sorries?
 def runProofStep (s : ProofStep) : M IO (ProofStepResponse ⊕ Error) := do
   match (← get).proofStates[s.proofState]? with
   | none => return .inr ⟨"Unknown proof state."⟩
diff --git a/REPL/Snapshots.lean b/REPL/Snapshots.lean
index f6936245..6d456516 100644
--- a/REPL/Snapshots.lean
+++ b/REPL/Snapshots.lean
@@ -114,6 +114,20 @@ namespace ProofSnapshot
 
 open Lean Elab Tactic
 
+/-- Transform `sorry` expressions into fresh opaque metavariables, collecting their IDs. -/
+def sorryToHole (src : Expr) : StateRefT (List MVarId) MetaM Expr :=
+  Meta.transform src λ expr =>
+    if expr.isSorry then do
+      -- extract the proof type from `sorry` (the first binder argument)
+      let type ← instantiateMVars (expr.getArg! 0 |>.bindingBody!)
+      if type.hasSorry then
+        throwError s!"Nested sorry in type not supported: {← Meta.ppExpr type}"
+      let mvar ← Meta.mkFreshExprSyntheticOpaqueMVar type
+      modify (mvar.mvarId! :: ·)
+      pure $ .done mvar
+    else
+      pure .continue
+
 /-- New messages in a `ProofSnapshot`, relative to an optional previous `ProofSnapshot`. -/
 def newMessages (new : ProofSnapshot) (old? : Option ProofSnapshot := none) : List Lean.Message :=
   match old? with
@@ -180,7 +194,27 @@ and run it in the current `ProofSnapshot`.
 def runString (p : ProofSnapshot) (t : String) : IO ProofSnapshot :=
   match Parser.runParserCategory p.coreState.env `tactic t with
   | .error e => throw (IO.userError e)
-  | .ok stx => p.runSyntax stx
+  | .ok stx => do
+    let result ← p.runSyntax stx
+
+    -- Process all goals after tactic execution to find and transform any sorries
+    let (newGoals, result') ← result.runMetaM do
+      let processExpr (acc : List MVarId) (mvarId : MVarId) (expr : Expr) : MetaM (List MVarId) := do
+        if expr.hasSorry then
+          mvarId.withContext do
+            let (newExpr, exprHoles) ← sorryToHole expr |>.run []
+            mvarId.assign newExpr
+            pure (acc ++ exprHoles)
+        else
+          pure acc
+
+      -- Process all expressions in the metavariable context
+      let mctx := result.metaState.mctx
+      let exprHoles ← mctx.eAssignment.foldlM processExpr []
+      pure exprHoles
+
+    let combinedGoals := newGoals ++ result'.tacticState.goals
+    return { result' with tacticState := { goals := combinedGoals } }
 
 /-- Pretty print the current goals in the `ProofSnapshot`. -/
 def ppGoals (p : ProofSnapshot) : IO (List Format) :=
diff --git a/test/Mathlib/test/20240209.expected.out b/test/Mathlib/test/20240209.expected.out
index b7cfc2da..cabececb 100644
--- a/test/Mathlib/test/20240209.expected.out
+++ b/test/Mathlib/test/20240209.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 22},
-   "goal": "⊢ False",
+   "parentDecl": "_example",
+   "goals": ["⊢ False"],
    "endPos": {"line": 1, "column": 27}}],
  "messages":
  [{"severity": "warning",
@@ -10,12 +11,12 @@
    "data": "declaration uses 'sorry'"}],
  "env": 0}
 
-{"proofStatus": "Incomplete: contains sorry",
+{"proofStatus": "Incomplete: open goals remain",
  "proofState": 1,
  "messages":
  [{"severity": "error",
    "pos": {"line": 0, "column": 0},
    "endPos": {"line": 0, "column": 0},
    "data": "unsolved goals\n⊢ False"}],
- "goals": []}
+ "goals": ["⊢ False"]}
 
diff --git a/test/Mathlib/test/20240209.in b/test/Mathlib/test/20240209.in
index 08ebbb21..28f4d8ea 100644
--- a/test/Mathlib/test/20240209.in
+++ b/test/Mathlib/test/20240209.in
@@ -1,3 +1,3 @@
-{"cmd": "example : False := by sorry"}
+{"cmd": "example : False := by sorry", "sorries": "individual"}
 
 {"tactic": "simpa using show False by done", "proofState": 0}
diff --git a/test/Mathlib/test/H20231115.expected.out b/test/Mathlib/test/H20231115.expected.out
index e283b375..4d7cbd6f 100644
--- a/test/Mathlib/test/H20231115.expected.out
+++ b/test/Mathlib/test/H20231115.expected.out
@@ -3,7 +3,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 36},
-   "goal": "x : Nat\n⊢ x + 1 > x",
+   "parentDecl": "_example",
+   "goals": ["x : Nat\n⊢ x + 1 > x"],
    "endPos": {"line": 1, "column": 41}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/Mathlib/test/H20231115.in b/test/Mathlib/test/H20231115.in
index 4bca3cda..d780d278 100644
--- a/test/Mathlib/test/H20231115.in
+++ b/test/Mathlib/test/H20231115.in
@@ -1,5 +1,5 @@
 {"cmd": "import Mathlib.Tactic.Cases"}
 
-{"cmd": "example {x : Nat} : x + 1 > x := by sorry", "env": 0}
+{"cmd": "example {x : Nat} : x + 1 > x := by sorry", "env": 0, "sorries": "individual"}
 
 {"tactic": "induction' x with x hx", "proofState": 0}
diff --git a/test/Mathlib/test/H20231115_2.expected.out b/test/Mathlib/test/H20231115_2.expected.out
index 3c19b57e..4c85f89a 100644
--- a/test/Mathlib/test/H20231115_2.expected.out
+++ b/test/Mathlib/test/H20231115_2.expected.out
@@ -3,11 +3,13 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 3, "column": 12},
-   "goal": "case zero\n⊢ 0 + 1 > 0",
+   "parentDecl": "_example",
+   "goals": ["case zero\n⊢ 0 + 1 > 0"],
    "endPos": {"line": 3, "column": 17}},
   {"proofState": 1,
    "pos": {"line": 3, "column": 12},
-   "goal": "case succ\nx : Nat\nhx : x + 1 > x\n⊢ x + 1 + 1 > x + 1",
+   "parentDecl": "_example",
+   "goals": ["case succ\nx : Nat\nhx : x + 1 > x\n⊢ x + 1 + 1 > x + 1"],
    "endPos": {"line": 3, "column": 17}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/Mathlib/test/H20231115_2.in b/test/Mathlib/test/H20231115_2.in
index bab26d4b..9f6da6c6 100644
--- a/test/Mathlib/test/H20231115_2.in
+++ b/test/Mathlib/test/H20231115_2.in
@@ -1,4 +1,4 @@
 {"cmd": "import Mathlib.Tactic.Cases"}
 
-{"cmd": "example {x : Nat} : x + 1 > x := by\n  induction' x with x hx\n  all_goals sorry", "env": 0}
+{"cmd": "example {x : Nat} : x + 1 > x := by\n  induction' x with x hx\n  all_goals sorry", "env": 0, "sorries": "individual"}
 
diff --git a/test/Mathlib/test/H20231215_2.expected.out b/test/Mathlib/test/H20231215_2.expected.out
index 1a83bcff..408dc2a2 100644
--- a/test/Mathlib/test/H20231215_2.expected.out
+++ b/test/Mathlib/test/H20231215_2.expected.out
@@ -3,7 +3,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 2, "column": 20},
-   "goal": "⊢ 9! % 10 = 0",
+   "parentDecl": "mathd_numbertheory_739",
+   "goals": ["⊢ 9! % 10 = 0"],
    "endPos": {"line": 2, "column": 25}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/Mathlib/test/H20231215_2.in b/test/Mathlib/test/H20231215_2.in
index 72323c8b..cb9f4ff0 100644
--- a/test/Mathlib/test/H20231215_2.in
+++ b/test/Mathlib/test/H20231215_2.in
@@ -1,3 +1,3 @@
 {"unpickleEnvFrom": "test/H20231215.olean"}
 
-{"cmd": "theorem mathd_numbertheory_739 :\n  9! % 10 = 0 := by sorry", "env": 0}
+{"cmd": "theorem mathd_numbertheory_739 :\n  9! % 10 = 0 := by sorry", "env": 0, "sorries": "individual"}
diff --git a/test/Mathlib/test/exact.expected.out b/test/Mathlib/test/exact.expected.out
index 39e77965..6a6793a0 100644
--- a/test/Mathlib/test/exact.expected.out
+++ b/test/Mathlib/test/exact.expected.out
@@ -3,7 +3,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 27},
-   "goal": "⊢ 0 < 1",
+   "parentDecl": "test",
+   "goals": ["⊢ 0 < 1"],
    "endPos": {"line": 1, "column": 32}}],
  "messages":
  [{"severity": "warning",
@@ -24,7 +25,8 @@
 {"sorries":
  [{"proofState": 2,
    "pos": {"line": 1, "column": 27},
-   "goal": "⊢ 3 = 7",
+   "parentDecl": "test",
+   "goals": ["⊢ 3 = 7"],
    "endPos": {"line": 1, "column": 32}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/Mathlib/test/exact.in b/test/Mathlib/test/exact.in
index 72b4c503..3eff4b9e 100644
--- a/test/Mathlib/test/exact.in
+++ b/test/Mathlib/test/exact.in
@@ -1,10 +1,10 @@
 {"cmd": "import Mathlib"}
 
-{"cmd": "theorem test : 0 < 1 := by sorry", "env": 0}
+{"cmd": "theorem test : 0 < 1 := by sorry", "env": 0, "sorries": "individual"}
 
 {"tactic": "exact?", "proofState": 0}
 
-{"cmd": "theorem test : 3 = 7 := by sorry", "env": 0}
+{"cmd": "theorem test : 3 = 7 := by sorry", "env": 0, "sorries": "individual"}
 
 {"tactic": "exact?", "proofState": 2}
 
diff --git a/test/Mathlib/test/induction.expected.out b/test/Mathlib/test/induction.expected.out
index 7f80087a..5e672ee7 100644
--- a/test/Mathlib/test/induction.expected.out
+++ b/test/Mathlib/test/induction.expected.out
@@ -3,7 +3,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 36},
-   "goal": "x : ℕ\n⊢ x = x",
+   "parentDecl": "foo",
+   "goals": ["x : ℕ\n⊢ x = x"],
    "endPos": {"line": 1, "column": 41}}],
  "messages":
  [{"severity": "warning",
@@ -21,10 +22,7 @@
  "proofState": 2,
  "goals": ["case succ\nn✝ : ℕ\na✝ : n✝ = n✝\n⊢ n✝ + 1 = n✝ + 1"]}
 
-{"sorries":
- [{"proofState": 3, "goal": "case zero\n⊢ 0 = 0"},
-  {"proofState": 4, "goal": "case succ\nx : ℕ\na✝ : x = x\n⊢ x + 1 = x + 1"}],
- "proofStatus": "Incomplete: contains sorry",
- "proofState": 5,
- "goals": []}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 3,
+ "goals": ["⊢ 0 = 0", "x : ℕ\na✝ : x = x\n⊢ x + 1 = x + 1"]}
 
diff --git a/test/Mathlib/test/induction.in b/test/Mathlib/test/induction.in
index f739d556..c98728f1 100644
--- a/test/Mathlib/test/induction.in
+++ b/test/Mathlib/test/induction.in
@@ -1,6 +1,6 @@
 {"cmd": "import Mathlib"}
 
-{"env" : 0, "cmd": "theorem foo (x : Nat) : x = x := by sorry"}
+{"env" : 0, "cmd": "theorem foo (x : Nat) : x = x := by sorry", "sorries": "individual"}
 
 {"proofState" : 0, "tactic": "induction x"}
 
diff --git a/test/Mathlib/test/on_goal.expected.out b/test/Mathlib/test/on_goal.expected.out
index 510cfe1b..4221aa86 100644
--- a/test/Mathlib/test/on_goal.expected.out
+++ b/test/Mathlib/test/on_goal.expected.out
@@ -3,7 +3,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 60},
-   "goal": "x : ℝ\nh0 : |x| > 1\n⊢ x < 0 ∨ 2 * x > 2",
+   "parentDecl": "_example",
+   "goals": ["x : ℝ\nh0 : |x| > 1\n⊢ x < 0 ∨ 2 * x > 2"],
    "endPos": {"line": 1, "column": 65}}],
  "messages":
  [{"severity": "warning",
@@ -12,12 +13,11 @@
    "data": "declaration uses 'sorry'"}],
  "env": 1}
 
-{"sorries":
- [{"proofState": 1, "goal": "x : ℝ\nh0 : |x| > 1\n⊢ x = x"},
-  {"proofState": 2, "goal": "x : ℝ\nh0 : |x| > 1\nh1 : x = x\n⊢ x = x"}],
- "proofStatus": "Incomplete: open goals remain",
- "proofState": 3,
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
  "goals":
- ["case pos\nx : ℝ\nh0 : |x| > 1\nh1 h2 : x = x\nh3 : x < 0\n⊢ x < 0 ∨ 2 * x > 2",
+ ["x : ℝ\nh0 : |x| > 1\n⊢ x = x",
+  "x : ℝ\nh0 : |x| > 1\nh1 : x = x\n⊢ x = x",
+  "case pos\nx : ℝ\nh0 : |x| > 1\nh1 h2 : x = x\nh3 : x < 0\n⊢ x < 0 ∨ 2 * x > 2",
   "case neg\nx : ℝ\nh0 : |x| > 1\nh1 h2 : x = x\nh3 : ¬x < 0\n⊢ x < 0 ∨ 2 * x > 2"]}
 
diff --git a/test/Mathlib/test/on_goal.in b/test/Mathlib/test/on_goal.in
index 3fd2baa9..04bfc188 100644
--- a/test/Mathlib/test/on_goal.in
+++ b/test/Mathlib/test/on_goal.in
@@ -1,5 +1,5 @@
 {"cmd": "import Mathlib\nopen Real"}
 
-{"cmd": "example {x : ℝ} (h0: |x| > 1) : (x < 0) ∨ (2 * x > 2) := by sorry", "env": 0}
+{"cmd": "example {x : ℝ} (h0: |x| > 1) : (x < 0) ∨ (2 * x > 2) := by sorry", "env": 0, "sorries": "individual"}
 
 {"tactic": "on_goal 1 =>\n  have h1 : x = x := by sorry\n  have h2 : x = x := by sorry\n  by_cases h3 : x < 0", "proofState": 0}
diff --git a/test/Mathlib/test/pickle.expected.out b/test/Mathlib/test/pickle.expected.out
index e3d1c163..a5ca0d85 100644
--- a/test/Mathlib/test/pickle.expected.out
+++ b/test/Mathlib/test/pickle.expected.out
@@ -3,7 +3,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 4, "column": 14},
-   "goal": "x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3",
+   "parentDecl": "mathd_algebra_455",
+   "goals": ["x : ℕ\nh : 2 * (2 * (2 * (2 * x))) = 48\n⊢ x = 3"],
    "endPos": {"line": 4, "column": 19}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/Mathlib/test/pickle.in b/test/Mathlib/test/pickle.in
index 0951e383..4893d0c4 100644
--- a/test/Mathlib/test/pickle.in
+++ b/test/Mathlib/test/pickle.in
@@ -1,6 +1,6 @@
 {"cmd": "import Mathlib\nopen BigOperators\nopen Real\nopen Nat"}
 
-{"cmd": "theorem mathd_algebra_455\n  (x : Nat)\n  (h : 2 * (2 * (2 * (2 * x))) = 48) :\n  x = 3 := by sorry", "env": 0}
+{"cmd": "theorem mathd_algebra_455\n  (x : Nat)\n  (h : 2 * (2 * (2 * (2 * x))) = 48) :\n  x = 3 := by sorry", "env": 0, "sorries": "individual"}
 
 {"pickleTo": "test/pickle.olean", "proofState": 0}
 
diff --git a/test/Mathlib/test/placeholder_synthesis.expected.out b/test/Mathlib/test/placeholder_synthesis.expected.out
index ad26358f..ccd4c02f 100644
--- a/test/Mathlib/test/placeholder_synthesis.expected.out
+++ b/test/Mathlib/test/placeholder_synthesis.expected.out
@@ -11,7 +11,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 19},
-   "goal": "⊢ 1 = 0",
+   "parentDecl": "_example",
+   "goals": ["⊢ 1 = 0"],
    "endPos": {"line": 1, "column": 24}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/Mathlib/test/placeholder_synthesis.in b/test/Mathlib/test/placeholder_synthesis.in
index 040097d3..c77d4fda 100644
--- a/test/Mathlib/test/placeholder_synthesis.in
+++ b/test/Mathlib/test/placeholder_synthesis.in
@@ -2,7 +2,7 @@
 
 {"cmd": "example : 1 = 0 := by\n  cases' exists_ne 2 with n h\n  simpa [] using h _", "env": 0}
 
-{"cmd": "example : 1 = 0 := sorry", "env": 0}
+{"cmd": "example : 1 = 0 := sorry", "env": 0, "sorries": "individual"}
 
 {"tactic": "cases' exists_ne 2 with n h", "proofState": 0}
 
diff --git a/test/all_tactics-20250622.expected.out b/test/all_tactics-20250622.expected.out
index 3b16cd5b..4124bd0f 100644
--- a/test/all_tactics-20250622.expected.out
+++ b/test/all_tactics-20250622.expected.out
@@ -3,6 +3,7 @@
    "tactic": "exact hp",
    "proofState": 0,
    "pos": {"line": 2, "column": 2},
+   "parentDecl": "_example",
    "goals": "P : Prop\nhp : P\n⊢ P",
    "endPos": {"line": 2, "column": 10}}],
  "env": 0}
diff --git a/test/all_tactics.expected.out b/test/all_tactics.expected.out
index 6a08ee4b..79c2df79 100644
--- a/test/all_tactics.expected.out
+++ b/test/all_tactics.expected.out
@@ -3,12 +3,14 @@
    "tactic": "have t := 37",
    "proofState": 0,
    "pos": {"line": 1, "column": 18},
+   "parentDecl": "f",
    "goals": "⊢ Nat",
    "endPos": {"line": 1, "column": 30}},
   {"usedConstants": [],
    "tactic": "exact t",
    "proofState": 1,
    "pos": {"line": 1, "column": 32},
+   "parentDecl": "f",
    "goals": "t : Nat\n⊢ Nat",
    "endPos": {"line": 1, "column": 39}}],
  "env": 0}
diff --git a/test/app_type_mismatch.expected.out b/test/app_type_mismatch.expected.out
index 317d655e..13a2888c 100644
--- a/test/app_type_mismatch.expected.out
+++ b/test/app_type_mismatch.expected.out
@@ -8,7 +8,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 19},
-   "goal": "⊢ 1 = 0",
+   "parentDecl": "_example",
+   "goals": ["⊢ 1 = 0"],
    "endPos": {"line": 1, "column": 24}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/app_type_mismatch.in b/test/app_type_mismatch.in
index 4fc13b04..eb9ab9ee 100644
--- a/test/app_type_mismatch.in
+++ b/test/app_type_mismatch.in
@@ -1,6 +1,6 @@
 {"cmd": "example : 1 = 0 := by\n  cases 1\n  rfl\n  apply ?succ"}
 
-{"cmd": "example : 1 = 0 := sorry"}
+{"cmd": "example : 1 = 0 := sorry", "sorries": "individual"}
 
 {"tactic": "cases 1", "proofState": 0}
 
diff --git a/test/app_type_mismatch2.expected.out b/test/app_type_mismatch2.expected.out
index 23d93247..63127c71 100644
--- a/test/app_type_mismatch2.expected.out
+++ b/test/app_type_mismatch2.expected.out
@@ -9,7 +9,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 19},
-   "goal": "⊢ 1 = 0",
+   "parentDecl": "_example",
+   "goals": ["⊢ 1 = 0"],
    "endPos": {"line": 1, "column": 24}}],
  "messages":
  [{"severity": "warning",
@@ -31,11 +32,18 @@
  "proofState": 3,
  "goals": []}
 
-{"sorries": [{"proofState": 4, "goal": "n✝ : Nat\n⊢ true = true"}],
- "proofStatus": "Incomplete: open goals remain",
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 4,
+ "goals":
+ ["n✝ : Nat\n⊢ true = true",
+  "case succ\nn✝ : Nat\nthis : true = true\n⊢ n✝ + 1 = 0"]}
+
+{"proofStatus": "Incomplete: open goals remain",
  "proofState": 5,
- "goals": ["case succ\nn✝ : Nat\nthis : true = true\n⊢ n✝ + 1 = 0"]}
+ "goals": ["case succ\nn✝ : Nat\n⊢ true = true"]}
 
-{"message":
- "Lean error:\ntactic 'apply' failed, could not unify the type of `?succ`\n  n✝ + 1 = 0\nwith the goal\n  true = true\nn✝ : Nat\n⊢ true = true"}
+{"proofStatus":
+ "Error: kernel type check failed: (kernel) application type mismatch\n  @Eq.ndrec Nat (n✝ + 1) (fun x => x = 0)\n    (have this := of_decide_eq_true (id (Eq.refl true));\n    of_decide_eq_true (id (Eq.refl true)))\nargument has type\n  true = true\nbut function has type\n  (fun x => x = 0) (n✝ + 1) → ∀ {b : Nat}, n✝ + 1 = b → (fun x => x = 0) b",
+ "proofState": 6,
+ "goals": []}
 
diff --git a/test/app_type_mismatch2.in b/test/app_type_mismatch2.in
index 2e85827b..bf1c1f79 100644
--- a/test/app_type_mismatch2.in
+++ b/test/app_type_mismatch2.in
@@ -1,6 +1,6 @@
 {"cmd": "example : 1 = 0 := by\n  cases 1\n  rfl\n  have: true := by\n    apply ?succ\n    trivial"}
 
-{"cmd": "example : 1 = 0 := sorry"}
+{"cmd": "example : 1 = 0 := sorry", "sorries": "individual"}
 
 {"tactic": "cases 1", "proofState": 0}
 
@@ -12,3 +12,5 @@
 
 {"tactic": "apply ?succ", "proofState": 4}
 
+{"tactic": "trivial", "proofState": 5}
+
diff --git a/test/assumption_proof.expected.out b/test/assumption_proof.expected.out
index 0c253350..01b03e58 100644
--- a/test/assumption_proof.expected.out
+++ b/test/assumption_proof.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 49},
-   "goal": "x : Nat\nh1 : x = 2\n⊢ x = 2",
+   "parentDecl": "aa",
+   "goals": ["x : Nat\nh1 : x = 2\n⊢ x = 2"],
    "endPos": {"line": 1, "column": 54}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/assumption_proof.in b/test/assumption_proof.in
index af5348c4..cd914697 100644
--- a/test/assumption_proof.in
+++ b/test/assumption_proof.in
@@ -1,3 +1,3 @@
-{"cmd": "theorem aa (x : Nat) (h1 : x  = 2) : x = 2 := by sorry"}
+{"cmd": "theorem aa (x : Nat) (h1 : x  = 2) : x = 2 := by sorry", "sorries": "individual"}
 
 {"tactic": "assumption", "proofState": 0}
diff --git a/test/by_cases.expected.out b/test/by_cases.expected.out
index 978df508..7dc6574b 100644
--- a/test/by_cases.expected.out
+++ b/test/by_cases.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 36},
-   "goal": "x : Int\n⊢ x = x",
+   "parentDecl": "foo",
+   "goals": ["x : Int\n⊢ x = x"],
    "endPos": {"line": 1, "column": 41}}],
  "messages":
  [{"severity": "warning",
@@ -20,10 +21,7 @@
  "proofState": 2,
  "goals": ["case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"]}
 
-{"sorries":
- [{"proofState": 3, "goal": "case pos\nx : Int\nh : x < 0\n⊢ x = x"},
-  {"proofState": 4, "goal": "case neg\nx : Int\nh : ¬x < 0\n⊢ x = x"}],
- "proofStatus": "Incomplete: contains sorry",
- "proofState": 5,
- "goals": []}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 3,
+ "goals": ["x : Int\nh : x < 0\n⊢ x = x", "x : Int\nh : ¬x < 0\n⊢ x = x"]}
 
diff --git a/test/by_cases.in b/test/by_cases.in
index 031c43f6..2580c708 100644
--- a/test/by_cases.in
+++ b/test/by_cases.in
@@ -1,4 +1,4 @@
-{"cmd": "theorem foo (x : Int) : x = x := by sorry"}
+{"cmd": "theorem foo (x : Int) : x = x := by sorry", "sorries": "individual"}
 
 {"proofState" : 0, "tactic": "by_cases h : x < 0"}
 
diff --git a/test/calc.expected.out b/test/calc.expected.out
index 8db4c61b..1d896a3d 100644
--- a/test/calc.expected.out
+++ b/test/calc.expected.out
@@ -15,12 +15,14 @@
    "tactic": "calc\n  3 = 4 := by sorry\n  4 = 5 := by sorry",
    "proofState": 2,
    "pos": {"line": 1, "column": 22},
+   "parentDecl": "_example",
    "goals": "⊢ 3 = 5",
    "endPos": {"line": 3, "column": 19}},
   {"usedConstants": [],
    "tactic": "\n  3 = 4 := by sorry\n  4 = 5 := by sorry",
    "proofState": 3,
    "pos": {"line": 2, "column": 2},
+   "parentDecl": "_example",
    "goals": "no goals",
    "endPos": {"line": 3, "column": 19}},
   {"usedConstants":
@@ -37,6 +39,7 @@
    "tactic": "sorry",
    "proofState": 4,
    "pos": {"line": 2, "column": 14},
+   "parentDecl": "_example",
    "goals": "⊢ 3 = 4",
    "endPos": {"line": 2, "column": 19}},
   {"usedConstants":
@@ -53,16 +56,19 @@
    "tactic": "sorry",
    "proofState": 5,
    "pos": {"line": 3, "column": 14},
+   "parentDecl": "_example",
    "goals": "⊢ 4 = 5",
    "endPos": {"line": 3, "column": 19}}],
  "sorries":
  [{"proofState": 0,
    "pos": {"line": 2, "column": 14},
-   "goal": "⊢ 3 = 4",
+   "parentDecl": "_example",
+   "goals": ["⊢ 3 = 4"],
    "endPos": {"line": 2, "column": 19}},
   {"proofState": 1,
    "pos": {"line": 3, "column": 14},
-   "goal": "⊢ 4 = 5",
+   "parentDecl": "_example",
+   "goals": ["⊢ 4 = 5"],
    "endPos": {"line": 3, "column": 19}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/calc.in b/test/calc.in
index 895da449..c268372d 100644
--- a/test/calc.in
+++ b/test/calc.in
@@ -1 +1 @@
-{"cmd": "example : 3 = 5 := by calc\n  3 = 4 := by sorry\n  4 = 5 := by sorry", "allTactics": true }
+{"cmd": "example : 3 = 5 := by calc\n  3 = 4 := by sorry\n  4 = 5 := by sorry", "allTactics": true, "sorries": "individual"}
diff --git a/test/dup_sorries.expected.out b/test/dup_sorries.expected.out
index d01dd9b0..65f30c99 100644
--- a/test/dup_sorries.expected.out
+++ b/test/dup_sorries.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 24},
-   "goal": "⊢ 1 = 1",
+   "parentDecl": "thm1",
+   "goals": ["⊢ 1 = 1"],
    "endPos": {"line": 1, "column": 29}}],
  "messages":
  [{"severity": "warning",
@@ -13,7 +14,8 @@
 {"sorries":
  [{"proofState": 1,
    "pos": {"line": 1, "column": 24},
-   "goal": "⊢ 2 = 2",
+   "parentDecl": "thm2",
+   "goals": ["⊢ 2 = 2"],
    "endPos": {"line": 1, "column": 29}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/dup_sorries.in b/test/dup_sorries.in
index 78c8e1d3..477d52b5 100644
--- a/test/dup_sorries.in
+++ b/test/dup_sorries.in
@@ -1,3 +1,3 @@
-{"cmd": "theorem thm1 : 1 = 1 := sorry"}
+{"cmd": "theorem thm1 : 1 = 1 := sorry", "sorries": "individual"}
 
-{"cmd": "theorem thm2 : 2 = 2 := sorry", "env": 0}
+{"cmd": "theorem thm2 : 2 = 2 := sorry", "sorries": "individual", "env": 0}
diff --git a/test/file.expected.out b/test/file.expected.out
index dcfd7e8d..446a1feb 100644
--- a/test/file.expected.out
+++ b/test/file.expected.out
@@ -4,6 +4,7 @@
    "tactic": "exact rfl",
    "proofState": 0,
    "pos": {"line": 5, "column": 29},
+   "parentDecl": "h",
    "goals": "⊢ f + g = 39",
    "endPos": {"line": 5, "column": 38}}],
  "env": 0}
diff --git a/test/file2.expected.out b/test/file2.expected.out
index 0fe4f6e7..fdda1d31 100644
--- a/test/file2.expected.out
+++ b/test/file2.expected.out
@@ -17,6 +17,7 @@
    "tactic": "rw [Nat.add_assoc, Nat.add_comm y, h1]",
    "proofState": 0,
    "pos": {"line": 7, "column": 2},
+   "parentDecl": "h",
    "goals": "x y z : Nat\n⊢ x + y + (z + a) = x + (z + b + y)",
    "endPos": {"line": 7, "column": 40}}],
  "env": 0}
diff --git a/test/goal_branching.expected.out b/test/goal_branching.expected.out
new file mode 100644
index 00000000..9d6de033
--- /dev/null
+++ b/test/goal_branching.expected.out
@@ -0,0 +1,31 @@
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 53},
+   "parentDecl": "branching_test",
+   "goals": ["⊢ 1 = 1 ∧ 2 = 2 ∧ 3 = 3"],
+   "endPos": {"line": 1, "column": 58}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 22},
+   "data": "declaration uses 'sorry'"}],
+ "env": 0}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
+ "goals": ["case left\n⊢ 1 = 1", "case right\n⊢ 2 = 2 ∧ 3 = 3"]}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 2,
+ "goals": ["case right\n⊢ 2 = 2 ∧ 3 = 3"]}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 3,
+ "goals": ["case right.left\n⊢ 2 = 2", "case right.right\n⊢ 3 = 3"]}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 4,
+ "goals": ["case right.right\n⊢ 3 = 3"]}
+
+{"proofStatus": "Completed", "proofState": 5, "goals": []}
+
diff --git a/test/goal_branching.in b/test/goal_branching.in
new file mode 100644
index 00000000..aec374aa
--- /dev/null
+++ b/test/goal_branching.in
@@ -0,0 +1,11 @@
+{"cmd" : "theorem branching_test : 1 = 1 ∧ 2 = 2 ∧ 3 = 3 := by sorry", "sorries" : "individual"}
+
+{"tactic": "constructor", "proofState": 0}
+
+{"tactic": "exact rfl", "proofState": 1}
+
+{"tactic": "constructor", "proofState": 2}
+
+{"tactic": "exact rfl", "proofState": 3}
+
+{"tactic": "exact rfl", "proofState": 4}
diff --git a/test/have_by_sorry.expected.out b/test/have_by_sorry.expected.out
index 03c79017..33129473 100644
--- a/test/have_by_sorry.expected.out
+++ b/test/have_by_sorry.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 2, "column": 23},
-   "goal": "x : Int\n⊢ x = 1",
+   "parentDecl": "foo",
+   "goals": ["x : Int\n⊢ x = 1"],
    "endPos": {"line": 2, "column": 28}}],
  "messages":
  [{"severity": "error",
@@ -13,7 +14,8 @@
 {"sorries":
  [{"proofState": 1,
    "pos": {"line": 1, "column": 36},
-   "goal": "x : Int\n⊢ x = x",
+   "parentDecl": "foo",
+   "goals": ["x : Int\n⊢ x = x"],
    "endPos": {"line": 1, "column": 41}}],
  "messages":
  [{"severity": "warning",
@@ -22,8 +24,7 @@
    "data": "declaration uses 'sorry'"}],
  "env": 1}
 
-{"sorries": [{"proofState": 2, "goal": "x : Int\n⊢ x = 1"}],
- "proofStatus": "Incomplete: open goals remain",
- "proofState": 3,
- "goals": ["x : Int\nh : x = 1\n⊢ x = 1"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 2,
+ "goals": ["x : Int\n⊢ x = 1", "x : Int\nh : x = 1\n⊢ x = 1"]}
 
diff --git a/test/have_by_sorry.in b/test/have_by_sorry.in
index adb2b520..af6f7c10 100644
--- a/test/have_by_sorry.in
+++ b/test/have_by_sorry.in
@@ -1,6 +1,6 @@
-{"cmd": "theorem foo (x : Int) : x = x := by\n  have h : x = 1 := by sorry"}
+{"cmd": "theorem foo (x : Int) : x = x := by\n  have h : x = 1 := by sorry", "sorries": "individual"}
 
-{"cmd": "theorem foo (x : Int) : x = x := by sorry"}
+{"cmd": "theorem foo (x : Int) : x = x := by sorry", "sorries": "individual"}
 
-{"proofState" : 0, "tactic": "have h : x = 1 := by sorry"}
+{"proofState" : 0, "tactic": "have h : x = 1 := by sorry", "sorries": "individual"}
 
diff --git a/test/invalid_tactic.expected.out b/test/invalid_tactic.expected.out
index 3ba2c50f..ee390307 100644
--- a/test/invalid_tactic.expected.out
+++ b/test/invalid_tactic.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 43},
-   "goal": "x : Nat\n⊢ x = x",
+   "parentDecl": "my_theorem",
+   "goals": ["x : Nat\n⊢ x = x"],
    "endPos": {"line": 1, "column": 48}}],
  "messages":
  [{"severity": "warning",
@@ -10,12 +11,12 @@
    "data": "declaration uses 'sorry'"}],
  "env": 0}
 
-{"proofStatus": "Incomplete: contains sorry",
+{"proofStatus": "Incomplete: open goals remain",
  "proofState": 1,
  "messages":
  [{"severity": "error",
    "pos": {"line": 0, "column": 0},
    "endPos": {"line": 0, "column": 0},
    "data": "unknown identifier 'my_fake_premise'"}],
- "goals": []}
+ "goals": ["x : Nat\n⊢ x = x"]}
 
diff --git a/test/invalid_tactic.in b/test/invalid_tactic.in
index df92192c..64887fd9 100644
--- a/test/invalid_tactic.in
+++ b/test/invalid_tactic.in
@@ -1,3 +1,3 @@
-{"cmd": "theorem my_theorem (x : Nat) : x = x := by sorry"}
+{"cmd": "theorem my_theorem (x : Nat) : x = x := by sorry", "sorries": "individual"}
 
 {"tactic": "exact my_fake_premise", "proofState": 0}
diff --git a/test/line_breaks.expected.out b/test/line_breaks.expected.out
index d6e980af..24b76f61 100644
--- a/test/line_breaks.expected.out
+++ b/test/line_breaks.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 2, "column": 0},
-   "goal": "⊢ 1 = 1",
+   "parentDecl": "foo",
+   "goals": ["⊢ 1 = 1"],
    "endPos": {"line": 2, "column": 5}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/line_breaks.in b/test/line_breaks.in
index 6ac457a1..7e6a776f 100644
--- a/test/line_breaks.in
+++ b/test/line_breaks.in
@@ -1,5 +1,5 @@
 {"cmd": "theorem foo : 1 = 1 := by\n
-sorry"}
+sorry", "sorries": "individual"}
 
 {"cmd": "theorem bar : 1 = 1 := by\n
 /- Some long comment here -/\n
diff --git a/test/name_generator.expected.out b/test/name_generator.expected.out
index 987d0593..34483e57 100644
--- a/test/name_generator.expected.out
+++ b/test/name_generator.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 2, "column": 45},
-   "goal": "x : Int\nh0 : x > 0\n⊢ False",
+   "parentDecl": "_example",
+   "goals": ["x : Int\nh0 : x > 0\n⊢ False"],
    "endPos": {"line": 2, "column": 50}}],
  "messages":
  [{"severity": "warning",
@@ -10,54 +11,59 @@
    "data": "declaration uses 'sorry'"}],
  "env": 0}
 
-{"sorries": [{"proofState": 1, "goal": "x : Int\nh0 : x > 0\n⊢ x > 0"}],
- "proofStatus": "Incomplete: open goals remain",
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
+ "goals": ["x : Int\nh0 : x > 0\n⊢ x > 0", "x : Int\nh0 h : x > 0\n⊢ False"]}
+
+{"proofStatus": "Incomplete: open goals remain",
  "proofState": 2,
  "goals": ["x : Int\nh0 h : x > 0\n⊢ False"]}
 
-{"proofStatus": "Incomplete: contains metavariable(s)",
+{"proofStatus": "Incomplete: open goals remain",
  "proofState": 3,
- "goals": []}
-
-{"proofStatus": "Incomplete: contains metavariable(s)",
- "proofState": 4,
- "goals": []}
+ "goals": ["x : Int\nh0 h : x > 0\n⊢ False"]}
 
 {"traces":
  ["[Meta.Tactic.simp.rewrite] of_eq_true (eq_true h0):1000:\n      x > 0\n    ==>\n      True"],
- "proofStatus": "Incomplete: contains metavariable(s)",
- "proofState": 5,
- "goals": []}
+ "proofStatus": "Incomplete: open goals remain",
+ "proofState": 4,
+ "goals": ["x : Int\nh0 h : x > 0\n⊢ False"]}
 
 {"traces":
  ["[Meta.Tactic.simp.rewrite] gt_iff_lt:1000:\n      x > 0\n    ==>\n      0 < x",
   "[Meta.Tactic.simp.rewrite] h0:1000:\n      0 < x\n    ==>\n      True"],
- "proofStatus": "Incomplete: contains metavariable(s)",
- "proofState": 6,
- "goals": []}
+ "proofStatus": "Incomplete: open goals remain",
+ "proofState": 5,
+ "goals": ["x : Int\nh0 h : x > 0\n⊢ False"]}
 
 {"traces":
  ["[Meta.Tactic.simp.rewrite] gt_iff_lt:1000:\n      x > 0\n    ==>\n      0 < x",
   "[Meta.Tactic.simp.rewrite] h0:1000:\n      0 < x\n    ==>\n      True"],
- "proofStatus": "Incomplete: contains metavariable(s)",
- "proofState": 7,
- "goals": []}
+ "proofStatus": "Incomplete: open goals remain",
+ "proofState": 6,
+ "goals": ["x : Int\nh0 h : x > 0\n⊢ False"]}
 
-{"proofStatus": "Incomplete: contains metavariable(s)",
- "proofState": 8,
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 7,
  "messages":
  [{"severity": "error",
    "pos": {"line": 0, "column": 0},
    "endPos": {"line": 0, "column": 0},
    "data": "unsolved goals\nx : Int\nh0 : x > 0\n⊢ x > 0"}],
- "goals": []}
+ "goals":
+ ["x : Int\nh0 : x > 0\n⊢ x > 0",
+  "x : Int\nh0 : x > 0\n⊢ x > 0",
+  "x : Int\nh0 h : x > 0\n⊢ False"]}
 
-{"proofStatus": "Incomplete: contains metavariable(s)",
- "proofState": 9,
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 8,
  "messages":
  [{"severity": "error",
    "pos": {"line": 0, "column": 0},
    "endPos": {"line": 0, "column": 0},
    "data": "unsolved goals\nx : Int\nh0 : x > 0\n⊢ x > 0"}],
- "goals": []}
+ "goals":
+ ["x : Int\nh0 : x > 0\n⊢ x > 0",
+  "x : Int\nh0 : x > 0\n⊢ x > 0",
+  "x : Int\nh0 h : x > 0\n⊢ False"]}
 
diff --git a/test/name_generator.in b/test/name_generator.in
index 232c37da..4fe6a58d 100644
--- a/test/name_generator.in
+++ b/test/name_generator.in
@@ -1,4 +1,4 @@
-{"cmd": "set_option trace.Meta.Tactic.simp true\nexample {x : Int} (h0 : x > 0) : False := by sorry"}
+{"cmd": "set_option trace.Meta.Tactic.simp true\nexample {x : Int} (h0 : x > 0) : False := by sorry", "sorries": "individual"}
 
 {"tactic": "have h : x > 0 := by sorry", "proofState": 0}
 
diff --git a/test/no_goal_sorry_2.expected.out b/test/no_goal_sorry_2.expected.out
index 31e74936..f509f934 100644
--- a/test/no_goal_sorry_2.expected.out
+++ b/test/no_goal_sorry_2.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 2, "column": 2},
-   "goal": "⊢ True",
+   "parentDecl": "_example",
+   "goals": ["⊢ True"],
    "endPos": {"line": 2, "column": 7}}],
  "messages":
  [{"severity": "error",
diff --git a/test/no_goal_sorry_2.in b/test/no_goal_sorry_2.in
index 07211903..5d3be350 100644
--- a/test/no_goal_sorry_2.in
+++ b/test/no_goal_sorry_2.in
@@ -1 +1 @@
-{"cmd" : "example : True := by\n  sorry\n  sorry"}
+{"cmd" : "example : True := by\n  sorry\n  sorry", "sorries": "individual"}
diff --git a/test/pickle_open_scoped.expected.out b/test/pickle_open_scoped.expected.out
index df23507a..c6f22edd 100644
--- a/test/pickle_open_scoped.expected.out
+++ b/test/pickle_open_scoped.expected.out
@@ -5,7 +5,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 22},
-   "goal": "⊢ ◾",
+   "parentDecl": "_example",
+   "goals": ["⊢ ◾"],
    "endPos": {"line": 1, "column": 27}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/pickle_open_scoped.in b/test/pickle_open_scoped.in
index dafcbc65..e13fb5e8 100644
--- a/test/pickle_open_scoped.in
+++ b/test/pickle_open_scoped.in
@@ -2,7 +2,7 @@
 
 {"cmd": "open Lean.Compiler", "env": 0}
 
-{"cmd": "unsafe example : ◾ := sorry", "env": 1}
+{"cmd": "unsafe example : ◾ := sorry", "env": 1, "sorries": "individual"}
 
 {"pickleTo": "test/f.olean", "env": 1}
 
diff --git a/test/pickle_open_scoped_2.expected.out b/test/pickle_open_scoped_2.expected.out
index f21692d2..9aee3bd1 100644
--- a/test/pickle_open_scoped_2.expected.out
+++ b/test/pickle_open_scoped_2.expected.out
@@ -3,7 +3,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 22},
-   "goal": "⊢ ◾",
+   "parentDecl": "_example",
+   "goals": ["⊢ ◾"],
    "endPos": {"line": 1, "column": 27}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/pickle_open_scoped_2.in b/test/pickle_open_scoped_2.in
index 6b587fc0..8177a8b4 100644
--- a/test/pickle_open_scoped_2.in
+++ b/test/pickle_open_scoped_2.in
@@ -1,3 +1,3 @@
 {"unpickleEnvFrom": "test/f.olean"}
 
-{"cmd": "unsafe example : ◾ := sorry", "env": 0}
+{"cmd": "unsafe example : ◾ := sorry", "env": 0, "sorries": "individual"}
diff --git a/test/pickle_proof_state_1.expected.out b/test/pickle_proof_state_1.expected.out
index 238b74c9..e902b67d 100644
--- a/test/pickle_proof_state_1.expected.out
+++ b/test/pickle_proof_state_1.expected.out
@@ -3,7 +3,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 18},
-   "goal": "⊢ Nat",
+   "parentDecl": "f",
+   "goals": ["⊢ Nat"],
    "endPos": {"line": 1, "column": 23}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/pickle_proof_state_1.in b/test/pickle_proof_state_1.in
index 1b1afdf5..0ea70a0d 100644
--- a/test/pickle_proof_state_1.in
+++ b/test/pickle_proof_state_1.in
@@ -1,6 +1,6 @@
 {"cmd" : "import Lean"}
 
-{"cmd" : "def f : Nat := by sorry", "env": 0}
+{"cmd" : "def f : Nat := by sorry", "env": 0, "sorries": "individual"}
 
 {"pickleTo": "test/c.olean", "proofState": 0}
 
diff --git a/test/pickle_proof_state_env.expected.out b/test/pickle_proof_state_env.expected.out
index 238b74c9..e902b67d 100644
--- a/test/pickle_proof_state_env.expected.out
+++ b/test/pickle_proof_state_env.expected.out
@@ -3,7 +3,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 18},
-   "goal": "⊢ Nat",
+   "parentDecl": "f",
+   "goals": ["⊢ Nat"],
    "endPos": {"line": 1, "column": 23}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/pickle_proof_state_env.in b/test/pickle_proof_state_env.in
index fdd99f75..292d9b1d 100644
--- a/test/pickle_proof_state_env.in
+++ b/test/pickle_proof_state_env.in
@@ -1,6 +1,6 @@
 {"cmd" : "import Lean"}
 
-{"cmd" : "def f : Nat := by sorry", "env": 0}
+{"cmd" : "def f : Nat := by sorry", "env": 0, "sorries": "individual"}
 
 {"pickleTo": "test/c.olean", "proofState": 0}
 
diff --git a/test/proof_branching.expected.out b/test/proof_branching.expected.out
index bfea811d..2218e577 100644
--- a/test/proof_branching.expected.out
+++ b/test/proof_branching.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 75},
-   "goal": "p q r : Prop\nh1 : p ∧ q\nh2 : q → r\n⊢ p ∧ r",
+   "parentDecl": "complex_and",
+   "goals": ["p q r : Prop\nh1 : p ∧ q\nh2 : q → r\n⊢ p ∧ r"],
    "endPos": {"line": 1, "column": 80}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/proof_branching.in b/test/proof_branching.in
index 0c32a386..04549ae4 100644
--- a/test/proof_branching.in
+++ b/test/proof_branching.in
@@ -1,4 +1,4 @@
-{"cmd": "theorem complex_and (p q r : Prop) (h1 : p ∧ q) (h2 : q → r) : p ∧ r := by sorry"}
+{"cmd": "theorem complex_and (p q r : Prop) (h1 : p ∧ q) (h2 : q → r) : p ∧ r := by sorry", "sorries": "individual"}
 
 {"tactic": "apply And.intro", "proofState": 0}
 
diff --git a/test/proof_branching2.expected.out b/test/proof_branching2.expected.out
index 1bcd8e1e..01d5e055 100644
--- a/test/proof_branching2.expected.out
+++ b/test/proof_branching2.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 43},
-   "goal": "p q : Prop\n⊢ p ∧ q → q ∧ p",
+   "parentDecl": "_example",
+   "goals": ["p q : Prop\n⊢ p ∧ q → q ∧ p"],
    "endPos": {"line": 1, "column": 48}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/proof_branching2.in b/test/proof_branching2.in
index 0b25f70e..35ad189d 100644
--- a/test/proof_branching2.in
+++ b/test/proof_branching2.in
@@ -1,4 +1,4 @@
-{"cmd": "example (p q : Prop) : p ∧ q → q ∧ p := by sorry"}
+{"cmd": "example (p q : Prop) : p ∧ q → q ∧ p := by sorry", "sorries": "individual"}
 
 {"tactic": "intro h", "proofState": 0}
 
diff --git a/test/proof_step.expected.out b/test/proof_step.expected.out
index 013889b6..628df81b 100644
--- a/test/proof_step.expected.out
+++ b/test/proof_step.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 18},
-   "goal": "⊢ Nat",
+   "parentDecl": "f",
+   "goals": ["⊢ Nat"],
    "endPos": {"line": 1, "column": 23}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/proof_step.in b/test/proof_step.in
index a0b5d533..a1393bd0 100644
--- a/test/proof_step.in
+++ b/test/proof_step.in
@@ -1,4 +1,4 @@
-{"cmd" : "def f : Nat := by sorry"}
+{"cmd" : "def f : Nat := by sorry", "sorries" : "individual"}
 
 {"tactic": "apply Int.natAbs", "proofState": 0}
 
diff --git a/test/proof_transitivity.expected.out b/test/proof_transitivity.expected.out
index 45f4b082..cb113dfb 100644
--- a/test/proof_transitivity.expected.out
+++ b/test/proof_transitivity.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 62},
-   "goal": "x y z : Nat\nh1 : x = y\nh2 : y = z\n⊢ x = z",
+   "parentDecl": "_example",
+   "goals": ["x y z : Nat\nh1 : x = y\nh2 : y = z\n⊢ x = z"],
    "endPos": {"line": 1, "column": 67}}],
  "messages":
  [{"severity": "warning",
@@ -15,7 +16,8 @@
 {"sorries":
  [{"proofState": 2,
    "pos": {"line": 1, "column": 64},
-   "goal": "f : Nat → Nat\nn : Nat\nh : n = 3\n⊢ f n = f 3",
+   "parentDecl": "_example",
+   "goals": ["f : Nat → Nat\nn : Nat\nh : n = 3\n⊢ f n = f 3"],
    "endPos": {"line": 1, "column": 69}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/proof_transitivity.in b/test/proof_transitivity.in
index 9245305c..aca370f0 100644
--- a/test/proof_transitivity.in
+++ b/test/proof_transitivity.in
@@ -1,8 +1,8 @@
-{"cmd": "example (x y z : Nat) (h1 : x = y) (h2 : y = z) : x = z := by sorry"}
+{"cmd": "example (x y z : Nat) (h1 : x = y) (h2 : y = z) : x = z := by sorry", "sorries": "individual"}
 
 {"tactic": "exact Eq.trans h1 h2", "proofState": 0}
 
-{"cmd": "example (f : Nat → Nat) (n : Nat) (h : n = 3) : f n = f 3 := by sorry"}
+{"cmd": "example (f : Nat → Nat) (n : Nat) (h : n = 3) : f n = f 3 := by sorry", "sorries": "individual"}
 
 {"tactic": "exact congrArg f h", "proofState": 2}
 
diff --git a/test/readme.expected.out b/test/readme.expected.out
index 7ffa1109..a6e854a0 100644
--- a/test/readme.expected.out
+++ b/test/readme.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 29},
-   "goal": "x : Unit\n⊢ Nat",
+   "parentDecl": "f",
+   "goals": ["x : Unit\n⊢ Nat"],
    "endPos": {"line": 1, "column": 34}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/readme.in b/test/readme.in
index a13635c9..2116ad7e 100644
--- a/test/readme.in
+++ b/test/readme.in
@@ -1,4 +1,4 @@
-{"cmd" : "def f (x : Unit) : Nat := by sorry"}
+{"cmd" : "def f (x : Unit) : Nat := by sorry", "sorries" : "individual"}
 
 {"tactic": "apply Int.natAbs", "proofState": 0}
 
diff --git a/test/root_goals.expected.out b/test/root_goals.expected.out
index 053aeeac..533106fe 100644
--- a/test/root_goals.expected.out
+++ b/test/root_goals.expected.out
@@ -1,12 +1,12 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 17},
-   "goal": "⊢ 1 = 1",
-   "endPos": {"line": 1, "column": 17}},
+   "parentDecl": "_example",
+   "goals": ["⊢ 1 = 1"]},
   {"proofState": 1,
    "pos": {"line": 5, "column": 22},
-   "goal": "⊢ 1 + 1 = 2",
-   "endPos": {"line": 5, "column": 22}}],
+   "parentDecl": "bb",
+   "goals": ["⊢ 1 + 1 = 2"]}],
  "messages":
  [{"severity": "info",
    "pos": {"line": 3, "column": 2},
diff --git a/test/root_goals.in b/test/root_goals.in
index 487ad72a..d5392ae8 100644
--- a/test/root_goals.in
+++ b/test/root_goals.in
@@ -1,4 +1,4 @@
-{"cmd": "example : 1=1 := by\n  skip\n  exact?\n\ntheorem bb : 1+1=2 := by rfl", "rootGoals": true}
+{"cmd": "example : 1=1 := by\n  skip\n  exact?\n\ntheorem bb : 1+1=2 := by rfl", "sorries": "rootGoals"}
 
 {"proofState" : 0, "tactic": "rfl"}
 
diff --git a/test/self_proof_apply_check.expected.out b/test/self_proof_apply_check.expected.out
index ba526f4f..f7cf74f6 100644
--- a/test/self_proof_apply_check.expected.out
+++ b/test/self_proof_apply_check.expected.out
@@ -9,7 +9,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 22},
-   "goal": "⊢ False",
+   "parentDecl": "ex",
+   "goals": ["⊢ False"],
    "endPos": {"line": 1, "column": 27}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/self_proof_apply_check.in b/test/self_proof_apply_check.in
index f01ccc4c..0e680a23 100644
--- a/test/self_proof_apply_check.in
+++ b/test/self_proof_apply_check.in
@@ -1,5 +1,5 @@
 {"cmd": "theorem ex : False := by apply ex"}
 
-{"cmd": "theorem ex : False := sorry"}
+{"cmd": "theorem ex : False := sorry", "sorries": "individual"}
 
 {"proofState": 0, "tactic": "apply ex"}
diff --git a/test/self_proof_check.expected.out b/test/self_proof_check.expected.out
index 48253d70..8af7cd48 100644
--- a/test/self_proof_check.expected.out
+++ b/test/self_proof_check.expected.out
@@ -9,7 +9,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 22},
-   "goal": "⊢ False",
+   "parentDecl": "ex",
+   "goals": ["⊢ False"],
    "endPos": {"line": 1, "column": 27}}],
  "messages":
  [{"severity": "warning",
@@ -24,7 +25,8 @@
 {"sorries":
  [{"proofState": 1,
    "pos": {"line": 1, "column": 25},
-   "goal": "⊢ False",
+   "parentDecl": "ex",
+   "goals": ["⊢ False"],
    "endPos": {"line": 1, "column": 30}}],
  "messages":
  [{"severity": "warning",
@@ -51,12 +53,14 @@
    "tactic": "sorry",
    "proofState": 3,
    "pos": {"line": 1, "column": 25},
+   "parentDecl": "ex",
    "goals": "⊢ False",
    "endPos": {"line": 1, "column": 30}}],
  "sorries":
  [{"proofState": 2,
    "pos": {"line": 1, "column": 25},
-   "goal": "⊢ False",
+   "parentDecl": "ex",
+   "goals": ["⊢ False"],
    "endPos": {"line": 1, "column": 30}}],
  "messages":
  [{"severity": "warning",
@@ -70,13 +74,9 @@
 
 {"sorries":
  [{"proofState": 4,
-   "pos": {"line": 1, "column": 25},
-   "goal": "⊢ False",
-   "endPos": {"line": 1, "column": 30}},
-  {"proofState": 5,
    "pos": {"line": 1, "column": 22},
-   "goal": "⊢ False",
-   "endPos": {"line": 1, "column": 22}}],
+   "parentDecl": "ex",
+   "goals": ["⊢ False"]}],
  "messages":
  [{"severity": "warning",
    "pos": {"line": 1, "column": 8},
diff --git a/test/self_proof_check.in b/test/self_proof_check.in
index 216d80f6..bd521adf 100644
--- a/test/self_proof_check.in
+++ b/test/self_proof_check.in
@@ -1,18 +1,18 @@
 {"cmd": "theorem ex : False := by exact?"}
 
-{"cmd": "theorem ex : False := sorry"}
+{"cmd": "theorem ex : False := sorry", "sorries": "individual"}
 
 {"proofState": 0, "tactic": "exact?"}
 
-{"cmd": "theorem ex : False := by sorry"}
+{"cmd": "theorem ex : False := by sorry", "sorries": "individual"}
 
 {"proofState": 1, "tactic": "exact?"}
 
-{"cmd": "theorem ex : False := by sorry", "allTactics": true}
+{"cmd": "theorem ex : False := by sorry", "allTactics": true, "sorries": "individual"}
 
 {"proofState": 3, "tactic": "exact?"}
 
-{"cmd": "theorem ex : False := by sorry", "rootGoals": true}
+{"cmd": "theorem ex : False := by sorry", "sorries": "rootGoals"}
 
-{"proofState": 5, "tactic": "exact?"}
+{"proofState": 4, "tactic": "exact?"}
 
diff --git a/test/self_proof_exact_check.expected.out b/test/self_proof_exact_check.expected.out
index ba526f4f..f7cf74f6 100644
--- a/test/self_proof_exact_check.expected.out
+++ b/test/self_proof_exact_check.expected.out
@@ -9,7 +9,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 22},
-   "goal": "⊢ False",
+   "parentDecl": "ex",
+   "goals": ["⊢ False"],
    "endPos": {"line": 1, "column": 27}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/self_proof_exact_check.in b/test/self_proof_exact_check.in
index aa1dac4c..8e1acfea 100644
--- a/test/self_proof_exact_check.in
+++ b/test/self_proof_exact_check.in
@@ -1,5 +1,5 @@
 {"cmd": "theorem ex : False := by exact ex"}
 
-{"cmd": "theorem ex : False := sorry"}
+{"cmd": "theorem ex : False := sorry", "sorries": "individual"}
 
 {"proofState": 0, "tactic": "exact ex"}
diff --git a/test/self_proof_rw.expected.out b/test/self_proof_rw.expected.out
index f424072d..9cfb3d41 100644
--- a/test/self_proof_rw.expected.out
+++ b/test/self_proof_rw.expected.out
@@ -9,7 +9,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 39},
-   "goal": "⊢ 1 = 0",
+   "parentDecl": "self_application",
+   "goals": ["⊢ 1 = 0"],
    "endPos": {"line": 1, "column": 44}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/self_proof_rw.in b/test/self_proof_rw.in
index 945894ef..2a7eb5d9 100644
--- a/test/self_proof_rw.in
+++ b/test/self_proof_rw.in
@@ -1,5 +1,5 @@
 {"cmd": "theorem self_application : 1 = 0 := by rw [self_application]"}
 
-{"cmd": "theorem self_application : 1 = 0 := by sorry"}
+{"cmd": "theorem self_application : 1 = 0 := by sorry", "sorries": "individual"}
 
 {"proofState": 0, "tactic": "rw [self_application]"}
diff --git a/test/sketch_file.expected.out b/test/sketch_file.expected.out
new file mode 100644
index 00000000..12aa7732
--- /dev/null
+++ b/test/sketch_file.expected.out
@@ -0,0 +1,47 @@
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 70},
+   "parentDecl": "add_comm_proved_formal_sketch",
+   "goals":
+   ["m : Nat\nh_base : 0 + m = m\n⊢ m + 0 = m",
+    "m : Nat\nh_base : 0 + m = m\nh_symm : m + 0 = m\n⊢ 0 + m = m + 0",
+    "m n : Nat\nih : n + m = m + n\n⊢ n + 1 + m = m + (n + 1)",
+    "m : Nat\n⊢ 0 + m = m"],
+   "endPos": {"line": 8, "column": 24}},
+  {"proofState": 1,
+   "pos": {"line": 11, "column": 49},
+   "parentDecl": "add_rfl2",
+   "goals": ["⊢ ∀ (n m : Nat), n + m = n + m"],
+   "endPos": {"line": 11, "column": 57}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 37},
+   "data": "declaration uses 'sorry'"},
+  {"severity": "warning",
+   "pos": {"line": 11, "column": 8},
+   "endPos": {"line": 11, "column": 16},
+   "data": "declaration uses 'sorry'"}],
+ "env": 0}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 2,
+ "goals":
+ ["m : Nat\nh_base : 0 + m = m\nh_symm : m + 0 = m\n⊢ 0 + m = m + 0",
+  "m n : Nat\nih : n + m = m + n\n⊢ n + 1 + m = m + (n + 1)",
+  "m : Nat\n⊢ 0 + m = m"]}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 3,
+ "goals":
+ ["m n : Nat\nih : n + m = m + n\n⊢ n + 1 + m = m + (n + 1)",
+  "m : Nat\n⊢ 0 + m = m"]}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 4,
+ "goals": ["m : Nat\n⊢ 0 + m = m"]}
+
+{"proofStatus": "Completed", "proofState": 5, "goals": []}
+
+{"proofStatus": "Completed", "proofState": 6, "goals": []}
+
diff --git a/test/sketch_file.in b/test/sketch_file.in
new file mode 100644
index 00000000..d8010b96
--- /dev/null
+++ b/test/sketch_file.in
@@ -0,0 +1,11 @@
+{"path": "test/sketch_file.lean", "sorries": "grouped"}
+
+{"tactic": "apply Nat.add_zero", "proofState": 0}
+
+{"tactic": "rw [h_base, h_symm]", "proofState": 2}
+
+{"tactic": "rw [Nat.succ_add, Nat.add_succ, ih]", "proofState": 3}
+
+{"tactic": "apply Nat.zero_add", "proofState": 4}
+
+{"tactic": "(\nintros; rfl)", "proofState": 1}
diff --git a/test/sketch_file.lean b/test/sketch_file.lean
new file mode 100644
index 00000000..2301763b
--- /dev/null
+++ b/test/sketch_file.lean
@@ -0,0 +1,11 @@
+theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := by
+  intros n m
+  induction n with
+    | zero =>
+      have h_base: 0 + m = m := sorry
+      have h_symm: m + 0 = m := sorry
+      sorry
+    | succ n ih => sorry
+
+theorem add_rfl : ∀ n m : Nat, n + m = n + m := by intros; rfl
+theorem add_rfl2 : ∀ n m : Nat, n + m = n + m := by sorry
diff --git a/test/sketch_tactic.expected.out b/test/sketch_tactic.expected.out
new file mode 100644
index 00000000..db2cc091
--- /dev/null
+++ b/test/sketch_tactic.expected.out
@@ -0,0 +1,40 @@
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 70},
+   "parentDecl": "add_comm_proved_formal_sketch",
+   "goals": ["⊢ ∀ (n m : Nat), n + m = m + n"],
+   "endPos": {"line": 1, "column": 75}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 8},
+   "endPos": {"line": 1, "column": 37},
+   "data": "declaration uses 'sorry'"}],
+ "env": 0}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
+ "goals":
+ ["m n : Nat\nih : n + m = m + n\n⊢ n + 1 + m = m + (n + 1)",
+  "m : Nat\n⊢ 0 + m = m",
+  "m : Nat\nh_base : 0 + m = m\n⊢ m + 0 = m",
+  "m : Nat\nh_base : 0 + m = m\nh_symm : m + 0 = m\n⊢ 0 + m = m + 0"]}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 2,
+ "goals":
+ ["m : Nat\n⊢ 0 + m = m",
+  "m : Nat\nh_base : 0 + m = m\n⊢ m + 0 = m",
+  "m : Nat\nh_base : 0 + m = m\nh_symm : m + 0 = m\n⊢ 0 + m = m + 0"]}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 3,
+ "goals":
+ ["m : Nat\nh_base : 0 + m = m\n⊢ m + 0 = m",
+  "m : Nat\nh_base : 0 + m = m\nh_symm : m + 0 = m\n⊢ 0 + m = m + 0"]}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 4,
+ "goals": ["m : Nat\nh_base : 0 + m = m\nh_symm : m + 0 = m\n⊢ 0 + m = m + 0"]}
+
+{"proofStatus": "Completed", "proofState": 5, "goals": []}
+
diff --git a/test/sketch_tactic.in b/test/sketch_tactic.in
new file mode 100644
index 00000000..b789c451
--- /dev/null
+++ b/test/sketch_tactic.in
@@ -0,0 +1,11 @@
+{"cmd": "theorem add_comm_proved_formal_sketch : ∀ n m : Nat, n + m = m + n := sorry", "sorries": "individual"}
+
+{"tactic": "(\n   intros n m\n   induction n with\n   | zero =>\n     have h_base: 0 + m = m := sorry\n     have h_symm: m + 0 = m := sorry\n     sorry\n   | succ n ih => sorry)", "proofState": 0}
+
+{"tactic": "rw [Nat.succ_add, Nat.add_succ, ih]", "proofState": 1}
+
+{"tactic": "apply Nat.zero_add", "proofState": 2}
+
+{"tactic": "apply Nat.add_zero", "proofState": 3}
+
+{"tactic": "rw [h_base, h_symm]", "proofState": 4}
diff --git a/test/sorry_hypotheses.expected.out b/test/sorry_hypotheses.expected.out
index d59e9b1e..96546942 100644
--- a/test/sorry_hypotheses.expected.out
+++ b/test/sorry_hypotheses.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 36},
-   "goal": "x : Int\n⊢ x = x",
+   "parentDecl": "foo",
+   "goals": ["x : Int\n⊢ x = x"],
    "endPos": {"line": 1, "column": 41}}],
  "messages":
  [{"severity": "warning",
@@ -10,8 +11,7 @@
    "data": "declaration uses 'sorry'"}],
  "env": 0}
 
-{"sorries": [{"proofState": 1, "goal": "x : Int\n⊢ x = 1"}],
- "proofStatus": "Incomplete: open goals remain",
- "proofState": 2,
- "goals": ["x : Int\nh : x = 1\n⊢ x = x"]}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
+ "goals": ["x : Int\n⊢ x = 1", "x : Int\nh : x = 1\n⊢ x = x"]}
 
diff --git a/test/sorry_hypotheses.in b/test/sorry_hypotheses.in
index 515c15cc..0f6e2899 100644
--- a/test/sorry_hypotheses.in
+++ b/test/sorry_hypotheses.in
@@ -1,4 +1,4 @@
-{"cmd": "theorem foo (x : Int) : x = x := by sorry"}
+{"cmd": "theorem foo (x : Int) : x = x := by sorry", "sorries": "individual"}
 
 {"proofState" : 0, "tactic": "have h : x = 1 := sorry"}
 
diff --git a/test/tactic_have_branching.expected.out b/test/tactic_have_branching.expected.out
new file mode 100644
index 00000000..5c8798c4
--- /dev/null
+++ b/test/tactic_have_branching.expected.out
@@ -0,0 +1,34 @@
+{"sorries":
+ [{"proofState": 0,
+   "pos": {"line": 1, "column": 22},
+   "parentDecl": "_example",
+   "goals": ["⊢ 1 = 1"],
+   "endPos": {"line": 1, "column": 27}}],
+ "messages":
+ [{"severity": "warning",
+   "pos": {"line": 1, "column": 0},
+   "endPos": {"line": 1, "column": 7},
+   "data": "declaration uses 'sorry'"}],
+ "env": 0}
+
+{"proofStatus": "Completed", "proofState": 1, "goals": []}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 2,
+ "goals": ["⊢ True", "this : True\n⊢ 1 = 1"]}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 3,
+ "messages":
+ [{"severity": "error",
+   "pos": {"line": 0, "column": 0},
+   "endPos": {"line": 0, "column": 0},
+   "data": "unknown identifier 'h1'"}],
+ "goals": ["⊢ True", "this : True\n⊢ 1 = 1"]}
+
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 4,
+ "goals": ["this : True\n⊢ 1 = 1"]}
+
+{"proofStatus": "Completed", "proofState": 5, "goals": []}
+
diff --git a/test/tactic_have_branching.in b/test/tactic_have_branching.in
new file mode 100644
index 00000000..47259fbb
--- /dev/null
+++ b/test/tactic_have_branching.in
@@ -0,0 +1,12 @@
+{"cmd": "example : 1 = 1 := by sorry", "sorries": "individual"}
+
+{"tactic": "rfl", "proofState": 0}
+
+{"tactic": "have : True := by sorry", "proofState": 0}
+
+{"tactic": "exact h1", "proofState": 2}
+
+{"tactic": "exact True.intro", "proofState": 2}
+
+{"tactic": "rfl", "proofState": 4}
+
diff --git a/test/tactic_mode_sorry.expected.out b/test/tactic_mode_sorry.expected.out
index 15c007e6..50edb259 100644
--- a/test/tactic_mode_sorry.expected.out
+++ b/test/tactic_mode_sorry.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 18},
-   "goal": "⊢ Nat",
+   "parentDecl": "f",
+   "goals": ["⊢ Nat"],
    "endPos": {"line": 1, "column": 23}}],
  "messages":
  [{"severity": "warning",
@@ -10,8 +11,7 @@
    "data": "declaration uses 'sorry'"}],
  "env": 0}
 
-{"sorries": [{"proofState": 1, "goal": "⊢ Nat"}],
- "proofStatus": "Incomplete: contains sorry",
- "proofState": 2,
- "goals": []}
+{"proofStatus": "Incomplete: open goals remain",
+ "proofState": 1,
+ "goals": ["⊢ Nat"]}
 
diff --git a/test/tactic_mode_sorry.in b/test/tactic_mode_sorry.in
index 32465b9c..b9b1197b 100644
--- a/test/tactic_mode_sorry.in
+++ b/test/tactic_mode_sorry.in
@@ -1,3 +1,3 @@
-{"cmd": "def f : Nat := by sorry"}
+{"cmd": "def f : Nat := by sorry", "sorries": "individual"}
 
 {"proofState": 0, "tactic": "sorry"}
diff --git a/test/tactic_sorry.expected.out b/test/tactic_sorry.expected.out
index 0394d4f8..5644af1a 100644
--- a/test/tactic_sorry.expected.out
+++ b/test/tactic_sorry.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 18},
-   "goal": "⊢ Nat",
+   "parentDecl": "f",
+   "goals": ["⊢ Nat"],
    "endPos": {"line": 1, "column": 23}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/tactic_sorry.in b/test/tactic_sorry.in
index 7e9e61da..ce7c5872 100644
--- a/test/tactic_sorry.in
+++ b/test/tactic_sorry.in
@@ -1 +1 @@
-{"cmd": "def f : Nat := by sorry"}
+{"cmd": "def f : Nat := by sorry", "sorries": "individual"}
diff --git a/test/term_sorry.expected.out b/test/term_sorry.expected.out
index ab332e35..be9674e1 100644
--- a/test/term_sorry.expected.out
+++ b/test/term_sorry.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 15},
-   "goal": "⊢ Nat",
+   "parentDecl": "f",
+   "goals": ["⊢ Nat"],
    "endPos": {"line": 1, "column": 20}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/term_sorry.in b/test/term_sorry.in
index 1bf62faa..91d2ac25 100644
--- a/test/term_sorry.in
+++ b/test/term_sorry.in
@@ -1 +1 @@
-{"cmd": "def f : Nat := sorry"}
+{"cmd": "def f : Nat := sorry", "sorries": "individual"}
diff --git a/test/trace_simp.expected.out b/test/trace_simp.expected.out
index 0f3bbba7..e916edf1 100644
--- a/test/trace_simp.expected.out
+++ b/test/trace_simp.expected.out
@@ -15,7 +15,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 23},
-   "goal": "⊢ f = 37",
+   "parentDecl": "_example",
+   "goals": ["⊢ f = 37"],
    "endPos": {"line": 1, "column": 28}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/trace_simp.in b/test/trace_simp.in
index 7e2a4a2e..583fc5d3 100644
--- a/test/trace_simp.in
+++ b/test/trace_simp.in
@@ -6,7 +6,7 @@
 
 {"cmd": "example : f = 37 := by simp", "env": 2}
 
-{"cmd": "example : f = 37 := by sorry", "env": 2}
+{"cmd": "example : f = 37 := by sorry", "env": 2, "sorries": "individual"}
 
 {"tactic": "trace \"37\"", "proofState": 0}
 
diff --git a/test/unknown_proof_state.expected.out b/test/unknown_proof_state.expected.out
index ee52464f..9f1dfc33 100644
--- a/test/unknown_proof_state.expected.out
+++ b/test/unknown_proof_state.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 18},
-   "goal": "⊢ Nat",
+   "parentDecl": "f",
+   "goals": ["⊢ Nat"],
    "endPos": {"line": 1, "column": 23}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/unknown_proof_state.in b/test/unknown_proof_state.in
index bdd1a68f..ef2f8daf 100644
--- a/test/unknown_proof_state.in
+++ b/test/unknown_proof_state.in
@@ -1,3 +1,3 @@
-{"cmd" : "def f : Nat := by sorry"}
+{"cmd" : "def f : Nat := by sorry", "sorries" : "individual"}
 
 {"tactic": "exact 42", "proofState": 1}
diff --git a/test/unknown_tactic.expected.out b/test/unknown_tactic.expected.out
index 7e55103b..c016420c 100644
--- a/test/unknown_tactic.expected.out
+++ b/test/unknown_tactic.expected.out
@@ -1,7 +1,8 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 1, "column": 18},
-   "goal": "⊢ Nat",
+   "parentDecl": "f",
+   "goals": ["⊢ Nat"],
    "endPos": {"line": 1, "column": 23}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/unknown_tactic.in b/test/unknown_tactic.in
index d1af2492..a8f771b3 100644
--- a/test/unknown_tactic.in
+++ b/test/unknown_tactic.in
@@ -1,3 +1,3 @@
-{"cmd" : "def f : Nat := by sorry"}
+{"cmd" : "def f : Nat := by sorry", "sorries" : "individual"}
 
 {"tactic": "exat 42", "proofState": 0}
diff --git a/test/variables.expected.out b/test/variables.expected.out
index d67e84bd..7cab6396 100644
--- a/test/variables.expected.out
+++ b/test/variables.expected.out
@@ -11,8 +11,9 @@
 {"sorries":
  [{"proofState": 0,
    "pos": {"line": 3, "column": 2},
-   "goal":
-   "x y : Nat\nf : Nat → Nat\nh0 : f 5 = 3\nh1 : f (4 * x * y) = 2 * y * (f (x + y) + f (x - y))\n⊢ ∃ k, f 2015 = k",
+   "parentDecl": "problem",
+   "goals":
+   ["x y : Nat\nf : Nat → Nat\nh0 : f 5 = 3\nh1 : f (4 * x * y) = 2 * y * (f (x + y) + f (x - y))\n⊢ ∃ k, f 2015 = k"],
    "endPos": {"line": 3, "column": 7}}],
  "messages":
  [{"severity": "warning",
diff --git a/test/variables.in b/test/variables.in
index 4682e37f..e699263a 100644
--- a/test/variables.in
+++ b/test/variables.in
@@ -2,4 +2,4 @@
 
 {"cmd": "variable (f : Nat → Nat)", "env": 0}
 
-{"cmd": "theorem problem (h0 : f 5 = 3) (h1 : f (4 * x * y) = 2 * y * (f (x + y) + f (x - y))) :\n    ∃ (k : Nat), f 2015 = k := by\n  sorry", "env": 1}
+{"cmd": "theorem problem (h0 : f 5 = 3) (h1 : f (4 * x * y) = 2 * y * (f (x + y) + f (x - y))) :\n    ∃ (k : Nat), f 2015 = k := by\n  sorry", "env": 1, "sorries": "individual"}