use toml key operations properly;
authorFabian Huch <huch@in.tum.de>
Sat, 18 Nov 2023 12:34:10 +0100
changeset 79004 39373f2151c4
parent 79003 9d1c4824a055
child 79005 6201057b98dd
use toml key operations properly; clarified module;
src/Pure/General/toml.scala
--- a/src/Pure/General/toml.scala	Sat Nov 18 12:25:16 2023 +0100
+++ b/src/Pure/General/toml.scala	Sat Nov 18 12:34:10 2023 +0100
@@ -388,7 +388,7 @@
     def dotted(s: Str): Keys = new Keys(s.split('.').toList)
   }
 
-  class Keys private(val rep: List[Key]) extends Positional {
+  class Keys private(private val rep: List[Key]) extends Positional {
     override def hashCode(): Int = rep.hashCode()
     override def equals(obj: Any): Bool =
       obj match {
@@ -503,7 +503,9 @@
 
     def convert(ks0: Keys, ks1: Keys, v: Parsers.V): T = {
       def to_table(ks: Keys, t: T): Table =
-        ks.parent.rep.foldRight(Table(ks.the_last -> t))((k, v) => Table(k -> v))
+        if (ks.length == 1) Table(ks.the_head -> t)
+        else Table(ks.the_head -> to_table(ks.split(1)._2, t))
+
       def to_toml(v: Parsers.V): (T, Set[Keys]) = v match {
         case Parsers.Primitive(t) => (t, Set.empty)
         case Parsers.Array(rep) => (Array(rep.map(to_toml(_)._1)), Set.empty)