diff -r fbfc18be1f8c -r 10c5871ec684 src/Pure/General/scan.scala
--- a/src/Pure/General/scan.scala	Sun Dec 27 21:34:23 2009 +0100
+++ b/src/Pure/General/scan.scala	Sun Dec 27 22:16:41 2009 +0100
@@ -187,7 +187,14 @@
     def quoted_content(quote: String, source: String): String =
     {
       require(parseAll(quoted(quote), source).successful)
-      source.substring(1, source.length - 1)  // FIXME proper escapes
+      val body = source.substring(1, source.length - 1)
+      if (body.exists(_ == '\\')) {
+        val content =
+          rep(many1(sym => sym != quote && sym != "\\" && Symbol.is_closed(sym)) |
+              "\\" ~> (quote | "\\" | """\d\d\d""".r ^^ { case x => x.toInt.toChar.toString }))
+        parseAll(content ^^ (_.mkString), body).get
+      }
+      else body
     }