--- a/src/Pure/General/bytes.ML Wed Feb 05 21:29:13 2025 +0100
+++ b/src/Pure/General/bytes.ML Wed Feb 05 22:54:47 2025 +0100
@@ -36,6 +36,7 @@
val split_lines: T -> string list
val trim_split_lines: T -> string list
val cat_lines: string list -> T
+ val terminate_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
@@ -190,6 +191,8 @@
fun cat_lines lines = build (fold add (separate "\n" lines));
+fun terminate_lines lines = build (fold (fn line => add line #> add "\n") lines);
+
(* IO *)