From fd3bf289c44577a6beae25deae4f6fc6ba77ea25 Mon Sep 17 00:00:00 2001
From: Wojciech Nawrocki <t-wnawrocki@microsoft.com>
Date: Tue, 3 Aug 2021 18:10:39 -0400
Subject: [PATCH] fix: text ordering

---
 src/Lean/Widget/TaggedText.lean | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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