src/Pure/library.scala

--- a/src/Pure/library.scala	Thu May 24 21:46:11 2012 +0200
+++ b/src/Pure/library.scala	Thu May 24 22:07:00 2012 +0200
@@ -172,7 +172,7 @@
   class Zoom_Box(apply_factor: Int => Unit) extends ComboBox[String](
     List("50%", "70%", "85%", "100%", "125%", "150%", "175%", "200%", "300%", "400%"))
   {
-    val Factor = "([0-9]+)%?"r
+    val Factor = "([0-9]+)%?".r
     def parse(text: String): Int =
       text match {
         case Factor(s) =>