diff --git a/src/Lean/Widget/TaggedText.lean b/src/Lean/Widget/TaggedText.lean index fd3ba7ad41..35dc0daf8e 100644 --- a/src/Lean/Widget/TaggedText.lean +++ b/src/Lean/Widget/TaggedText.lean @@ -120,7 +120,7 @@ where go (acc : String) : Array (TaggedText α) → String | #[] => acc | ts => match ts.back with | text s => go (acc ++ s) ts.pop - | append as => go acc (ts.pop ++ as) + | append as => go acc (ts.pop ++ as.reverse) | tag _ a => go acc (ts.set! (ts.size - 1) a) end TaggedText