fix: allow multi-arg roles when generating string previews

leanprover · Jan 31, 2025 · fa26ae2 · fa26ae2
1 parent d9c0352
commit fa26ae2
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean
@@ -55,8 +55,8 @@ def _root_.Verso.Syntax.code.inline_to_string : InlineToString
 
 @[inline_to_string Verso.Syntax.role]
 def _root_.Verso.Syntax.role.inline_to_string : InlineToString
-  | env, `(inline| role{ $_ $_* }[ $body ]) =>
-    inlineToString env body
+  | env, `(inline| role{ $_ $_* }[ $body* ]) =>
+    String.join (body.toList.map (inlineToString env <| ·.raw))
   | _, _ => none
 
 @[inline_to_string null]