diff --git a/doc/UsersGuide/Markup.lean b/doc/UsersGuide/Markup.lean
index 33c72b92..29aa0251 100644
--- a/doc/UsersGuide/Markup.lean
+++ b/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
diff --git a/src/verso-blog/VersoBlog.lean b/src/verso-blog/VersoBlog.lean
index 1d361988..45411b8b 100644
--- a/src/verso-blog/VersoBlog.lean
+++ b/src/verso-blog/VersoBlog.lean
@@ -60,10 +60,10 @@ def htmlSpan : RoleExpanderOf ClassArgs
Wraps the contents in an HTML `
` 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
diff --git a/src/verso-manual/VersoManual.lean b/src/verso-manual/VersoManual.lean
index fefbe59a..68343cb7 100644
--- a/src/verso-manual/VersoManual.lean
+++ b/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"
diff --git a/src/verso-manual/VersoManual/Docstring.lean b/src/verso-manual/VersoManual/Docstring.lean
index 20214e8b..7185689f 100644
--- a/src/verso-manual/VersoManual/Docstring.lean
+++ b/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 := {
diff --git a/src/verso-manual/VersoManual/Docstring/Progress.lean b/src/verso-manual/VersoManual/Docstring/Progress.lean
index 0234019a..fe511d19 100644
--- a/src/verso-manual/VersoManual/Docstring/Progress.lean
+++ b/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
diff --git a/src/verso-manual/VersoManual/Draft.lean b/src/verso-manual/VersoManual/Draft.lean
index 332fdfb7..5aa5c8c1 100644
--- a/src/verso-manual/VersoManual/Draft.lean
+++ b/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')
diff --git a/src/verso-manual/VersoManual/Table.lean b/src/verso-manual/VersoManual/Table.lean
index 6994de2d..a0dc1092 100644
--- a/src/verso-manual/VersoManual/Table.lean
+++ b/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)
diff --git a/src/verso/Verso/Doc/Elab.lean b/src/verso/Verso/Doc/Elab.lean
index c59b35eb..55d1852f 100644
--- a/src/verso/Verso/Doc/Elab.lean
+++ b/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 ()
diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean
index e843d735..cea569e6 100644
--- a/src/verso/Verso/Doc/Elab/Monad.lean
+++ b/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))
diff --git a/test-projects/website/DemoSite/About.lean b/test-projects/website/DemoSite/About.lean
index db62beae..b0ec0116 100644
--- a/test-projects/website/DemoSite/About.lean
+++ b/test-projects/website/DemoSite/About.lean
@@ -24,9 +24,9 @@ def redBox : BlockComponent where
pure {{
{{← contents.mapM goB}}
}}
@[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,17 +49,17 @@ 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)
@@ -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])) #[$(← 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