diff -r fb4352e89022 -r 32692ce4c61a src/Pure/library.scala
--- a/src/Pure/library.scala	Tue May 14 14:17:56 2013 +0200
+++ b/src/Pure/library.scala	Tue May 14 15:40:18 2013 +0200
@@ -77,6 +77,12 @@
 
   /* lines */
 
+  def terminate_lines(lines: Iterable[CharSequence]): Iterable[CharSequence] =
+    new Iterable[CharSequence] {
+      def iterator: Iterator[CharSequence] =
+        lines.iterator.map(line => new Line_Termination(line))
+    }
+
   def cat_lines(lines: TraversableOnce[String]): String = lines.mkString("\n")
 
   def split_lines(str: String): List[String] = space_explode('\n', str)
@@ -109,7 +115,7 @@
   def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")
 
 
-  /* reverse CharSequence */
+  /* CharSequence */
 
   class Reverse(text: CharSequence, start: Int, end: Int) extends CharSequence
   {
@@ -133,6 +139,16 @@
     }
   }
 
+  class Line_Termination(text: CharSequence) extends CharSequence
+  {
+    def length: Int = text.length + 1
+    def charAt(i: Int): Char = if (i == text.length) '\n' else text.charAt(i)
+    def subSequence(i: Int, j: Int): CharSequence =
+      if (j == text.length + 1) new Line_Termination(text.subSequence(i, j - 1))
+      else text.subSequence(i, j)
+    override def toString: String = text.toString + "\n"
+  }
+
 
   /* Java futures */