From f90542ac3071707a76a3591786255c863a21dd23 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Sun, 28 Dec 2025 14:30:28 -0500
Subject: [PATCH 1/8] feat: allow block elaboration to target a typed syntax

---
 src/tests/Tests/VersoManual/Markdown.lean     |  2 +-
 src/verso-blog/VersoBlog.lean                 |  4 +-
 .../VersoBlog/LiterateLeanPage.lean           |  2 +-
 src/verso-manual/VersoManual.lean             | 10 +--
 src/verso-manual/VersoManual/Docstring.lean   |  4 +-
 src/verso-manual/VersoManual/Draft.lean       |  2 +-
 src/verso-manual/VersoManual/InlineLean.lean  |  2 +-
 .../VersoManual/InlineLean/IO.lean            |  2 +-
 src/verso-manual/VersoManual/Markdown.lean    |  2 +-
 src/verso-manual/VersoManual/Table.lean       |  2 +-
 src/verso/Verso/Doc/Elab.lean                 | 88 ++++++++-----------
 src/verso/Verso/Doc/Elab/Basic.lean           | 84 +++++++++++++++---
 src/verso/Verso/Doc/Elab/Block.lean           | 34 +++++--
 src/verso/Verso/Doc/Elab/Inline.lean          |  2 +-
 src/verso/Verso/Doc/Elab/Monad.lean           | 31 +++++--
 15 files changed, 177 insertions(+), 94 deletions(-)

diff --git a/src/tests/Tests/VersoManual/Markdown.lean b/src/tests/Tests/VersoManual/Markdown.lean
index cc18014e..fdceaff6 100644
--- a/src/tests/Tests/VersoManual/Markdown.lean
+++ b/src/tests/Tests/VersoManual/Markdown.lean
@@ -20,7 +20,7 @@ To avoid off-by-one misunderstandings: The heading level is equal to
 the number of # characters in the opening sequence. (cf. [CommonMark
 Spec](https://spec.commonmark.org/0.31.2/))
 -/
-def displayPartStructure (part : FinishedPart) (level : Nat := 1) : String := match part with
+def displayPartStructure (part : Part) (level : Nat := 1) : String := match part with
   | .mk _ _ title _ _ subParts _ =>
        let partsStr : String := subParts.map (displayPartStructure · (level + 1))
          |>.toList |> String.join
diff --git a/src/verso-blog/VersoBlog.lean b/src/verso-blog/VersoBlog.lean
index 8ce187b0..1d361988 100644
--- a/src/verso-blog/VersoBlog.lean
+++ b/src/verso-blog/VersoBlog.lean
@@ -62,7 +62,7 @@ Wraps the contents in an HTML `<div>` element with the provided `class`.
 @[directive]
 def htmlDiv : DirectiveExpanderOf ClassArgs
   | {«class»}, stxs => do
-    let contents ← stxs.mapM elabBlock
+    let contents ← stxs.mapM elabBlockTerm
     ``(Block.other (Blog.BlockExt.htmlDiv $(quote «class»)) #[ $contents,* ])
 
 
@@ -83,7 +83,7 @@ instance : FromArgs HtmlArgs DocElabM where
 def html : DirectiveExpanderOf HtmlArgs
   | {name, attrs}, stxs => do
     let tag := name.toString (escape := false)
-    let contents ← stxs.mapM elabBlock
+    let contents ← stxs.mapM elabBlockTerm
     ``(Block.other (Blog.BlockExt.htmlWrapper $(quote tag) $(quote attrs)) #[ $contents,* ])
 
 structure BlobArgs where
diff --git a/src/verso-blog/VersoBlog/LiterateLeanPage.lean b/src/verso-blog/VersoBlog/LiterateLeanPage.lean
index 8266cdd8..99cbcf40 100644
--- a/src/verso-blog/VersoBlog/LiterateLeanPage.lean
+++ b/src/verso-blog/VersoBlog/LiterateLeanPage.lean
@@ -524,7 +524,7 @@ def elabLiteratePage (x : Ident) (path : StrLit) (mod : Ident) (config : LitPage
       match p with
       | .mk t1 t2 t3 _ bs ps pos =>
         -- Propagate metadata fields
-        FinishedPart.mk t1 t2 t3 «meta» bs ps pos
+        Part.mk t1 t2 t3 «meta» bs ps pos
       | _ => p
     else finished
 
diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean
index 6098fd9a..ecd98bdc 100644
--- a/src/verso-manual/VersoManual.lean
+++ b/src/verso-manual/VersoManual.lean
@@ -47,7 +47,7 @@ open Std (HashMap)
 
 open Verso.FS
 
-open Verso.Doc Elab
+open Verso.Doc
 open Verso.Multi
 open Verso.Genre.Manual.TeX
 open Verso.Genre.Manual.WordCount
@@ -139,9 +139,9 @@ end
 Inserts a reference to the provided tag.
 -/
 @[role]
-def ref : RoleExpanderOf RoleArgs
+def ref : Elab.RoleExpanderOf RoleArgs
   | {canonicalName, domain, remote}, content => do
-    let content ← content.mapM elabInline
+    let content ← content.mapM Elab.elabInline
     ``(Inline.other (Inline.ref $(quote canonicalName) $(quote domain) $(quote remote)) #[$content,*])
 
 block_extension Block.paragraph where
@@ -161,9 +161,9 @@ paragraph. In HTML output, they are rendered with less space between them, and L
 a single paragraph (e.g. without extraneous indentation).
 -/
 @[directive]
-def paragraph : DirectiveExpanderOf Unit
+def paragraph : Elab.DirectiveExpanderOf Unit
   | (), stxs => do
-    let args ← stxs.mapM elabBlock
+    let args ← stxs.mapM Elab.elabBlockTerm
     ``(Block.other Block.paragraph #[ $[ $args ],* ])
 
 structure Config extends HtmlConfig where
diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean
index 1cccc1e7..20214e8b 100644
--- a/src/verso-manual/VersoManual/Docstring.lean
+++ b/src/verso-manual/VersoManual/Docstring.lean
@@ -1695,7 +1695,7 @@ def tactic : DirectiveExpanderOf TacticDocsOptions
         let some mdAst := MD4Lean.parse str
           | throwError m!"Failed to parse docstring as Markdown. Docstring contents:\n{repr str}"
         mdAst.blocks.mapM (blockFromMarkdownWithLean [])
-    let userContents ← more.mapM elabBlock
+    let userContents ← more.mapM elabBlockTerm
     ``(Verso.Doc.Block.other (Block.tactic $(quote tactic) $(quote opts.show)) #[$(contents ++ userContents),*])
 
 def Inline.tactic : Inline where
@@ -1851,7 +1851,7 @@ def conv : DirectiveExpanderOf TacticDocsOptions
           | throwError "Failed to parse docstring as Markdown"
         mdAst.blocks.mapM (blockFromMarkdownWithLean [])
       else pure #[]
-    let userContents ← more.mapM elabBlock
+    let userContents ← more.mapM elabBlockTerm
     let some toShow := opts.show
       | throwError "An explicit 'show' is mandatory for conv docs (for now)"
     ``(Verso.Doc.Block.other (Block.conv $(quote tactic.name) $(quote toShow) $(quote tactic.docs?)) #[$(contents ++ userContents),*])
diff --git a/src/verso-manual/VersoManual/Draft.lean b/src/verso-manual/VersoManual/Draft.lean
index c2af1dbd..332fdfb7 100644
--- a/src/verso-manual/VersoManual/Draft.lean
+++ b/src/verso-manual/VersoManual/Draft.lean
@@ -59,4 +59,4 @@ def draft : RoleExpanderOf Unit
 @[directive draft]
 def draftBlock : DirectiveExpanderOf Unit
   | (), contents => do
-    ``(Verso.Doc.Block.other Block.draft #[$[$(← contents.mapM elabBlock)],*])
+    ``(Verso.Doc.Block.other Block.draft #[$[$(← contents.mapM elabBlockTerm)],*])
diff --git a/src/verso-manual/VersoManual/InlineLean.lean b/src/verso-manual/VersoManual/InlineLean.lean
index 6b79e893..6d0b2e8b 100644
--- a/src/verso-manual/VersoManual/InlineLean.lean
+++ b/src/verso-manual/VersoManual/InlineLean.lean
@@ -536,7 +536,7 @@ def leanSection : DirectiveExpander
     let start ← `(block|```lean $arg | $(quote code) ```)
     let code := name?.map (s!"end {·}") |>.getD "end"
     let «end» ← `(block|```lean $arg | $(quote code) ```)
-    return #[← elabBlock start] ++ (← contents.mapM elabBlock) ++ #[← elabBlock «end»]
+    return #[← elabBlockTerm start] ++ (← contents.mapM elabBlockTerm) ++ #[← elabBlockTerm «end»]
 
 private def getClass : MessageSeverity → String
   | .error => "error"
diff --git a/src/verso-manual/VersoManual/InlineLean/IO.lean b/src/verso-manual/VersoManual/InlineLean/IO.lean
index f7df2961..b7ba8bd1 100644
--- a/src/verso-manual/VersoManual/InlineLean/IO.lean
+++ b/src/verso-manual/VersoManual/InlineLean/IO.lean
@@ -545,5 +545,5 @@ open IOExample in
 def ioExample : DirectiveExpanderOf Unit
  | (), blocks => do
     startExample
-    let body ← blocks.mapM elabBlock
+    let body ← blocks.mapM elabBlockTerm
     ``(Verso.Doc.Block.concat #[$body,*]) >>= endExample
diff --git a/src/verso-manual/VersoManual/Markdown.lean b/src/verso-manual/VersoManual/Markdown.lean
index a8499c84..3af7709c 100644
--- a/src/verso-manual/VersoManual/Markdown.lean
+++ b/src/verso-manual/VersoManual/Markdown.lean
@@ -359,7 +359,7 @@ To avoid off-by-one misunderstandings: The heading level is equal to
 the number of # characters in the opening sequence. (cf. [CommonMark
 Spec](https://spec.commonmark.org/0.31.2/))
 -/
-def displayPartStructure (part : FinishedPart) (level : Nat := 1) : String := match part with
+def displayPartStructure (part : Part) (level : Nat := 1) : String := match part with
   | .mk _ _ title _ _ subParts _ =>
        let partsStr : String := subParts.map (displayPartStructure · (level + 1))
          |>.toList |> String.join
diff --git a/src/verso-manual/VersoManual/Table.lean b/src/verso-manual/VersoManual/Table.lean
index 7f6f2ba0..6994de2d 100644
--- a/src/verso-manual/VersoManual/Table.lean
+++ b/src/verso-manual/VersoManual/Table.lean
@@ -210,7 +210,7 @@ def table : DirectiveExpanderOf TableConfig
         throwErrorAt oneBlock s!"Expected all rows to have same number of columns, but got {rows.map (·.size)}"
 
       let flattened := rows.flatten
-      let blocks : Array (Syntax.TSepArray `term ",") ← flattened.mapM (·.mapM elabBlock)
+      let blocks : Array (Syntax.TSepArray `term ",") ← flattened.mapM (·.mapM elabBlockTerm)
       ``(Block.other (Block.table $(quote columns) $(quote cfg.header) $(quote cfg.name) $(quote cfg.alignment)) #[Block.ul #[$[Verso.Doc.ListItem.mk #[$blocks,*]],*]])
 
 where
diff --git a/src/verso/Verso/Doc/Elab.lean b/src/verso/Verso/Doc/Elab.lean
index 0313aa2e..d594732b 100644
--- a/src/verso/Verso/Doc/Elab.lean
+++ b/src/verso/Verso/Doc/Elab.lean
@@ -136,7 +136,7 @@ public meta def _root_.Lean.Doc.Syntax.role.expand : InlineExpander
           try
             let termStxs ← withFreshMacroScope <| e argVals subjects
             expanderDocHover name "Role" resolvedName doc? sig?
-            let termStxs ← termStxs.mapM fun t => (``(($t : Inline $(⟨genre⟩))))
+            let termStxs ← termStxs.mapM fun t => (``(($t : Doc.Inline $(⟨genre⟩))))
             if h : termStxs.size = 1 then return termStxs[0]
             else return (← ``(Inline.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*]))
           catch
@@ -234,7 +234,7 @@ where
       throwErrorAt cmd "{msg}\n{note}"
     let hygenicName := some <| mkIdent (← mkFreshUserName `docReconstInBlock)
     let blk ← withTheReader DocElabContext ({ · with docReconstructionPlaceholder := hygenicName }) <|
-      elabBlock cmd
+      elabBlockTerm cmd
     addBlock blk (blockInternalDocReconstructionPlaceholder := hygenicName)
 
 @[part_command Lean.Doc.Syntax.footnote_ref]
@@ -327,23 +327,22 @@ public meta def includeSection : PartCommand
 where
  resolved id := mkIdentFrom id <$> realizeGlobalConstNoOverloadWithInfo (mkIdentFrom id (docName id.getId))
 
-@[block_expander Lean.Doc.Syntax.command]
-public meta def _root_.Lean.Doc.Syntax.command.expand : BlockExpander := fun block =>
+@[block_elab Lean.Doc.Syntax.command]
+public meta def _root_.Lean.Doc.Syntax.command.expand : BlockElab := fun block =>
   match block with
   | `(block|command{$name $args*}) => do
     withTraceNode `Elab.Verso.block (fun _ => pure m!"Block role {name}") <|
     withRef block <| withFreshMacroScope <| withIncRecDepth <| do
-      let genre := (← readThe DocElabContext).genreSyntax
       let resolvedName ← realizeGlobalConstNoOverloadWithInfo name
       let exp ← blockCommandExpandersFor resolvedName
       let argVals ← parseArgs args
       if exp.isEmpty then
-        return ← appFallback block name resolvedName argVals none
+        return .stx (← appFallback block name resolvedName argVals none)
       for (e, doc?, sig?) in exp do
         try
           let termStxs ← withFreshMacroScope <| e argVals
           expanderDocHover name "Command" resolvedName doc? sig?
-          return (← ``(Block.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*]))
+          return Block.concat (termStxs.map .stx)
         catch
           | ex@(.internal id) =>
             if id == unsupportedSyntaxExceptionId then pure ()
@@ -352,31 +351,26 @@ public meta def _root_.Lean.Doc.Syntax.command.expand : BlockExpander := fun blo
       throwUnsupportedSyntax
   | _ => throwUnsupportedSyntax
 
-@[block_expander Lean.Doc.Syntax.para]
-public meta partial def _root_.Lean.Doc.Syntax.para.expand : BlockExpander
+@[block_elab Lean.Doc.Syntax.para]
+public meta partial def _root_.Lean.Doc.Syntax.para.expand : BlockElab
   | `(block| para[ $args:inline* ]) => do
-    let genre := (← readThe DocElabContext).genreSyntax
-    ``(Block.para (genre := $(⟨genre⟩)) #[$[$(← args.mapM elabInline)],*])
+    return Block.para (← args.mapM elabInline)
   | _ =>
     throwUnsupportedSyntax
 
-
-meta def elabLi (block : Syntax) : DocElabM (Syntax × TSyntax `term) :=
+meta def elabLi (block : Syntax) : DocElabM (Syntax × Array Block) :=
   withRef block <|
   match block with
   | `(list_item|*%$dot $contents:block*) => do
-    let genre := (← readThe DocElabContext).genreSyntax
-    let item ← ``(ListItem.mk (α := Block $(⟨genre⟩)) #[$[$(← contents.mapM elabBlock)],*])
-    pure (dot, item)
+    pure (dot, ← contents.mapM elabBlock')
   | _ =>
     throwUnsupportedSyntax
 
-@[block_expander Lean.Doc.Syntax.ul]
-public meta def _root_.Lean.Doc.Syntax.ul.expand : BlockExpander
+@[block_elab Lean.Doc.Syntax.ul]
+public meta def _root_.Lean.Doc.Syntax.ul.expand : BlockElab
   | `(block|ul{$itemStxs*}) => do
-    let genre := (← readThe DocElabContext).genreSyntax
     let mut bullets : Array Syntax := #[]
-    let mut items : Array (TSyntax `term) := #[]
+    let mut items : Array (Array Block) := #[]
     for i in itemStxs do
       let (b, item) ← elabLi i
       bullets := bullets.push b
@@ -384,16 +378,15 @@ public meta def _root_.Lean.Doc.Syntax.ul.expand : BlockExpander
     let info := DocListInfo.mk bullets itemStxs
     for b in bullets do
       pushInfoLeaf <| .ofCustomInfo {stx := b, value := Dynamic.mk info}
-    ``(Block.ul (genre := $(⟨genre⟩)) #[$items,*])
+    return Block.ul items
   | _ =>
     throwUnsupportedSyntax
 
-@[block_expander Lean.Doc.Syntax.ol]
-public meta def _root_.Lean.Doc.Syntax.ol.expand : BlockExpander
+@[block_elab Lean.Doc.Syntax.ol]
+public meta def _root_.Lean.Doc.Syntax.ol.expand : BlockElab
   | `(block|ol($start:num){$itemStxs*}) => do
-    let genre := (← readThe DocElabContext).genreSyntax
     let mut bullets : Array Syntax := #[]
-    let mut items : Array (TSyntax `term) := #[]
+    let mut items : Array (Array Block) := #[]
     for i in itemStxs do
       let (b, item) ← elabLi i
       bullets := bullets.push b
@@ -401,49 +394,45 @@ public meta def _root_.Lean.Doc.Syntax.ol.expand : BlockExpander
     let info := DocListInfo.mk bullets itemStxs
     for b in bullets do
       pushInfoLeaf <| .ofCustomInfo {stx := b, value := Dynamic.mk info}
-    ``(Block.ol (genre := $(⟨genre⟩)) $start #[$items,*])
+    return Block.ol start.getNat items
   | _ =>
     throwUnsupportedSyntax
 
-meta def elabDesc (block : Syntax) : DocElabM (Syntax × TSyntax `term) :=
+meta def elabDesc (block : Syntax) : DocElabM (Syntax × Array Inline × Array Block) :=
   withRef block <|
   match block with
   | `(desc_item|:%$colon $dts* => $dds*) => do
-    let genre := (← readThe DocElabContext).genreSyntax
-    let item ← ``(DescItem.mk (α := Inline $(⟨genre⟩)) (β := Block $(⟨genre⟩))  #[$[$(← dts.mapM elabInline)],*] #[$[$(← dds.mapM elabBlock)],*])
-    pure (colon, item)
+    return (colon, ← dts.mapM elabInline, ← dds.mapM elabBlock')
   | _ =>
     throwUnsupportedSyntax
 
-@[block_expander Lean.Doc.Syntax.dl]
-public meta def _root_.Lean.Doc.Syntax.dl.expand : BlockExpander
+@[block_elab Lean.Doc.Syntax.dl]
+public meta def _root_.Lean.Doc.Syntax.dl.expand : BlockElab
   | `(block|dl{$itemStxs*}) => do
-    let genre := (← readThe DocElabContext).genreSyntax
     let mut colons : Array Syntax := #[]
-    let mut items : Array (TSyntax `term) := #[]
+    let mut items : Array (Array Inline × Array Block) := #[]
     for i in itemStxs do
-      let (b, item) ← elabDesc i
+      let (b, term, desc) ← elabDesc i
       colons := colons.push b
-      items := items.push item
+      items := items.push (term, desc)
     let info := DocListInfo.mk colons itemStxs
     for b in colons do
       pushInfoLeaf <| .ofCustomInfo {stx := b, value := Dynamic.mk info}
-    ``(Block.dl (genre := $(⟨genre⟩)) #[$[$items],*])
+    return Block.dl items
   | _ =>
     throwUnsupportedSyntax
 
-@[block_expander Lean.Doc.Syntax.blockquote]
-public meta def _root_.Lean.Doc.Syntax.blockquote.expand : BlockExpander
+@[block_elab Lean.Doc.Syntax.blockquote]
+public meta def _root_.Lean.Doc.Syntax.blockquote.expand : BlockElab
   | `(block|> $innerBlocks*) => do
-    ``(Block.blockquote #[$[$(← innerBlocks.mapM elabBlock)],*])
+    return Block.blockquote (← innerBlocks.mapM elabBlock')
   | _ =>
     throwUnsupportedSyntax
 
 
-@[block_expander Lean.Doc.Syntax.codeblock]
-public meta def _root_.Lean.Doc.Syntax.codeblock.expand : BlockExpander
+@[block_elab Lean.Doc.Syntax.codeblock]
+public meta def _root_.Lean.Doc.Syntax.codeblock.expand : BlockElab
   | `(block|``` $nameStx:ident $argsStx* | $contents:str ```) => do
-    let genre := (← readThe DocElabContext).genreSyntax
     let name ← realizeGlobalConstNoOverloadWithInfo nameStx
     let exp ← codeBlockExpandersFor name
     -- TODO typed syntax here
@@ -452,22 +441,21 @@ public meta def _root_.Lean.Doc.Syntax.codeblock.expand : BlockExpander
       try
         let termStxs ← withFreshMacroScope <| e args contents
         expanderDocHover nameStx "Code block" name doc? sig?
-        return (← ``(Block.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*]))
+        return Block.concat (termStxs.map Block.stx)
       catch
         | ex@(.internal id) =>
           if id == unsupportedSyntaxExceptionId then pure ()
           else throw ex
         | ex => throw ex
     throwUnsupportedSyntax
-  | `(block|``` | $contents:str ```) => do
-    ``(Block.code $(quote contents.getString))
+  | `(block|``` | $contents:str ```) =>
+    pure <| Block.code contents.getString
   | _ =>
     throwUnsupportedSyntax
 
-@[block_expander Lean.Doc.Syntax.directive]
-public meta def _root_.Lean.Doc.Syntax.directive.expand : BlockExpander
+@[block_elab Lean.Doc.Syntax.directive]
+public meta def _root_.Lean.Doc.Syntax.directive.expand : BlockElab
   | `(block| ::: $nameStx:ident $argsStx* { $contents:block* } ) => do
-    let genre := (← readThe DocElabContext).genreSyntax
     let name ← realizeGlobalConstNoOverloadWithInfo nameStx
     let exp ← directiveExpandersFor name
     let args ← parseArgs argsStx
@@ -475,7 +463,7 @@ public meta def _root_.Lean.Doc.Syntax.directive.expand : BlockExpander
       try
         let termStxs ← withFreshMacroScope <| e args contents
         expanderDocHover nameStx "Directive" name doc? sig?
-        return (← ``(Block.concat (genre := $(⟨genre⟩)) #[$[$termStxs],*]))
+        return Block.concat (termStxs.map Block.stx)
       catch
         | ex@(.internal id) =>
           if id == unsupportedSyntaxExceptionId then pure ()
diff --git a/src/verso/Verso/Doc/Elab/Basic.lean b/src/verso/Verso/Doc/Elab/Basic.lean
index 5e5e9a14..091e239f 100644
--- a/src/verso/Verso/Doc/Elab/Basic.lean
+++ b/src/verso/Verso/Doc/Elab/Basic.lean
@@ -20,18 +20,74 @@ public inductive TOC where
   | included (name : Ident)
 deriving Repr, TypeName, Inhabited
 
-public inductive FinishedPart where
-  | mk (titleSyntax : Syntax) (expandedTitle : Array (TSyntax `term)) (titlePreview : String) (metadata : Option (TSyntax `term)) (blocks : Array (TSyntax `term)) (subParts : Array FinishedPart) (endPos : String.Pos.Raw)
+/--
+The result of elaborating an inline component of a document
+-/
+public abbrev Inline := Term
+
+variable (genre : Genre) in
+public section
+/--
+The result of elaborating a document block. Concretely denotes a {lean}`Doc.Block genre` for some
+unspecified {name}`genre`.
+-/
+public inductive Block where
+  | para (contents : Array Inline)
+  | code (content : String)
+  | ul (items : Array (Array Block))
+  | ol (start : Int) (items : Array (Array Block))
+  | dl (items : Array ((Array Inline) × (Array Block)))
+  | blockquote (items : Array Block)
+  | concat (content : Array Block)
+  | other (container : Term) (content : Array Block)
+  | stx (stx : Term)
+deriving Repr, BEq
+
+end
+
+mutual
+public partial def ListItem.toTerm [Monad m] [MonadRef m] [MonadQuotation m] (genre : Term) : Array Block → m Term
+  | contents => do ``(Doc.ListItem.mk #[$(← contents.mapM (Block.toTerm genre)),*])
+
+public partial def DescItem.toTerm [Monad m] [MonadRef m] [MonadQuotation m] (genre : Term) : Array Inline × Array Block → m Term
+  | (term, desc) => do ``(Doc.DescItem.mk #[$term,*] #[$(← desc.mapM (Block.toTerm genre)),*])
+
+public partial def Block.toTerm [Monad m] [MonadRef m] [MonadQuotation m] (genre : Term) : Block → m Term
+  | .para contents => ``(Doc.Block.para (genre := $(genre)) #[$contents,*])
+  | .code contents => ``(Doc.Block.code (genre := $(genre)) $(quote contents))
+  | .ul contents => do ``(Doc.Block.ul (genre := $(genre)) #[$(← contents.mapM (ListItem.toTerm genre)),*])
+  | .ol start contents => do ``(Doc.Block.ol (genre := $(genre)) $(← quoteInt start) #[$(← contents.mapM (ListItem.toTerm genre)),*])
+  | .dl contents => do ``(Doc.Block.dl (genre := $(genre)) #[$(← contents.mapM (DescItem.toTerm genre)),*])
+  | .blockquote contents => do ``(Doc.Block.blockquote (genre := $(genre)) #[$(← contents.mapM (Block.toTerm genre)),*])
+  | .concat content => do ``(Doc.Block.concat (genre := $(genre)) #[$(← content.mapM (Block.toTerm genre)),*])
+  | .other container content => do ``(Doc.Block.other (genre := $(genre)) $container #[$(← content.mapM (Block.toTerm genre)),*])
+  | .stx stx => pure stx
+where
+  quoteInt : Int → m Term
+  | .ofNat n => ``(Int.ofNat $(quote n))
+  | .negSucc n => ``(Int.negSucc $(quote n))
+end
+
+variable (genre : Genre) in
+/--
+The result of elaborating a document part. Concretely denotes a {lean}`Doc.Part genre` for some
+unspecified {name}`genre`.
+-/
+public inductive Part where
+  | mk (titleSyntax : Syntax) (expandedTitle : Array Inline) (titlePreview : String) (metadata : Option Term) (blocks : Array Block) (subParts : Array Part) (endPos : String.Pos.Raw)
     /-- A name representing a value of type {lean}`DocThunk` -/
   | included (name : Ident)
 deriving Repr, BEq
 
+@[deprecated Part (since := "2025-12-28")]
+public def FinishedPart := Part
+
 /--
 From a finished part, constructs syntax that denotes its {lean}`Part` value.
 -/
-public partial def FinishedPart.toSyntax [Monad m] [MonadQuotation m]
+public partial def Part.toSyntax [Monad m] [MonadQuotation m]
     (genre : TSyntax `term)
-    : FinishedPart → m Term
+    : Part → m Term
   | .mk _titleStx titleInlines titleString metadata blocks subParts _endPos => do
     let subStx ← subParts.mapM (toSyntax genre)
     let metaStx ←
@@ -40,11 +96,11 @@ public partial def FinishedPart.toSyntax [Monad m] [MonadQuotation m]
       | some stx => `(some $stx)
     -- Adding type annotations works around a limitation in list and array elaboration, where intermediate
     -- let bindings introduced by "chunking" the elaboration may fail to infer types
-    let typedBlocks ← blocks.mapM fun b => `(($b : Block $genre))
-    ``(Part.mk #[$titleInlines,*] $(quote titleString) $metaStx #[$typedBlocks,*] #[$subStx,*])
+    let typedBlocks ← blocks.mapM fun b => do ``(($(← b.toTerm genre) : Doc.Block $genre))
+    ``(Doc.Part.mk #[$titleInlines,*] $(quote titleString) $metaStx #[$typedBlocks,*] #[$subStx,*])
   | .included name => ``(DocThunk.force $name)
 
-public partial def FinishedPart.toTOC : FinishedPart → TOC
+public partial def Part.toTOC : Part → TOC
   | .mk titleStx _titleInlines titleString _metadata _blocks subParts endPos =>
     .mk titleString titleStx endPos (subParts.map toTOC)
   | .included name => .included name
@@ -61,18 +117,18 @@ indicated by the header's level.
 -/
 public structure PartFrame where
   titleSyntax : Syntax
-  expandedTitle : Option (String × Array (TSyntax `term)) := none
-  metadata : Option (TSyntax `term)
-  blocks : Array (TSyntax `term)
+  expandedTitle : Option (String × Array Inline) := none
+  metadata : Option Term
+  blocks : Array Block
   /--
   The sibling parts at the same nesting level as the part represented by this frame. These siblings
   are earlier in the document and have the same parent.
   -/
-  priorParts : Array FinishedPart
+  priorParts : Array Part
 deriving Repr, Inhabited
 
-/-- Turn an previously active {name}`PartFrame` into a {name}`FinishedPart`. -/
-public def PartFrame.close (fr : PartFrame) (endPos : String.Pos.Raw) : FinishedPart :=
+/-- Turn an previously active {name}`PartFrame` into a {name}`Part`. -/
+public def PartFrame.close (fr : PartFrame) (endPos : String.Pos.Raw) : Part :=
   let (titlePreview, titleInlines) := fr.expandedTitle.getD ("<anonymous>", #[])
   .mk fr.titleSyntax titleInlines titlePreview fr.metadata fr.blocks fr.priorParts endPos
 
@@ -107,7 +163,7 @@ parts being built.
 public def PartContext.level (ctxt : PartContext) : Nat := ctxt.parents.size
 
 /--
-Closes the current part. The resulting {name}`FinishedPart` is appended to
+Closes the current part. The resulting {name}`Part` is appended to
 {name (full := PartFrame.priorParts)}`priorParts`, and
 the top of the stack of our parents becomes the current frame. Returns
 {name}`none` if there are no parents.
diff --git a/src/verso/Verso/Doc/Elab/Block.lean b/src/verso/Verso/Doc/Elab/Block.lean
index 9bef0b29..debba665 100644
--- a/src/verso/Verso/Doc/Elab/Block.lean
+++ b/src/verso/Verso/Doc/Elab/Block.lean
@@ -4,11 +4,14 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
 module
+public import Verso.Doc.Elab.Basic
 public import Verso.Doc.Elab.Monad
 meta import Verso.Doc.Elab.Monad
 public import Lean.DocString.Syntax
 import Verso.Doc.Elab.Inline
 
+set_option doc.verso true
+
 namespace Verso.Doc.Elab
 
 open Lean Elab
@@ -26,14 +29,14 @@ def decorateClosing : TSyntax `block → DocElabM Unit
   | _ => pure ()
 
 
-/-- Elaborates a parsed block into syntax denoting an expression of type `Block genre`. -/
-public partial def elabBlock (block : TSyntax `block) : DocElabM (TSyntax `term) :=
+/-- Elaborates a parsed block -/
+public partial def elabBlock' (block : TSyntax `block) : DocElabM Elab.Block :=
   withTraceNode `Elab.Verso.block (fun _ => pure m!"Block {block}") <|
   withRef block <| withFreshMacroScope <| withIncRecDepth <| do
   decorateClosing block
   match block.raw with
   | .missing =>
-    ``(sorryAx Block (synthetic := true))
+    return .stx (← ``(sorryAx Doc.Block (synthetic := true)))
   | stx@(.node _ kind _) =>
     let env ← getEnv
     let result ← match (← liftMacroM (expandMacroImpl? env stx)) with
@@ -41,13 +44,23 @@ public partial def elabBlock (block : TSyntax `block) : DocElabM (TSyntax `term)
       let stxNew ← liftMacroM <| liftExcept stxNew?
       withMacroExpansionInfo stx stxNew <|
         withRef stxNew <|
-          elabBlock ⟨stxNew⟩
+          elabBlock' ⟨stxNew⟩
     | none =>
       let exp ← blockExpandersFor kind
       for e in exp do
         try
           let termStx ← withFreshMacroScope <| e stx
-          return termStx
+          return .stx termStx
+        catch
+          | ex@(.internal id) =>
+            if id == unsupportedSyntaxExceptionId then continue
+            else throw ex
+          | ex => throw ex
+      let exp ← blockElabsFor kind
+      for e in exp do
+        try
+          let block ← withFreshMacroScope <| e stx
+          return block
         catch
           | ex@(.internal id) =>
             if id == unsupportedSyntaxExceptionId then continue
@@ -56,3 +69,14 @@ public partial def elabBlock (block : TSyntax `block) : DocElabM (TSyntax `term)
       throwUnexpected block
   | _ =>
     throwUnexpected block
+
+variable (genre : Genre) in
+/--
+Elaborates a parsed block into syntax denoting an expression of type {lean}`Doc.Block genre`.
+Consider using {name}`elabBlock'` instead.
+-/
+public partial def elabBlockTerm (block : TSyntax `block) : DocElabM Term := do
+  (← elabBlock' block).toTerm ⟨(← readThe DocElabContext).genreSyntax⟩
+
+@[deprecated elabBlockTerm "use `elabBlockTerm` for a precise replacement, or rewrite to use `elabBlock'`" (since := "2025-12-28")]
+public def elabBlock := elabBlockTerm
diff --git a/src/verso/Verso/Doc/Elab/Inline.lean b/src/verso/Verso/Doc/Elab/Inline.lean
index 2f5ace2c..650538c7 100644
--- a/src/verso/Verso/Doc/Elab/Inline.lean
+++ b/src/verso/Verso/Doc/Elab/Inline.lean
@@ -25,7 +25,7 @@ public partial def elabInline (inline : TSyntax `inline) : DocElabM (TSyntax `te
   withRef inline <| withFreshMacroScope <| withIncRecDepth <| do
   match inline.raw with
   | .missing =>
-    ``(sorryAx (Inline _) (synthetic := true))
+    ``(sorryAx (Doc.Inline _) (synthetic := true))
   | stx@(.node _ kind _) =>
     let env ← getEnv
     let result ← match (← liftMacroM (expandMacroImpl? env stx)) with
diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean
index 9b40c6cf..75ad8766 100644
--- a/src/verso/Verso/Doc/Elab/Monad.lean
+++ b/src/verso/Verso/Doc/Elab/Monad.lean
@@ -41,7 +41,7 @@ class HasLink (name : String) (doc : Name) where
   url : String
 
 class HasNote (name : String) (doc : Name) (genre : Genre) where
-  contents : Array (Inline genre)
+  contents : Array (Doc.Inline genre)
 
 private def linkRefName [Monad m] [MonadQuotation m] (docName : Name) (ref : TSyntax `str) : m Term := do
   ``(HasLink.url $(quote ref.getString) $(quote docName))
@@ -343,11 +343,11 @@ public def PartElabM.addBlock (block : TSyntax `term) (blockInternalDocReconstru
 
   modifyThe PartElabM.State fun st =>
     { st with
-      partContext.blocks := st.partContext.blocks.push blockRefSyntax
+      partContext.blocks := st.partContext.blocks.push (.stx blockRefSyntax)
       deferredBlocks := st.deferredBlocks.push (name, blockDefSyntax)
     }
 
-public def PartElabM.addPart (finished : FinishedPart) : PartElabM Unit := modifyThe State fun st =>
+public def PartElabM.addPart (finished : Part) : PartElabM Unit := modifyThe State fun st =>
   { st with partContext.priorParts := st.partContext.priorParts.push finished }
 
 public def PartElabM.addLinkDef (refName : TSyntax `str) (url : String) : PartElabM Unit := do
@@ -464,12 +464,12 @@ unsafe def inlineExpandersForUnsafe (x : Name) : DocElabM (Array InlineExpander)
 public opaque inlineExpandersFor (x : Name) : DocElabM (Array InlineExpander)
 
 /--
-Creates a term denoting a {lean}`DocThunk` value from a {lean}`FinishedPart`. This is the final step
+Creates a term denoting a {lean}`DocThunk` value from a {lean}`Part`. This is the final step
 in turning a parsed verso doc into syntax.
 -/
-public def FinishedPart.toThunkTerm
+public def Part.toThunkTerm
     (genreSyntax : Term)
-    (finished : FinishedPart)
+    (finished : Part)
     (ctx : DocElabContext)
     (docElabState : DocElabM.State)
     (partElabState : PartElabM.State)
@@ -535,8 +535,23 @@ public def FinishedPart.toThunkTerm
 
   ``(DocThunk.serialized (fun $docReconstructionPlaceholder => $finishedSyntax) $(quote reconstJson.compress) none)
 
-@[deprecated FinishedPart.toThunkTerm (since := "2025-11-28")]
-public def FinishedPart.toVersoDoc : Term → FinishedPart → DocElabContext → DocElabM.State → PartElabM.State → TermElabM Term := FinishedPart.toThunkTerm
+@[deprecated Part.toThunkTerm (since := "2025-11-28")]
+public def FinishedPart.toVersoDoc : Term → Part → DocElabContext → DocElabM.State → PartElabM.State → TermElabM Term := Part.toThunkTerm
+
+@[deprecated Part.toThunkTerm (since := "2025-11-28")]
+public def Part.toVersoDoc : Term → Part → DocElabContext → DocElabM.State → PartElabM.State → TermElabM Term := Part.toThunkTerm
+
+public abbrev BlockElab := Syntax → DocElabM Elab.Block
+
+initialize blockElabAttr : KeyedDeclsAttribute BlockElab ←
+  mkDocExpanderAttribute `block_elab ``BlockElab "Indicates that this function expands block elements of a given name" `blockElabAttr
+
+unsafe def blockElabsForUnsafe (x : Name) : DocElabM (Array BlockElab) := do
+  let expanders := blockElabAttr.getEntries (← getEnv) x
+  return expanders.map (·.value) |>.toArray
+
+@[implemented_by blockElabsForUnsafe]
+public opaque blockElabsFor (x : Name) : DocElabM (Array BlockElab)
 
 public abbrev BlockExpander := Syntax → DocElabM (TSyntax `term)
 

From 052dcb41a5606859df85d4d0cec66ac69f11405b Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Sun, 28 Dec 2025 15:15:05 -0500
Subject: [PATCH 2/8] Back out of some changes due to level of namespace
 conflicts

---
 .../VersoBlog/LiterateLeanPage.lean           |  2 +-
 src/verso-manual/VersoManual/Markdown.lean    |  2 +-
 src/verso/Verso/Doc/Elab.lean                 | 28 ++++++++---------
 src/verso/Verso/Doc/Elab/Basic.lean           | 30 +++++++++----------
 src/verso/Verso/Doc/Elab/Block.lean           |  2 +-
 src/verso/Verso/Doc/Elab/Inline.lean          |  2 +-
 src/verso/Verso/Doc/Elab/Monad.lean           | 15 ++++------
 7 files changed, 39 insertions(+), 42 deletions(-)

diff --git a/src/verso-blog/VersoBlog/LiterateLeanPage.lean b/src/verso-blog/VersoBlog/LiterateLeanPage.lean
index 99cbcf40..8266cdd8 100644
--- a/src/verso-blog/VersoBlog/LiterateLeanPage.lean
+++ b/src/verso-blog/VersoBlog/LiterateLeanPage.lean
@@ -524,7 +524,7 @@ def elabLiteratePage (x : Ident) (path : StrLit) (mod : Ident) (config : LitPage
       match p with
       | .mk t1 t2 t3 _ bs ps pos =>
         -- Propagate metadata fields
-        Part.mk t1 t2 t3 «meta» bs ps pos
+        FinishedPart.mk t1 t2 t3 «meta» bs ps pos
       | _ => p
     else finished
 
diff --git a/src/verso-manual/VersoManual/Markdown.lean b/src/verso-manual/VersoManual/Markdown.lean
index 3af7709c..a8499c84 100644
--- a/src/verso-manual/VersoManual/Markdown.lean
+++ b/src/verso-manual/VersoManual/Markdown.lean
@@ -359,7 +359,7 @@ To avoid off-by-one misunderstandings: The heading level is equal to
 the number of # characters in the opening sequence. (cf. [CommonMark
 Spec](https://spec.commonmark.org/0.31.2/))
 -/
-def displayPartStructure (part : Part) (level : Nat := 1) : String := match part with
+def displayPartStructure (part : FinishedPart) (level : Nat := 1) : String := match part with
   | .mk _ _ title _ _ subParts _ =>
        let partsStr : String := subParts.map (displayPartStructure · (level + 1))
          |>.toList |> String.join
diff --git a/src/verso/Verso/Doc/Elab.lean b/src/verso/Verso/Doc/Elab.lean
index d594732b..c59b35eb 100644
--- a/src/verso/Verso/Doc/Elab.lean
+++ b/src/verso/Verso/Doc/Elab.lean
@@ -342,7 +342,7 @@ public meta def _root_.Lean.Doc.Syntax.command.expand : BlockElab := fun block =
         try
           let termStxs ← withFreshMacroScope <| e argVals
           expanderDocHover name "Command" resolvedName doc? sig?
-          return Block.concat (termStxs.map .stx)
+          return .concat (termStxs.map .stx)
         catch
           | ex@(.internal id) =>
             if id == unsupportedSyntaxExceptionId then pure ()
@@ -354,11 +354,11 @@ public meta def _root_.Lean.Doc.Syntax.command.expand : BlockElab := fun block =
 @[block_elab Lean.Doc.Syntax.para]
 public meta partial def _root_.Lean.Doc.Syntax.para.expand : BlockElab
   | `(block| para[ $args:inline* ]) => do
-    return Block.para (← args.mapM elabInline)
+    return .para (← args.mapM elabInline)
   | _ =>
     throwUnsupportedSyntax
 
-meta def elabLi (block : Syntax) : DocElabM (Syntax × Array Block) :=
+meta def elabLi (block : Syntax) : DocElabM (Syntax × Array Target.Block) :=
   withRef block <|
   match block with
   | `(list_item|*%$dot $contents:block*) => do
@@ -370,7 +370,7 @@ meta def elabLi (block : Syntax) : DocElabM (Syntax × Array Block) :=
 public meta def _root_.Lean.Doc.Syntax.ul.expand : BlockElab
   | `(block|ul{$itemStxs*}) => do
     let mut bullets : Array Syntax := #[]
-    let mut items : Array (Array Block) := #[]
+    let mut items : Array (Array Target.Block) := #[]
     for i in itemStxs do
       let (b, item) ← elabLi i
       bullets := bullets.push b
@@ -378,7 +378,7 @@ public meta def _root_.Lean.Doc.Syntax.ul.expand : BlockElab
     let info := DocListInfo.mk bullets itemStxs
     for b in bullets do
       pushInfoLeaf <| .ofCustomInfo {stx := b, value := Dynamic.mk info}
-    return Block.ul items
+    return .ul items
   | _ =>
     throwUnsupportedSyntax
 
@@ -386,7 +386,7 @@ public meta def _root_.Lean.Doc.Syntax.ul.expand : BlockElab
 public meta def _root_.Lean.Doc.Syntax.ol.expand : BlockElab
   | `(block|ol($start:num){$itemStxs*}) => do
     let mut bullets : Array Syntax := #[]
-    let mut items : Array (Array Block) := #[]
+    let mut items : Array (Array Target.Block) := #[]
     for i in itemStxs do
       let (b, item) ← elabLi i
       bullets := bullets.push b
@@ -394,11 +394,11 @@ public meta def _root_.Lean.Doc.Syntax.ol.expand : BlockElab
     let info := DocListInfo.mk bullets itemStxs
     for b in bullets do
       pushInfoLeaf <| .ofCustomInfo {stx := b, value := Dynamic.mk info}
-    return Block.ol start.getNat items
+    return .ol start.getNat items
   | _ =>
     throwUnsupportedSyntax
 
-meta def elabDesc (block : Syntax) : DocElabM (Syntax × Array Inline × Array Block) :=
+meta def elabDesc (block : Syntax) : DocElabM (Syntax × Array Target.Inline × Array Target.Block) :=
   withRef block <|
   match block with
   | `(desc_item|:%$colon $dts* => $dds*) => do
@@ -410,7 +410,7 @@ meta def elabDesc (block : Syntax) : DocElabM (Syntax × Array Inline × Array B
 public meta def _root_.Lean.Doc.Syntax.dl.expand : BlockElab
   | `(block|dl{$itemStxs*}) => do
     let mut colons : Array Syntax := #[]
-    let mut items : Array (Array Inline × Array Block) := #[]
+    let mut items : Array (Array Target.Inline × Array Target.Block) := #[]
     for i in itemStxs do
       let (b, term, desc) ← elabDesc i
       colons := colons.push b
@@ -418,14 +418,14 @@ public meta def _root_.Lean.Doc.Syntax.dl.expand : BlockElab
     let info := DocListInfo.mk colons itemStxs
     for b in colons do
       pushInfoLeaf <| .ofCustomInfo {stx := b, value := Dynamic.mk info}
-    return Block.dl items
+    return .dl items
   | _ =>
     throwUnsupportedSyntax
 
 @[block_elab Lean.Doc.Syntax.blockquote]
 public meta def _root_.Lean.Doc.Syntax.blockquote.expand : BlockElab
   | `(block|> $innerBlocks*) => do
-    return Block.blockquote (← innerBlocks.mapM elabBlock')
+    return .blockquote (← innerBlocks.mapM elabBlock')
   | _ =>
     throwUnsupportedSyntax
 
@@ -441,7 +441,7 @@ public meta def _root_.Lean.Doc.Syntax.codeblock.expand : BlockElab
       try
         let termStxs ← withFreshMacroScope <| e args contents
         expanderDocHover nameStx "Code block" name doc? sig?
-        return Block.concat (termStxs.map Block.stx)
+        return .concat (termStxs.map .stx)
       catch
         | ex@(.internal id) =>
           if id == unsupportedSyntaxExceptionId then pure ()
@@ -449,7 +449,7 @@ public meta def _root_.Lean.Doc.Syntax.codeblock.expand : BlockElab
         | ex => throw ex
     throwUnsupportedSyntax
   | `(block|``` | $contents:str ```) =>
-    pure <| Block.code contents.getString
+    pure <| .code contents.getString
   | _ =>
     throwUnsupportedSyntax
 
@@ -463,7 +463,7 @@ public meta def _root_.Lean.Doc.Syntax.directive.expand : BlockElab
       try
         let termStxs ← withFreshMacroScope <| e args contents
         expanderDocHover nameStx "Directive" name doc? sig?
-        return Block.concat (termStxs.map Block.stx)
+        return .concat (termStxs.map .stx)
       catch
         | ex@(.internal id) =>
           if id == unsupportedSyntaxExceptionId then pure ()
diff --git a/src/verso/Verso/Doc/Elab/Basic.lean b/src/verso/Verso/Doc/Elab/Basic.lean
index 091e239f..f27b084b 100644
--- a/src/verso/Verso/Doc/Elab/Basic.lean
+++ b/src/verso/Verso/Doc/Elab/Basic.lean
@@ -20,6 +20,8 @@ public inductive TOC where
   | included (name : Ident)
 deriving Repr, TypeName, Inhabited
 
+/- Elaboration targets -/
+namespace Target
 /--
 The result of elaborating an inline component of a document
 -/
@@ -46,8 +48,8 @@ deriving Repr, BEq
 end
 
 mutual
-public partial def ListItem.toTerm [Monad m] [MonadRef m] [MonadQuotation m] (genre : Term) : Array Block → m Term
-  | contents => do ``(Doc.ListItem.mk #[$(← contents.mapM (Block.toTerm genre)),*])
+public partial def ListItem.toTerm [Monad m] [MonadRef m] [MonadQuotation m] (genre : Term) : Array Target.Block → m Term
+  | contents => do ``(Doc.ListItem.mk #[$(← contents.mapM (Target.Block.toTerm genre)),*])
 
 public partial def DescItem.toTerm [Monad m] [MonadRef m] [MonadQuotation m] (genre : Term) : Array Inline × Array Block → m Term
   | (term, desc) => do ``(Doc.DescItem.mk #[$term,*] #[$(← desc.mapM (Block.toTerm genre)),*])
@@ -68,26 +70,25 @@ where
   | .negSucc n => ``(Int.negSucc $(quote n))
 end
 
+end Target
+
 variable (genre : Genre) in
 /--
 The result of elaborating a document part. Concretely denotes a {lean}`Doc.Part genre` for some
 unspecified {name}`genre`.
 -/
-public inductive Part where
-  | mk (titleSyntax : Syntax) (expandedTitle : Array Inline) (titlePreview : String) (metadata : Option Term) (blocks : Array Block) (subParts : Array Part) (endPos : String.Pos.Raw)
+public inductive FinishedPart where
+  | mk (titleSyntax : Syntax) (expandedTitle : Array Target.Inline) (titlePreview : String) (metadata : Option Term) (blocks : Array Target.Block) (subParts : Array FinishedPart) (endPos : String.Pos.Raw)
     /-- A name representing a value of type {lean}`DocThunk` -/
   | included (name : Ident)
 deriving Repr, BEq
 
-@[deprecated Part (since := "2025-12-28")]
-public def FinishedPart := Part
-
 /--
 From a finished part, constructs syntax that denotes its {lean}`Part` value.
 -/
-public partial def Part.toSyntax [Monad m] [MonadQuotation m]
+public partial def FinishedPart.toSyntax [Monad m] [MonadQuotation m]
     (genre : TSyntax `term)
-    : Part → m Term
+    : FinishedPart → m Term
   | .mk _titleStx titleInlines titleString metadata blocks subParts _endPos => do
     let subStx ← subParts.mapM (toSyntax genre)
     let metaStx ←
@@ -100,12 +101,11 @@ public partial def Part.toSyntax [Monad m] [MonadQuotation m]
     ``(Doc.Part.mk #[$titleInlines,*] $(quote titleString) $metaStx #[$typedBlocks,*] #[$subStx,*])
   | .included name => ``(DocThunk.force $name)
 
-public partial def Part.toTOC : Part → TOC
+public partial def FinishedPart.toTOC : FinishedPart → TOC
   | .mk titleStx _titleInlines titleString _metadata _blocks subParts endPos =>
     .mk titleString titleStx endPos (subParts.map toTOC)
   | .included name => .included name
 
-
 /--
 Information describing a part still under construction.
 
@@ -117,18 +117,18 @@ indicated by the header's level.
 -/
 public structure PartFrame where
   titleSyntax : Syntax
-  expandedTitle : Option (String × Array Inline) := none
+  expandedTitle : Option (String × Array Target.Inline) := none
   metadata : Option Term
-  blocks : Array Block
+  blocks : Array Target.Block
   /--
   The sibling parts at the same nesting level as the part represented by this frame. These siblings
   are earlier in the document and have the same parent.
   -/
-  priorParts : Array Part
+  priorParts : Array FinishedPart
 deriving Repr, Inhabited
 
 /-- Turn an previously active {name}`PartFrame` into a {name}`Part`. -/
-public def PartFrame.close (fr : PartFrame) (endPos : String.Pos.Raw) : Part :=
+public def PartFrame.close (fr : PartFrame) (endPos : String.Pos.Raw) : FinishedPart :=
   let (titlePreview, titleInlines) := fr.expandedTitle.getD ("<anonymous>", #[])
   .mk fr.titleSyntax titleInlines titlePreview fr.metadata fr.blocks fr.priorParts endPos
 
diff --git a/src/verso/Verso/Doc/Elab/Block.lean b/src/verso/Verso/Doc/Elab/Block.lean
index debba665..6250feb9 100644
--- a/src/verso/Verso/Doc/Elab/Block.lean
+++ b/src/verso/Verso/Doc/Elab/Block.lean
@@ -30,7 +30,7 @@ def decorateClosing : TSyntax `block → DocElabM Unit
 
 
 /-- Elaborates a parsed block -/
-public partial def elabBlock' (block : TSyntax `block) : DocElabM Elab.Block :=
+public partial def elabBlock' (block : TSyntax `block) : DocElabM Target.Block :=
   withTraceNode `Elab.Verso.block (fun _ => pure m!"Block {block}") <|
   withRef block <| withFreshMacroScope <| withIncRecDepth <| do
   decorateClosing block
diff --git a/src/verso/Verso/Doc/Elab/Inline.lean b/src/verso/Verso/Doc/Elab/Inline.lean
index 650538c7..58245534 100644
--- a/src/verso/Verso/Doc/Elab/Inline.lean
+++ b/src/verso/Verso/Doc/Elab/Inline.lean
@@ -21,7 +21,7 @@ set_option backward.privateInPublic false
 public def throwUnexpected [Monad m] [MonadError m] (stx : Syntax) : m α :=
   throwErrorAt stx "unexpected syntax{indentD stx}"
 
-public partial def elabInline (inline : TSyntax `inline) : DocElabM (TSyntax `term) :=
+public partial def elabInline (inline : TSyntax `inline) : DocElabM Target.Inline :=
   withRef inline <| withFreshMacroScope <| withIncRecDepth <| do
   match inline.raw with
   | .missing =>
diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean
index 75ad8766..c8a12cdd 100644
--- a/src/verso/Verso/Doc/Elab/Monad.lean
+++ b/src/verso/Verso/Doc/Elab/Monad.lean
@@ -347,7 +347,7 @@ public def PartElabM.addBlock (block : TSyntax `term) (blockInternalDocReconstru
       deferredBlocks := st.deferredBlocks.push (name, blockDefSyntax)
     }
 
-public def PartElabM.addPart (finished : Part) : PartElabM Unit := modifyThe State fun st =>
+public def PartElabM.addPart (finished : FinishedPart) : PartElabM Unit := modifyThe State fun st =>
   { st with partContext.priorParts := st.partContext.priorParts.push finished }
 
 public def PartElabM.addLinkDef (refName : TSyntax `str) (url : String) : PartElabM Unit := do
@@ -467,9 +467,9 @@ public opaque inlineExpandersFor (x : Name) : DocElabM (Array InlineExpander)
 Creates a term denoting a {lean}`DocThunk` value from a {lean}`Part`. This is the final step
 in turning a parsed verso doc into syntax.
 -/
-public def Part.toThunkTerm
+public def FinishedPart.toThunkTerm
     (genreSyntax : Term)
-    (finished : Part)
+    (finished : FinishedPart)
     (ctx : DocElabContext)
     (docElabState : DocElabM.State)
     (partElabState : PartElabM.State)
@@ -535,13 +535,10 @@ public def Part.toThunkTerm
 
   ``(DocThunk.serialized (fun $docReconstructionPlaceholder => $finishedSyntax) $(quote reconstJson.compress) none)
 
-@[deprecated Part.toThunkTerm (since := "2025-11-28")]
-public def FinishedPart.toVersoDoc : Term → Part → DocElabContext → DocElabM.State → PartElabM.State → TermElabM Term := Part.toThunkTerm
+@[deprecated FinishedPart.toThunkTerm (since := "2025-11-28")]
+public def FinishedPart.toVersoDoc : Term → FinishedPart → DocElabContext → DocElabM.State → PartElabM.State → TermElabM Term := FinishedPart.toThunkTerm
 
-@[deprecated Part.toThunkTerm (since := "2025-11-28")]
-public def Part.toVersoDoc : Term → Part → DocElabContext → DocElabM.State → PartElabM.State → TermElabM Term := Part.toThunkTerm
-
-public abbrev BlockElab := Syntax → DocElabM Elab.Block
+public abbrev BlockElab := Syntax → DocElabM Target.Block
 
 initialize blockElabAttr : KeyedDeclsAttribute BlockElab ←
   mkDocExpanderAttribute `block_elab ``BlockElab "Indicates that this function expands block elements of a given name" `blockElabAttr

From c078470075043ceed492f0b2c8baa9e06d922de1 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Sun, 28 Dec 2025 15:29:08 -0500
Subject: [PATCH 3/8] add markdown test and fix it

---
 src/tests/Tests/VersoManual.lean          | 1 +
 src/tests/Tests/VersoManual/Markdown.lean | 6 +++---
 2 files changed, 4 insertions(+), 3 deletions(-)

diff --git a/src/tests/Tests/VersoManual.lean b/src/tests/Tests/VersoManual.lean
index 04b05cd8..370a0a72 100644
--- a/src/tests/Tests/VersoManual.lean
+++ b/src/tests/Tests/VersoManual.lean
@@ -5,3 +5,4 @@ Author: David Thrane Christiansen
 -/
 import Tests.VersoManual.Html
 import Tests.VersoManual.Html.SoftHyphenate
+import Tests.VersoManual.Markdown
diff --git a/src/tests/Tests/VersoManual/Markdown.lean b/src/tests/Tests/VersoManual/Markdown.lean
index fdceaff6..190d0cbb 100644
--- a/src/tests/Tests/VersoManual/Markdown.lean
+++ b/src/tests/Tests/VersoManual/Markdown.lean
@@ -8,7 +8,7 @@ import Verso.Doc.Elab.Monad
 import Lean.Elab.Term
 
 open Verso Doc Elab
-open Verso.Genre Manual Markdown
+open Verso.Genre Manual
 open Lean
 
 /--
@@ -20,7 +20,7 @@ To avoid off-by-one misunderstandings: The heading level is equal to
 the number of # characters in the opening sequence. (cf. [CommonMark
 Spec](https://spec.commonmark.org/0.31.2/))
 -/
-def displayPartStructure (part : Part) (level : Nat := 1) : String := match part with
+def displayPartStructure (part : FinishedPart) (level : Nat := 1) : String := match part with
   | .mk _ _ title _ _ subParts _ =>
        let partsStr : String := subParts.map (displayPartStructure · (level + 1))
          |>.toList |> String.join
@@ -38,7 +38,7 @@ def testAddPartFromMarkdown (input : String) : Elab.TermElabM String := do
   let addParts : PartElabM Unit := do
     let mut levels := []
     for block in parsed.blocks do
-      levels ← addPartFromMarkdown block levels
+      levels ← Markdown.addPartFromMarkdown block levels
     closePartsUntil 0 0
   let (_, _, part) ← addParts.run ⟨Syntax.node .none identKind #[], mkConst ``Manual, .always, .none⟩ default default
   part.partContext.priorParts.toList.map displayPartStructure |> String.join |> pure

From 53b60a4f1afa51bfb7513a1270e68a5e73d78efe Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Sun, 28 Dec 2025 15:30:46 -0500
Subject: [PATCH 4/8] diff minimization

---
 src/verso-manual/VersoManual.lean | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean
index ecd98bdc..4759d035 100644
--- a/src/verso-manual/VersoManual.lean
+++ b/src/verso-manual/VersoManual.lean
@@ -47,7 +47,7 @@ open Std (HashMap)
 
 open Verso.FS
 
-open Verso.Doc
+open Verso.Doc Elab
 open Verso.Multi
 open Verso.Genre.Manual.TeX
 open Verso.Genre.Manual.WordCount
@@ -139,7 +139,7 @@ end
 Inserts a reference to the provided tag.
 -/
 @[role]
-def ref : Elab.RoleExpanderOf RoleArgs
+def ref : RoleExpanderOf RoleArgs
   | {canonicalName, domain, remote}, content => do
     let content ← content.mapM Elab.elabInline
     ``(Inline.other (Inline.ref $(quote canonicalName) $(quote domain) $(quote remote)) #[$content,*])
@@ -161,9 +161,9 @@ paragraph. In HTML output, they are rendered with less space between them, and L
 a single paragraph (e.g. without extraneous indentation).
 -/
 @[directive]
-def paragraph : Elab.DirectiveExpanderOf Unit
+def paragraph : DirectiveExpanderOf Unit
   | (), stxs => do
-    let args ← stxs.mapM Elab.elabBlockTerm
+    let args ← stxs.mapM elabBlockTerm
     ``(Block.other Block.paragraph #[ $[ $args ],* ])
 
 structure Config extends HtmlConfig where

From cbffafacb6bf1d69e2d1e17dafc84966cbb0eb94 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Sun, 28 Dec 2025 15:33:09 -0500
Subject: [PATCH 5/8] diff minimization

---
 src/verso-manual/VersoManual.lean   | 2 +-
 src/verso/Verso/Doc/Elab/Block.lean | 2 +-
 2 files changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean
index 4759d035..fefbe59a 100644
--- a/src/verso-manual/VersoManual.lean
+++ b/src/verso-manual/VersoManual.lean
@@ -141,7 +141,7 @@ Inserts a reference to the provided tag.
 @[role]
 def ref : RoleExpanderOf RoleArgs
   | {canonicalName, domain, remote}, content => do
-    let content ← content.mapM Elab.elabInline
+    let content ← content.mapM elabInline
     ``(Inline.other (Inline.ref $(quote canonicalName) $(quote domain) $(quote remote)) #[$content,*])
 
 block_extension Block.paragraph where
diff --git a/src/verso/Verso/Doc/Elab/Block.lean b/src/verso/Verso/Doc/Elab/Block.lean
index 6250feb9..b4841d6e 100644
--- a/src/verso/Verso/Doc/Elab/Block.lean
+++ b/src/verso/Verso/Doc/Elab/Block.lean
@@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
 module
-public import Verso.Doc.Elab.Basic
+
 public import Verso.Doc.Elab.Monad
 meta import Verso.Doc.Elab.Monad
 public import Lean.DocString.Syntax

From f72ffc4916524ced339aaef2f04c716834350d78 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Sun, 28 Dec 2025 15:36:56 -0500
Subject: [PATCH 6/8] diff minimization

---
 src/verso/Verso/Doc/Elab/Basic.lean | 2 +-
 src/verso/Verso/Doc/Elab/Block.lean | 7 +++++--
 src/verso/Verso/Doc/Elab/Monad.lean | 2 +-
 3 files changed, 7 insertions(+), 4 deletions(-)

diff --git a/src/verso/Verso/Doc/Elab/Basic.lean b/src/verso/Verso/Doc/Elab/Basic.lean
index f27b084b..5a849ee9 100644
--- a/src/verso/Verso/Doc/Elab/Basic.lean
+++ b/src/verso/Verso/Doc/Elab/Basic.lean
@@ -163,7 +163,7 @@ parts being built.
 public def PartContext.level (ctxt : PartContext) : Nat := ctxt.parents.size
 
 /--
-Closes the current part. The resulting {name}`Part` is appended to
+Closes the current part. The resulting {name}`FinishedPart` is appended to
 {name (full := PartFrame.priorParts)}`priorParts`, and
 the top of the stack of our parents becomes the current frame. Returns
 {name}`none` if there are no parents.
diff --git a/src/verso/Verso/Doc/Elab/Block.lean b/src/verso/Verso/Doc/Elab/Block.lean
index b4841d6e..08d366bf 100644
--- a/src/verso/Verso/Doc/Elab/Block.lean
+++ b/src/verso/Verso/Doc/Elab/Block.lean
@@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
 Author: David Thrane Christiansen
 -/
 module
-
 public import Verso.Doc.Elab.Monad
 meta import Verso.Doc.Elab.Monad
 public import Lean.DocString.Syntax
@@ -29,7 +28,11 @@ def decorateClosing : TSyntax `block → DocElabM Unit
   | _ => pure ()
 
 
-/-- Elaborates a parsed block -/
+variable (genre : Genre) in
+/--
+Elaborates a parsed block into a {name}`Target.Block`, which denotes an expression of type
+{lean}`Doc.Block genre` in an unspecified {name}`genre`.
+-/
 public partial def elabBlock' (block : TSyntax `block) : DocElabM Target.Block :=
   withTraceNode `Elab.Verso.block (fun _ => pure m!"Block {block}") <|
   withRef block <| withFreshMacroScope <| withIncRecDepth <| do
diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean
index c8a12cdd..43290b3a 100644
--- a/src/verso/Verso/Doc/Elab/Monad.lean
+++ b/src/verso/Verso/Doc/Elab/Monad.lean
@@ -464,7 +464,7 @@ unsafe def inlineExpandersForUnsafe (x : Name) : DocElabM (Array InlineExpander)
 public opaque inlineExpandersFor (x : Name) : DocElabM (Array InlineExpander)
 
 /--
-Creates a term denoting a {lean}`DocThunk` value from a {lean}`Part`. This is the final step
+Creates a term denoting a {lean}`DocThunk` value from a {lean}`FinishedPart`. This is the final step
 in turning a parsed verso doc into syntax.
 -/
 public def FinishedPart.toThunkTerm

From 231754b2e2d568e7c695a9bd54b8da013fc0a1b6 Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Sun, 28 Dec 2025 15:37:47 -0500
Subject: [PATCH 7/8] diff minimization

---
 src/verso/Verso/Doc/Elab/Monad.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean
index 43290b3a..e843d735 100644
--- a/src/verso/Verso/Doc/Elab/Monad.lean
+++ b/src/verso/Verso/Doc/Elab/Monad.lean
@@ -41,7 +41,7 @@ class HasLink (name : String) (doc : Name) where
   url : String
 
 class HasNote (name : String) (doc : Name) (genre : Genre) where
-  contents : Array (Doc.Inline genre)
+  contents : Array (Inline genre)
 
 private def linkRefName [Monad m] [MonadQuotation m] (docName : Name) (ref : TSyntax `str) : m Term := do
   ``(HasLink.url $(quote ref.getString) $(quote docName))

From 8b74f1faf14106938cebf579e8ea0e01077b32fb Mon Sep 17 00:00:00 2001
From: Rob Simmons <rob@lean-fro.org>
Date: Sun, 28 Dec 2025 18:17:01 -0500
Subject: [PATCH 8/8] Remove more deprecation warnings

---
 src/verso-blog/VersoBlog/Component.lean   | 2 +-
 test-projects/website/DemoSite/About.lean | 4 ++--
 2 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/src/verso-blog/VersoBlog/Component.lean b/src/verso-blog/VersoBlog/Component.lean
index 3f291b0e..bc87c18c 100644
--- a/src/verso-blog/VersoBlog/Component.lean
+++ b/src/verso-blog/VersoBlog/Component.lean
@@ -312,7 +312,7 @@ elab_rules : command
         `(command|
           @[directive $x]
           def $dirName : DirectiveExpanderOf T
-            | $argPat, blocks => do `($qArgs #[$$(← blocks.mapM elabBlock),*]))
+            | $argPat, blocks => do `($qArgs #[$$(← blocks.mapM elabBlockTerm),*]))
       elabCommand cmd3
 
 
diff --git a/test-projects/website/DemoSite/About.lean b/test-projects/website/DemoSite/About.lean
index 93bae3fd..db62beae 100644
--- a/test-projects/website/DemoSite/About.lean
+++ b/test-projects/website/DemoSite/About.lean
@@ -26,7 +26,7 @@ def redBox : BlockComponent where
 @[directive redBox]
 def redBoxImpl : DirectiveExpanderOf Unit
   | (), stxs => do
-    ``(Block.other (Blog.BlockExt.component $(quote `redBox) Json.null) #[$(← stxs.mapM elabBlock),*])
+    ``(Block.other (Blog.BlockExt.component $(quote `redBox) Json.null) #[$(← stxs.mapM elabBlockTerm),*])
 
 block_component gallery where
   toHtml id _data _goI goB contents := do
@@ -67,7 +67,7 @@ where
         | throwErrorAt (mkNullNode inls) "Expected one inline"
       let `(inline|image($alt)($url)) := inl
         | throwErrorAt inl "Expected an image"
-      `(Block.other (.component $(quote `image) (.arr #[$alt, $url])) #[$(← elabBlock desc), $(← descs.mapM elabBlock),*])
+      `(Block.other (.component $(quote `image) (.arr #[$alt, $url])) #[$(← elabBlockTerm desc), $(← descs.mapM elabBlockTerm),*])
     | stx => throwErrorAt stx "Expected an image and description, got {stx}"
 
 block_component +directive button' (onclick : String) where