# HG changeset patch
# User wenzelm
# Date 1699452619 -3600
# Node ID 30e0c15a71f7db41904455ed3528e2b8498082e9
# Parent  e97fa2edf4b2ccf053b0daba2052d168207ead97
more direct indentation, using Symbol.spaces;

diff -r e97fa2edf4b2 -r 30e0c15a71f7 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 =>