Update src/Lean/Server/InfoUtils.lean

Co-authored-by: David Thrane Christiansen <david@davidchristiansen.dk>

src/Lean/Server/InfoUtils.lean

@@ -84,7 +84,28 @@ where go ctx? a
       | none => a
       | some ctx => f ctx i a
     ts.foldl (init := a) (go <| i.updateContext? ctx?)
-  | _ => a
+  | hole _ => a
+
+/--
+Fold an info tree as follows, while ensuring that the correct `ContextInfo` is supplied at each stage:
+
+ * Nodes are combined with the initial value `init` using `f`, and the result is then combined with the children using a left fold
+ * On InfoTree holes, we just return the initial value.
+
+This is like `InfoTree.foldInfo`, but it also passes the whole node to `f` instead of just the head.
+-/
+partial def InfoTree.foldInfoTree (init : α) (f : ContextInfo → InfoTree → α → α) : InfoTree → α :=
+  go none init
+where
+  /-- `foldInfoTree.go` is like `foldInfoTree` but with an additional outer context parameter `ctx?`. -/
+  go ctx? a
+  | context ctx t => go (ctx.mergeIntoOuter? ctx?) a t
+  | t@(node i ts) =>
+    let a := match ctx? with
+      | none => a
+      | some ctx => f ctx t a
+    ts.foldl (init := a) (go <| i.updateContext? ctx?)
+  | hole _ => a
 
 def Info.isTerm : Info → Bool
   | ofTermInfo _ => true