feat: extensible Markdown rendering of Verso docstrings

This PR adds support for extensible Markdown rendering of Verso
docstrings.

Markdown rendering is used when docstrings are prepared for LSP hovers
as well as for legacy clients that don't directly support
Verso. Previously, when the docstring contained a custom element,
Markdown rendering simply delegated to the alternate fallback
rendering. Now, the custom elements can have custom rendering to
Markdown.

Example use cases include:

* Including a docstring in another: with the module system, docstrings
are part of the server olean and are loaded only in interactive
sessions. If one docstring is to include another, it must be fetched
at a time when the docstrings are loaded and available. A custom
element can save which docstring is to be included at elaboration
time, and then look it up at rendering time.

* Showing a list of all currently-available instances of a class.

* Showing names with respect to the currently-open namespaces.

* Custom links to e.g. library notes that look up the destination in
an environment extension.

Author: david-christiansen

src/Lean/BuiltinDocAttr.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.Compiler.InitAttr
+import Lean.DocString.Markdown
 
 public section
 

src/Lean/DocString.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.DocString.Extension
+public import Lean.DocString.Markdown
 public import Lean.DocString.Links
 public import Lean.Parser.Tactic.Doc
 public import Lean.Parser.Term.Doc
@@ -30,9 +31,13 @@ account.
 Use `Lean.findSimpleDocString?` to look up the raw docstring without resolving alternate forms or
 including extensions.
 -/
-def findDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) := do
+def findDocString? (env : Environment) (declName : Name) (includeBuiltin := true)
+    (options : Options := {}) (currNamespace : Name := .anonymous) (openDecls : List OpenDecl := []) :
+    IO (Option String) := do
   let declName := alternativeOfTactic env declName |>.getD declName
   let exts := getTacticExtensionString env declName
   let spellings := getRecommendedSpellingString env declName
-  let str := (← findSimpleDocString? env declName (includeBuiltin := includeBuiltin)).map (· ++ exts ++ spellings)
+  let str := (← findSimpleDocString? env declName (includeBuiltin := includeBuiltin)
+      (options := options) (currNamespace := currNamespace) (openDecls := openDecls)).map
+    (· ++ exts ++ spellings)
   str.mapM (rewriteManualLinks ·)

src/Lean/DocString/Extension.lean

@@ -7,8 +7,11 @@ module
 
 prelude
 public import Lean.DeclarationRange
-public import Lean.DocString.Markdown
+public import Lean.DocString.Types
 public import Init.Data.String.Extra
+public import Init.Data.String.TakeDrop
+public import Init.Data.String.Search
+public import Init.Data.String.Length
 import Init.Omega
 
 public section
@@ -22,46 +25,32 @@ namespace Lean
 
 
 /--
-Saved data that describes the contents. The `name` should determine both the type of the value and
-its interpretation; if in doubt, use the name of the elaborator that produces the data.
+Saved data that describes a custom inline element.
+
+The type of value contained within the `Dynamic` determines the interpretation of the custom
+element, including how it is rendered to Markdown for the language server.
 -/
 structure ElabInline where
-  name : Name
   val : Dynamic
 
 instance : Repr ElabInline where
   reprPrec v _ :=
     .group <| .nestD <|
-      .group (.nestD ("{ name :=" ++ .line ++ repr v.name)) ++ .line ++
-      .group (.nestD ("val :=" ++ .line ++ "Dynamic.mk " ++ repr v.val.typeName ++ " _ }"))
-
-instance : Doc.MarkdownInline ElabInline where
-  -- TODO extensibility
-  toMarkdown go _i content := do
-    let parts ← content.mapM go
-    return Doc.joinInlines parts
-
+      .group (.nestD ("{ val :=" ++ .line ++ "Dynamic.mk " ++ repr v.val.typeName ++ " _ }"))
 
 /--
-Saved data that describes the contents. The `name` should determine both the type of the value and
-its interpretation; if in doubt, use the name of the elaborator that produces the data.
+Saved data that describes a custom block element.
+
+The type of value contained within the `Dynamic` determines the interpretation of the custom
+element, including how it is rendered to Markdown for the language server.
 -/
 structure ElabBlock where
-  name : Name
   val : Dynamic
 
 instance : Repr ElabBlock where
   reprPrec v _ :=
     .group <| .nestD <|
-      .group (.nestD ("{ name :=" ++ .line ++ repr v.name)) ++ .line ++
-      .group (.nestD ("val :=" ++ .line ++ "Dynamic.mk " ++ repr v.val.typeName ++ " _ }"))
-
-
--- TODO extensible toMarkdown
-instance : Doc.MarkdownBlock ElabInline ElabBlock where
-  toMarkdown _goI goB _b content := do
-    let parts ← content.mapM goB
-    return Doc.joinBlocks parts
+      .group (.nestD ("{ val :=" ++ .line ++ "Dynamic.mk " ++ repr v.val.typeName ++ " _ }"))
 
 structure VersoDocString where
   text : Array (Doc.Block ElabInline ElabBlock)
@@ -165,26 +154,6 @@ partial def findInternalDocString? (env : Environment) (declName : Name) (includ
       return some (.inr doc)
   return none
 
-/--
-Finds a docstring without performing any alias resolution or enrichment with extra metadata. The
-result is rendered as Markdown.
-
-Docstrings to be shown to a user should be looked up with `Lean.findDocString?` instead.
--/
-def findSimpleDocString? (env : Environment) (declName : Name) (includeBuiltin := true) : IO (Option String) := do
-  match (← findInternalDocString? env declName (includeBuiltin := includeBuiltin)) with
-  | some (.inl str) => return some str
-  | some (.inr verso) => return some (toMarkdown verso)
-  | none => return none
-
-where
-  toMarkdown : VersoDocString → String
-  | .mk bs ps => Doc.MarkdownM.run' do
-      let blockLines ← bs.mapM Doc.ToMarkdown.toMarkdown
-      let partLines ← ps.mapM Doc.ToMarkdown.toMarkdown
-      return Doc.joinBlocks (blockLines ++ partLines)
-
-
 structure ModuleDoc where
   doc : String
   declarationRange : DeclarationRange
@@ -276,14 +245,6 @@ def addPart (snippet : Snippet) (level : Nat) (range : DeclarationRange) (part :
 
 end VersoModuleDocs.Snippet
 
-open Lean Doc ToMarkdown in
-instance : ToMarkdown VersoModuleDocs.Snippet where
-  toMarkdown
-    | {text, sections, ..} => do
-      let textBlocks ← text.mapM toMarkdown
-      let sectionBlocks ← sections.mapM fun (level, _, part) => partMarkdown level part
-      return joinBlocks (textBlocks ++ sectionBlocks)
-
 structure VersoModuleDocs where
   snippets : PersistentArray VersoModuleDocs.Snippet := {}
 deriving Inhabited