feat: hovering over omission term shows reason for omission (#3751)

This avoids printing the entire docstring for `⋯` when hovering over it,
which is rather long, and instead it gives a brief reason for omission
and what option to set to pretty print the omitted term.

src/Lean/Elab/InfoTree/Main.lean

@@ -187,7 +187,7 @@ def FieldRedeclInfo.format (ctx : ContextInfo) (info : FieldRedeclInfo) : Format
   f!"FieldRedecl @ {formatStxRange ctx info.stx}"
 
 def OmissionInfo.format (ctx : ContextInfo) (info : OmissionInfo) : IO Format := do
-  return f!"Omission @ {← TermInfo.format ctx info.toTermInfo}"
+  return f!"Omission @ {← TermInfo.format ctx info.toTermInfo}\nReason: {info.reason}"
 
 def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofTacticInfo i         => i.format ctx

src/Lean/Elab/InfoTree/Types.lean

@@ -157,12 +157,13 @@ structure FieldRedeclInfo where
 
 /--
 Denotes information for the term `⋯` that is emitted by the delaborator when omitting a term
-due to `pp.deepTerms false`. Omission needs to be treated differently from regular terms because
+due to `pp.deepTerms false` or `pp.proofs false`. Omission needs to be treated differently from regular terms because
 it has to be delaborated differently in `Lean.Widget.InteractiveDiagnostics.infoToInteractive`:
 Regular terms are delaborated explicitly, whereas omitted terms are simply to be expanded with
 regular delaboration settings.
 -/
-structure OmissionInfo extends TermInfo
+structure OmissionInfo extends TermInfo where
+  reason : String
 
 /-- Header information for a node in `InfoTree`. -/
 inductive Info where

src/Lean/PrettyPrinter/Delaborator/Basic.lean

@@ -232,12 +232,21 @@ where
     stx := stx
   }
 
-def addOmissionInfo (pos : Pos) (stx : Syntax) (e : Expr) : DelabM Unit := do
+inductive OmissionReason
+  | deep
+  | proof
+
+def OmissionReason.toString : OmissionReason → String
+  | deep => "Term omitted due to its depth (see option `pp.deepTerms`)."
+  | proof => "Proof omitted (see option `pp.proofs`)."
+
+def addOmissionInfo (pos : Pos) (stx : Syntax) (e : Expr) (reason : OmissionReason) : DelabM Unit := do
   let info := Info.ofOmissionInfo <| ← mkOmissionInfo stx e
   modify fun s => { s with infos := s.infos.insert pos info }
 where
   mkOmissionInfo stx e := return {
     toTermInfo := ← addTermInfo.mkTermInfo stx e (isBinder := false)
+    reason := reason.toString
   }
 
 /--
@@ -327,10 +336,10 @@ def withAnnotateTermInfo (d : Delab) : Delab := do
 Delaborates the current expression as `⋯` and attaches `Elab.OmissionInfo`, which influences how the
 subterm omitted by `⋯` is delaborated when hovered over.
 -/
-def omission : Delab := do
+def omission (reason : OmissionReason) : Delab := do
   let stx ← `(⋯)
   let stx ← annotateCurPos stx
-  addOmissionInfo (← getPos) stx (← getExpr)
+  addOmissionInfo (← getPos) stx (← getExpr) reason
   pure stx
 
 partial def delabFor : Name → Delab
@@ -345,10 +354,10 @@ partial def delab : Delab := do
   let e ← getExpr
 
   if ← shouldOmitExpr e then
-    return ← omission
+    return ← omission .deep
 
   if ← shouldOmitProof e then
-    let pf ← omission
+    let pf ← omission .proof
     if ← getPPOption getPPProofsWithType then
       let stx ← withType delab
       return ← annotateCurPos (← `(($pf : $stx)))

src/Lean/Server/FileWorker/WidgetRequests.lean

@@ -55,7 +55,7 @@ def makePopup : WithRpcRef InfoWithCtx → RequestM (RequestTask InfoPopup)
       let exprExplicit? ← match i.info with
         | Elab.Info.ofTermInfo ti =>
           pure <| some <| ← ppExprTaggedWithoutTopLevelHighlight ti.expr (explicit := true)
-        | Elab.Info.ofOmissionInfo { toTermInfo := ti } =>
+        | Elab.Info.ofOmissionInfo { toTermInfo := ti, .. } =>
           -- Omitted terms are simply to be expanded, not printed explicitly.
           -- Keep the top-level tag so that users can also see the explicit version
           -- of the omitted term.

src/Lean/Server/InfoUtils.lean

@@ -252,7 +252,7 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
     if let some decl := (← getOptionDecls).find? oi.optionName then
       return decl.descr
     return none
-  | .ofOmissionInfo _ => pure () -- Fall through to display the docstring of `⋯` for omitted terms
+  | .ofOmissionInfo { reason := s, .. } => return s -- Show the omission reason for the docstring.
   | _ => pure ()
   if let some ei := i.toElabInfo? then
     return ← findDocString? env ei.stx.getKind <||> findDocString? env ei.elaborator
@@ -398,7 +398,7 @@ where go ci?
   | .node i cs =>
     match ci?, i with
     | some ci, .ofTermInfo ti
-    | some ci, .ofOmissionInfo { toTermInfo := ti } => do
+    | some ci, .ofOmissionInfo { toTermInfo := ti, .. } => do
       let expr ← ti.runMetaM ci (instantiateMVars ti.expr)
       return expr.hasSorry
       -- we assume that `cs` are subterms of `ti.expr` and