more specialized operations;

--- a/src/Pure/General/bytes.scala	Tue Jul 02 21:54:12 2024 +0200
+++ b/src/Pure/General/bytes.scala	Tue Jul 02 22:38:00 2024 +0200
@@ -390,6 +390,40 @@
     else this
 
 
+  /* separated chunks */
+
+  def separated_chunks(sep: Byte): Iterator[Bytes] =
+    new Iterator[Bytes] {
+      private var start: Long = -1
+      private var stop: Long = -1
+
+      private def end(i: Long): Long = {
+        var j = i
+        while (j < Bytes.this.size && byte_unchecked(j) != sep) { j += 1 }
+        j
+      }
+
+      // init
+      if (!Bytes.this.is_empty) { start = 0; stop = end(0) }
+
+      def hasNext: Boolean =
+        0 <= start && start <= stop && stop <= Bytes.this.size
+
+      def next(): Bytes =
+        if (hasNext) {
+          val chunk = Bytes.this.slice(start, stop)
+          if (stop < Bytes.this.size) { start = stop + 1; stop = end(start) }
+          else { start = -1; stop = -1 }
+          chunk
+        }
+        else throw new NoSuchElementException
+    }
+
+  def space_explode(sep: Byte): List[Bytes] = separated_chunks(sep).toList
+
+  def split_lines: List[Bytes] = space_explode(10)
+
+
   /* hash and equality */
 
   lazy val sha1_digest: SHA1.Digest =