feat: improvements to Verso docstrings (#10479)

This PR implements module docstrings in Verso syntax, as well as adding
a number of improvements and fixes to Verso docstrings in general. In
particular, they now have language server support and are parsed at
parse time rather than elaboration time, so the snapshot's syntax tree
includes the parsed documentation.

src/Lean/DocString/Add.lean

@@ -50,23 +50,20 @@ def validateDocComment
     else
       logError err
 
-
-open Lean.Doc in
-open Parser in
+open Lean.Parser Command in
 /--
-Adds a Verso docstring to the specified declaration, which should already be present in the
-environment.
-
-`binders` should be the syntax of the parameters to the constant that is being documented, as a null
-node that contains a sequence of bracketed binders. It is used to allow interactive features such as
-document highlights and “find references” to work for documented parameters. If no parameter binders
-are available, pass `Syntax.missing` or an empty null node.
+Parses a docstring as Verso, returning the syntax if successful.
 
+When not successful, parser errors are logged.
 -/
-def versoDocString
-    (declName : Name) (binders : Syntax) (docComment : TSyntax `Lean.Parser.Command.docComment) :
-    TermElabM (Array (Doc.Block ElabInline ElabBlock) × Array (Doc.Part ElabInline ElabBlock Empty)) := do
-
+def parseVersoDocString
+    [Monad m] [MonadFileMap m] [MonadError m] [MonadEnv m] [MonadOptions m] [MonadLog m]
+    [MonadResolveName m]
+    (docComment : TSyntax [``docComment, ``moduleDoc]) : m (Option Syntax) := do
+  if docComment.raw.getKind == ``docComment then
+    match docComment.raw[0] with
+    | docStx@(.node _ ``versoCommentBody _) => return docStx[1]?
+    | _ => pure ()
   let text ← getFileMap
   -- TODO fallback to string version without nice interactivity
   let some startPos := docComment.raw[1].getPos? (canonicalOnly := true)
@@ -93,7 +90,7 @@ def versoDocString
   }
   let s := mkParserState text.source |>.setPos startPos
   -- TODO parse one block at a time for error recovery purposes
-  let s := (Doc.Parser.document).run ictx pmctx (getTokenTable env) s
+  let s := Doc.Parser.document.run ictx pmctx (getTokenTable env) s
 
   if !s.allErrors.isEmpty then
     for (pos, _, err) in s.allErrors do
@@ -103,11 +100,42 @@ def versoDocString
         -- TODO end position
         data := err.toString
       }
-    return (#[], #[])
-  else
-    let stx := s.stxStack.back
-    let stx := stx.getArgs
-    Doc.elabBlocks (stx.map (⟨·⟩)) |>.exec declName binders
+    return none
+  return some s.stxStack.back
+
+
+
+open Lean.Doc in
+open Lean.Parser.Command in
+/--
+Elaborates a Verso docstring for the specified declaration, which should already be present in the
+environment.
+
+`binders` should be the syntax of the parameters to the constant that is being documented, as a null
+node that contains a sequence of bracketed binders. It is used to allow interactive features such as
+document highlights and “find references” to work for documented parameters. If no parameter binders
+are available, pass `Syntax.missing` or an empty null node.
+-/
+
+def versoDocString
+    (declName : Name) (binders : Syntax) (docComment : TSyntax ``docComment) :
+    TermElabM (Array (Doc.Block ElabInline ElabBlock) × Array (Doc.Part ElabInline ElabBlock Empty)) := do
+  if let some stx ← parseVersoDocString docComment then
+    Doc.elabBlocks (stx.getArgs.map (⟨·⟩)) |>.exec declName binders
+  else return (#[], #[])
+
+open Lean.Doc Parser in
+open Lean.Parser.Command in
+/--
+Parses and elaborates a Verso module docstring.
+-/
+def versoModDocString
+    (range : DeclarationRange) (doc : TSyntax ``document) :
+    TermElabM VersoModuleDocs.Snippet := do
+  let level := getVersoModuleDocs (← getEnv) |>.terminalNesting |>.map (· + 1)
+  Doc.elabModSnippet range (doc.raw.getArgs.map (⟨·⟩)) (level.getD 0) |>.execForModule
+
+
 
 open Lean.Doc in
 open Parser in
@@ -185,6 +213,19 @@ def addVersoDocStringCore [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] [MonadErr
   modifyEnv fun env =>
     versoDocStringExt.insert env declName docs
 
+/--
+Adds an elaborated Verso module docstring to the environment.
+-/
+def addVersoModDocStringCore [Monad m] [MonadEnv m] [MonadLiftT BaseIO m] [MonadError m]
+  (docs : VersoModuleDocs.Snippet) : m Unit := do
+  if (getMainModuleDoc (← getEnv)).isEmpty then
+    match addVersoModuleDocSnippet (← getEnv) docs with
+    | .error e => throwError "Error adding module docs: {indentD <| toMessageData e}"
+    | .ok env' => setEnv env'
+  else
+    throwError m!"Can't add Verso-format module docs because there is already Markdown-format content present."
+
+open Lean.Parser.Command in
 /--
 Adds a Verso docstring to the environment.
 
@@ -194,7 +235,7 @@ document highlights and “find references” to work for documented parameters.
 are available, pass `Syntax.missing` or an empty null node.
 -/
 def addVersoDocString
-    (declName : Name) (binders : Syntax) (docComment : TSyntax `Lean.Parser.Command.docComment) :
+    (declName : Name) (binders : Syntax) (docComment : TSyntax ``docComment) :
     TermElabM Unit := do
   unless (← getEnv).getModuleIdxFor? declName |>.isNone do
     throwError s!"invalid doc string, declaration '{declName}' is in an imported module"
@@ -278,3 +319,20 @@ def addDocString'
   match docString? with
   | some docString => addDocString declName binders docString
   | none => return ()
+
+
+open Lean.Parser.Command in
+open Lean.Doc.Parser in
+/--
+Adds a Verso docstring to the environment.
+
+`binders` should be the syntax of the parameters to the constant that is being documented, as a null
+node that contains a sequence of bracketed binders. It is used to allow interactive features such as
+document highlights and “find references” to work for documented parameters. If no parameter binders
+are available, pass `Syntax.missing` or an empty null node.
+-/
+def addVersoModDocString
+    (range : DeclarationRange) (docComment : TSyntax ``document) :
+    TermElabM Unit := do
+  let snippet ← versoModDocString range docComment
+  addVersoModDocStringCore snippet

src/Lean/DocString/Extension.lean

@@ -12,7 +12,7 @@ public import Lean.DocString.Links
 public import Lean.MonadEnv
 public import Init.Data.String.Extra
 public import Lean.DocString.Types
-import Lean.DocString.Markdown
+public import Lean.DocString.Markdown
 
 public section
 
@@ -38,7 +38,7 @@ instance : Repr ElabInline where
       .group (.nestD ("{ name :=" ++ .line ++ repr v.name)) ++ .line ++
       .group (.nestD ("val :=" ++ .line ++ "Dynamic.mk " ++ repr v.val.typeName ++ " _ }"))
 
-private instance : Doc.MarkdownInline ElabInline where
+instance : Doc.MarkdownInline ElabInline where
   -- TODO extensibility
   toMarkdown go _i content := content.forM go
 
@@ -59,7 +59,7 @@ instance : Repr ElabBlock where
 
 
 -- TODO extensible toMarkdown
-private instance : Doc.MarkdownBlock ElabInline ElabBlock where
+instance : Doc.MarkdownBlock ElabInline ElabBlock where
   toMarkdown _goI goB _b content := content.forM goB
 
 structure VersoDocString where
@@ -214,5 +214,211 @@ def getModuleDoc? (env : Environment) (moduleName : Name) : Option (Array Module
 
 def getDocStringText [Monad m] [MonadError m] (stx : TSyntax `Lean.Parser.Command.docComment) : m String :=
   match stx.raw[1] with
-  | Syntax.atom _ val => return val.extract 0 (val.endPos - ⟨2⟩)
-  | _                 => throwErrorAt stx "unexpected doc string{indentD stx.raw[1]}"
+  | Syntax.atom _ val =>
+    return val.extract 0 (val.endPos - ⟨2⟩)
+  | Syntax.node _ `Lean.Parser.Command.versoCommentBody _ =>
+    match stx.raw[1][0] with
+    | Syntax.atom _ val =>
+      return val.extract 0 (val.endPos - ⟨2⟩)
+    | _ =>
+      throwErrorAt stx "unexpected doc string{indentD stx}"
+  | _ =>
+    throwErrorAt stx "unexpected doc string{indentD stx}"
+
+
+
+/--
+A snippet of a Verso module text.
+
+A snippet consists of text followed by subsections. Because the sequence of snippets that occur in a
+source file are conceptually a single document, they have a consistent header nesting structure.
+This means that initial textual content of a snippet is a continuation of the text at the end of the
+prior snippet.
+
+The actual hierarchical structure of the document is reconstructed from the sequence of snippets.
+
+The _terminal nesting_ of a sequence of snippets is 0 if there are no sections in the sequence.
+Otherwise, it is one greater than the nesting of the last snippet's last section. The module
+docstring elaborator maintains the invariant that each snippet's first section's level is at most
+the terminal nesting of the preceding snippets, and that the level of each section within a snippet
+is at most one greater than the preceding section's level.
+-/
+structure VersoModuleDocs.Snippet where
+  /-- Text to be inserted after the prior snippet's ending text. -/
+  text : Array (Doc.Block ElabInline ElabBlock) := #[]
+  /--
+  A sequence of parts with their absolute document nesting levels and header positions.
+  None of these parts may contain sub-parts.
+  -/
+  sections : Array (Nat × DeclarationRange × Doc.Part ElabInline ElabBlock Empty) := #[]
+  /--
+  The location of the snippet in the source file.
+  -/
+  declarationRange : DeclarationRange
+deriving Inhabited, Repr
+
+namespace VersoModuleDocs.Snippet
+
+def canNestIn (level : Nat) (snippet : Snippet) : Bool :=
+  if let some s := snippet.sections[0]? then s.1 ≤ level + 1 else true
+
+def terminalNesting (snippet : Snippet) : Option Nat :=
+  if let some s := snippet.sections.back? then s.1
+  else none
+
+def addBlock (snippet : Snippet) (block : Doc.Block ElabInline ElabBlock) : Snippet :=
+  if h : snippet.sections.size = 0 then
+    { snippet with text := snippet.text.push block }
+  else
+    { snippet with
+      sections[snippet.sections.size - 1].2.2.content :=
+        snippet.sections[snippet.sections.size - 1].2.2.content.push block }
+
+def addPart (snippet : Snippet) (level : Nat) (range : DeclarationRange) (part : Doc.Part ElabInline ElabBlock Empty) : Snippet :=
+  { snippet with
+    sections := snippet.sections.push (level, range, part) }
+
+end VersoModuleDocs.Snippet
+
+open Lean Doc ToMarkdown MarkdownM in
+instance : ToMarkdown VersoModuleDocs.Snippet where
+  toMarkdown
+    | {text, sections, ..} => do
+      text.forM toMarkdown
+      endBlock
+      for (level, _, part) in sections do
+        push ("".pushn '#' (level + 1))
+        push " "
+        for i in part.title do toMarkdown i
+        endBlock
+        for b in part.content do toMarkdown b
+        endBlock
+
+structure VersoModuleDocs where
+  snippets : PersistentArray VersoModuleDocs.Snippet := {}
+  terminalNesting : Option Nat := snippets.findSomeRev? (·.terminalNesting)
+deriving Inhabited
+
+instance : Repr VersoModuleDocs where
+  reprPrec v _ :=
+    .group <| .nest 2 <|
+      "{ " ++
+      (.group <| .nest 2 <| "snippets := " ++ .line ++ repr v.snippets.toArray) ++ .line ++
+      (.group <| .nest 2 <| "snippets := " ++ .line ++ repr v.snippets.toArray) ++
+      " }"
+
+namespace VersoModuleDocs
+
+def isEmpty (docs : VersoModuleDocs) : Bool := docs.snippets.isEmpty
+
+def canAdd (docs : VersoModuleDocs) (snippet : Snippet) : Bool :=
+  if let some level := docs.terminalNesting then
+    snippet.canNestIn level
+  else true
+
+
+def add (docs : VersoModuleDocs) (snippet : Snippet) : Except String VersoModuleDocs := do
+  unless docs.canAdd snippet do
+    throw "Can't nest this snippet here"
+
+  return { docs with
+    snippets := docs.snippets.push snippet,
+    terminalNesting := snippet.terminalNesting
+  }
+
+def add! (docs : VersoModuleDocs) (snippet : Snippet) : VersoModuleDocs :=
+  let ok :=
+    if let some level := docs.terminalNesting then
+      snippet.canNestIn level
+    else true
+  if not ok then
+    panic! "Can't nest this snippet here"
+  else
+    { docs with
+      snippets := docs.snippets.push snippet,
+      terminalNesting := snippet.terminalNesting
+    }
+
+
+private structure DocFrame where
+  content : Array (Doc.Block ElabInline ElabBlock)
+  priorParts : Array (Doc.Part ElabInline ElabBlock Empty)
+  titleString : String
+  title : Array (Doc.Inline ElabInline)
+
+private structure DocContext where
+  content : Array (Doc.Block ElabInline ElabBlock)
+  priorParts : Array (Doc.Part ElabInline ElabBlock Empty)
+  context : Array DocFrame
+
+private def DocContext.level (ctx : DocContext) : Nat := ctx.context.size
+
+private def DocContext.close (ctx : DocContext) : Except String DocContext := do
+  if h : ctx.context.size = 0 then
+    throw "Can't close a section: none are open"
+  else
+    let last := ctx.context.back
+    pure {
+      content := last.content,
+      priorParts := last.priorParts.push {
+        title := last.title,
+        titleString := last.titleString,
+        metadata := none,
+        content := ctx.content,
+        subParts := ctx.priorParts,
+      },
+      context := ctx.context.pop
+    }
+
+private partial def DocContext.closeAll (ctx : DocContext) : Except String DocContext := do
+  if ctx.context.size = 0 then
+    return ctx
+  else
+    (← ctx.close).closeAll
+
+private partial def DocContext.addPart (ctx : DocContext) (partLevel : Nat) (part : Doc.Part ElabInline ElabBlock Empty) : Except String DocContext := do
+  if partLevel > ctx.level then throw s!"Invalid nesting: expected at most {ctx.level} but got {partLevel}"
+  else if partLevel = ctx.level then pure { ctx with priorParts := ctx.priorParts.push part }
+  else
+    let ctx ← ctx.close
+    ctx.addPart partLevel part
+
+private def DocContext.addBlocks (ctx : DocContext) (blocks : Array (Doc.Block ElabInline ElabBlock)) : Except String DocContext := do
+  if ctx.priorParts.isEmpty then pure { ctx with content := ctx.content ++ blocks }
+  else throw "Can't add content after sub-parts"
+
+private def DocContext.addSnippet (ctx : DocContext) (snippet : Snippet) : Except String DocContext := do
+  let mut ctx ← ctx.addBlocks snippet.text
+  for (l, _, p) in snippet.sections do
+    ctx ← ctx.addPart l p
+  return ctx
+
+def assemble (docs : VersoModuleDocs) : Except String VersoDocString := do
+  let mut ctx : DocContext := {content := #[], priorParts := #[], context := #[]}
+  for snippet in docs.snippets do
+    ctx ← ctx.addSnippet snippet
+  ctx ← ctx.closeAll
+  return { text := ctx.content, subsections := ctx.priorParts }
+
+end VersoModuleDocs
+
+private builtin_initialize versoModuleDocExt :
+    SimplePersistentEnvExtension VersoModuleDocs.Snippet VersoModuleDocs ← registerSimplePersistentEnvExtension {
+  addImportedFn := fun _ => {}
+  addEntryFn    := fun s e => s.add! e
+  exportEntriesFnEx? := some fun _ _ es level =>
+    if level < .server then
+      #[]
+    else
+      es.toArray
+}
+
+
+def getVersoModuleDocs (env : Environment) : VersoModuleDocs :=
+  versoModuleDocExt.getState env
+
+def addVersoModuleDocSnippet (env : Environment) (snippet : VersoModuleDocs.Snippet) : Except String Environment :=
+  let docs := getVersoModuleDocs env
+  if docs.canAdd snippet then
+    pure <| versoModuleDocExt.addEntry env snippet
+  else throw s!"Can't add - incorrect nesting {docs.terminalNesting.map (s!"(expected at most {·})") |>.getD ""})"

src/Lean/DocString/Formatter.lean

@@ -0,0 +1,224 @@
+/-
+Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: David Thrane Christiansen
+-/
+
+module
+prelude
+public import Lean.PrettyPrinter.Formatter
+import Lean.DocString.Syntax
+
+
+namespace Lean.Doc.Parser
+
+open Lean.PrettyPrinter Formatter
+open Lean.Syntax.MonadTraverser
+
+open Lean.Doc.Syntax
+
+def atomString : Syntax → String
+  | .node _ _ #[x] => atomString x
+  | .atom _ x => x
+  | stx => s!"NON-ATOM {stx}"
+
+def pushAtomString : Formatter := do
+  push <| atomString (← getCur)
+  goLeft
+
+def pushAtomStrLit : Formatter := do
+  push <| (Syntax.decodeStrLit (atomString (← getCur))).getD ""
+  goLeft
+
+
+def identString : Syntax → String
+  | .node _ _ #[x] => identString x
+  | .ident _ _ x _ => toString x
+  | stx => s!"NON-IDENT {stx}"
+
+def pushIdent : Formatter := do
+  push <| identString (← getCur)
+  goLeft
+
+def rep (f : Formatter) : Formatter := concat do
+  let count := (← getCur).getArgs.size
+  visitArgs do count.forM fun _ _ => do f
+
+partial def versoSyntaxToString' (stx : Syntax) : ReaderT Nat (StateM String) Unit := do
+  if stx.getKind == nullKind then
+    stx.getArgs.forM versoSyntaxToString'
+  else
+    match stx with
+    | `(arg_val|$s:str) => out <| atomString s
+    | `(arg_val|$n:num) => out <| atomString n
+    | `(arg_val|$x:ident) => out <| identString x
+    | `(doc_arg|($x := $v)) | `(doc_arg|$x:ident := $v) =>
+      out "("
+      out <| identString x
+      out " := "
+      versoSyntaxToString' v
+      out ")"
+    | `(doc_arg|+%$tk$x:ident) | `(doc_arg|-%$tk$x:ident) =>
+      out <| atomString tk
+      out <| identString x
+    | `(doc_arg|$x:arg_val) => versoSyntaxToString' x
+    | `(inline|$s:str) => out s.getString
+    | `(inline|_[%$tk1 $inl* ]%$tk2) | `(inline|*[%$tk1 $inl* ]%$tk2) =>
+      out <| atomString tk1
+      inl.forM versoSyntaxToString'
+      out <| atomString tk2
+    | `(inline|link[%$tk1 $inl* ]%$tk2 $tgt) =>
+      out <| atomString tk1
+      inl.forM versoSyntaxToString'
+      out <| atomString tk2
+      versoSyntaxToString' tgt
+    | `(inline|image(%$tk1 $alt )%$tk2 $tgt) =>
+      out <| atomString tk1
+      out <| (Syntax.decodeStrLit (atomString alt)).getD ""
+      out <| atomString tk2
+      versoSyntaxToString' tgt
+    | `(inline|role{$name $args*}[$inls*]) =>
+      out "{"
+      out <| identString name
+      for arg in args do
+        out " "
+        versoSyntaxToString' arg
+      out "}["
+      inls.forM versoSyntaxToString'
+      out "]"
+    | `(inline|code(%$tk1$s)%$tk2) =>
+      out <| atomString tk1
+      out <| (Syntax.decodeStrLit (atomString s)).getD ""
+      out <| atomString tk2
+    | `(inline|footnote(%$tk1 $ref )%$tk2) =>
+      out <| atomString tk1
+      out <| (Syntax.decodeStrLit (atomString ref)).getD ""
+      out <| atomString tk2
+    | `(inline|line! $s) =>
+      out <| (Syntax.decodeStrLit (atomString s)).getD ""
+    | `(inline|\math%$tk1 code(%$tk2 $s )%$tk3)
+    | `(inline|\displaymath%$tk1 code(%$tk2 $s )%$tk3) =>
+      out <| atomString tk1
+      out <| atomString tk2
+      out <| (Syntax.decodeStrLit (atomString s)).getD ""
+      out <| atomString tk3
+    | `(link_target|[%$tk1 $ref ]%$tk2) =>
+      out <| atomString tk1
+      out <| (Syntax.decodeStrLit (atomString ref)).getD ""
+      out <| atomString tk2
+    | `(link_target|(%$tk1 $url )%$tk2) =>
+      out <| atomString tk1
+      out <| (Syntax.decodeStrLit (atomString url)).getD ""
+      out <| atomString tk2
+    | `(block|header($n){$inl*}) =>
+      out <| "#".pushn '#' n.getNat ++ " "
+      inl.forM versoSyntaxToString'
+      endBlock
+    | `(block|para[$inl*]) =>
+      startBlock
+      inl.forM versoSyntaxToString'
+      endBlock
+    | `(block|ul{$items*}) =>
+      startBlock
+      items.forM fun
+        | `(list_item|* $blks*) => do
+          out "* "
+          withReader (· + 2) (blks.forM versoSyntaxToString')
+          endBlock
+        | _ => pure ()
+      endBlock
+    | `(block|ol($n){$items*}) =>
+      startBlock
+      let mut n := n.getNat
+      for item in items do
+        match item with
+        | `(list_item|* $blks*) => do
+          out s!"{n}. "
+          withReader (· + 2) (blks.forM versoSyntaxToString')
+          endBlock
+          n := n + 1
+        | _ => pure ()
+      endBlock
+    | `(block| > $blks*) =>
+      startBlock
+      out "> "
+      withReader (· + 2) (blks.forM versoSyntaxToString')
+      endBlock
+    | `(block| ```%$tk1 $name $args* | $s ```%$tk2) =>
+      startBlock
+      out <| atomString tk1
+      out <| identString name
+      for arg in args do
+        out " "
+        versoSyntaxToString' arg
+      out "\n"
+      let i ← read
+      let s := Syntax.decodeStrLit (atomString s) |>.getD ""
+        |>.split (· == '\n')
+        |>.map ("".pushn ' ' i ++ · ) |> "\n".intercalate
+      out s
+      out <| "".pushn ' ' i
+      out <| atomString tk2
+      endBlock
+    | `(block| :::%$tk1 $name $args* {$blks*}%$tk2) =>
+      startBlock
+      out <| atomString tk1
+      out " "
+      out <| identString name
+      for arg in args do
+        out " "
+        versoSyntaxToString' arg
+      out "\n"
+      blks.forM versoSyntaxToString'
+      let i ← read
+      out <| "".pushn ' ' i
+      out <| atomString tk2
+      endBlock
+    | `(block|command{ $name $args* }) =>
+      startBlock
+      out <| "{"
+      out <| identString name
+      for arg in args do
+        out " "
+        versoSyntaxToString' arg
+      out "}"
+      endBlock
+
+    | other => out (toString other)
+where
+  out (s : String) : ReaderT Nat (StateM String) Unit := modify (· ++ s)
+  nl : ReaderT Nat (StateM String) Unit := read >>= fun n => modify (· ++ "\n".pushn ' ' n)
+  startBlock : ReaderT Nat (StateM String) Unit := do
+    let s ← get
+    if s.endsWith "\n" then
+      let i ← read
+      out ("".pushn ' ' i)
+  endBlock : ReaderT Nat (StateM String) Unit := do
+    let s ← get
+    if s.endsWith "\n\n" then return
+    else if s.endsWith "\n" then out "\n"
+    else out "\n\n"
+
+def formatMetadata : Formatter := do
+  visitArgs do
+    pushLine
+    visitAtom .anonymous
+    pushLine
+    metadataContents.formatter
+    pushLine
+    visitAtom .anonymous
+
+def versoSyntaxToString (stx : Syntax) : String :=
+  versoSyntaxToString' stx |>.run 0 |>.run "" |>.2
+
+public def document.formatter : Formatter := concat do
+  let stx ← getCur
+  let i := stx.getArgs.size
+  visitArgs do
+    for _ in [0:i] do
+      let blk ← getCur
+      if blk.getKind == ``Doc.Syntax.metadata_block then
+        formatMetadata
+      else
+        push (versoSyntaxToString blk)
+        goLeft

src/Lean/DocString/Markdown.lean

@@ -85,11 +85,20 @@ Generates Markdown, rendering the result from the final state, without producing
 public def MarkdownM.run' (act : MarkdownM Unit) (context : Context := {}) (state : State := {}) : String :=
   act.run context state |>.2
 
-private def MarkdownM.push (txt : String) : MarkdownM Unit := modify (·.push txt)
+/--
+Adds a string to the current Markdown output.
+-/
+public def MarkdownM.push (txt : String) : MarkdownM Unit := modify (·.push txt)
 
-private def MarkdownM.endBlock : MarkdownM Unit := modify (·.endBlock)
+/--
+Terminates the current block.
+-/
+public def MarkdownM.endBlock : MarkdownM Unit := modify (·.endBlock)
 
-private def MarkdownM.indent: MarkdownM α → MarkdownM α :=
+/--
+Increases the indentation level by one.
+-/
+public def MarkdownM.indent: MarkdownM α → MarkdownM α :=
   withReader fun st => { st with linePrefix := st.linePrefix ++ "  " }
 
 /--
@@ -159,6 +168,41 @@ private def quoteCode (str : String) : String := Id.run do
   let str := if str.startsWith "`" || str.endsWith "`" then " " ++ str ++ " " else str
   backticks ++ str ++ backticks
 
+private partial def trimLeft (inline : Inline i) : (String × Inline i) := go [inline]
+where
+  go : List (Inline i) → String × Inline i
+    | [] => ("", .empty)
+    | .text s :: more =>
+      if s.all (·.isWhitespace) then
+        let (pre, post) := go more
+        (s ++ pre, post)
+      else
+        let s1 := s.takeWhile (·.isWhitespace)
+        let s2 := s.drop s1.length
+        (s1, .text s2 ++ .concat more.toArray)
+    | .concat xs :: more => go (xs.toList ++ more)
+    | here :: more => ("", here ++ .concat more.toArray)
+
+private partial def trimRight (inline : Inline i) : (Inline i × String) := go [inline]
+where
+  go : List (Inline i) → Inline i × String
+    | [] => (.empty, "")
+    | .text s :: more =>
+      if s.all (·.isWhitespace) then
+        let (pre, post) := go more
+        (pre, post ++ s)
+      else
+        let s1 := s.takeRightWhile (·.isWhitespace)
+        let s2 := s.dropRight s1.length
+        (.concat more.toArray.reverse ++ .text s2, s1)
+    | .concat xs :: more => go (xs.reverse.toList ++ more)
+    | here :: more => (.concat more.toArray.reverse ++ here, "")
+
+private def trim (inline : Inline i) : (String × Inline i × String) :=
+  let (pre, more) := trimLeft inline
+  let (mid, post) := trimRight more
+  (pre, mid, post)
+
 open MarkdownM in
 private partial def inlineMarkdown [MarkdownInline i] : Inline i → MarkdownM Unit
   | .text s =>
@@ -166,19 +210,25 @@ private partial def inlineMarkdown [MarkdownInline i] : Inline i → MarkdownM U
   | .linebreak s => do
     push <| s.replace "\n" ("\n" ++ (← read).linePrefix )
   | .emph xs => do
+    let (pre, mid, post) := trim (.concat xs)
+    push pre
     unless (← read).inEmph do
       push "*"
     withReader (fun ρ => { ρ with inEmph := true }) do
-      for i in xs do inlineMarkdown i
+      inlineMarkdown mid
     unless (← read).inEmph do
       push "*"
+    push post
   | .bold xs => do
+    let (pre, mid, post) := trim (.concat xs)
+    push pre
     unless (← read).inBold do
       push "**"
     withReader (fun ρ => { ρ with inEmph := true }) do
-      for i in xs do inlineMarkdown i
+      inlineMarkdown mid
     unless (← read).inBold do
       push "**"
+    push post
   | .concat xs =>
     for i in xs do inlineMarkdown i
   | .link content url => do

src/Lean/DocString/Parser.lean

@@ -7,6 +7,8 @@ module
 prelude
 public import Lean.Parser.Types
 public import Lean.DocString.Syntax
+import Lean.PrettyPrinter.Formatter
+import Lean.Parser.Term.Basic
 
 set_option linter.missingDocs true
 
@@ -231,6 +233,16 @@ public def fakeAtom (str : String) (info : SourceInfo := SourceInfo.none) : Pars
   let atom := .atom info str
   s.pushSyntax atom
 
+/--
+Construct a “fake” atom with the given string content, with zero-width source information at the
+current position.
+
+Normally, atoms are always substrings of the original input; however, Verso's concrete syntax is
+different enough from Lean's that this isn't always a good match.
+-/
+private def fakeAtomHere (str : String) : ParserFn :=
+  withInfoSyntaxFn skip.fn (fun info => fakeAtom str (info := info))
+
 private def pushMissing : ParserFn := fun _c s =>
   s.pushSyntax .missing
 
@@ -586,7 +598,7 @@ A linebreak that isn't a block break (that is, there's non-space content on the
 def linebreak (ctxt : InlineCtxt) : ParserFn :=
   if ctxt.allowNewlines then
     nodeFn ``linebreak <|
-      andthenFn (withInfoSyntaxFn skip.fn (fun info => fakeAtom "line!" info)) <|
+      andthenFn (fakeAtomHere "line!") <|
         nodeFn strLitKind <|
         asStringFn (quoted := true) <|
           atomicFn (chFn '\n' >> lookaheadFn (manyFn (chFn ' ') >> notFollowedByFn (chFn '\n' <|> blockOpener) "newline"))
@@ -795,6 +807,9 @@ open Lean.Parser.Term in
 def metadataContents : Parser :=
   structInstFields (sepByIndent structInstField ", " (allowTrailingSep := true))
 
+def withPercents : ParserFn → ParserFn := fun p =>
+  adaptUncacheableContextFn (fun c => {c with tokens := c.tokens.insert "%%%" "%%%"}) p
+
 open Lean.Parser.Term in
 /--
 Parses a metadata block, which contains the contents of a Lean structure initialization but is
@@ -803,8 +818,7 @@ surrounded by `%%%` on each side.
 public def metadataBlock : ParserFn :=
   nodeFn ``metadata_block <|
     opener >>
-    metadataContents.fn >>
-    takeWhileFn (·.isWhitespace) >>
+    withPercents metadataContents.fn >>
     closer
 where
   opener := atomicFn (bolThen (eatSpaces >> strFn "%%%") "%%% (at line beginning)") >> eatSpaces >> ignoreFn (chFn '\n')
@@ -956,35 +970,35 @@ mutual
     nodeFn ``ul <|
       lookaheadUnorderedListIndicator ctxt fun type =>
         withCurrentColumn fun c =>
-          fakeAtom "ul{" >>
+          fakeAtomHere "ul{" >>
           many1Fn (listItem {ctxt with minIndent := c + 1 , inLists := ⟨c, .inr type⟩  :: ctxt.inLists}) >>
-          fakeAtom "}"
+          fakeAtomHere "}"
 
   /-- Parses an ordered list. -/
   public partial def orderedList (ctxt : BlockCtxt) : ParserFn :=
     nodeFn ``ol <|
-      fakeAtom "ol(" >>
+      fakeAtomHere "ol(" >>
       lookaheadOrderedListIndicator ctxt fun type _start => -- TODO? Validate list numbering?
         withCurrentColumn fun c =>
-          fakeAtom ")" >> fakeAtom "{" >>
+          fakeAtomHere ")" >> fakeAtomHere "{" >>
           many1Fn (listItem {ctxt with minIndent := c + 1 , inLists := ⟨c, .inl type⟩  :: ctxt.inLists}) >>
-          fakeAtom "}"
+          fakeAtomHere "}"
 
   /-- Parses a definition list. -/
   public partial def definitionList (ctxt : BlockCtxt) : ParserFn :=
     nodeFn ``dl <|
       atomicFn (onlyBlockOpeners >> takeWhileFn (· == ' ') >> ignoreFn (lookaheadFn (chFn ':' >> chFn ' ')) >> guardMinColumn ctxt.minIndent) >>
-      withInfoSyntaxFn skip.fn (fun info => fakeAtom "dl{" info) >>
+      fakeAtomHere "dl{" >>
       withCurrentColumn (fun c => many1Fn (descItem {ctxt with minIndent := c})) >>
-      withInfoSyntaxFn skip.fn (fun info => fakeAtom "}" info)
+      fakeAtomHere "}"
 
   /-- Parses a paragraph (that is, a sequence of otherwise-undecorated inlines). -/
   public partial def para (ctxt : BlockCtxt) : ParserFn :=
     nodeFn ``para <|
       atomicFn (takeWhileFn (· == ' ') >> notFollowedByFn blockOpener "block opener" >> guardMinColumn ctxt.minIndent) >>
-      withInfoSyntaxFn skip.fn (fun info => fakeAtom "para{" (info := info)) >>
+      fakeAtomHere "para{" >>
       textLine >>
-      withInfoSyntaxFn skip.fn (fun info => fakeAtom "}" (info := info))
+      fakeAtomHere "}"
 
   /-- Parses a header. -/
   public partial def header (ctxt : BlockCtxt) : ParserFn :=
@@ -999,7 +1013,7 @@ mutual
             fakeAtom ")") >>
       fakeAtom "{" >>
       textLine (allowNewlines := false) >>
-      fakeAtom "}"
+      fakeAtomHere "}"
 
   /--
   Parses a code block. The resulting string literal has already had the fences' leading indentation
@@ -1170,3 +1184,56 @@ mutual
   -/
   public partial def document (blockContext : BlockCtxt := {}) : ParserFn := ignoreFn (manyFn blankLine) >> blocks blockContext
 end
+
+section
+open Lean.PrettyPrinter
+
+/--
+Parses as `ifVerso` if the option `doc.verso` is `true`, or as `ifNotVerso` otherwise.
+-/
+public def ifVersoFn (ifVerso ifNotVerso : ParserFn) : ParserFn := fun c s =>
+  if c.options.getBool `doc.verso then ifVerso c s
+  else ifNotVerso c s
+
+@[inherit_doc ifVersoFn]
+public def ifVerso (ifVerso ifNotVerso : Parser) : Parser where
+  fn :=
+    ifVersoFn ifVerso.fn ifNotVerso.fn
+
+/--
+Formatter for `ifVerso`—formats according to the underlying formatters.
+-/
+@[combinator_formatter ifVerso, expose]
+public def ifVerso.formatter (f1 f2 : Formatter) : Formatter := f1 <|> f2
+
+/--
+Parenthesizer for `ifVerso`—parenthesizes according to the underlying parenthesizers.
+-/
+@[combinator_parenthesizer ifVerso, expose]
+public def ifVerso.parenthesizer (p1 p2 : Parenthesizer) : Parenthesizer := p1 <|> p2
+
+/--
+Disables the option `doc.verso` while running a parser.
+-/
+public def withoutVersoSyntax (p : Parser) : Parser where
+  fn :=
+    adaptUncacheableContextFn
+      (fun c => { c with options := c.options.setBool `doc.verso false })
+      p.fn
+  info := p.info
+
+/--
+Formatter for `withoutVersoSyntax`—formats according to the underlying formatter.
+-/
+@[combinator_formatter withoutVersoSyntax, expose]
+public def withoutVersoSyntax.formatter (p : Formatter) : Formatter := p
+/--
+Parenthesizer for `withoutVersoSyntax`—parenthesizes according to the underlying parenthesizer.
+-/
+@[combinator_parenthesizer withoutVersoSyntax, expose]
+public def withoutVersoSyntax.parenthesizer (p : Parenthesizer) : Parenthesizer := p
+
+end
+
+builtin_initialize
+  register_parser_alias withoutVersoSyntax

src/Lean/DocString/Syntax.lean

@@ -7,14 +7,8 @@ Author: David Thrane Christiansen
 module
 
 prelude
-
-import Init.Prelude
-import Init.Notation
-public import Lean.Parser.Types
-import Lean.Syntax
-import Lean.Parser.Extra
-public import Lean.Parser.Term
-meta import Lean.Parser.Term
+public import Lean.Parser.Term.Basic
+meta import Lean.Parser.Term.Basic
 
 
 /-!
@@ -63,22 +57,28 @@ scoped syntax (name:=arg_num) num : arg_val
 
 /-- Arguments -/
 declare_syntax_cat doc_arg
-/-- Anonymous positional arguments -/
+/-- Anonymous positional argument -/
+@[builtin_doc]
 scoped syntax (name:=anon) arg_val : doc_arg
-/-- Named arguments -/
+/-- Named argument -/
+@[builtin_doc]
 scoped syntax (name:=named) "(" ident " := " arg_val ")": doc_arg
-/-- Named arguments, without parentheses. -/
+@[inherit_doc named, builtin_doc]
 scoped syntax (name:=named_no_paren) ident " := " arg_val : doc_arg
-/-- Boolean flags, turned on -/
+/-- Boolean flag, turned on -/
+@[builtin_doc]
 scoped syntax (name:=flag_on) "+" ident : doc_arg
-/-- Boolean flags, turned off -/
+/-- Boolean flag, turned off -/
+@[builtin_doc]
 scoped syntax (name:=flag_off) "-" ident : doc_arg
 
 /-- Link targets, which may be URLs or named references -/
 declare_syntax_cat link_target
-/-- A reference to a URL -/
+/-- A URL target, written explicitly. Use square brackets for a named target. -/
+@[builtin_doc]
 scoped syntax (name:=url) "(" str ")" : link_target
-/-- A named reference -/
+/-- A named reference to a URL defined elsewhere. Use parentheses to write the URL here. -/
+@[builtin_doc]
 scoped syntax (name:=ref) "[" str "]" : link_target
 
 /--
@@ -91,26 +91,87 @@ This syntax uses the following conventions:
 -/
 declare_syntax_cat inline
 scoped syntax (name:=text) str : inline
-/-- Emphasis (often rendered as italics) -/
+/--
+Emphasis, often rendered as italics.
+
+Emphasis may be nested by using longer sequences of `_` for the outer delimiters. For example:
+```
+Remember: __always butter the _rugbrød_ before adding toppings!__
+```
+Here, the outer `__` is used to emphasize the instructions, while the inner `_` indicates the use of
+a non-English word.
+-/
+@[builtin_doc]
 scoped syntax (name:=emph) "_[" inline* "]" : inline
-/-- Bold emphasis   -/
+/--
+Bold emphasis.
+
+A single `*` suffices to make text bold. Using `_` for emphasis.
+
+Bold text may be nested by using longer sequences of `*` for the outer delimiters.
+-/
+@[builtin_doc]
 scoped syntax (name:=bold) "*[" inline* "]" : inline
-/-- Link -/
+/--
+A link. The link's target may either be a concrete URL (written in parentheses) or a named URL
+(written in square brackets).
+-/
+@[builtin_doc]
 scoped syntax (name:=link) "link[" inline* "]" link_target : inline
-/-- Image -/
+/--
+An image, with alternate text and a URL.
+
+The alternate text is a plain string, rather than Verso markup.
+
+The image URL may either be a concrete URL (written in parentheses) or a named URL (written in
+square brackets).
+-/
+
+@[builtin_doc]
 scoped syntax (name:=image) "image(" str ")" link_target : inline
-/-- A footnote use -/
+/--
+A footnote use site.
+
+Footnotes must be defined elsewhere using the `[^NAME]: TEXT` syntax.
+-/
+@[builtin_doc]
 scoped syntax (name:=footnote) "footnote(" str ")" : inline
-/-- Line break -/
 scoped syntax (name:=linebreak) "line!" str : inline
-/-- Literal code. If the first and last characters are space, and it contains at least one non-space
-  character, then the resulting string has a single space stripped from each end.-/
+/--
+Literal code.
+
+Code may begin with any non-zero number of backticks. It must be terminated with the same number,
+and it may not contain a sequence of backticks that is at least as long as its starting or ending
+delimiters.
+
+If the first and last characters are space, and it contains at least one non-space character, then
+the resulting string has a single space stripped from each end. Thus, ``` `` `x `` ``` represents
+``"`x"``, not ``" `x "``.
+-/
+@[builtin_doc]
 scoped syntax (name:=code) "code(" str ")" : inline
-/-- A _role_: an extension to the Verso document language in an inline position -/
+/--
+A _role_: an extension to the Verso document language in an inline position.
+
+Text is given a role using the following syntax: `{NAME ARGS*}[CONTENT]`. The `NAME` is an
+identifier that determines which role is being used, akin to a function name. Each of the `ARGS` may
+have the following forms:
+* A value, which is a string literal, natural number, or identifier
+* A named argument, of the form `(NAME := VALUE)`
+* A flag, of the form `+NAME` or `-NAME`
+
+The `CONTENT` is a sequence of inline content. If there is only one piece of content and it has
+beginning and ending delimiters (e.g. code literals, links, or images, but not ordinary text), then
+the `[` and `]` may be omitted. In particular, `` {NAME ARGS*}`x` `` is equivalent to
+``{NAME ARGS*}[`x`]``.
+-/
+@[builtin_doc]
 scoped syntax (name:=role) "role{" ident doc_arg* "}" "[" inline* "]"  : inline
 /-- Inline mathematical notation (equivalent to LaTeX's `$` notation) -/
+@[builtin_doc]
 scoped syntax (name:=inline_math) "\\math" code : inline
 /-- Display-mode mathematical notation -/
+@[builtin_doc]
 scoped syntax (name:=display_math) "\\displaymath" code : inline
 
 /--
@@ -132,40 +193,130 @@ declare_syntax_cat block
 
 /-- Items from both ordered and unordered lists -/
 declare_syntax_cat list_item
-/-- List item -/
+/-- A list item -/
+@[builtin_doc]
 syntax (name:=li) "*" block* : list_item
 
 /-- A description of an item -/
 declare_syntax_cat desc_item
 /-- A description of an item -/
+@[builtin_doc]
 scoped syntax (name:=desc) ":" inline* "=>" block* : desc_item
 
+/-- Paragraph -/
+@[builtin_doc]
 scoped syntax (name:=para) "para[" inline+ "]" : block
 /-- Unordered List -/
+@[builtin_doc]
 scoped syntax (name:=ul) "ul{" list_item* "}" : block
-/-- Definition list -/
+/-- Description list -/
+@[builtin_doc]
 scoped syntax (name:=dl) "dl{" desc_item* "}" : block
 /-- Ordered list -/
+@[builtin_doc]
 scoped syntax (name:=ol) "ol(" num ")" "{" list_item* "}" : block
-/-- Literal code -/
+/--
+A code block that contains literal code.
+
+Code blocks have the following syntax:
+````
+```(NAME ARGS*)?
+CONTENT
+```
+````
+
+`CONTENT` is a literal string. If the `CONTENT` contains a sequence of three or more backticks, then
+the opening and closing ` ``` ` (called _fences_) should have more backticks than the longest
+sequence in `CONTENT`. Additionally, the opening and closing fences should have the same number of
+backticks.
+
+If `NAME` and `ARGS` are not provided, then the code block represents literal text. If provided, the
+`NAME` is an identifier that selects an interpretation of the block. Unlike Markdown, this name is
+not necessarily the language in which the code is written, though many custom code blocks are, in
+practice, named after the language that they contain. `NAME` is more akin to a function name. Each
+of the `ARGS` may have the following forms:
+* A value, which is a string literal, natural number, or identifier
+* A named argument, of the form `(NAME := VALUE)`
+* A flag, of the form `+NAME` or `-NAME`
+
+The `CONTENT` is interpreted according to the indentation of the fences. If the fences are indented
+`n` spaces, then `n` spaces are removed from the start of each line of `CONTENT`.
+-/
+@[builtin_doc]
 scoped syntax (name:=codeblock) "```" (ident doc_arg*)? "|" str "```" : block
-/-- Quotation -/
+/--
+A quotation, which contains a sequence of blocks that are at least as indented as the `>`.
+-/
+@[builtin_doc]
 scoped syntax (name:=blockquote) ">" block* : block
-/-- A link reference definition -/
+/--
+A named URL that can be used in links and images.
+-/
+@[builtin_doc]
 scoped syntax (name:=link_ref)  "[" str "]:" str : block
-/-- A footnote definition -/
+/--
+A footnote definition.
+-/
+@[builtin_doc]
 scoped syntax (name:=footnote_ref) "[^" str "]:" inline* : block
-/-- Custom directive -/
+/--
+A _directive_, which is an extension to the Verso language in block position.
+
+Directives have the following syntax:
+```
+:::NAME ARGS*
+CONTENT*
+:::
+```
+
+The `NAME` is an identifier that determines which directive is being used, akin to a function name.
+Each of the `ARGS` may have the following forms:
+* A value, which is a string literal, natural number, or identifier
+* A named argument, of the form `(NAME := VALUE)`
+* A flag, of the form `+NAME` or `-NAME`
+
+The `CONTENT` is a sequence of block content. Directives may be nested by using more colons in
+the outer directive. For example:
+```
+::::outer +flag (arg := 5)
+A paragraph.
+:::inner "label"
+* 1
+* 2
+:::
+::::
+```
+
+-/
+@[builtin_doc]
 scoped syntax (name:=directive) ":::" rawIdent doc_arg* "{" block:max* "}" : block
-/-- A header -/
+/--
+A header
+
+Headers must be correctly nested to form a tree structure. The first header in a document must
+start with `#`, and subsequent headers must have at most one more `#` than the preceding header.
+-/
+@[builtin_doc]
 scoped syntax (name:=header) "header(" num ")" "{" inline+ "}" : block
 
 open Lean.Parser Term in
-meta def metadataContents : Parser :=
+meta def metadataContents : Lean.Parser.Parser :=
   structInstFields (sepByIndent structInstField ", " (allowTrailingSep := true))
 
-/-- Metadata for this section, defined by the current genre -/
+/--
+Metadata for the preceding header.
+-/
+@[builtin_doc]
 scoped syntax (name:=metadata_block) "%%%" metadataContents "%%%" : block
 
-/-- A block-level command -/
+/--
+A block-level command, which invokes an extension during documentation processing.
+
+The `NAME` is an identifier that determines which command is being used, akin to a function name.
+Each of the `ARGS` may have the following forms:
+* A value, which is a string literal, natural number, or identifier
+* A named argument, of the form `(NAME := VALUE)`
+* A flag, of the form `+NAME` or `-NAME`
+-/
+@[builtin_doc]
 scoped syntax (name:=command) "command{" rawIdent doc_arg* "}" : block

src/Lean/Elab/BuiltinCommand.lean

@@ -23,13 +23,20 @@ public section
 namespace Lean.Elab.Command
 
 @[builtin_command_elab moduleDoc] def elabModuleDoc : CommandElab := fun stx => do
+  let some range ← Elab.getDeclarationRange? stx
+    | return  -- must be from partial syntax, ignore
+
   match stx[1] with
   | Syntax.atom _ val =>
-    let doc := val.extract 0 (val.endPos - ⟨2⟩)
-    let some range ← Elab.getDeclarationRange? stx
-      | return  -- must be from partial syntax, ignore
-    modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩
-  | _ => throwErrorAt stx "unexpected module doc string{indentD stx[1]}"
+    if getVersoModuleDocs (← getEnv) |>.isEmpty then
+      let doc := val.extract 0 (val.endPos - ⟨2⟩)
+      modifyEnv fun env => addMainModuleDoc env ⟨doc, range⟩
+    else
+      throwError m!"Can't add Markdown-format module docs because there is already Verso-format content present."
+  | Syntax.node _ ``Lean.Parser.Command.versoCommentBody args =>
+    runTermElabM fun _ => do
+      addVersoModDocString range ⟨args.getD 0 .missing⟩
+  | _ => throwErrorAt stx "unexpected module doc string{indentD <| stx}"
 
 private def addScope (isNewNamespace : Bool) (header : String) (newNamespace : Name)
     (isNoncomputable isPublic : Bool := false) (attrs : List (TSyntax ``Parser.Term.attrInstance) := []) :

src/Lean/Elab/DocString.lean

@@ -12,6 +12,8 @@ public import Lean.Elab.Term.TermElabM
 public import Lean.Elab.Command.Scope
 import Lean.DocString.Syntax
 import Lean.Meta.Hint
+import Lean.DocString.Markdown
+import Lean.BuiltinDocAttr
 
 set_option linter.missingDocs true
 
@@ -22,7 +24,6 @@ open Std
 open scoped Lean.Doc.Syntax
 
 
-
 public section
 
 private structure ElabLink where
@@ -112,8 +113,6 @@ deriving BEq, Repr
 
 /-- Context used as a reader in `DocM`. -/
 structure Context where
-  /-- The declaration for which documentation is being elaborated. -/
-  declName : Name
   /-- Whether suggestions should be provided interactively. -/
   suggestionMode : SuggestionMode
 
@@ -140,32 +139,95 @@ instance : MonadLift TermElabM DocM where
       act
     return v
 
+private structure ModuleDocstringState extends Lean.Doc.State where
+  scopedExts : Array (ScopedEnvExtension EnvExtensionEntry EnvExtensionEntry EnvExtensionState)
+
+
+private builtin_initialize modDocstringStateExt : EnvExtension (Option ModuleDocstringState) ←
+  registerEnvExtension (pure none)
+
+private def getModState
+    [Monad m] [MonadEnv m] [MonadLiftT IO m] [MonadLCtx m]
+    [MonadResolveName m] [MonadOptions m] : m ModuleDocstringState := do
+  if let some st := modDocstringStateExt.getState (← getEnv) then
+    return st
+  else
+    let lctx ← getLCtx
+    let openDecls ← getOpenDecls
+    let options ← getOptions
+    let scopes := [{header := "", isPublic := true}]
+    let st : ModuleDocstringState := { scopes, openDecls, lctx, options, scopedExts := #[] }
+    modifyEnv fun env =>
+      modDocstringStateExt.setState env st
+    return st
+
+private def setModState [Monad m] [MonadEnv m] (state : ModuleDocstringState) : m Unit := do
+  modifyEnv fun env =>
+    modDocstringStateExt.setState env state
+
+/--
+Runs a documentation elaborator in the module docstring context.
+-/
+def DocM.execForModule (act : DocM α) (suggestionMode : SuggestionMode := .interactive) :
+    TermElabM α := withoutModifyingEnv do
+  let sc ← scopedEnvExtensionsRef.get
+  let st ← getModState
+  try
+    scopedEnvExtensionsRef.set st.scopedExts
+    let ((v, _), _) ←
+      act.run { suggestionMode } |>.run {} |>.run st.toState
+    pure v
+  finally
+    scopedEnvExtensionsRef.set sc
+
 open Lean.Parser.Term in
 /--
-Runs a documentation elaborator, discarding changes made to the environment.
+Runs a documentation elaborator in a declaration's context, discarding changes made to the
+environment.
 -/
 def DocM.exec (declName : Name) (binders : Syntax) (act : DocM α)
     (suggestionMode : SuggestionMode := .interactive) :
     TermElabM α := withoutModifyingEnv do
   let some ci := (← getEnv).constants.find? declName
     | throwError "Unknown constant {declName} when building docstring"
-  let (lctx, localInstances) ← buildContext ci.type binders
-  let sc ← scopedEnvExtensionsRef.get
+  let st ← Term.saveState
+  Core.resetMessageLog -- We'll replay the messages after the elab loop
   try
-    let openDecls ← getOpenDecls
-    let options ← getOptions
-    let scopes := [{header := "", isPublic := true}]
-    let ((v, _), _) ← withTheReader Meta.Context (fun ρ => { ρ with localInstances }) <|
-      act.run { declName, suggestionMode } |>.run {} |>.run { scopes, openDecls, lctx, options }
-    pure v
+    let (lctx, localInstances) ← buildContext ci.type binders
+    let sc ← scopedEnvExtensionsRef.get
+    try
+      let openDecls ← getOpenDecls
+      let options ← getOptions
+      let scopes := [{header := "", isPublic := true}]
+      let ((v, _), _) ← withTheReader Meta.Context (fun ρ => { ρ with localInstances }) <|
+        act.run { suggestionMode } |>.run {} |>.run { scopes, openDecls, lctx, options }
+      pure v
+    finally
+      scopedEnvExtensionsRef.set sc
   finally
-    scopedEnvExtensionsRef.set sc
+    let msgs ← Core.getMessageLog
+    st.restore
+    Core.setMessageLog ((← Core.getMessageLog) ++ msgs)
 where
   buildContext (type : Expr) (binders : Syntax) : TermElabM (LocalContext × LocalInstances) := do
-    -- Create a local context with all binders
+    -- Create a local context with all binders. The type will be updated as we introduce parameters.
     let mut type := type
-    let mut localInstances := (← readThe Meta.Context).localInstances
-    let mut lctx := ← getLCtx
+
+    -- We start with a local context that's reset to only include section variables
+    let mut localInstances ← Meta.getLocalInstances
+    let mut lctx ← getLCtx
+    let sectionFVars := (← read).sectionFVars.valuesArray.filterMap fun
+      | .fvar fv => some fv
+      | _ => none
+    repeat
+      if lctx.size = 0 then break
+      if let some decl := lctx.lastDecl then
+        if sectionFVars.any (· == decl.fvarId) then break
+        else
+          lctx := lctx.pop
+          localInstances := localInstances.filter (·.fvar != .fvar decl.fvarId)
+      else break
+
     let names ← binders.getArgs.flatMapM binderNames
     let mut i := 0
     let mut x := none
@@ -724,6 +786,8 @@ builtin_initialize registerBuiltinAttribute {
     let ret := .app (.const ``Inline [0]) (.const ``ElabInline [])
     let ((wrapper, _), _) ← genWrapper decl (some argTy) ret |>.run {} {} |>.run {} {}
     docRoleExt.add (roleName, wrapper)
+    if (← findInternalDocString? (← getEnv) decl).isSome then
+      addInheritedDocString wrapper decl
 }
 
 /--
@@ -749,8 +813,12 @@ builtin_initialize registerBuiltinAttribute {
         (mkApp3 (.const ``List.cons [0]) (.const ``SyntaxNodeKind []) (toExpr `inline) (.app (.const ``List.nil [0]) (.const ``SyntaxNodeKind [])))
     let ret := .app (.const ``Inline [0]) (.const ``ElabInline [])
     let ((wrapper, _), _) ← genWrapper decl (some argTy) ret |>.run {} {} |>.run {} {}
+    addDeclarationRangesFromSyntax wrapper stx
     declareBuiltin roleName <|
       mkApp3 (.const ``addBuiltinDocRole []) (toExpr roleName) (toExpr wrapper) (.const wrapper [])
+    if (← findInternalDocString? (← getEnv) decl).isSome then
+      addInheritedDocString wrapper decl
+    declareBuiltinDocStringAndRanges wrapper
 }
 
 builtin_initialize registerBuiltinAttribute {
@@ -766,6 +834,8 @@ builtin_initialize registerBuiltinAttribute {
     let ret := mkApp2 (.const ``Block [0, 0]) (.const ``ElabInline []) (.const ``ElabBlock [])
     let ((wrapper, _), _) ← genWrapper decl (some (.const ``StrLit [])) ret |>.run {} {} |>.run {} {}
     docCodeBlockExt.add (blockName, wrapper)
+    if (← findInternalDocString? (← getEnv) decl).isSome then
+      addInheritedDocString wrapper decl
 }
 
 /--
@@ -788,9 +858,13 @@ builtin_initialize registerBuiltinAttribute {
         pure decl
     let ret := mkApp2 (.const ``Block [0, 0]) (.const ``ElabInline []) (.const ``ElabBlock [])
     let ((wrapper, _), _) ← genWrapper decl (some (.const ``StrLit [])) ret |>.run {} {} |>.run {} {}
+    addDeclarationRangesFromSyntax wrapper stx
     declareBuiltin blockName <|
       mkApp3 (.const ``addBuiltinDocCodeBlock [])
         (toExpr blockName) (toExpr wrapper) (.const wrapper [])
+    if (← findInternalDocString? (← getEnv) decl).isSome then
+      addInheritedDocString wrapper decl
+    declareBuiltinDocStringAndRanges wrapper
 }
 
 /-- A suggestion about an applicable code block -/
@@ -872,6 +946,9 @@ builtin_initialize registerBuiltinAttribute {
     let ret := mkApp2 (.const ``Block [0, 0]) (.const ``ElabInline []) (.const ``ElabBlock [])
     let ((wrapper, _), _) ← genWrapper decl (some argTy) ret |>.run {} {} |>.run {} {}
     docDirectiveExt.add (directiveName, wrapper)
+    if (← findInternalDocString? (← getEnv) decl).isSome then
+      addInheritedDocString wrapper decl
+
 }
 
 /--
@@ -897,9 +974,13 @@ builtin_initialize registerBuiltinAttribute {
         (mkApp3 (.const ``List.cons [0]) (.const ``SyntaxNodeKind []) (toExpr `block) (.app (.const ``List.nil [0]) (.const ``SyntaxNodeKind [])))
     let ret := mkApp2 (.const ``Block [0, 0]) (.const ``ElabInline []) (.const ``ElabBlock [])
     let ((wrapper, _), _) ← genWrapper decl (some argTy) ret |>.run {} {} |>.run {} {}
+    addDeclarationRangesFromSyntax wrapper stx
     declareBuiltin directiveName <|
       mkApp3 (.const ``addBuiltinDocDirective [])
         (toExpr directiveName) (toExpr wrapper) (.const wrapper [])
+    if (← findInternalDocString? (← getEnv) decl).isSome then
+      addInheritedDocString wrapper decl
+    declareBuiltinDocStringAndRanges wrapper
 }
 
 builtin_initialize registerBuiltinAttribute {
@@ -916,6 +997,8 @@ builtin_initialize registerBuiltinAttribute {
     let ret := mkApp2 (.const ``Block [0, 0]) (.const ``ElabInline []) (.const ``ElabBlock [])
     let ((wrapper, _), _) ← genWrapper decl none ret |>.run {} {} |>.run {} {}
     docCommandExt.add (commandName, wrapper)
+    if (← findInternalDocString? (← getEnv) decl).isSome then
+      addInheritedDocString wrapper decl
 }
 
 /--
@@ -939,9 +1022,13 @@ builtin_initialize registerBuiltinAttribute {
 
     let ret := mkApp2 (.const ``Block [0, 0]) (.const ``ElabInline []) (.const ``ElabBlock [])
     let ((wrapper, _), _) ← genWrapper decl none ret |>.run {} {} |>.run {} {}
+    addDeclarationRangesFromSyntax wrapper stx
     declareBuiltin commandName <|
       mkApp3 (.const ``addBuiltinDocCommand [])
         (toExpr commandName) (toExpr wrapper) (.const wrapper [])
+    if (← findInternalDocString? (← getEnv) decl).isSome then
+      addInheritedDocString wrapper decl
+    declareBuiltinDocStringAndRanges wrapper
 }
 end
 
@@ -959,76 +1046,88 @@ private unsafe def codeBlockSuggestionsUnsafe : TermElabM (Array (StrLit → Doc
 @[implemented_by codeBlockSuggestionsUnsafe]
 private opaque codeBlockSuggestions : TermElabM (Array (StrLit → DocM (Array CodeBlockSuggestion)))
 
-private unsafe def roleExpandersForUnsafe (roleName : Ident) : TermElabM (Array (TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline))) := do
+private def builtinElabName (n : Name) : Option Name :=
+  if (`Lean.Doc).isPrefixOf n then some n
+  else if n matches (.str .anonymous _) then some <| `Lean.Doc ++ n
+  else none
+
+private unsafe def roleExpandersForUnsafe (roleName : Ident) :
+    TermElabM (Array (Name × (TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)))) := do
   let x? ←
-    try some <$> realizeGlobalConstNoOverloadWithInfo roleName
+    try some <$> realizeGlobalConstNoOverload roleName
     catch | _ => pure none
   if let some x := x? then
     let names := (docRoleExt.getState (← getEnv)).get? x |>.getD #[]
     let builtins := (← builtinDocRoles.get).get? x |>.getD #[]
-    return (← names.mapM (evalConst _)) ++ builtins.map (·.2)
+    return (← names.mapM (fun x => do return (x, ← evalConst _ x))) ++ builtins
   else
     let x := roleName.getId
     let hasBuiltin :=
       (← builtinDocRoles.get).get? x <|> (← builtinDocRoles.get).get? (`Lean.Doc ++ x)
-    return hasBuiltin.toArray.flatten.map (·.2)
+    return hasBuiltin.toArray.flatten
 
 
 @[implemented_by roleExpandersForUnsafe]
 private opaque roleExpandersFor (roleName : Ident) :
-  TermElabM (Array (TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline)))
+  TermElabM (Array (Name × (TSyntaxArray `inline → StateT (Array (TSyntax `doc_arg)) DocM (Inline ElabInline))))
 
-private unsafe def codeBlockExpandersForUnsafe (codeBlockName : Ident) : TermElabM (Array (StrLit → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))) := do
+private unsafe def codeBlockExpandersForUnsafe (codeBlockName : Ident) :
+    TermElabM (Array (Name × (StrLit → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))) := do
   let x? ←
-    try some <$> realizeGlobalConstNoOverloadWithInfo codeBlockName
+    try some <$> realizeGlobalConstNoOverload codeBlockName
     catch | _ => pure none
   if let some x := x? then
     let names := (docCodeBlockExt.getState (← getEnv)).get? x |>.getD #[]
     let names' := (← builtinDocCodeBlocks.get).get? x |>.getD #[]
-    return (← names.mapM (evalConst _)) ++ names'.map (·.2)
+    return (← names.mapM (fun x => do return (x, ← evalConst _ x))) ++ names'
   else
     let x := codeBlockName.getId
     let hasBuiltin :=
       (← builtinDocCodeBlocks.get).get? x <|> (← builtinDocCodeBlocks.get).get? (`Lean.Doc ++ x)
-    return hasBuiltin.toArray.flatten.map (·.2)
+    return hasBuiltin.toArray.flatten
 
 
 @[implemented_by codeBlockExpandersForUnsafe]
-private opaque codeBlockExpandersFor (codeBlockName : Ident) : TermElabM (Array (StrLit → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))
+private opaque codeBlockExpandersFor (codeBlockName : Ident) :
+  TermElabM (Array (Name × (StrLit → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))))
 
-private unsafe def directiveExpandersForUnsafe (directiveName : Ident) : TermElabM (Array (TSyntaxArray `block → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))) := do
+private unsafe def directiveExpandersForUnsafe (directiveName : Ident) :
+    TermElabM (Array (Name × (TSyntaxArray `block → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))) := do
   let x? ←
-    try some <$> realizeGlobalConstNoOverloadWithInfo directiveName
+    try some <$> realizeGlobalConstNoOverload directiveName
     catch | _ => pure none
   if let some x := x? then
     let names := (docDirectiveExt.getState (← getEnv)).get? x |>.getD #[]
     let names' := (← builtinDocDirectives.get).get? x |>.getD #[]
-    return (← names.mapM (evalConst _)) ++ names'.map (·.2)
+    return (← names.mapM (fun x => do return (x, ← evalConst _ x))) ++ names'
   else
     let x := directiveName.getId
     let hasBuiltin :=
       (← builtinDocDirectives.get).get? x <|> (← builtinDocDirectives.get).get? (`Lean.Doc ++ x)
-    return hasBuiltin.toArray.flatten.map (·.2)
+    return hasBuiltin.toArray.flatten
 
 @[implemented_by directiveExpandersForUnsafe]
-private opaque directiveExpandersFor (directiveName : Ident) : TermElabM (Array (TSyntaxArray `block → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))
+private opaque directiveExpandersFor (directiveName : Ident) :
+  TermElabM (Array (Name × (TSyntaxArray `block → StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))))
 
-private unsafe def commandExpandersForUnsafe (commandName : Ident) : TermElabM (Array (StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))) := do
+private unsafe def commandExpandersForUnsafe (commandName : Ident) :
+    TermElabM (Array (Name × StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock))) := do
   let x? ←
-    try some <$> realizeGlobalConstNoOverloadWithInfo commandName
+    try some <$> realizeGlobalConstNoOverload commandName
     catch | _ => pure none
   if let some x := x? then
     let names := (docCommandExt.getState (← getEnv)).get? x |>.getD #[]
     let names' := (← builtinDocCommands.get).get? x |>.getD #[]
-    return (← names.mapM (evalConst _)) ++ names'.map (·.2)
+    return (← names.mapM (fun x => do return (x, ← evalConst _ x))) ++ names'
   else
     let x := commandName.getId
     let hasBuiltin :=
       (← builtinDocCommands.get).get? x <|> (← builtinDocCommands.get).get? (`Lean.Doc ++ x)
-    return hasBuiltin.toArray.flatten.map (·.2)
+    return hasBuiltin.toArray.flatten
 
 @[implemented_by commandExpandersForUnsafe]
-private opaque commandExpandersFor (commandName : Ident) : TermElabM (Array (StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))
+private opaque commandExpandersFor (commandName : Ident) :
+  TermElabM (Array (Name × StateT (Array (TSyntax `doc_arg)) DocM (Block ElabInline ElabBlock)))
 
 
 private def mkArgVal (arg : TSyntax `arg_val) : DocM Term :=
@@ -1117,12 +1216,17 @@ private def mkSuggestion  (ref : Syntax) (hintTitle : MessageData) (newStrings :
       toMessageData <| Diff.linesToString <| d.filter (·.1 != Action.skip)
     pure m!"\n\nHint: {hintTitle}\n{indentD <| m!"\n".joinSep edits.toList}"
 
+def nameOrBuiltinName [Monad m] [MonadEnv m] (x : Name) : m Name := do
+  let env ← getEnv
+  if env.contains x then return x
+  else return `Lean.Doc ++ x
 
 /--
 Elaborates the syntax of an inline document element to an actual inline document element.
 -/
 public partial def elabInline (stx : TSyntax `inline) : DocM (Inline ElabInline) :=
-  withRef stx do
+  withRef stx <|
+  withInfoContext (mkInfo := pure <| .ofDocInfo {elaborator := decl_name%, stx := stx}) do
   match stx with
   | `(inline|$s:str) =>
     return .text s.getString
@@ -1154,14 +1258,15 @@ public partial def elabInline (stx : TSyntax `inline) : DocM (Inline ElabInline)
         unless suggestions.isEmpty do
           let text ← getFileMap
           let str := text.source.extract b e
-          let ss : Array (String × Option String × Option String) ← suggestions.mapM fun {role, args, moreInfo} => do
-            pure {
-              fst :=
-                "{" ++ (← suggestionName role).toString ++
-                (args.map (" " ++ ·)).getD "" ++ "}" ++ str,
-              snd.fst := none
-              snd.snd := moreInfo.map withSpace
-            }
+          let ss : Array (String × Option String × Option String) ←
+            suggestions.mapM fun {role, args, moreInfo} => do
+              pure {
+                fst :=
+                  "{" ++ (← suggestionName role).toString ++
+                  (args.map (" " ++ ·)).getD "" ++ "}" ++ str,
+                snd.fst := none
+                snd.snd := moreInfo.map withSpace
+              }
           let ss := ss.qsort (fun x y => x.1 < y.1)
           let hint ← mkSuggestion stx m!"Insert a role to document it:" ss
           logWarning m!"Code element could be more specific.{hint}"
@@ -1172,9 +1277,15 @@ public partial def elabInline (stx : TSyntax `inline) : DocM (Inline ElabInline)
     return .math .display s.getString
   | `(inline|role{$name $args*}[$inl*]) =>
     let expanders ← roleExpandersFor name
-    for ex in expanders do
+    for (exName, ex) in expanders do
       try
         let res ← ex inl args <&> (·.1)
+        pushInfoLeaf <| .ofDocElabInfo {
+          elaborator := exName,
+          stx := name,
+          name := exName,
+          kind := .role
+        }
         return res
       catch
         | e@(.internal id _) =>
@@ -1193,7 +1304,8 @@ where
 Elaborates the syntax of an block-level document element to an actual block-level document element.
 -/
 public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline ElabBlock) :=
-  withRef stx do
+  withRef stx <|
+  withInfoContext (mkInfo := pure <| .ofDocInfo {elaborator := decl_name%, stx := stx}) do
   match stx with
   | `(block|para[$inls*]) =>
     .para <$> inls.mapM elabInline
@@ -1231,9 +1343,15 @@ public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline Ela
     return .empty
   | `(block| ::: $name $args* { $content*}) =>
     let expanders ← directiveExpandersFor name
-    for ex in expanders do
+    for (exName, ex) in expanders do
       try
         let res ← ex content args <&> (·.1)
+        pushInfoLeaf <| .ofDocElabInfo {
+          elaborator := exName,
+          stx := name,
+          name := exName,
+          kind := .directive
+        }
         return res
       catch
         | e@(.internal id _) =>
@@ -1253,24 +1371,30 @@ public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline Ela
         unless suggestions.isEmpty do
           let text ← getFileMap
           let str := text.source.extract b e
-          let ss : Array (String × Option String × Option String) ← suggestions.mapM fun {name, args, moreInfo} => do
-            pure {
-              fst :=
-                str ++ (← suggestionName name).toString ++
-                (args.map (" " ++ ·)).getD "",
-              snd.fst := moreInfo.map withSpace
-              snd.snd := none
-            }
+          let ss : Array (String × Option String × Option String) ←
+            suggestions.mapM fun {name, args, moreInfo} => do
+              pure {
+                fst :=
+                  str ++ (← suggestionName name).toString ++
+                  (args.map (" " ++ ·)).getD "",
+                snd.fst := moreInfo.map withSpace
+                snd.snd := none
+              }
           let ss := ss.qsort (fun x y => x.1 < y.1)
           let hint ← mkSuggestion opener m!"Insert a specific kind of code block:" ss
           logWarning m!"Code block could be more specific.{hint}"
-
     return .code s.getString
   | `(block| ```$name $args* | $s ```) =>
     let expanders ← codeBlockExpandersFor name
-    for ex in expanders do
+    for (exName, ex) in expanders do
       try
         let res ← ex s args <&> (·.1)
+        pushInfoLeaf <| .ofDocElabInfo {
+          elaborator := exName,
+          stx := name,
+          name := exName,
+          kind := .codeBlock
+        }
         return res
       catch
         | e@(.internal id _) =>
@@ -1281,9 +1405,15 @@ public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline Ela
     throwErrorAt name "No code block expander for `{name}`"
   | `(block| command{$name $args*}) =>
     let expanders ← commandExpandersFor name
-    for ex in expanders do
+    for (exName, ex) in expanders do
       try
         let res ← ex args <&> (·.1)
+        pushInfoLeaf <| .ofDocElabInfo {
+          elaborator := exName,
+          stx := name,
+          name := exName,
+          kind := .command
+        }
         return res
       catch
         | e@(.internal id _) =>
@@ -1292,6 +1422,12 @@ public partial def elabBlock (stx : TSyntax `block) : DocM (Block ElabInline Ela
           else throw e
         | e => throw e
     throwErrorAt name "No document command elaborator for `{name}`"
+  | `(block|%%%$_*%%%) =>
+    let h ←
+      if stx.raw.getRange?.isSome then m!"Remove it".hint #[""] (ref? := stx)
+      else pure m!""
+    logError m!"Part metadata is not supported in docstrings.{h}"
+    return .empty
   | other => throwErrorAt other "Unsupported syntax: {other}"
 where
   withSpace (s : String) : String :=
@@ -1314,10 +1450,13 @@ private partial def elabBlocks' (level : Nat) :
         else if n = level then
           set xs
           let (content, subParts) ← elabBlocks' (level + 1)
-          let title ← liftM <| name.mapM elabInline
+          let title ←
+            liftM <| withInfoContext (mkInfo := pure <| .ofDocInfo {elaborator := `no_elab, stx := x}) <|
+              name.mapM elabInline
+          let mdTitle := ToMarkdown.toMarkdown (Inline.concat title) |>.run'
           sub := sub.push {
             title,
-            titleString := "" -- TODO get string from filemap?
+            titleString := mdTitle
             metadata := none
             content, subParts
           }
@@ -1331,83 +1470,119 @@ private partial def elabBlocks' (level : Nat) :
         catch
           | e =>
             logErrorAt e.getRef e.toMessageData
-    else break
+    else
+      break
   return (pre, sub)
 
+private def elabModSnippet'
+    (range : DeclarationRange) (level : Nat) (blocks : TSyntaxArray `block) :
+    DocM VersoModuleDocs.Snippet := do
+  let mut snippet : VersoModuleDocs.Snippet := {
+    declarationRange := range
+  }
+  let mut maxLevel := level
+  for b in blocks do
+    if let `(block|header($n){$name*}) := b then
+        let n := n.getNat
+        if n > maxLevel then
+          logErrorAt b m!"Incorrect header nesting: expected at most `{"".pushn '#' n}`"
+        else
+          let title ←
+            liftM <| withInfoContext (mkInfo := pure <| .ofDocInfo {elaborator := `no_elab, stx := b}) <|
+              name.mapM elabInline
+          let some headerRange ← getDeclarationRange? b
+            | throwErrorAt b "Can't find header source position"
+          let mdTitle := ToMarkdown.toMarkdown (Inline.concat title) |>.run'
+          snippet := snippet.addPart n headerRange {
+            title,
+            titleString := mdTitle
+            metadata := none, content := #[], subParts := #[]
+          }
+      else
+        snippet := snippet.addBlock (← elabBlock b)
+  return snippet
+
+private partial def fixupInline (inl : Inline ElabInline) : DocM (Inline ElabInline) := do
+  match inl with
+  | .concat xs => .concat <$> xs.mapM fixupInline
+  | .emph xs => .emph <$> xs.mapM fixupInline
+  | .bold xs => .bold <$> xs.mapM fixupInline
+  | .link content url => (.link · url) <$> content.mapM fixupInline
+  | .footnote name content => .footnote name <$> content.mapM fixupInline
+  | .text s => pure (.text s)
+  | .image alt url => pure (.image alt url)
+  | .code s => pure (.code s)
+  | .math mode s => pure (.math mode s)
+  | .linebreak s => pure (.linebreak s)
+  | .other i@{ name, val } xs =>
+    match name with
+    | ``delayLink =>
+      let some {name} := val.get? ElabLink
+        | throwError "Wrong value for {name}: {val.typeName}"
+      let nameStr := name.getString
+      if let some r@{content := url, seen, .. } := (← getThe InternalState).urls[nameStr]? then
+        unless seen do modifyThe InternalState fun st => { st with urls := st.urls.insert nameStr { r with seen := true } }
+        return .link (← xs.mapM fixupInline) url
+      else
+        logErrorAt name "Reference not found"
+        return .concat (← xs.mapM fixupInline)
+    | ``delayImage =>
+      let some {alt, name} := val.get? ElabImage
+        | throwError "Wrong value for {name}: {val.typeName}"
+      let nameStr := name.getString
+      if let some r@{content := url, seen, ..} := (← getThe InternalState).urls[nameStr]? then
+        unless seen do modifyThe InternalState fun st => { st with urls := st.urls.insert nameStr { r with seen := true } }
+        return .image alt url
+      else
+        logErrorAt name "Reference not found"
+        return .empty
+    | ``delayFootnote =>
+      let some {name} := val.get? ElabFootnote
+        | throwError "Wrong value for {name}: {val.typeName}"
+      let nameStr := name.getString
+      if let some r@{content, seen, ..} := (← getThe InternalState).footnotes[nameStr]? then
+        unless seen do modifyThe InternalState fun st =>
+          { st with footnotes := st.footnotes.insert nameStr { r with seen := true } }
+        return .footnote nameStr #[← fixupInline content]
+      else
+        logErrorAt name "Footnote not found"
+        return .empty
+    | _ => .other i <$> xs.mapM fixupInline
+
+private partial def fixupBlock (block : Block ElabInline ElabBlock) : DocM (Block ElabInline ElabBlock) := do
+  match block with
+  | .para xs => .para <$> xs.mapM fixupInline
+  | .concat xs => .concat <$> xs.mapM fixupBlock
+  | .blockquote xs => .blockquote <$> xs.mapM fixupBlock
+  | .dl xs => .dl <$> xs.mapM fun { term, desc } => do
+    let term ← term.mapM fixupInline
+    let desc ← desc.mapM fixupBlock
+    pure { term, desc }
+  | .ul xs => .ul <$> xs.mapM fun ⟨bs⟩ => do return ⟨← bs.mapM fixupBlock⟩
+  | .ol n xs => .ol n <$> xs.mapM fun ⟨bs⟩ => do return ⟨← bs.mapM fixupBlock⟩
+  | .code s => pure (.code s)
+  | .other i xs => .other i <$> xs.mapM fixupBlock
+
+private partial def fixupPart (part : Part ElabInline ElabBlock Empty) : DocM (Part ElabInline ElabBlock Empty) := do
+  return { part with
+    title := ← part.title.mapM fixupInline
+    content := ← part.content.mapM fixupBlock,
+    subParts := ← part.subParts.mapM fixupPart
+  }
+
+
 private partial def fixupBlocks : (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty)) → DocM (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty))
   | (bs, ps) => do
-    let bs ← bs.mapM fixB
-    let ps ← ps.mapM fixP
+    let bs ← bs.mapM fixupBlock
+    let ps ← ps.mapM fixupPart
     return (bs, ps)
-where
-  fixI (inl : Inline ElabInline) : DocM (Inline ElabInline) := do
-    match inl with
-    | .concat xs => .concat <$> xs.mapM fixI
-    | .emph xs => .emph <$> xs.mapM fixI
-    | .bold xs => .bold <$> xs.mapM fixI
-    | .link content url => (.link · url) <$> content.mapM fixI
-    | .footnote name content => .footnote name <$> content.mapM fixI
-    | .text s => pure (.text s)
-    | .image alt url => pure (.image alt url)
-    | .code s => pure (.code s)
-    | .math mode s => pure (.math mode s)
-    | .linebreak s => pure (.linebreak s)
-    | .other i@{ name, val } xs =>
-      match name with
-      | ``delayLink =>
-        let some {name} := val.get? ElabLink
-          | throwError "Wrong value for {name}: {val.typeName}"
-        let nameStr := name.getString
-        if let some r@{content := url, seen, .. } := (← getThe InternalState).urls[nameStr]? then
-          unless seen do modifyThe InternalState fun st => { st with urls := st.urls.insert nameStr { r with seen := true } }
-          return .link (← xs.mapM fixI) url
-        else
-          logErrorAt name "Reference not found"
-          return .concat (← xs.mapM fixI)
-      | ``delayImage =>
-        let some {alt, name} := val.get? ElabImage
-          | throwError "Wrong value for {name}: {val.typeName}"
-        let nameStr := name.getString
-        if let some r@{content := url, seen, ..} := (← getThe InternalState).urls[nameStr]? then
-          unless seen do modifyThe InternalState fun st => { st with urls := st.urls.insert nameStr { r with seen := true } }
-          return .image alt url
-        else
-          logErrorAt name "Reference not found"
-          return .empty
-      | ``delayFootnote =>
-        let some {name} := val.get? ElabFootnote
-          | throwError "Wrong value for {name}: {val.typeName}"
-        let nameStr := name.getString
-        if let some r@{content, seen, ..} := (← getThe InternalState).footnotes[nameStr]? then
-          unless seen do modifyThe InternalState fun st =>
-            { st with footnotes := st.footnotes.insert nameStr { r with seen := true } }
-          return .footnote nameStr #[← fixI content]
-        else
-          logErrorAt name "Footnote not found"
-          return .empty
-      | _ => .other i <$> xs.mapM fixI
-
-  fixB (block : Block ElabInline ElabBlock) : DocM (Block ElabInline ElabBlock) := do
-    match block with
-    | .para xs => .para <$> xs.mapM fixI
-    | .concat xs => .concat <$> xs.mapM fixB
-    | .blockquote xs => .blockquote <$> xs.mapM fixB
-    | .dl xs => .dl <$> xs.mapM fun { term, desc } => do
-      let term ← term.mapM fixI
-      let desc ← desc.mapM fixB
-      pure { term, desc }
-    | .ul xs => .ul <$> xs.mapM fun ⟨bs⟩ => do return ⟨← bs.mapM fixB⟩
-    | .ol n xs => .ol n <$> xs.mapM fun ⟨bs⟩ => do return ⟨← bs.mapM fixB⟩
-    | .code s => pure (.code s)
-    | .other i xs => .other i <$> xs.mapM fixB
-
-  fixP (part : Part ElabInline ElabBlock Empty) : DocM (Part ElabInline ElabBlock Empty) := do
-    return { part with
-      title := ← part.title.mapM fixI
-      content := ← part.content.mapM fixB,
-      subParts := ← part.subParts.mapM fixP
-    }
 
+private partial def fixupSnippet (snippet : VersoModuleDocs.Snippet) : DocM VersoModuleDocs.Snippet := do
+  return {snippet with
+    text := ← snippet.text.mapM fixupBlock,
+    sections := ← snippet.sections.mapM fun (level, range, content) => do
+      return (level, range, ← fixupPart content)
+  }
 /--
 After fixing up the references, check to see which were not used and emit a suitable warning.
 -/
@@ -1419,10 +1594,19 @@ private def warnUnusedRefs : DocM Unit := do
     unless seen do
       logWarningAt location "Unused footnote"
 
-/-- Elaborates a sequence of blocks into a document -/
+/-- Elaborates a sequence of blocks into a document. -/
 public def elabBlocks (blocks : TSyntaxArray `block) :
     DocM (Array (Block ElabInline ElabBlock) × Array (Part ElabInline ElabBlock Empty)) := do
   let (v, _) ← elabBlocks' 0 |>.run blocks
   let res ← fixupBlocks v
   warnUnusedRefs
   return res
+
+/-- Elaborates a sequence of blocks into a module doc snippet. -/
+public def elabModSnippet
+    (range : DeclarationRange) (blocks : TSyntaxArray `block) (nestingLevel : Nat) :
+    DocM (VersoModuleDocs.Snippet) := do
+  let s ← elabModSnippet' range nestingLevel blocks
+  let s ← fixupSnippet s
+  warnUnusedRefs
+  return s

src/Lean/Elab/InfoTree/Main.lean

@@ -221,6 +221,12 @@ def DelabTermInfo.format (ctx : ContextInfo) (info : DelabTermInfo) : IO Format
 def ChoiceInfo.format (ctx : ContextInfo) (info : ChoiceInfo) : Format :=
   f!"[Choice] @ {formatElabInfo ctx info.toElabInfo}"
 
+def DocInfo.format (ctx : ContextInfo) (info : DocInfo) : Format :=
+  f!"[Doc] {info.stx.getKind} @ {formatElabInfo ctx info.toElabInfo}"
+
+def DocElabInfo.format (ctx : ContextInfo) (info : DocElabInfo) : Format :=
+  f!"[DocElab] {info.name} ({repr info.kind}) @ {formatElabInfo ctx info.toElabInfo}"
+
 def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofTacticInfo i         => i.format ctx
   | ofTermInfo i           => i.format ctx
@@ -237,6 +243,8 @@ def Info.format (ctx : ContextInfo) : Info → IO Format
   | ofFieldRedeclInfo i    => pure <| i.format ctx
   | ofDelabTermInfo i      => i.format ctx
   | ofChoiceInfo i         => pure <| i.format ctx
+  | ofDocInfo i            => pure <| i.format ctx
+  | ofDocElabInfo i        => pure <| i.format ctx
 
 def Info.toElabInfo? : Info → Option ElabInfo
   | ofTacticInfo i         => some i.toElabInfo
@@ -254,6 +262,8 @@ def Info.toElabInfo? : Info → Option ElabInfo
   | ofFieldRedeclInfo _    => none
   | ofDelabTermInfo i      => some i.toElabInfo
   | ofChoiceInfo i         => some i.toElabInfo
+  | ofDocInfo i            => some i.toElabInfo
+  | ofDocElabInfo i        => some i.toElabInfo
 
 /--
   Helper function for propagating the tactic metavariable context to its children nodes.

src/Lean/Elab/InfoTree/Types.lean

@@ -207,6 +207,23 @@ the language server provide interactivity even when all overloaded elaborators f
 -/
 structure ChoiceInfo extends ElabInfo where
 
+inductive DocElabKind where
+  | role | codeBlock | directive | command
+deriving Repr
+
+/--
+Indicates that an extensible document elaborator was used here.
+-/
+structure DocElabInfo extends ElabInfo where
+  name : Name
+  kind : DocElabKind
+
+/--
+Indicates that a piece of syntax was elaborated as documentation.
+-/
+structure DocInfo extends ElabInfo where
+
+
 /-- Header information for a node in `InfoTree`. -/
 inductive Info where
   | ofTacticInfo (i : TacticInfo)
@@ -224,6 +241,8 @@ inductive Info where
   | ofFieldRedeclInfo (i : FieldRedeclInfo)
   | ofDelabTermInfo (i : DelabTermInfo)
   | ofChoiceInfo (i : ChoiceInfo)
+  | ofDocInfo (i : DocInfo)
+  | ofDocElabInfo (i : DocElabInfo)
   deriving Inhabited
 
 /-- The InfoTree is a structure that is generated during elaboration and used

src/Lean/Parser/Command.lean

@@ -8,6 +8,8 @@ module
 prelude
 public import Lean.Parser.Term
 public import Lean.Parser.Do
+import Lean.DocString.Parser
+public import Lean.DocString.Formatter
 meta import Lean.Parser.Basic
 
 public section
@@ -49,6 +51,7 @@ match against a quotation in a command kind's elaborator). -/
 @[builtin_term_parser low] def quot := leading_parser
   "`(" >> withoutPosition (incQuotDepth (many1Unbox commandParser)) >> ")"
 
+
 /--
 `/-! <text> -/` defines a *module docstring* that can be displayed by documentation generation
 tools. The string is associated with the corresponding position in the file. It can be used
@@ -56,7 +59,8 @@ multiple times in the same file.
 -/
 @[builtin_command_parser]
 def moduleDoc := leading_parser ppDedent <|
-  "/-!" >> commentBody >> ppLine
+  "/-!" >> Doc.Parser.ifVerso versoCommentBody commentBody >> ppLine
+
 
 def namedPrio := leading_parser
   atomic (" (" >> nonReservedSymbol "priority") >> " := " >> withoutPosition priorityParser >> ")"
@@ -889,6 +893,7 @@ builtin_initialize
   register_parser_alias                                                 optDeclSig
   register_parser_alias                                                 openDecl
   register_parser_alias                                                 docComment
+  register_parser_alias                                                 plainDocComment
   register_parser_alias                                                 visibility
 
 /--

src/Lean/Parser/Term.lean

@@ -8,8 +8,13 @@ module
 prelude
 public import Lean.Parser.Attr
 public import Lean.Parser.Level
+public import Lean.Parser.Term.Basic
+public import Lean.Parser.Term.Basic
+meta import Lean.Parser.Term.Basic
 public import Lean.Parser.Term.Doc
 meta import Lean.Parser.Basic
+import Lean.DocString.Parser
+public import Lean.DocString.Formatter
 
 public section
 
@@ -17,6 +22,38 @@ namespace Lean
 namespace Parser
 
 namespace Command
+
+open Lean.Parser in
+def versoCommentBodyFn : ParserFn := fun c s =>
+  let startPos := s.pos
+  let s := finishCommentBlock (pushMissingOnError := true) 1 c s
+  if !s.hasError then
+    let commentEndPos := s.pos
+    let endPos := c.prev (c.prev commentEndPos)
+    let endPos := if endPos ≤ c.inputString.endPos then endPos else c.inputString.endPos
+    let c' := c.setEndPos endPos (by unfold endPos; split <;> simp [*])
+    let s := Doc.Parser.document {} c' (s.setPos startPos)
+    if s.hasError then
+      s.pushSyntax .missing
+    else
+      (rawFn (Doc.Parser.ignoreFn <| chFn '-' >> chFn '/') (trailingWs := true)) c s
+  else s
+
+public def versoCommentBody : Parser where
+  fn := nodeFn `Lean.Parser.Command.versoCommentBody versoCommentBodyFn
+
+@[combinator_parenthesizer versoCommentBody, expose]
+public def versoCommentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
+
+open PrettyPrinter Formatter in
+open Syntax.MonadTraverser in
+@[combinator_formatter versoCommentBody, expose]
+public def versoCommentBody.formatter : PrettyPrinter.Formatter := do
+  visitArgs $ do
+    visitAtom `«-/»
+    goLeft
+    Lean.Doc.Parser.document.formatter
+
 def commentBody : Parser :=
 { fn := rawFn (finishCommentBlock (pushMissingOnError := true) 1) (trailingWs := true) }
 
@@ -25,86 +62,31 @@ def commentBody.parenthesizer := PrettyPrinter.Parenthesizer.visitToken
 @[combinator_formatter commentBody, expose]
 def commentBody.formatter := PrettyPrinter.Formatter.visitAtom Name.anonymous
 
-/-- A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
+/--
+A `docComment` parses a "documentation comment" like `/-- foo -/`. This is not treated like
 a regular comment (that is, as whitespace); it is parsed and forms part of the syntax tree structure.
 
-A `docComment` node contains a `/--` atom and then the remainder of the comment, `foo -/` in this
-example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node. -/
+At parse time, `docComment` checks the value of the `doc.verso` option. If it is true, the contents
+are parsed as Verso markup. If not, the contents are treated as plain text or Markdown. Use
+`plainDocComment` to always treat the contents as plain text.
+
+A plain text doc comment node contains a `/--` atom and then the remainder of the comment, `foo -/`
+in this example. Use `TSyntax.getDocString` to extract the body text from a doc string syntax node.
+A Verso comment node contains the `/--` atom, the document's syntax tree, and a closing `-/` atom.
+-/
 -- @[builtin_doc] -- FIXME: suppress the hover
+@[run_builtin_parser_attribute_hooks]
 def docComment := leading_parser
-  ppDedent $ "/--" >> ppSpace >> commentBody >> ppLine
+  ppDedent $ "/--" >> ppSpace >> Doc.Parser.ifVerso versoCommentBody commentBody >> ppLine
+
+@[inherit_doc docComment, run_builtin_parser_attribute_hooks]
+def plainDocComment : Parser := Doc.Parser.withoutVersoSyntax docComment
+
 end Command
 
-builtin_initialize
-  registerBuiltinParserAttribute `builtin_tactic_parser ``Category.tactic .both
-  registerBuiltinDynamicParserAttribute `tactic_parser `tactic
-
-@[inline] def tacticParser (rbp : Nat := 0) : Parser :=
-  categoryParser `tactic rbp
-
-@[inline] def convParser (rbp : Nat := 0) : Parser :=
-  categoryParser `conv rbp
-
-namespace Tactic
-
-/-- `sepByIndentSemicolon(p)` parses a sequence of `p` optionally followed by `;`,
-similar to `manyIndent(p ";"?)`, except that if two occurrences of `p` occur on the same line,
-the `;` is mandatory. This is used by tactic parsing, so that
-```
-example := by
-  skip
-  skip
-```
-is legal, but `by skip skip` is not - it must be written as `by skip; skip`. -/
-@[run_builtin_parser_attribute_hooks, builtin_doc]
-def sepByIndentSemicolon (p : Parser) : Parser :=
-  sepByIndent p "; " (allowTrailingSep := true)
-
-/-- `sepBy1IndentSemicolon(p)` parses a (nonempty) sequence of `p` optionally followed by `;`,
-similar to `many1Indent(p ";"?)`, except that if two occurrences of `p` occur on the same line,
-the `;` is mandatory. This is used by tactic parsing, so that
-```
-example := by
-  skip
-  skip
-```
-is legal, but `by skip skip` is not - it must be written as `by skip; skip`. -/
-@[run_builtin_parser_attribute_hooks, builtin_doc]
-def sepBy1IndentSemicolon (p : Parser) : Parser :=
-  sepBy1Indent p "; " (allowTrailingSep := true)
-
-builtin_initialize
-  register_parser_alias sepByIndentSemicolon
-  register_parser_alias sepBy1IndentSemicolon
-
-@[builtin_doc] def tacticSeq1Indented : Parser := leading_parser
-  sepBy1IndentSemicolon tacticParser
-/-- The syntax `{ tacs }` is an alternative syntax for `· tacs`.
-It runs the tactics in sequence, and fails if the goal is not solved. -/
-@[builtin_doc] def tacticSeqBracketed : Parser := leading_parser
-  "{ " >> sepByIndentSemicolon tacticParser >> ppDedent ppLine >> "}"
-
-/-- A sequence of tactics in brackets, or a delimiter-free indented sequence of tactics.
-Delimiter-free indentation is determined by the *first* tactic of the sequence. -/
-@[builtin_doc] def tacticSeq := leading_parser
-  tacticSeqBracketed <|> tacticSeq1Indented
-
-/-- Same as [`tacticSeq`] but requires delimiter-free tactic sequence to have strict indentation.
-The strict indentation requirement only apply to *nested* `by`s, as top-level `by`s do not have a
-position set. -/
-@[builtin_doc] def tacticSeqIndentGt := withAntiquot (mkAntiquot "tacticSeq" ``tacticSeq) <| node ``tacticSeq <|
-  tacticSeqBracketed <|> (checkColGt "indented tactic sequence" >> tacticSeq1Indented)
-
-/- Raw sequence for quotation and grouping -/
-def seq1 :=
-  node `Lean.Parser.Tactic.seq1 $ sepBy1 tacticParser ";\n" (allowTrailingSep := true)
-
-end Tactic
-
 def darrow : Parser := " => "
 def semicolonOrLinebreak := ";" <|> checkLinebreakBefore >> pushNone
 
-
 namespace Term
 
 /-! # Built-in parsers -/
@@ -148,81 +130,8 @@ def optSemicolon (p : Parser) : Parser :=
 Every proposition is propositionally equal to either `True` or `False`. -/
 @[builtin_term_parser] def prop := leading_parser
   "Prop"
-/--
-A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
-For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.
 
-The way this works is that holes create fresh metavariables.
-The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
-This is often known as *unification*.
 
-Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
-* In `match` patterns, holes are catch-all patterns.
-* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.
-
-Related concept: implicit parameters are automatically filled in with holes during the elaboration process.
-
-See also `?m` syntax (synthetic holes).
--/
-@[builtin_term_parser] def hole := leading_parser
-  "_"
-/--
-A *synthetic hole* (or *synthetic placeholder*), which stands for an unknown term that should be synthesized using tactics.
-- `?_` creates a fresh metavariable with an auto-generated name.
-- `?m` either refers to a pre-existing metavariable named `m` or creates a fresh metavariable with that name.
-
-In particular, the synthetic hole syntax creates "synthetic opaque metavariables",
-the same kind of metavariable used to represent goals in the tactic state.
-
-Synthetic holes are similar to holes in that `_` also creates metavariables,
-but synthetic opaque metavariables have some different properties:
-- In tactics such as `refine`, only synthetic holes yield new goals.
-- During elaboration, unification will not solve for synthetic opaque metavariables, they are "opaque".
-  This is to prevent counterintuitive behavior such as disappearing goals.
-- When synthetic holes appear under binders, they capture local variables using a more complicated mechanism known as delayed assignment.
-
-## Delayed assigned metavariables
-
-This section gives an overview of some technical details of synthetic holes, which you should feel free to skip.
-Understanding delayed assignments is mainly useful for those who are working on tactics and other metaprogramming.
-It is included here until there is a suitable place for it in the reference manual.
-
-When a synthetic hole appears under a binding construct, such as for example `fun (x : α) (y : β) => ?s`,
-the system creates a *delayed assignment*. This consists of
-1. A metavariable `?m` of type `(x : α) → (y : β) → γ x y` whose local context is the local context outside the `fun`,
-  where `γ x y` is the type of `?s`. Recall that `x` and `y` appear in the local context of `?s`.
-2. A delayed assignment record associating `?m` to `?s` and the variables `#[x, y]` in the local context of `?s`
-
-Then, this function elaborates as `fun (x : α) (y : β) => ?m x y`, where one should understand `x` and `y` here
-as being De Bruijn indexes, since Lean uses the locally nameless encoding of lambda calculus.
-
-Once `?s` is fully solved for, in the sense that after metavariable instantiation it is a metavariable-free term `e`,
-then we can make the assignment `?m := fun (x' : α) (y' : β) => e[x := x', y := y']`.
-(Implementation note: Lean only instantiates full applications `?m x' y'` of delayed assigned metavariables, to skip forming this function.)
-This delayed assignment mechanism is essential to the operation of basic tactics like `intro`,
-and a good mental model is that it is a way to "apply" the metavariable `?s` by substituting values in for some of its local variables.
-While it would be easier to immediately assign `?s := ?m x y`,
-delayed assignment preserves `?s` as an unsolved-for metavariable with a local context that still contains `x` and `y`,
-which is exactly what tactics like `intro` need.
-
-By default, delayed assigned metavariables pretty print with what they are delayed assigned to.
-The delayed assigned metavariables themselves can be pretty printed using `set_option pp.mvars.delayed true`.
-
-For more information, see the "Gruesome details" module docstrings in `Lean.MetavarContext`.
--/
-@[builtin_term_parser] def syntheticHole := leading_parser
-  "?" >> (ident <|> "_")
-/--
-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
-  "⋯"
-def binderIdent : Parser  := ident <|> hole
 /--
 The `sorry` term is a temporary placeholder for a missing proof or value.
 
@@ -287,8 +196,6 @@ are turned into a new anonymous constructor application. For example,
 -/
 @[builtin_term_parser] def anonymousCtor := leading_parser
   "⟨" >> withoutPosition (withoutForbidden (sepBy termParser ", " (allowTrailingSep := true))) >> "⟩"
-def optIdent : Parser :=
-  optional (atomic (ident >> " : "))
 def fromTerm   := leading_parser
   "from " >> termParser
 def showRhs := fromTerm <|> byTactic'
@@ -299,8 +206,6 @@ an optional `x :`, then a term `ty`, then `from val` or `by tac`. -/
 @[builtin_term_parser] def «suffices» := leading_parser:leadPrec
   withPosition ("suffices " >> sufficesDecl) >> optSemicolon termParser
 @[builtin_term_parser] def «show»     := leading_parser:leadPrec "show " >> termParser >> ppSpace >> showRhs
-def typeSpec := leading_parser " : " >> termParser
-def optType : Parser := optional typeSpec
 /--
 `@x` disables automatic insertion of implicit parameters of the constant `x`.
 `@e` for any term `e` also disables the insertion of implicit lambdas at this position.
@@ -313,77 +218,6 @@ In contrast to regular patterns, `e` may be an arbitrary term of the appropriate
 -/
 @[builtin_term_parser] def inaccessible := leading_parser
   ".(" >> withoutPosition termParser >> ")"
-def binderType (requireType := false) : Parser :=
-  if requireType then node nullKind (" : " >> termParser) else optional (" : " >> termParser)
-def binderTactic  := leading_parser
-  atomic (symbol " := " >> " by ") >> Tactic.tacticSeq
-def binderDefault := leading_parser
-  " := " >> termParser
-
-open Lean.PrettyPrinter Parenthesizer Syntax.MonadTraverser in
-@[combinator_parenthesizer Lean.Parser.Term.binderDefault, expose] def binderDefault.parenthesizer : Parenthesizer := do
-  let prec := match (← getCur) with
-    -- must parenthesize to distinguish from `binderTactic`
-    | `(binderDefault| := by $_) => maxPrec
-    | _                          => 0
-  visitArgs do
-    term.parenthesizer prec
-    visitToken
-
-/--
-Explicit binder, like `(x y : A)` or `(x y)`.
-Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
--/
-@[builtin_doc] def explicitBinder (requireType := false) := leading_parser ppGroup <|
-  "(" >> withoutPosition (many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault)) >> ")"
-/--
-Implicit binder, like `{x y : A}` or `{x y}`.
-In regular applications, whenever all parameters before it have been specified,
-then a `_` placeholder is automatically inserted for this parameter.
-Implicit parameters should be able to be determined from the other arguments and the return type
-by unification.
-
-In `@` explicit mode, implicit binders behave like explicit binders.
--/
-@[builtin_doc] def implicitBinder (requireType := false) := leading_parser ppGroup <|
-  "{" >> withoutPosition (many1 binderIdent >> binderType requireType) >> "}"
-def strictImplicitLeftBracket := atomic (group (symbol "{" >> "{")) <|> "⦃"
-def strictImplicitRightBracket := atomic (group (symbol "}" >> "}")) <|> "⦄"
-/--
-Strict-implicit binder, like `⦃x y : A⦄` or `⦃x y⦄`.
-In contrast to `{ ... }` implicit binders, strict-implicit binders do not automatically insert
-a `_` placeholder until at least one subsequent explicit parameter is specified.
-Do *not* use strict-implicit binders unless there is a subsequent explicit parameter.
-Assuming this rule is followed, for fully applied expressions implicit and strict-implicit binders have the same behavior.
-
-Example: If `h : ∀ ⦃x : A⦄, x ∈ s → p x` and `hs : y ∈ s`,
-then `h` by itself elaborates to itself without inserting `_` for the `x : A` parameter,
-and `h hs` has type `p y`.
-In contrast, if `h' : ∀ {x : A}, x ∈ s → p x`, then `h` by itself elaborates to have type `?m ∈ s → p ?m`
-with `?m` a fresh metavariable.
--/
-@[builtin_doc] def strictImplicitBinder (requireType := false) := leading_parser ppGroup <|
-  strictImplicitLeftBracket >> many1 binderIdent >>
-  binderType requireType >> strictImplicitRightBracket
-/--
-Instance-implicit binder, like `[C]` or `[inst : C]`.
-In regular applications without `@` explicit mode, it is automatically inserted
-and solved for by typeclass inference for the specified class `C`.
-In `@` explicit mode, if `_` is used for an instance-implicit parameter, then it is still solved for by typeclass inference;
-use `(_)` to inhibit this and have it be solved for by unification instead, like an implicit argument.
--/
-@[builtin_doc] def instBinder := leading_parser ppGroup <|
-  "[" >> withoutPosition (optIdent >> termParser) >> "]"
-/-- A `bracketedBinder` matches any kind of binder group that uses some kind of brackets:
-* An explicit binder like `(x y : A)`
-* An implicit binder like `{x y : A}`
-* A strict implicit binder, `⦃y z : A⦄` or its ASCII alternative `{{y z : A}}`
-* An instance binder `[A]` or `[x : A]` (multiple variables are not allowed here)
--/
-@[builtin_doc] def bracketedBinder (requireType := false) :=
-  withAntiquot (mkAntiquot "bracketedBinder" decl_name% (isPseudoKind := true)) <|
-    explicitBinder requireType <|> strictImplicitBinder requireType <|>
-    implicitBinder requireType <|> instBinder
 
 /-
 It is feasible to support dependent arrows such as `{α} → α → α` without sacrificing the quality of the error messages for the longer case.
@@ -486,34 +320,6 @@ e.g. because it has no constructors.
 
 @[builtin_term_parser] def «nofun» := leading_parser "nofun"
 
-/-
-Syntax category for structure instance notation fields.
-Does not initialize `registerBuiltinDynamicParserAttribute` since this category is not meant to be user-extensible.
--/
-builtin_initialize
-  registerBuiltinParserAttribute `builtin_structInstFieldDecl_parser ``Category.structInstFieldDecl
-@[inline] def structInstFieldDeclParser (rbp : Nat := 0) : Parser :=
-  categoryParser `structInstFieldDecl rbp
-def optEllipsis := leading_parser
-  optional " .."
-def structInstArrayRef := leading_parser
-  "[" >> withoutPosition termParser >> "]"
-def structInstLVal := leading_parser
-  (ident <|> fieldIdx <|> structInstArrayRef) >>
-  many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
-def structInstFieldBinder :=
-  withAntiquot (mkAntiquot "structInstFieldBinder" decl_name% (isPseudoKind := true)) <|
-    binderIdent <|> bracketedBinder
-def optTypeForStructInst : Parser := optional (atomic (typeSpec >> notFollowedBy "}" "}"))
-/- `x` is an abbreviation for `x := x` -/
-def structInstField := ppGroup <| leading_parser
-  structInstLVal >> optional (many (checkColGt >> ppSpace >> structInstFieldBinder) >> optTypeForStructInst >> ppDedent structInstFieldDeclParser)
-/-
-Tags the structure instance field syntax with a `Lean.Parser.Term.structInstFields` syntax node.
-This node is used to enable structure instance field completion in the whitespace
-of a structure instance notation.
--/
-def structInstFields (p : Parser) : Parser := node `Lean.Parser.Term.structInstFields p
 /--
 Structure instance. `{ x := e, ... }` assigns `e` to field `x`, which may be
 inherited. If `e` is itself a variable called `x`, it can be elided:

src/Lean/Parser/Term/Basic.lean

@@ -0,0 +1,286 @@
+/-
+Copyright (c) 2019 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura, Sebastian Ullrich, Mario Carneiro
+-/
+module
+
+prelude
+public import Lean.Parser.Attr
+public import Lean.Parser.Level
+public import Lean.Parser.Term.Doc
+meta import Lean.Parser.Basic
+
+
+public section
+
+namespace Lean
+namespace Parser
+
+
+builtin_initialize
+  registerBuiltinParserAttribute `builtin_tactic_parser ``Category.tactic .both
+  registerBuiltinDynamicParserAttribute `tactic_parser `tactic
+
+@[inline] def tacticParser (rbp : Nat := 0) : Parser :=
+  categoryParser `tactic rbp
+
+@[inline] def convParser (rbp : Nat := 0) : Parser :=
+  categoryParser `conv rbp
+
+namespace Tactic
+
+/-- `sepByIndentSemicolon(p)` parses a sequence of `p` optionally followed by `;`,
+similar to `manyIndent(p ";"?)`, except that if two occurrences of `p` occur on the same line,
+the `;` is mandatory. This is used by tactic parsing, so that
+```
+example := by
+  skip
+  skip
+```
+is legal, but `by skip skip` is not - it must be written as `by skip; skip`. -/
+@[run_builtin_parser_attribute_hooks, builtin_doc]
+def sepByIndentSemicolon (p : Parser) : Parser :=
+  sepByIndent p "; " (allowTrailingSep := true)
+
+/-- `sepBy1IndentSemicolon(p)` parses a (nonempty) sequence of `p` optionally followed by `;`,
+similar to `many1Indent(p ";"?)`, except that if two occurrences of `p` occur on the same line,
+the `;` is mandatory. This is used by tactic parsing, so that
+```
+example := by
+  skip
+  skip
+```
+is legal, but `by skip skip` is not - it must be written as `by skip; skip`. -/
+@[run_builtin_parser_attribute_hooks, builtin_doc]
+def sepBy1IndentSemicolon (p : Parser) : Parser :=
+  sepBy1Indent p "; " (allowTrailingSep := true)
+
+builtin_initialize
+  register_parser_alias sepByIndentSemicolon
+  register_parser_alias sepBy1IndentSemicolon
+
+@[builtin_doc] def tacticSeq1Indented : Parser := leading_parser
+  sepBy1IndentSemicolon tacticParser
+/-- The syntax `{ tacs }` is an alternative syntax for `· tacs`.
+It runs the tactics in sequence, and fails if the goal is not solved. -/
+@[builtin_doc] def tacticSeqBracketed : Parser := leading_parser
+  "{ " >> sepByIndentSemicolon tacticParser >> ppDedent ppLine >> "}"
+
+/-- A sequence of tactics in brackets, or a delimiter-free indented sequence of tactics.
+Delimiter-free indentation is determined by the *first* tactic of the sequence. -/
+@[builtin_doc, run_builtin_parser_attribute_hooks] def tacticSeq := leading_parser
+  tacticSeqBracketed <|> tacticSeq1Indented
+
+/-- Same as [`tacticSeq`] but requires delimiter-free tactic sequence to have strict indentation.
+The strict indentation requirement only apply to *nested* `by`s, as top-level `by`s do not have a
+position set. -/
+@[builtin_doc, run_builtin_parser_attribute_hooks]
+def tacticSeqIndentGt := withAntiquot (mkAntiquot "tacticSeq" ``tacticSeq) <| node ``tacticSeq <|
+  tacticSeqBracketed <|> (checkColGt "indented tactic sequence" >> tacticSeq1Indented)
+
+/- Raw sequence for quotation and grouping -/
+@[run_builtin_parser_attribute_hooks]
+def seq1 :=
+  node `Lean.Parser.Tactic.seq1 $ sepBy1 tacticParser ";\n" (allowTrailingSep := true)
+
+end Tactic
+
+namespace Term
+/--
+A *hole* (or *placeholder term*), which stands for an unknown term that is expected to be inferred based on context.
+For example, in `@id _ Nat.zero`, the `_` must be the type of `Nat.zero`, which is `Nat`.
+
+The way this works is that holes create fresh metavariables.
+The elaborator is allowed to assign terms to metavariables while it is checking definitional equalities.
+This is often known as *unification*.
+
+Normally, all holes must be solved for. However, there are a few contexts where this is not necessary:
+* In `match` patterns, holes are catch-all patterns.
+* In some tactics, such as `refine'` and `apply`, unsolved-for placeholders become new goals.
+
+Related concept: implicit parameters are automatically filled in with holes during the elaboration process.
+
+See also `?m` syntax (synthetic holes).
+-/
+@[builtin_term_parser] def hole := leading_parser
+  "_"
+/--
+A *synthetic hole* (or *synthetic placeholder*), which stands for an unknown term that should be synthesized using tactics.
+- `?_` creates a fresh metavariable with an auto-generated name.
+- `?m` either refers to a pre-existing metavariable named `m` or creates a fresh metavariable with that name.
+
+In particular, the synthetic hole syntax creates "synthetic opaque metavariables",
+the same kind of metavariable used to represent goals in the tactic state.
+
+Synthetic holes are similar to holes in that `_` also creates metavariables,
+but synthetic opaque metavariables have some different properties:
+- In tactics such as `refine`, only synthetic holes yield new goals.
+- During elaboration, unification will not solve for synthetic opaque metavariables, they are "opaque".
+  This is to prevent counterintuitive behavior such as disappearing goals.
+- When synthetic holes appear under binders, they capture local variables using a more complicated mechanism known as delayed assignment.
+
+## Delayed assigned metavariables
+
+This section gives an overview of some technical details of synthetic holes, which you should feel free to skip.
+Understanding delayed assignments is mainly useful for those who are working on tactics and other metaprogramming.
+It is included here until there is a suitable place for it in the reference manual.
+
+When a synthetic hole appears under a binding construct, such as for example `fun (x : α) (y : β) => ?s`,
+the system creates a *delayed assignment*. This consists of
+1. A metavariable `?m` of type `(x : α) → (y : β) → γ x y` whose local context is the local context outside the `fun`,
+  where `γ x y` is the type of `?s`. Recall that `x` and `y` appear in the local context of `?s`.
+2. A delayed assignment record associating `?m` to `?s` and the variables `#[x, y]` in the local context of `?s`
+
+Then, this function elaborates as `fun (x : α) (y : β) => ?m x y`, where one should understand `x` and `y` here
+as being De Bruijn indexes, since Lean uses the locally nameless encoding of lambda calculus.
+
+Once `?s` is fully solved for, in the sense that after metavariable instantiation it is a metavariable-free term `e`,
+then we can make the assignment `?m := fun (x' : α) (y' : β) => e[x := x', y := y']`.
+(Implementation note: Lean only instantiates full applications `?m x' y'` of delayed assigned metavariables, to skip forming this function.)
+This delayed assignment mechanism is essential to the operation of basic tactics like `intro`,
+and a good mental model is that it is a way to "apply" the metavariable `?s` by substituting values in for some of its local variables.
+While it would be easier to immediately assign `?s := ?m x y`,
+delayed assignment preserves `?s` as an unsolved-for metavariable with a local context that still contains `x` and `y`,
+which is exactly what tactics like `intro` need.
+
+By default, delayed assigned metavariables pretty print with what they are delayed assigned to.
+The delayed assigned metavariables themselves can be pretty printed using `set_option pp.mvars.delayed true`.
+
+For more information, see the "Gruesome details" module docstrings in `Lean.MetavarContext`.
+-/
+@[builtin_term_parser] def syntheticHole := leading_parser
+  "?" >> (ident <|> "_")
+
+/--
+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
+  "⋯"
+@[run_builtin_parser_attribute_hooks]
+def binderIdent : Parser  := ident <|> hole
+
+@[run_builtin_parser_attribute_hooks]
+def binderType (requireType := false) : Parser :=
+  if requireType then node nullKind (" : " >> termParser) else optional (" : " >> termParser)
+@[run_builtin_parser_attribute_hooks]
+def binderTactic  := leading_parser
+  atomic (symbol " := " >> " by ") >> Tactic.tacticSeq
+def binderDefault := leading_parser
+  " := " >> termParser
+
+open Lean.PrettyPrinter Parenthesizer Syntax.MonadTraverser in
+@[combinator_parenthesizer Lean.Parser.Term.binderDefault, expose] def binderDefault.parenthesizer : Parenthesizer := do
+  let prec := match (← getCur) with
+    -- must parenthesize to distinguish from `binderTactic`
+    | `(binderDefault| := by $_) => maxPrec
+    | _                          => 0
+  visitArgs do
+    term.parenthesizer prec
+    visitToken
+
+/--
+Explicit binder, like `(x y : A)` or `(x y)`.
+Default values can be specified using `(x : A := v)` syntax, and tactics using `(x : A := by tac)`.
+-/
+@[builtin_doc] def explicitBinder (requireType := false) := leading_parser ppGroup <|
+  "(" >> withoutPosition (many1 binderIdent >> binderType requireType >> optional (binderTactic <|> binderDefault)) >> ")"
+/--
+Implicit binder, like `{x y : A}` or `{x y}`.
+In regular applications, whenever all parameters before it have been specified,
+then a `_` placeholder is automatically inserted for this parameter.
+Implicit parameters should be able to be determined from the other arguments and the return type
+by unification.
+
+In `@` explicit mode, implicit binders behave like explicit binders.
+-/
+@[builtin_doc] def implicitBinder (requireType := false) := leading_parser ppGroup <|
+  "{" >> withoutPosition (many1 binderIdent >> binderType requireType) >> "}"
+def strictImplicitLeftBracket := atomic (group (symbol "{" >> "{")) <|> "⦃"
+def strictImplicitRightBracket := atomic (group (symbol "}" >> "}")) <|> "⦄"
+/--
+Strict-implicit binder, like `⦃x y : A⦄` or `⦃x y⦄`.
+In contrast to `{ ... }` implicit binders, strict-implicit binders do not automatically insert
+a `_` placeholder until at least one subsequent explicit parameter is specified.
+Do *not* use strict-implicit binders unless there is a subsequent explicit parameter.
+Assuming this rule is followed, for fully applied expressions implicit and strict-implicit binders have the same behavior.
+
+Example: If `h : ∀ ⦃x : A⦄, x ∈ s → p x` and `hs : y ∈ s`,
+then `h` by itself elaborates to itself without inserting `_` for the `x : A` parameter,
+and `h hs` has type `p y`.
+In contrast, if `h' : ∀ {x : A}, x ∈ s → p x`, then `h` by itself elaborates to have type `?m ∈ s → p ?m`
+with `?m` a fresh metavariable.
+-/
+@[builtin_doc] def strictImplicitBinder (requireType := false) := leading_parser ppGroup <|
+  strictImplicitLeftBracket >> many1 binderIdent >>
+  binderType requireType >> strictImplicitRightBracket
+
+def optIdent : Parser :=
+  optional (atomic (ident >> " : "))
+
+/--
+Instance-implicit binder, like `[C]` or `[inst : C]`.
+In regular applications without `@` explicit mode, it is automatically inserted
+and solved for by typeclass inference for the specified class `C`.
+In `@` explicit mode, if `_` is used for an instance-implicit parameter, then it is still solved for by typeclass inference;
+use `(_)` to inhibit this and have it be solved for by unification instead, like an implicit argument.
+-/
+@[builtin_doc] def instBinder := leading_parser ppGroup <|
+  "[" >> withoutPosition (optIdent >> termParser) >> "]"
+/-- A `bracketedBinder` matches any kind of binder group that uses some kind of brackets:
+* An explicit binder like `(x y : A)`
+* An implicit binder like `{x y : A}`
+* A strict implicit binder, `⦃y z : A⦄` or its ASCII alternative `{{y z : A}}`
+* An instance binder `[A]` or `[x : A]` (multiple variables are not allowed here)
+-/
+@[builtin_doc, run_builtin_parser_attribute_hooks] def bracketedBinder (requireType := false) :=
+  withAntiquot (mkAntiquot "bracketedBinder" decl_name% (isPseudoKind := true)) <|
+    explicitBinder requireType <|> strictImplicitBinder requireType <|>
+    implicitBinder requireType <|> instBinder
+
+@[run_builtin_parser_attribute_hooks]
+def typeSpec := leading_parser " : " >> termParser
+
+@[run_builtin_parser_attribute_hooks]
+def optType : Parser := optional typeSpec
+
+/-
+Syntax category for structure instance notation fields.
+Does not initialize `registerBuiltinDynamicParserAttribute` since this category is not meant to be user-extensible.
+-/
+builtin_initialize
+  registerBuiltinParserAttribute `builtin_structInstFieldDecl_parser ``Category.structInstFieldDecl
+@[inline] def structInstFieldDeclParser (rbp : Nat := 0) : Parser :=
+  categoryParser `structInstFieldDecl rbp
+@[run_builtin_parser_attribute_hooks]
+def optEllipsis := leading_parser
+  optional " .."
+@[run_builtin_parser_attribute_hooks]
+def structInstArrayRef := leading_parser
+  "[" >> withoutPosition termParser >> "]"
+@[run_builtin_parser_attribute_hooks]
+def structInstLVal := leading_parser
+  (ident <|> fieldIdx <|> structInstArrayRef) >>
+  many (group ("." >> (ident <|> fieldIdx)) <|> structInstArrayRef)
+@[run_builtin_parser_attribute_hooks]
+def structInstFieldBinder :=
+  withAntiquot (mkAntiquot "structInstFieldBinder" decl_name% (isPseudoKind := true)) <|
+    binderIdent <|> bracketedBinder
+@[run_builtin_parser_attribute_hooks]
+def optTypeForStructInst : Parser := optional (atomic (typeSpec >> notFollowedBy "}" "}"))
+/- `x` is an abbreviation for `x := x` -/
+@[run_builtin_parser_attribute_hooks]
+def structInstField := ppGroup <| leading_parser
+  structInstLVal >> optional (many (checkColGt >> ppSpace >> structInstFieldBinder) >> optTypeForStructInst >> ppDedent structInstFieldDeclParser)
+/-
+Tags the structure instance field syntax with a `Lean.Parser.Term.structInstFields` syntax node.
+This node is used to enable structure instance field completion in the whitespace
+of a structure instance notation.
+-/
+@[run_builtin_parser_attribute_hooks]
+def structInstFields (p : Parser) : Parser := node `Lean.Parser.Term.structInstFields p

src/Lean/Server/FileWorker/SemanticHighlighting.lean

@@ -7,6 +7,7 @@ module
 
 prelude
 public import Lean.Server.Requests
+import Lean.DocString.Syntax
 
 public section
 
@@ -23,9 +24,13 @@ def noHighlightKinds : Array SyntaxNodeKind := #[
   ``Lean.Parser.Term.type,
   ``Lean.Parser.Term.prop,
   -- not really keywords
-  `antiquotName,
+  `antiquotName]
+
+def docKinds : Array SyntaxNodeKind := #[
+  ``Lean.Parser.Command.plainDocComment,
   ``Lean.Parser.Command.docComment,
-  ``Lean.Parser.Command.moduleDoc]
+  ``Lean.Parser.Command.moduleDoc
+]
 
 -- TODO: make extensible, or don't
 /-- Keywords for which a specific semantic token is provided. -/
@@ -93,6 +98,131 @@ def computeDeltaLspSemanticTokens (tokens : Array AbsoluteLspSemanticToken) : Se
     lastPos := pos
   return { data }
 
+open Lean.Doc.Syntax in
+def isVersoKind (k : SyntaxNodeKind) : Bool :=
+  (`Lean.Doc.Syntax).isPrefixOf k
+
+
+open Lean.Doc.Syntax in
+private partial def collectVersoTokens
+    (stx : Syntax) (getTokens : (stx : Syntax) → Array LeanSemanticToken) :
+    Array LeanSemanticToken :=
+  go stx |>.run #[] |>.2
+where
+  tok (tk : Syntax) (k : SemanticTokenType) : StateM (Array LeanSemanticToken) Unit :=
+    modify (·.push ⟨tk, k⟩)
+
+  go (stx : Syntax) : StateM (Array LeanSemanticToken) Unit := do
+  match stx with
+  | `(arg_val| $x:ident )
+  | `(arg_val| $x:str )
+  | `(arg_val| $x:num ) =>
+    tok x .parameter
+  | `(named| (%$tk1 $x:ident :=%$tk2 $v:arg_val )%$tk3) =>
+    tok tk1 .keyword
+    tok x .property
+    tok tk2 .keyword
+    go v
+    tok tk3 .keyword
+  | `(named_no_paren| $x:ident :=%$tk $v:arg_val ) =>
+    tok x .property
+    tok tk .keyword
+    go v
+  | `(flag_on| +%$tk$x)  | `(flag_off| -%$tk$x) =>
+    tok tk .keyword
+    tok x .property
+  | `(link_target| [%$tk1 $s ]%$tk2) =>
+    tok tk1 .keyword
+    tok s .string
+    tok tk2 .keyword
+  | `(link_target| (%$tk1 $s )%$tk2) =>
+    tok tk1 .keyword
+    tok s .property
+    tok tk2 .keyword
+  | `(inline|$_:str) | `(inline|line! $_) => pure () -- No tokens for plain text or line breaks
+  | `(inline| *[%$tk1 $inls* ]%$tk2) | `(inline|_[%$tk1 $inls* ]%$tk2) =>
+    tok tk1 .keyword
+    inls.forM go
+    tok tk2 .keyword
+  | `(inline| link[%$tk1 $inls* ]%$tk2 $ref) =>
+    tok tk1 .keyword
+    inls.forM go
+    tok tk2 .keyword
+    go ref
+  | `(inline| image(%$tk1 $s )%$tk2 $ref) =>
+    tok tk1 .keyword
+    tok s .string
+    tok tk2 .keyword
+    go ref
+  | `(inline| footnote(%$tk1 $s )%$tk2) =>
+    tok tk1 .keyword
+    tok s .property
+    tok tk2 .keyword
+  | `(inline| code(%$tk1 $s )%$tk2) =>
+    tok tk1 .keyword
+    tok s .string
+    tok tk2 .keyword
+  | `(inline| role{%$tk1 $x $args* }%$tk2 [%$tk3 $inls* ]%$tk4) =>
+    tok tk1 .keyword
+    tok x .function
+    args.forM go
+    tok tk2 .keyword
+    tok tk3 .keyword
+    inls.forM go
+    tok tk4 .keyword
+  | `(inline| \math%$tk1 code(%$tk2 $s )%$tk3)
+  | `(inline| \displaymath%$tk1 code(%$tk2 $s )%$tk3) =>
+    tok tk1 .keyword
+    tok s .string
+    tok tk2 .keyword
+    tok tk3 .keyword
+  | `(list_item| *%$tk $inls*) =>
+    tok tk .keyword
+    inls.forM go
+  | `(desc| :%$tk $inls* => $blks*) =>
+    tok tk .keyword
+    inls.forM go
+    blks.forM go
+  | `(block|para[$inl*]) => inl.forM go
+  | `(block| ```%$tk1 $x $args* | $s ```%$tk2)=>
+    tok tk1 .keyword
+    tok x .function
+    args.forM go
+    tok s .string
+    tok tk2 .keyword
+  | `(block| :::%$tk1 $x $args* { $blks* }%$tk2)=>
+    tok tk1 .keyword
+    tok x .function
+    args.forM go
+    blks.forM go
+    tok tk2 .keyword
+  | `(block| command{%$tk1 $x $args*}%$tk2)=>
+    tok tk1 .keyword
+    tok x .function
+    args.forM go
+    tok tk2 .keyword
+  | `(block| %%%%$tk1 $vals* %%%%$tk2)=>
+    tok tk1 .keyword
+    modify (· ++ getTokens (mkNullNode vals))
+    tok tk2 .keyword
+  | `(block| [%$tk1 $s ]:%$tk2 $url) =>
+    tok tk1 .keyword
+    tok s .property
+    tok tk2 .keyword
+    tok url .string
+  | `(block| [^%$tk1 $s ]:%$tk2 $inls*) =>
+    tok tk1 .keyword
+    tok s .property
+    tok tk2 .keyword
+    inls.forM go
+  | `(block| header(%$tk $_ ){ $inls* })=>
+    tok tk .keyword
+    inls.forM go
+  | `(block|ul{$items*}) | `(block|ol($_){$items*}) | `(block|dl{$items*}) =>
+    items.forM go
+  | _ =>
+    pure ()
+
 /--
 Collects all semantic tokens that can be deduced purely from `Syntax`
 without elaboration information.
@@ -107,6 +237,12 @@ partial def collectSyntaxBasedSemanticTokens : (stx : Syntax) → Array LeanSema
   | stx => Id.run do
     if noHighlightKinds.contains stx.getKind then
       return #[]
+    if docKinds.contains stx.getKind then
+      -- Docs are only highlighted in Verso format, in which case `stx[1]` is a node.
+      if stx[1].isAtom then
+        return #[]
+      else
+        return collectVersoTokens stx[1] collectSyntaxBasedSemanticTokens
     let mut tokens :=
       if stx.isOfKind choiceKind then
         collectSyntaxBasedSemanticTokens stx[0]
@@ -120,10 +256,12 @@ partial def collectSyntaxBasedSemanticTokens : (stx : Syntax) → Array LeanSema
       return tokens
     return tokens.push ⟨stx, keywordSemanticTokenMap.getD val .keyword⟩
 
+
+open Lean.Doc.Syntax in
 /-- Collects all semantic tokens from the given `Elab.InfoTree`. -/
 def collectInfoBasedSemanticTokens (i : Elab.InfoTree) : Array LeanSemanticToken :=
-  List.toArray <| i.deepestNodes fun _ i _ => do
-    let .ofTermInfo ti := i
+  Array.flatten <| List.toArray <| i.deepestNodes fun _ info _ => do
+    let .ofTermInfo ti := info
       | none
     let .original .. := ti.stx.getHeadInfo
       | none
@@ -133,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)

src/Lean/Server/GoTo.lean

@@ -324,6 +324,8 @@ def locationLinksOfInfo (doc : DocumentMeta) (kind : GoToKind) (ictx : InfoWithC
         locationLinksFromCommandInfo cci
       | .ofErrorNameInfo eni =>
         locationLinksFromErrorNameInfo eni
+      | .ofDocElabInfo dei =>
+        locationLinksFromDecl dei.name
       | _ =>
         pure #[]
     if kind == .declaration || ll.isEmpty then

src/Lean/Server/InfoUtils.lean

@@ -186,6 +186,8 @@ def Info.stx : Info → Syntax
   | ofFieldRedeclInfo i    => i.stx
   | ofDelabTermInfo i      => i.stx
   | ofChoiceInfo i         => i.stx
+  | ofDocInfo i            => i.stx
+  | ofDocElabInfo i        => i.stx
 
 def Info.lctx : Info → LocalContext
   | .ofTermInfo i           => i.lctx
@@ -343,6 +345,10 @@ def Info.docString? (i : Info) : MetaM (Option String) := do
   | .ofErrorNameInfo eni => do
     let some errorExplanation := getErrorExplanationRaw? (← getEnv) eni.errorName | return none
     return errorExplanation.summaryWithSeverity
+  | .ofDocInfo di =>
+    return (← findDocString? env di.stx.getKind)
+  | .ofDocElabInfo dei =>
+    return (← findDocString? env dei.name)
   | _ => pure ()
   if let some ei := i.toElabInfo? then
     return ← findDocString? env ei.stx.getKind <||> findDocString? env ei.elaborator

src/Lean/Server/References.lean

@@ -252,6 +252,8 @@ def identOf (ci : ContextInfo) (i : Info) : Option (RefIdent × Bool) := do
     some (RefIdent.const (← getModuleContainingDecl? ci.env fi.projName).toString fi.projName.toString, false)
   | Info.ofOptionInfo oi =>
     some (RefIdent.const (← getModuleContainingDecl? ci.env oi.declName).toString oi.declName.toString, false)
+  | Info.ofDocElabInfo dei =>
+    some (RefIdent.const (← getModuleContainingDecl? ci.env dei.name).toString dei.name.toString, false)
   | _ => none
 
 /-- Finds all references in `trees`. -/

stage0/src/stdlib_flags.h

@@ -1,5 +1,7 @@
 #include "util/options.h"
 
+// Dear CI, please update stage0
+
 namespace lean {
 options get_default_options() {
     options opts;

tests/lean/run/versoDocs.lean

@@ -1,10 +1,14 @@
-
 import Lean
 
+set_option doc.verso true
+
+/-!
+This test checks that the basic features of Verso docstrings work.
+-/
 
 open Lean Doc Elab Term
 
-set_option doc.verso true
+
 
 
 
@@ -23,6 +27,7 @@ def d (s : TSyntaxArray `block) : DocM (Block ElabInline ElabBlock) := do
  -/
 def oneLine := "one line"
 
+set_option doc.verso false
 /--
 x
 yz
@@ -74,6 +79,8 @@ def x (y : Nat) : Nat := y * 5
 #eval show TermElabM Unit from do (← findDocString? (← getEnv) ``x).forM (IO.println ·.quote)
 
 
+set_option doc.verso true
+
 /--
 {name}`inst`
 -/
@@ -197,12 +204,14 @@ def a := "a"
 def b := "b"
 end A
 
+/- Commented out for bootstrapping
 /-- error: Unknown constant `a` -/
 #guard_msgs in
 /--
-{name}`a`
+role {name}`a` here
 -/
 def testDef := 15
+-/
 
 #guard_msgs in
 /--
@@ -220,6 +229,7 @@ def testDef' := 15
 -/
 def testDef'' := 15
 
+/- Commented out for bootstrapping
 /-- error: Unknown constant `b` -/
 #guard_msgs in
 /--
@@ -228,6 +238,7 @@ def testDef'' := 15
 {name}`b`
 -/
 def testDef''' := 15
+-/
 
 #guard_msgs in
 /--
@@ -289,7 +300,7 @@ Examples:
 -/
 def somethingElseAgain := ()
 
-
+/- Commented out for bootstrapping
 /--
 error: Unknown option `pp.alll`
 ---
@@ -308,13 +319,14 @@ Examples:
  * {option}`set_option pp.all "true"` to set it
 -/
 def somethingElseAgain' := ()
-
+-/
 
 /--
 {kw (cat := term)}`Type` {kw (of := termIfLet)}`if`
 -/
 def somethingElseAgain'' := ()
 
+/- Commented out for bootstrapping
 /--
 info:
 
@@ -326,7 +338,7 @@ Hint: Specify the syntax kind:
 {kw?}`Type`
 -/
 def somethingElseAgain''' := ()
-
+-/
 
 /--
 {syntaxCat}`term`