feat: elaborate block structures as concrete elements

doc/UsersGuide/Markup.lean

@@ -282,7 +282,7 @@ open Lean Elab in
 open Verso.Parser in
 open Lean.Doc.Syntax in
 @[directive]
-def markupPreview : DirectiveExpanderOf MarkupPreviewConfig
+def markupPreview : DirectiveElabOf MarkupPreviewConfig
   | {title}, contents => do
     let #[blk1, blk2] := contents.filter nonempty
       | throwError "Expected precisely two code blocks, got {contents.filter nonempty}"
@@ -304,10 +304,10 @@ def markupPreview : DirectiveExpanderOf MarkupPreviewConfig
       throwErrorAt expected m!"Expected {indentD expected.getString} but got {indentD p}\n{hint}"
 
     Hover.addCustomHover contents s!"```\n{p}\n```"
-    ``(Block.other (MarkupExample $(quote title.getString)) #[
-      Block.code $(quote contents.getString),
-      Block.code $(quote <| toString <| p)
-    ])
+    return .other (← ``(MarkupExample $(quote title.getString))) #[
+      .code contents.getString,
+      .code p
+    ]
 where
   eq (s1 s2 : String) : Bool :=
     let lines1 := s1.trimAscii.split (· == '\n') |>.map (·.trimAsciiEnd) |>.toArray

src/verso-blog/VersoBlog.lean

@@ -60,10 +60,10 @@ def htmlSpan : RoleExpanderOf ClassArgs
 Wraps the contents in an HTML `<div>` element with the provided `class`.
 -/
 @[directive]
-def htmlDiv : DirectiveExpanderOf ClassArgs
+def htmlDiv : DirectiveElabOf ClassArgs
   | {«class»}, stxs => do
-    let contents ← stxs.mapM elabBlockTerm
-    ``(Block.other (Blog.BlockExt.htmlDiv $(quote «class»)) #[ $contents,* ])
+    let contents ← stxs.mapM elabBlock'
+    return .other (← ``(Blog.BlockExt.htmlDiv $(quote «class»))) contents
 
 
 private partial def attrs : ArgParse DocElabM (Array (String × String)) := List.toArray <$> .many attr
@@ -80,11 +80,11 @@ instance : FromArgs HtmlArgs DocElabM where
 
 
 @[directive]
-def html : DirectiveExpanderOf HtmlArgs
+def html : DirectiveElabOf HtmlArgs
   | {name, attrs}, stxs => do
     let tag := name.toString (escape := false)
-    let contents ← stxs.mapM elabBlockTerm
-    ``(Block.other (Blog.BlockExt.htmlWrapper $(quote tag) $(quote attrs)) #[ $contents,* ])
+    let contents ← stxs.mapM elabBlock'
+    return .other (← ``(Blog.BlockExt.htmlWrapper $(quote tag) $(quote attrs))) contents
 
 structure BlobArgs where
   blobName : Ident
@@ -93,11 +93,11 @@ instance : FromArgs BlobArgs DocElabM where
   fromArgs := BlobArgs.mk <$> .positional `blobName .ident
 
 @[directive]
-def blob : DirectiveExpanderOf BlobArgs
+def blob : DirectiveElabOf BlobArgs
   | {blobName}, stxs => do
     if h : stxs.size > 0 then logErrorAt stxs[0] "Expected no contents"
     let actualName ← realizeGlobalConstNoOverloadWithInfo blobName
-    ``(Block.other (Blog.BlockExt.blob ($(mkIdentFrom blobName actualName) : Html)) #[])
+    return .other (← ``(Blog.BlockExt.blob ($(mkIdentFrom blobName actualName) : Html))) #[]
 
 @[role blob]
 def inlineBlob : RoleExpanderOf BlobArgs

src/verso-manual/VersoManual.lean

@@ -161,10 +161,10 @@ 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 : DirectiveElabOf Unit
   | (), stxs => do
-    let args ← stxs.mapM elabBlockTerm
-    ``(Block.other Block.paragraph #[ $[ $args ],* ])
+    let args ← stxs.mapM elabBlock'
+    return .other (← ``(Block.paragraph)) args
 
 structure Config extends HtmlConfig where
   destination : System.FilePath := "_out"

src/verso-manual/VersoManual/Docstring.lean

@@ -1672,7 +1672,7 @@ private def getTactic? (name : String ⊕ Name) : TermElabM (Option TacticDoc) :
   return none
 
 @[directive]
-def tactic : DirectiveExpanderOf TacticDocsOptions
+def tactic : DirectiveElabOf TacticDocsOptions
   | opts, more => do
     let tactics ← getTacticOverloads opts.name
     let blame : Syntax := opts.name.elim TSyntax.raw TSyntax.raw
@@ -1695,8 +1695,8 @@ 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 elabBlockTerm
-    ``(Verso.Doc.Block.other (Block.tactic $(quote tactic) $(quote opts.show)) #[$(contents ++ userContents),*])
+    let userContents ← more.mapM elabBlock'
+    return .other (← ``(Block.tactic $(quote tactic) $(quote opts.show))) (contents.map .stx ++ userContents)
 
 def Inline.tactic : Inline where
   name := `Verso.Genre.Manual.tacticInline
@@ -1842,7 +1842,7 @@ def getConvTactic (name : StrLit ⊕ Ident) (allowMissing : Option Bool) : TermE
     throwError m!"Conv tactic not found: {kind}"
 
 @[directive]
-def conv : DirectiveExpanderOf TacticDocsOptions
+def conv : DirectiveElabOf TacticDocsOptions
   | opts, more => do
     let tactic ← getConvTactic opts.name opts.allowMissing
     Doc.PointOfInterest.save (← getRef) tactic.name.toString
@@ -1851,10 +1851,10 @@ def conv : DirectiveExpanderOf TacticDocsOptions
           | throwError "Failed to parse docstring as Markdown"
         mdAst.blocks.mapM (blockFromMarkdownWithLean [])
       else pure #[]
-    let userContents ← more.mapM elabBlockTerm
+    let userContents ← more.mapM elabBlock'
     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),*])
+    return .other (← ``(Block.conv $(quote tactic.name) $(quote toShow) $(quote tactic.docs?))) (contents.map (.stx ·) ++ userContents)
 
 open Verso.Search in
 def convDomainMapper : DomainMapper := {

src/verso-manual/VersoManual/Docstring/Progress.lean

@@ -63,7 +63,7 @@ run_cmd do
   elabCommand <| ← `(private def $(mkIdent `allRootNames) : Array Name := #[$(names.map (quote · : Name → Term)),*])
 
 @[directive]
-public def progress : DirectiveExpanderOf Unit
+public def progress : DirectiveElabOf Unit
   | (), blocks => do
     let mut namespaces : NameSet := {}
     let mut exceptions : NameSet := {}
@@ -111,7 +111,7 @@ public def progress : DirectiveExpanderOf Unit
     let present' := present.toList.map (fun x => (x.1, String.intercalate " " (x.2.toList.map Name.toString)))
     let allTactics : Array Name := (← Elab.Tactic.Doc.allTacticDocs).map (fun t => t.internalName)
 
-    ``(Verso.Doc.Block.other (Verso.Genre.Manual.Block.progress $(quote namespaces.toArray) $(quote exceptions.toArray) $(quote present') $(quote allTactics)) #[])
+    return .other (← ``(Verso.Genre.Manual.Block.progress $(quote namespaces.toArray) $(quote exceptions.toArray) $(quote present') $(quote allTactics))) #[]
 
 @[block_extension Block.progress]
 public def progress.descr : BlockDescr where

src/verso-manual/VersoManual/Draft.lean

@@ -57,6 +57,6 @@ def draft : RoleExpanderOf Unit
 
 /-- Hide draft-only content when in not in draft mode -/
 @[directive draft]
-def draftBlock : DirectiveExpanderOf Unit
+def draftBlock : DirectiveElabOf Unit
   | (), contents => do
-    ``(Verso.Doc.Block.other Block.draft #[$[$(← contents.mapM elabBlockTerm)],*])
+    return .other (← ``(Block.draft)) (← contents.mapM elabBlock')

src/verso-manual/VersoManual/Table.lean

@@ -185,7 +185,7 @@ instance : FromArgs TableConfig m := ⟨TableConfig.parse⟩
 end
 
 @[directive]
-def table : DirectiveExpanderOf TableConfig
+def table : DirectiveElabOf TableConfig
   | cfg, contents => do
     -- The table should be a list of lists. Extract them!
     let #[oneBlock] := contents
@@ -210,8 +210,9 @@ 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 elabBlockTerm)
-      ``(Block.other (Block.table $(quote columns) $(quote cfg.header) $(quote cfg.name) $(quote cfg.alignment)) #[Block.ul #[$[Verso.Doc.ListItem.mk #[$blocks,*]],*]])
+      let blocks : Array (Array Target.Block) ← flattened.mapM (·.mapM elabBlock')
+      return .other (← ``(Block.table $(quote columns) $(quote cfg.header) $(quote cfg.name) $(quote cfg.alignment)))
+        #[.ul blocks]
 
 where
   getLi : Syntax → DocElabM (TSyntaxArray `block)

src/verso/Verso/Doc/Elab.lean

@@ -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 .concat (termStxs.map .stx)
+        return .concat termStxs
       catch
         | ex@(.internal id) =>
           if id == unsupportedSyntaxExceptionId then pure ()

src/verso/Verso/Doc/Elab/Monad.lean

@@ -799,11 +799,27 @@ public abbrev DirectiveExpander := Array Arg → TSyntaxArray `block → DocElab
 
 public abbrev DirectiveExpanderOf α := α → TSyntaxArray `block → DocElabM Term
 
+public abbrev DirectiveElaborator := Array Arg → TSyntaxArray `block → DocElabM (Array Target.Block)
+
+/--
+The type of directive elaborators. In order to give a declaration of type {lean}`DirectiveElabOf α`
+the {lit}`@[directive]` annotation, it must be possible to synthesize {lean}`FromArgs α DocElabM`.
+-/
+public abbrev DirectiveElabOf (α : Type) := α → TSyntaxArray `block → DocElabM Target.Block
+
+public def directiveExpanderToElaborator (expander : DirectiveExpander) : DirectiveElaborator
+  | args, contents => do return (← expander args contents).map (.stx ·)
+
 
 initialize directiveExpanderAttr : KeyedDeclsAttribute DirectiveExpander ←
   mkDocExpanderAttribute `directive_expander ``DirectiveExpander "Indicates that this function is used to implement a given directive" `directiveExpanderAttr
 
-public def toDirective {α : Type} [FromArgs α DocElabM] (expander : α → TSyntaxArray `block → DocElabM Term) : DirectiveExpander :=
+public def toDirectiveTerm {α : Type} [FromArgs α DocElabM] (expander : α → TSyntaxArray `block → DocElabM Term) : DirectiveElaborator :=
+  fun args blocks => do
+    let v ← ArgParse.parse args
+    return #[.stx (← expander v blocks)]
+
+public def toDirective {α : Type} [FromArgs α DocElabM] (expander : α → TSyntaxArray `block → DocElabM Target.Block) : DirectiveElaborator :=
   fun args blocks => do
     let v ← ArgParse.parse args
     return #[← expander v blocks]
@@ -838,14 +854,29 @@ unsafe initialize registerBuiltinAttribute {
 
     let n ← mkFreshUserName <| declName ++ `directive
 
+    -- Find the appropriate adapter for both new (`DirectiveElabOf`) and legacy (`DirectiveExpanderOf`) declarations
+    let constructor ← match (← getEnv).find? declName |>.map (·.type.getAppFn) with
+      | some (Expr.const ``DirectiveExpanderOf _) => pure ``toDirectiveTerm
+      | some (Expr.const ``DirectiveElabOf _) => pure ``toDirective
+      | some e =>
+        logWarning m!"Declaration tagged with `@[directive]` has type{indentD e}\nwhich is not in \
+          one of the expected forms `{.ofConstName ``DirectiveExpanderOf} _` or \
+          `{.ofConstName ``DirectiveElabOf} _`"
+        pure ``toDirective
+      | none =>
+        logError m!"Unexpected error: definition of `{declName}` not found"
+        return
+
     let ((e, t), _) ← Meta.MetaM.run (ctx := {}) (s := {}) do
-      let e ← Meta.mkAppM ``toDirective #[.const declName []]
+      let e ← Meta.mkAppM constructor #[.const declName []]
       let e ← instantiateMVars e
       let t ← Meta.inferType e
 
-
       match_expr e with
-      | toDirective ty _ _ => saveSignature n ty
+      | toDirectiveTerm ty _ _ =>
+        saveSignature n ty
+      | toDirective ty _ _ =>
+        saveSignature n ty
       | _ => pure ()
 
       pure (e, t)
@@ -865,10 +896,10 @@ unsafe initialize registerBuiltinAttribute {
       directiveExpanderExt.addEntry env (directiveName, n)
 }
 
-private unsafe def directiveExpandersForUnsafe' (x : Name) : DocElabM (Array (DirectiveExpander × Option String × Option SigDoc)) := do
+private unsafe def directiveExpandersForUnsafe' (x : Name) : DocElabM (Array (DirectiveElaborator × Option String × Option SigDoc)) := do
   let expanders := directiveExpanderExt.getState (← getEnv) |>.find? x |>.getD #[]
   expanders.mapM fun n => do
-    let e ← evalConst DirectiveExpander n
+    let e ← evalConst DirectiveElaborator n
     let doc? ← findDocString? (← getEnv) n
     let sig := expanderSignatureExt.getState (← getEnv) |>.find? n
     return (e, doc?, sig)
@@ -877,11 +908,11 @@ private unsafe def directiveExpandersForUnsafe'' (x : Name) : DocElabM (Array Di
   let expanders := directiveExpanderAttr.getEntries (← getEnv) x
   return expanders.map (·.value) |>.toArray
 
-private unsafe def directiveExpandersForUnsafe (x : Name) : DocElabM (Array (DirectiveExpander × Option String × Option SigDoc)) := do
-  return (← directiveExpandersForUnsafe' x) ++ (← directiveExpandersForUnsafe'' x).map (·, none, none)
+private unsafe def directiveExpandersForUnsafe (x : Name) : DocElabM (Array (DirectiveElaborator × Option String × Option SigDoc)) := do
+  return (← directiveExpandersForUnsafe' x) ++ (← directiveExpandersForUnsafe'' x).map (directiveExpanderToElaborator ·, none, none)
 
 @[implemented_by directiveExpandersForUnsafe]
-public opaque directiveExpandersFor (x : Name) : DocElabM (Array (DirectiveExpander × Option String × Option SigDoc))
+public opaque directiveExpandersFor (x : Name) : DocElabM (Array (DirectiveElaborator × Option String × Option SigDoc))
 
 
 public abbrev BlockCommandExpander := Array Arg → DocElabM (Array (TSyntax `term))

test-projects/website/DemoSite/About.lean

@@ -24,9 +24,9 @@ def redBox : BlockComponent where
     pure {{<div class="red-box" id={{id}}>{{← contents.mapM goB}}</div>}}
 
 @[directive redBox]
-def redBoxImpl : DirectiveExpanderOf Unit
+def redBoxImpl : DirectiveElabOf Unit
   | (), stxs => do
-    ``(Block.other (Blog.BlockExt.component $(quote `redBox) Json.null) #[$(← stxs.mapM elabBlockTerm),*])
+    return .other (← ``(Blog.BlockExt.component $(quote `redBox) Json.null)) (← stxs.mapM elabBlock')
 
 block_component gallery where
   toHtml id _data _goI goB contents := do
@@ -49,25 +49,25 @@ block_component image where
 
 
 @[directive gallery]
-def galleryImpl : DirectiveExpanderOf Unit
+def galleryImpl : DirectiveElabOf Unit
   | (), stxs => do
     let #[stx] := stxs
       | logErrorAt (mkNullNode stxs) "Expected one block"
-        return (← `(sorry))
+        return .other (← `(sorry)) #[]
     let `(block| dl{ $item*}) := stx
       | throwErrorAt stx "Expected definition list"
     let items ← item.mapM getItem
-    ``(Block.other (Blog.BlockExt.component $(quote `gallery) Json.null) #[$(items),*])
+    return .other (← ``(Blog.BlockExt.component $(quote `gallery) Json.null)) items
 where
-  getItem : TSyntax `desc_item → DocElabM Term
+  getItem : TSyntax `desc_item → DocElabM Target.Block
     | `(desc_item|: $inls* => $desc $descs*) => do
       let #[inl] := inls.filter (fun
           | `(inline|$s:str) => s.getString.any (not ∘ Char.isWhitespace)
           | _ => true)
         | 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])) #[$(← elabBlockTerm desc), $(← descs.mapM elabBlockTerm),*])
+      return .other (← `(.component $(quote `image) (.arr #[$alt, $url]))) (#[← elabBlock' desc] ++ (← descs.mapM elabBlock'))
     | stx => throwErrorAt stx "Expected an image and description, got {stx}"
 
 block_component +directive button' (onclick : String) where