# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1700331376 -3600
# Node ID 6201057b98ddb7fa05ef1f655907fd1ea9ce9d9b
# Parent  39373f2151c48b9015ac67be673a74685fabec47
clarified toml keys: more operations;

diff -r 39373f2151c4 -r 6201057b98dd src/Pure/General/toml.scala
--- 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