diff --git a/src/Lean/DocString/Add.lean b/src/Lean/DocString/Add.lean
index 9709597308..ac82683ffd 100644
--- a/src/Lean/DocString/Add.lean
+++ b/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
diff --git a/src/Lean/DocString/Extension.lean b/src/Lean/DocString/Extension.lean
index bce9256a2c..0cef53046a 100644
--- a/src/Lean/DocString/Extension.lean
+++ b/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 ""})"
diff --git a/src/Lean/DocString/Formatter.lean b/src/Lean/DocString/Formatter.lean
new file mode 100644
index 0000000000..7dd919124b
--- /dev/null
+++ b/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
diff --git a/src/Lean/DocString/Markdown.lean b/src/Lean/DocString/Markdown.lean
index ea5818126e..bee8a5d705 100644
--- a/src/Lean/DocString/Markdown.lean
+++ b/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
diff --git a/src/Lean/DocString/Parser.lean b/src/Lean/DocString/Parser.lean
index 2ae30749c1..e73615d8fa 100644
--- a/src/Lean/DocString/Parser.lean
+++ b/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
diff --git a/src/Lean/DocString/Syntax.lean b/src/Lean/DocString/Syntax.lean
index 305411b2b0..d6d3453746 100644
--- a/src/Lean/DocString/Syntax.lean
+++ b/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
diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean
index 24674909e2..80f7cee65a 100644
--- a/src/Lean/Elab/BuiltinCommand.lean
+++ b/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) := []) :
diff --git a/src/Lean/Elab/DocString.lean b/src/Lean/Elab/DocString.lean
index 1ca066dda8..70b80d3027 100644
--- a/src/Lean/Elab/DocString.lean
+++ b/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
diff --git a/src/Lean/Elab/InfoTree/Main.lean b/src/Lean/Elab/InfoTree/Main.lean
index 0e245aa192..f7f847c286 100644
--- a/src/Lean/Elab/InfoTree/Main.lean
+++ b/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.
diff --git a/src/Lean/Elab/InfoTree/Types.lean b/src/Lean/Elab/InfoTree/Types.lean
index da7e1d0235..9159a5e8b5 100644
--- a/src/Lean/Elab/InfoTree/Types.lean
+++ b/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
diff --git a/src/Lean/Parser/Command.lean b/src/Lean/Parser/Command.lean
index 539eb983e3..f30e77c94b 100644
--- a/src/Lean/Parser/Command.lean
+++ b/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
 
 /--
diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean
index 218a95ccef..8d55a787d8 100644
--- a/src/Lean/Parser/Term.lean
+++ b/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:
diff --git a/src/Lean/Parser/Term/Basic.lean b/src/Lean/Parser/Term/Basic.lean
new file mode 100644
index 0000000000..deae0ddb19
--- /dev/null
+++ b/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
diff --git a/src/Lean/Server/FileWorker/SemanticHighlighting.lean b/src/Lean/Server/FileWorker/SemanticHighlighting.lean
index 0ccd2729b6..d7219480a6 100644
--- a/src/Lean/Server/FileWorker/SemanticHighlighting.lean
+++ b/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)
diff --git a/src/Lean/Server/GoTo.lean b/src/Lean/Server/GoTo.lean
index 9bfbbfe7b3..b76607710d 100644
--- a/src/Lean/Server/GoTo.lean
+++ b/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
diff --git a/src/Lean/Server/InfoUtils.lean b/src/Lean/Server/InfoUtils.lean
index 280df1d40b..9bdae6fcf8 100644
--- a/src/Lean/Server/InfoUtils.lean
+++ b/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
diff --git a/src/Lean/Server/References.lean b/src/Lean/Server/References.lean
index fff1a78d72..1bd4fffcf2 100644
--- a/src/Lean/Server/References.lean
+++ b/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`. -/
diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h
index 79a0e58edd..0b833d9dc4 100644
--- a/stage0/src/stdlib_flags.h
+++ b/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;
diff --git a/tests/lean/run/versoDocs.lean b/tests/lean/run/versoDocs.lean
index e254b006bd..6df7bb1d6c 100644
--- a/tests/lean/run/versoDocs.lean
+++ b/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`