diff --git a/src/Lean/Elab/InfoTree.lean b/src/Lean/Elab/InfoTree.lean
index 4b55314acd..e803cace59 100644
--- a/src/Lean/Elab/InfoTree.lean
+++ b/src/Lean/Elab/InfoTree.lean
@@ -133,8 +133,11 @@ where fmtPos pos info :=
     | SourceInfo.original ..  => pos
     | _                       => f!"{pos}†"
 
+def TermInfo.runMetaM (info : TermInfo) (ctx : ContextInfo) (x : MetaM α) : IO α :=
+  ctx.runMetaM info.lctx x
+
 def TermInfo.format (cinfo : ContextInfo) (info : TermInfo) : IO Format := do
-  cinfo.runMetaM info.lctx do
+  info.runMetaM cinfo do
     return f!"{← Meta.ppExpr info.expr} : {← Meta.ppExpr (← Meta.inferType info.expr)} @ {formatStxRange cinfo info.stx}"
 
 def CommandInfo.format (cinfo : ContextInfo) (info : CommandInfo) : IO Format := do
diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index eaa0facdb7..61661641f9 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/src/Lean/Server/InfoUtils.lean
@@ -29,6 +29,21 @@ where go ctx?
       | _        => []
   | _ => []
 
+partial def InfoTree.foldInfo (f : ContextInfo → Info → α → α) (init : α) : InfoTree → α :=
+  go none init
+where go ctx? a
+  | context ctx t => go ctx a t
+  | node i ts =>
+    let a := match ctx? with
+      | none => a
+      | some ctx => f ctx i a
+    ts.foldl (init := a) (go ctx?)
+  | _ => a
+
+def Info.isTerm : Info → Bool
+  | ofTermInfo _ => true
+  | _ => false
+
 def Info.stx : Info → Syntax
   | ofTacticInfo i         => i.stx
   | ofTermInfo i           => i.stx
@@ -42,6 +57,23 @@ def Info.pos? (i : Info) : Option String.Pos :=
 def Info.tailPos? (i : Info) : Option String.Pos :=
   i.stx.getTailPos? (originalOnly := true)
 
+def Info.size? (i : Info) : Option Nat := OptionM.run do
+  let pos ← i.pos?
+  let tailPos ← i.tailPos?
+  return tailPos - pos
+
+-- `Info` without position information are considered to have "infinite" size
+def Info.isSmaller (i₁ i₂ : Info) : Bool :=
+  match i₁.size?, i₂.pos? with
+  | some sz₁, some sz₂ => sz₁ < sz₂
+  | some _, none => true
+  | _, _ => false
+
+def Info.occursBefore? (i : Info) (hoverPos : String.Pos) : Option Nat := OptionM.run do
+  let tailPos ← i.tailPos?
+  guard (tailPos ≤ hoverPos)
+  return hoverPos - tailPos
+
 def InfoTree.smallestInfo? (p : Info → Bool) (t : InfoTree) : Option (ContextInfo × Info) :=
   let ts := t.deepestNodes fun ctx i => if p i then some (ctx, i) else none