--- a/src/Pure/General/bytes.ML Wed Jun 22 16:25:22 2022 +0200
+++ b/src/Pure/General/bytes.ML Wed Jun 22 16:54:30 2022 +0200
@@ -32,6 +32,7 @@
val buffer: Buffer.T -> T
val space_explode: string -> T -> string list
val split_lines: T -> string list
+ val trim_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
@@ -177,6 +178,8 @@
val split_lines = space_explode "\n";
+val trim_split_lines = trim_line #> split_lines #> map Library.trim_line;
+
fun cat_lines lines = build (fold add (separate "\n" lines));