# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1700306716 -3600
# Node ID 9d1c4824a05590e39e181d0af74d28d3f61a224f
# Parent  16fa55f8958d6cfe92db2eb65c5860610417bbe8
clarified toml keys formatting vs. toString;

diff -r 16fa55f8958d -r 9d1c4824a055 src/Pure/General/toml.scala
--- a/src/Pure/General/toml.scala	Sat Nov 18 12:18:44 2023 +0100
+++ b/src/Pure/General/toml.scala	Sat Nov 18 12:25:16 2023 +0100
@@ -112,9 +112,9 @@
             case Some(value) => value
             case None =>
               error("Expected" + classTag[A].runtimeClass.getName +
-                ", got " + v.getClass.getSimpleName + " for key " + Format.key(k))
+                ", got " + v.getClass.getSimpleName + " for key " + quote(k))
           }
-          case None => error("Key " + Format.key(k) + " does not exist")
+          case None => error("Key " + quote(k) + " does not exist")
         }
     }
 
@@ -475,7 +475,7 @@
     def for_file(file: Path): Parse_Context = new Parse_Context(seen_tables, Some(file))
 
     def error[A](s: Str, pos: input.Position, key: Option[Keys] = None): A = {
-      val key_msg = if_proper(key, " in table " + Format.keys(key.get.rep))
+      val key_msg = if_proper(key, " in table " + key.get)
       val file_msg = if_proper(file, " in " + file.get)
       isabelle.error(s + key_msg + " at line " + pos.line + file_msg)
     }
@@ -510,7 +510,7 @@
         case Parsers.Inline_Table(elems) =>
           elems.find(e => elems.count(_._1 == e._1) > 1).foreach((ks, _) =>
             context.error(
-              "Duplicate key " + Format.keys(ks.rep) + " in inline table", v.pos, Some(ks0 + ks1)))
+              "Duplicate " + ks + " in inline table", v.pos, Some(ks0 + ks1)))
 
           val (tables, pfxs, key_spaces) =
             elems.map { (ks, v) =>
@@ -608,7 +608,7 @@
           if (c <= '\u001f' || c == '\u007f') "\\u%04x".format(c.toInt) else c
       }.mkString.replace("\"\"\"", "\"\"\\\"") + "\"\"\""
 
-    def key(k: Key): Str = {
+    private def key(k: Key): Str = {
       val Bare_Key = """[A-Za-z0-9_-]+""".r
       k match {
         case Bare_Key() => k
@@ -616,9 +616,9 @@
       }
     }
 
-    def keys(ks: List[Key]): Str = ks.map(key).mkString(".")
+    private def keys(ks: List[Key]): Str = ks.map(key).mkString(".")
 
-    def inline(t: T, indent: Int = 0): Str = {
+    private def inline(t: T, indent: Int = 0): Str = {
       val result = new StringBuilder
 
       result ++= Symbol.spaces(indent * 2)