clarified signature: more operations;

--- a/src/Pure/General/bytes.ML	Wed Jun 22 14:31:18 2022 +0200
+++ b/src/Pure/General/bytes.ML	Wed Jun 22 16:24:57 2022 +0200
@@ -30,6 +30,9 @@
   val string: string -> T
   val newline: T
   val buffer: Buffer.T -> T
+  val space_explode: string -> T -> string list
+  val split_lines: T -> string list
+  val cat_lines: string list -> T
   val read_block: int -> BinIO.instream -> string
   val read_stream: int -> BinIO.instream -> T
   val write_stream: BinIO.outstream -> T -> unit
@@ -139,6 +142,44 @@
 val buffer = build o fold add o Buffer.contents;
 
 
+(* space_explode *)
+
+fun space_explode sep bytes =
+  if is_empty bytes then []
+  else if size sep <> 1 then [content bytes]
+  else
+    let
+      val sep_char = String.sub (sep, 0);
+
+      fun add_part s part =
+        Buffer.add (Substring.string s) (the_default Buffer.empty part);
+
+      fun explode head tail part res =
+        if Substring.isEmpty head then
+          (case tail of
+            [] =>
+              (case part of
+                NONE => rev res
+              | SOME buf => rev (Buffer.content buf :: res))
+          | chunk :: chunks => explode (Substring.full chunk) chunks part res)
+        else
+          (case Substring.fields (fn c => c = sep_char) head of
+            [a] => explode Substring.empty tail (SOME (add_part a part)) res
+          | a :: rest =>
+              let
+                val (bs, c) = split_last rest;
+                val res' = res
+                  |> cons (Buffer.content (add_part a part))
+                  |> fold (cons o Substring.string) bs;
+                val part' = SOME (add_part c NONE);
+              in explode Substring.empty tail part' res' end)
+    in explode Substring.empty (contents bytes) NONE [] end;
+
+val split_lines = space_explode "\n";
+
+fun cat_lines lines = build (fold add (separate "\n" lines));
+
+
 (* IO *)
 
 fun read_block limit =

--- a/src/Pure/ML/ml_init.ML	Wed Jun 22 14:31:18 2022 +0200
+++ b/src/Pure/ML/ml_init.ML	Wed Jun 22 16:24:57 2022 +0200
@@ -33,3 +33,9 @@
     if n = 1 then String.str (String.sub (s, i))
     else String.substring (s, i, n);
 end;
+
+structure Substring =
+struct
+  open Substring;
+  val empty = full "";
+end;