src/Pure/library.scala

--- a/src/Pure/library.scala	Mon Oct 06 14:21:38 2014 +0200
+++ b/src/Pure/library.scala	Mon Oct 06 16:54:35 2014 +0200
@@ -145,6 +145,8 @@
     if (s.startsWith("\"") && s.endsWith("\"")) Some(s.substring(1, s.length - 1))
     else None
 
+  def perhaps_unquote(s: String): String = try_unquote(s) getOrElse s
+
   def commas(ss: Iterable[String]): String = ss.iterator.mkString(", ")
   def commas_quote(ss: Iterable[String]): String = ss.iterator.map(quote).mkString(", ")