# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1700307250 -3600
# Node ID 39373f2151c48b9015ac67be673a74685fabec47
# Parent  9d1c4824a05590e39e181d0af74d28d3f61a224f
use toml key operations properly;
clarified module;

diff -r 9d1c4824a055 -r 39373f2151c4 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)