more direct indentation, using Symbol.spaces;
authorwenzelm
Wed, 08 Nov 2023 15:10:19 +0100
changeset 78917 30e0c15a71f7
parent 78916 e97fa2edf4b2
child 78918 8378354bbdad
more direct indentation, using Symbol.spaces;
src/Pure/General/toml.scala
--- a/src/Pure/General/toml.scala	Wed Nov 08 13:14:59 2023 +0100
+++ b/src/Pure/General/toml.scala	Wed Nov 08 15:10:19 2023 +0100
@@ -535,9 +535,8 @@
 
     def inline(t: T, indent: Int = 0): Str = {
       val result = new StringBuilder
-      def indentation(i: Int): Unit = for (_ <- Range(0, i)) result ++= "  "
 
-      indentation(indent)
+      result ++= Symbol.spaces(indent * 2)
       t match {
         case s: String =>
           if (s.rep.contains("\n") && s.rep.length > 20) result ++= multiline_basic_string(s.rep)
@@ -557,7 +556,7 @@
               result ++= inline(elem, indent + 1)
               result ++= ",\n"
             }
-            indentation(indent)
+            result ++= Symbol.spaces(indent * 2)
             result += ']'
           }
         case table: Table =>