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 cc18014e..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
 
 /--
@@ -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
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/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/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean
index 6098fd9a..fefbe59a 100644
--- a/src/verso-manual/VersoManual.lean
+++ b/src/verso-manual/VersoManual.lean
@@ -163,7 +163,7 @@ a single paragraph (e.g. without extraneous indentation).
 @[directive]
 def paragraph : DirectiveExpanderOf Unit
   | (), stxs => do
-    let args ← stxs.mapM elabBlock
+    let args ← stxs.mapM 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/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..c59b35eb 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 .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 .para (← args.mapM elabInline)
   | _ =>
     throwUnsupportedSyntax
 
-
-meta def elabLi (block : Syntax) : DocElabM (Syntax × TSyntax `term) :=
+meta def elabLi (block : Syntax) : DocElabM (Syntax × Array Target.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 Target.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 .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 Target.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 .ol start.getNat items
   | _ =>
     throwUnsupportedSyntax
 
-meta def elabDesc (block : Syntax) : DocElabM (Syntax × TSyntax `term) :=
+meta def elabDesc (block : Syntax) : DocElabM (Syntax × Array Target.Inline × Array Target.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 Target.Inline × Array Target.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 .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 .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 .concat (termStxs.map .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 <| .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 .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 5e5e9a14..5a849ee9 100644
--- a/src/verso/Verso/Doc/Elab/Basic.lean
+++ b/src/verso/Verso/Doc/Elab/Basic.lean
@@ -20,8 +20,65 @@ 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
+-/
+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 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)),*])
+
+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
+
+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 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)
+  | 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
@@ -40,8 +97,8 @@ 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
@@ -49,7 +106,6 @@ public partial def FinishedPart.toTOC : FinishedPart → TOC
     .mk titleString titleStx endPos (subParts.map toTOC)
   | .included name => .included name
 
-
 /--
 Information describing a part still under construction.
 
@@ -61,9 +117,9 @@ 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 Target.Inline) := none
+  metadata : Option Term
+  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.
@@ -71,7 +127,7 @@ public structure PartFrame where
   priorParts : Array FinishedPart
 deriving Repr, Inhabited
 
-/-- Turn an previously active {name}`PartFrame` into a {name}`FinishedPart`. -/
+/-- Turn an previously active {name}`PartFrame` into a {name}`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 9bef0b29..08d366bf 100644
--- a/src/verso/Verso/Doc/Elab/Block.lean
+++ b/src/verso/Verso/Doc/Elab/Block.lean
@@ -9,6 +9,8 @@ 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 +28,18 @@ 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) :=
+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
   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 +47,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 +72,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..58245534 100644
--- a/src/verso/Verso/Doc/Elab/Inline.lean
+++ b/src/verso/Verso/Doc/Elab/Inline.lean
@@ -21,11 +21,11 @@ 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 =>
-    ``(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..e843d735 100644
--- a/src/verso/Verso/Doc/Elab/Monad.lean
+++ b/src/verso/Verso/Doc/Elab/Monad.lean
@@ -343,7 +343,7 @@ 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)
     }
 
@@ -538,6 +538,18 @@ public def FinishedPart.toThunkTerm
 @[deprecated FinishedPart.toThunkTerm (since := "2025-11-28")]
 public def FinishedPart.toVersoDoc : Term → FinishedPart → DocElabContext → DocElabM.State → PartElabM.State → TermElabM Term := FinishedPart.toThunkTerm
 
+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
+
+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)
 
 initialize blockExpanderAttr : KeyedDeclsAttribute BlockExpander ←
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