1.1 --- a/src/Pure/General/symbol.scala	Thu May 24 21:46:11 2012 +0200
     1.2 +++ b/src/Pure/General/symbol.scala	Thu May 24 22:07:00 2012 +0200
     1.3 @@ -243,7 +243,7 @@
     1.4      private val symbols: List[(Symbol, Map[String, String])] =
     1.5        Map((
     1.6          for (decl <- split_lines(symbols_spec) if !empty.pattern.matcher(decl).matches)
     1.7 -          yield read_decl(decl)): _*) toList
     1.8 +          yield read_decl(decl)): _*).toList
     1.9  
    1.10  
    1.11      /* misc properties */

     2.1 --- a/src/Pure/General/time.scala	Thu May 24 21:46:11 2012 +0200
     2.2 +++ b/src/Pure/General/time.scala	Thu May 24 22:07:00 2012 +0200
     2.3 @@ -10,7 +10,7 @@
     2.4  
     2.5  object Time
     2.6  {
     2.7 -  def seconds(s: Double): Time = new Time((s * 1000.0) round)
     2.8 +  def seconds(s: Double): Time = new Time((s * 1000.0).round)
     2.9    def ms(m: Long): Time = new Time(m)
    2.10  }
    2.11  

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

     4.1 --- a/src/Tools/jEdit/src/document_view.scala	Thu May 24 21:46:11 2012 +0200
     4.2 +++ b/src/Tools/jEdit/src/document_view.scala	Thu May 24 22:07:00 2012 +0200
     4.3 @@ -329,7 +329,7 @@
     4.4  
     4.5    /* text status overview left of scrollbar */
     4.6  
     4.7 -  private val overview = new Text_Overview(this)
     4.8 +  private object overview extends Text_Overview(this)
     4.9    {
    4.10      val delay_repaint =
    4.11        Swing_Thread.delay_first(Isabelle.session.update_delay) { repaint() }