src/Pure/library.scala

--- a/src/Pure/library.scala	Sat Jan 12 16:43:38 2013 +0100
+++ b/src/Pure/library.scala	Sat Jan 12 17:28:07 2013 +0100
@@ -82,6 +82,9 @@
     else ""
   }
 
+
+  /* strings */
+
   def lowercase(str: String): String = str.toLowerCase(Locale.ENGLISH)
   def uppercase(str: String): String = str.toUpperCase(Locale.ENGLISH)
 
@@ -89,6 +92,9 @@
     if (str.length == 0) str
     else uppercase(str.substring(0, 1)) + str.substring(1)
 
+  def try_unprefix(prfx: String, s: String): Option[String] =
+    if (s.startsWith(prfx)) Some(s.substring(prfx.length)) else None
+
 
   /* quote */