feat: automatic signature docstrings for Verso elements

Main.lean

@@ -18,13 +18,13 @@ open Lean Elab Term
 
 set_option pp.rawOnError true
 
-@[role_expander vanish]
-def vanish : RoleExpander
-   | _args, _stxs => pure #[]
+@[role]
+def vanish : RoleExpanderOf Unit
+   | (), _stxs => pure #[]
 
-@[role_expander rev]
-def rev : RoleExpander
-  | _args, stxs => .reverse <$> stxs.mapM elabInline
+@[role]
+def rev : RoleExpanderOf Unit
+  | (), stxs => .reverse <$> stxs.mapM elabInline
 
 def html [Monad m] (doc : Part .none) : m Html := (·.fst) <$> Genre.none.toHtml {logError := fun _ => pure ()} () () {} {} {} doc .empty
 

doc/UsersGuide/Markup.lean

@@ -37,16 +37,12 @@ partial def preview [Monad m] [MonadError m] (stx : Syntax) : m String :=
       throwErrorAt stx "Didn't understand {Verso.SyntaxUtils.ppSyntax stx} for preview"
 
 open Lean Verso Doc Elab Parser in
-@[code_block_expander markupPreview]
-def markupPreview : CodeBlockExpander
-  | #[], contents => do
+@[code_block]
+def markupPreview : CodeBlockExpanderOf Unit
+  | (), contents => do
     let stx ← blocks {} |>.parseString contents.getString
     let p ← preview stx
-    pure #[
-      ← ``(Block.code $(quote contents.getString)),
-      ← ``(Block.code $(quote <| toString <| p))
-    ]
-  | _, contents => throwErrorAt contents "Unexpected arguments"
+    ``(Block.concat #[Block.code $(quote contents.getString), Block.code $(quote <| toString <| p)])
 
 
 #doc (Manual) "Lean Markup" =>

examples/textbook/DemoTextbook/Meta/Lean.lean

@@ -32,29 +32,26 @@ block_extension Block.savedImport (file : String) (source : String) where
 /--
 Lean code that is saved to the examples file.
 -/
-@[code_block_expander savedLean]
-def savedLean : CodeBlockExpander
+@[code_block savedLean]
+def savedLean : CodeBlockExpanderOf InlineLean.LeanBlockConfig
   | args, code => do
     let underlying ← InlineLean.lean args code
-    return #[← ``(Block.other (Block.savedLean $(quote (← getFileName)) $(quote (code.getString))) #[$underlying,*])]
+    ``(Block.other (Block.savedLean $(quote (← getFileName)) $(quote (code.getString))) #[$underlying])
 
 /--
 An import of some other module, to be located in the saved code. Not rendered.
 -/
-@[code_block_expander savedImport]
-def savedImport : CodeBlockExpander
-  | args, code => do
-    ArgParse.done.run args
-    return #[← ``(Block.other (Block.savedImport $(quote (← getFileName)) $(quote (code.getString))) #[])]
-
+@[code_block]
+def savedImport : CodeBlockExpanderOf Unit
+  | (), code => do
+    ``(Block.other (Block.savedImport $(quote (← getFileName)) $(quote (code.getString))) #[])
 
 /--
 Comments to be added as module docstrings to the examples file.
 -/
-@[code_block_expander savedComment]
-def savedComment : CodeBlockExpander
-  | args, code => do
-    ArgParse.done.run args
+@[code_block]
+def savedComment : CodeBlockExpanderOf Unit
+  | (), code => do
     let str := code.getString.trimRight
     let comment := s!"/-!\n{str}\n-/"
-    return #[← ``(Block.other (Block.savedLean $(quote (← getFileName)) $(quote comment)) #[])]
+    ``(Block.other (Block.savedLean $(quote (← getFileName)) $(quote comment)) #[])

examples/website/DemoSite/About.lean

@@ -20,11 +20,10 @@ def redBox : BlockComponent where
     saveCss ".red-box { border: 2px solid red; }"
     pure {{<div class="red-box" id={{id}}>{{← contents.mapM goB}}</div>}}
 
-@[directive_expander redBox]
-def redBoxImpl : DirectiveExpander
-  | args, stxs => do
-    ArgParse.done.run args
-    return #[← ``(Block.other (Blog.BlockExt.component $(quote `redBox) Json.null) #[$(← stxs.mapM elabBlock),*])]
+@[directive redBox]
+def redBoxImpl : DirectiveExpanderOf Unit
+  | (), stxs => do
+    ``(Block.other (Blog.BlockExt.component $(quote `redBox) Json.null) #[$(← stxs.mapM elabBlock),*])
 
 block_component gallery where
   toHtml id _data _goI goB contents := do
@@ -46,17 +45,16 @@ block_component image where
     }}
 
 
-@[directive_expander gallery]
-def galleryImpl : DirectiveExpander
-  | args, stxs => do
-    ArgParse.done.run args
+@[directive gallery]
+def galleryImpl : DirectiveExpanderOf Unit
+  | (), stxs => do
     let #[stx] := stxs
       | logErrorAt (mkNullNode stxs) "Expected one block"
-        return #[← `(sorry)]
+        return (← `(sorry))
     let `(block| dl{ $item*}) := stx
       | throwErrorAt stx "Expected definition list"
     let items ← item.mapM getItem
-    return #[← ``(Block.other (Blog.BlockExt.component $(quote `gallery) Json.null) #[$(items),*])]
+    ``(Block.other (Blog.BlockExt.component $(quote `gallery) Json.null) #[$(items),*])
 where
   getItem : TSyntax `desc_item → DocElabM Term
     | `(desc_item|: $inls* => $desc $descs*) => do
@@ -92,11 +90,16 @@ inline_component button (onclick : String) where
       </button>
     }}
 
-@[role_expander button]
-def buttonImpl : RoleExpander
-  | args, contents => do
-    let onclick ← ArgParse.run (.positional `onClick .string) args
-    pure #[← ``(button $(quote onclick) #[$(← contents.mapM elabInline),*])]
+structure ButtonArgs where
+  onClick : String
+
+instance : FromArgs ButtonArgs DocElabM where
+  fromArgs := ButtonArgs.mk <$> .positional `onClick .string
+
+@[role button]
+def buttonImpl : RoleExpanderOf ButtonArgs
+  | {onClick}, contents => do
+    ``(button $(quote onClick) #[$(← contents.mapM elabInline),*])
 
 end
 

examples/website/DemoSite/Blog/Conditionals.lean

@@ -26,9 +26,11 @@ categories := [examples, other]
 %%%
 
 
+:::htmlDiv (class := "some-other-class")
 Finally started blogging!
-This post describes the syntax and semantics of conditional expressions in Lean.
+This post {htmlSpan (class := "some-class")}[describes] the syntax and semantics of conditional expressions in Lean.
 Here are some examples:
+:::
 
 ```leanInit demo
 -- This block initializes a Lean context