From fa26ae20aa70e1770743671347017cc7f3e2ea8b Mon Sep 17 00:00:00 2001
From: David Thrane Christiansen <david@davidchristiansen.dk>
Date: Fri, 31 Jan 2025 23:13:08 +0100
Subject: [PATCH] fix: allow multi-arg roles when generating string previews

---
 src/verso/Verso/Doc/Elab/Monad.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/verso/Verso/Doc/Elab/Monad.lean b/src/verso/Verso/Doc/Elab/Monad.lean
index a1f060c..8ba030b 100644
--- 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]