src/Pure/library.scala

--- a/src/Pure/library.scala	Tue Jun 25 11:41:16 2013 +0200
+++ b/src/Pure/library.scala	Tue Jun 25 12:17:19 2013 +0200
@@ -107,6 +107,11 @@
   def try_unprefix(prfx: String, s: String): Option[String] =
     if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
 
+  def trim_line(s: String): String =
+    if (s.endsWith("\r\n")) s.substring(0, s.length - 2)
+    else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1)
+    else s
+
 
   /* quote */