feat: make ⋯ in Infoview hovers show docstring (#3663)

The docstring for `⋯` gives information about why the omission term
might appear in an expression, and it helps with discoverability to give
documentation right in the hover.

This was mentioned by Patrick Massot [on
Zulip](https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/Deep.20terms.20ellipses/near/426133597)
as being an issue.

src/Lean/Parser/Term.lean

@@ -147,9 +147,12 @@ This syntax is used to construct named metavariables. -/
 @[builtin_term_parser] def syntheticHole := leading_parser
   "?" >> (ident <|> hole)
 /--
-Denotes a term that was omitted by the pretty printer.
-This is only meant to be used for pretty printing, however for copy/paste friendliness it elaborates like `_` while logging a warning.
-The presence of `⋯` in pretty printer output is controlled by the `pp.deepTerms` and `pp.proofs` options.
+The `⋯` term denotes a term that was omitted by the pretty printer.
+The presence of `⋯` in pretty printer output is controlled by the `pp.deepTerms` and `pp.proofs` options,
+and these options can be further adjusted using `pp.deepTerms.threshold` and `pp.proofs.threshold`.
+
+It is only meant to be used for pretty printing.
+However, in case it is copied and pasted from the Infoview, `⋯` logs a warning and elaborates like `_`.
 -/
 @[builtin_term_parser] def omission := leading_parser
   "⋯"

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 _ => return none -- Do not display the docstring of ⋯ for omitted terms
+  | .ofOmissionInfo _ => pure () -- Fall through to display the docstring of `⋯` for omitted terms
   | _ => pure ()
   if let some ei := i.toElabInfo? then
     return ← findDocString? env ei.stx.getKind <||> findDocString? env ei.elaborator