diff -r a7352cbde7d7 -r 2c5039363ea3 src/Pure/library.scala
--- a/src/Pure/library.scala	Thu Oct 06 11:13:12 2016 +0200
+++ b/src/Pure/library.scala	Thu Oct 06 11:27:03 2016 +0200
@@ -130,6 +130,9 @@
     else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1)
     else s
 
+  def trim_split_lines(s: String): List[String] =
+    split_lines(trim_line(s)).map(trim_line(_))
+
 
   /* quote */