# HG changeset patch
# User wenzelm
# Date 1655909670 -7200
# Node ID 7ff9745609d7cf03d33de6cd68ee9f34982be9ec
# Parent  ecbd0b38256b1e21b0372a9d9a507a63b6baa4d5
more operations;

diff -r ecbd0b38256b -r 7ff9745609d7 src/Pure/General/bytes.ML
--- 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));