clarified toml keys: more operations;

--- a/src/Pure/General/toml.scala	Sat Nov 18 12:34:10 2023 +0100
+++ b/src/Pure/General/toml.scala	Sat Nov 18 19:16:16 2023 +0100
@@ -401,7 +401,9 @@
     def the_last: Key = rep.last
 
     def head: Keys = new Keys(rep.take(1))
+    def next: Keys = new Keys(rep.drop(1))
     def the_head: Key = rep.head
+    def the_key: Key = Library.the_single(rep)
 
     def length: Int = rep.length