chore: cleanup and better docs for #10479 (#10504)

This PR cleans up a half-reverted refactor and adds documentation to
#10479.

Author: david-christiansen

src/Lean/Elab/InfoTree/Types.lean

@@ -212,14 +212,23 @@ inductive DocElabKind where
 deriving Repr
 
 /--
-Indicates that an extensible document elaborator was used here.
+Indicates that an extensible document elaborator was used. This info is applied to the name on a
+role, directive, code block, or command, and is used to generate the hover.
+
+A `TermInfo` would not give the correct hover for a few reasons:
+ 1. The name used to invoke a document extension is not necessarily the name of the elaborator that
+    was used, but the elaborator's docstring should be shown rather than that of the name as
+    written.
+ 2. The underlying elaborator's Lean type is not an appropriate signature to show to users.
 -/
 structure DocElabInfo extends ElabInfo where
   name : Name
   kind : DocElabKind
 
 /--
-Indicates that a piece of syntax was elaborated as documentation.
+Indicates that a piece of syntax was elaborated as documentation. This info is used for ordinary
+documentation constructs, such as paragraphs, list items, and links. It can be used to determine
+that a given piece of documentation syntax in fact has been elaborated.
 -/
 structure DocInfo extends ElabInfo where
 

src/Lean/Parser/Term/Basic.lean

@@ -11,6 +11,17 @@ public import Lean.Parser.Level
 public import Lean.Parser.Term.Doc
 meta import Lean.Parser.Basic
 
+/-!
+This module contains the bare minimum of term syntax that's required to get documentation syntax to
+parse, namely structure initializers and their dependencies.
+
+This matters because some term syntax (such as `let rec`) includes docstrings, but docstrings
+include metadata blocks that themselves include a structure initializer. Separating these layers
+prevents an import cycle.
+
+The remaining term syntax is found in `Lean.Parser.Term`. It may freely make use of documentation
+comments.
+-/
 
 public section
 

src/Lean/Server/FileWorker/SemanticHighlighting.lean

@@ -260,7 +260,7 @@ partial def collectSyntaxBasedSemanticTokens : (stx : Syntax) → Array LeanSema
 open Lean.Doc.Syntax in
 /-- Collects all semantic tokens from the given `Elab.InfoTree`. -/
 def collectInfoBasedSemanticTokens (i : Elab.InfoTree) : Array LeanSemanticToken :=
-  Array.flatten <| List.toArray <| i.deepestNodes fun _ info _ => do
+  List.toArray <| i.deepestNodes fun _ info _ => do
     let .ofTermInfo ti := info
       | none
     let .original .. := ti.stx.getHeadInfo
@@ -271,11 +271,11 @@ def collectInfoBasedSemanticTokens (i : Elab.InfoTree) : Array LeanSemanticToken
           -- Recall that `isAuxDecl` is an auxiliary declaration used to elaborate a recursive definition.
           if localDecl.isAuxDecl then
             if ti.isBinder then
-              return #[⟨ti.stx, SemanticTokenType.function⟩]
+              return ⟨ti.stx, SemanticTokenType.function⟩
           else if ! localDecl.isImplementationDetail then
-            return #[⟨ti.stx, SemanticTokenType.variable⟩]
+            return ⟨ti.stx, SemanticTokenType.variable⟩
     if ti.stx.getKind == Parser.Term.identProjKind then
-      return #[⟨ti.stx, SemanticTokenType.property⟩]
+      return ⟨ti.stx, SemanticTokenType.property⟩
     none
 
 def computeSemanticTokens  (doc : EditableDocument) (beginPos : String.Pos)