src/Pure/library.scala

--- a/src/Pure/library.scala	Sat May 03 20:31:29 2014 +0200
+++ b/src/Pure/library.scala	Sat May 03 22:47:43 2014 +0200
@@ -112,6 +112,11 @@
   /* quote */
 
   def quote(s: String): String = "\"" + s + "\""
+
+  def try_unquote(s: String): Option[String] =
+    if (s.startsWith("\"") && s.endsWith("\"")) Some(s.substring(1, s.length - 1))
+    else None
+
   def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
   def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")