refactor: speed up list operation

Seasawher · Apr 2, 2024 · 12e9169 · 12e9169
1 parent 059dc77
commit 12e9169
Showing 1 changed file with 5 additions and 5 deletions.
diff --git a/Mdgen/ConvertToMd.lean b/Mdgen/ConvertToMd.lean
@@ -27,26 +27,26 @@ private def buildBlocks (lines : List String) : List Block := Id.run do
           s!" line {i+1}: {line}"
 
       if content != "" then
-        blocks ++= [{content := content.trim, toCodeBlock := toCodeBlock}]
+        blocks := {content := content.trim, toCodeBlock := toCodeBlock} :: blocks
       toCodeBlock := ! toCodeBlock
       content := line ++ "\n"
 
       if line.endsWith "-/" then
-        blocks ++= [{content := content.trim, toCodeBlock := toCodeBlock}]
+        blocks := {content := content.trim, toCodeBlock := toCodeBlock} :: blocks
         toCodeBlock := ! toCodeBlock
         content := ""
 
     else if line.endsWith "-/" && ! toCodeBlock then
       content ++= line
-      blocks ++= [{content := content.trim, toCodeBlock := toCodeBlock}]
+      blocks := {content := content.trim, toCodeBlock := toCodeBlock} :: blocks
       toCodeBlock := ! toCodeBlock
       content := ""
     else
       content ++= line ++ "\n"
 
   if content != "" then
-    blocks ++= [{content := content.trim, toCodeBlock := toCodeBlock}]
-  return blocks
+    blocks := {content := content.trim, toCodeBlock := toCodeBlock} :: blocks
+  return blocks.reverse
 
 /-- markdown text -/
 abbrev Md := String