--- 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 */
--- 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)
}
--- 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) =>
--- 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() }