1.1 --- a/src/Pure/library.scala	Fri Jan 17 20:51:36 2014 +0100
     1.2 +++ b/src/Pure/library.scala	Sat Jan 18 19:15:12 2014 +0100
     1.3 @@ -110,6 +110,9 @@
     1.4    def try_unprefix(prfx: String, s: String): Option[String] =
     1.5      if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
     1.6  
     1.7 +  def try_unsuffix(sffx: String, s: String): Option[String] =
     1.8 +    if (s.endsWith(sffx)) Some(s.substring(0, s.length - sffx.length)) else None
     1.9 +
    1.10    def trim_line(s: String): String =
    1.11      if (s.endsWith("\r\n")) s.substring(0, s.length - 2)
    1.12      else if (s.endsWith("\r") || s.endsWith("\n")) s.substring(0, s.length - 1)