# HG changeset patch
# User wenzelm
# Date 1337890020 -7200
# Node ID 135fd6f2dadd4d77a0c3a07db4b7886622271207
# Parent  7700f0e9618c4a567874b2c690fea12c4043383c
less warning in scala-2.10.0-M3;

diff -r 7700f0e9618c -r 135fd6f2dadd src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Thu May 24 21:46:11 2012 +0200
+++ b/src/Pure/General/symbol.scala	Thu May 24 22:07:00 2012 +0200
@@ -243,7 +243,7 @@
     private val symbols: List[(Symbol, Map[String, String])] =
       Map((
         for (decl <- split_lines(symbols_spec) if !empty.pattern.matcher(decl).matches)
-          yield read_decl(decl)): _*) toList
+          yield read_decl(decl)): _*).toList
 
 
     /* misc properties */
diff -r 7700f0e9618c -r 135fd6f2dadd src/Pure/General/time.scala
--- a/src/Pure/General/time.scala	Thu May 24 21:46:11 2012 +0200
+++ b/src/Pure/General/time.scala	Thu May 24 22:07:00 2012 +0200
@@ -10,7 +10,7 @@
 
 object Time
 {
-  def seconds(s: Double): Time = new Time((s * 1000.0) round)
+  def seconds(s: Double): Time = new Time((s * 1000.0).round)
   def ms(m: Long): Time = new Time(m)
 }
 
diff -r 7700f0e9618c -r 135fd6f2dadd 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) =>
diff -r 7700f0e9618c -r 135fd6f2dadd src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Thu May 24 21:46:11 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Thu May 24 22:07:00 2012 +0200
@@ -329,7 +329,7 @@
 
   /* text status overview left of scrollbar */
 
-  private val overview = new Text_Overview(this)
+  private object overview extends Text_Overview(this)
   {
     val delay_repaint =
       Swing_Thread.delay_first(Isabelle.session.update_delay) { repaint() }