1.1 --- a/src/Pure/Tools/build_dialog.scala	Sat Jan 12 19:53:24 2013 +0100
     1.2 +++ b/src/Pure/Tools/build_dialog.scala	Sat Jan 12 20:13:34 2013 +0100
     1.3 @@ -75,10 +75,10 @@
     1.4      /* text */
     1.5  
     1.6      val text = new TextArea {
     1.7 -      font = new Font("SansSerif", Font.PLAIN, 14)
     1.8 +      font = new Font("SansSerif", Font.PLAIN, Library.resolution_scale(10))
     1.9        editable = false
    1.10 -      columns = 40
    1.11 -      rows = 10
    1.12 +      columns = 50
    1.13 +      rows = 20
    1.14      }
    1.15  
    1.16      val progress = new Build.Progress

     2.1 --- a/src/Pure/library.scala	Sat Jan 12 19:53:24 2013 +0100
     2.2 +++ b/src/Pure/library.scala	Sat Jan 12 20:13:34 2013 +0100
     2.3 @@ -11,7 +11,7 @@
     2.4  import java.lang.System
     2.5  import java.util.Locale
     2.6  import java.util.concurrent.{Future => JFuture, TimeUnit}
     2.7 -import java.awt.Component
     2.8 +import java.awt.{Component, Toolkit}
     2.9  import javax.swing.JOptionPane
    2.10  
    2.11  import scala.swing.{ComboBox, TextArea, ScrollPane}
    2.12 @@ -200,6 +200,12 @@
    2.13    }
    2.14  
    2.15  
    2.16 +  /* screen resolution */
    2.17 +
    2.18 +  def resolution_scale(): Double = Toolkit.getDefaultToolkit.getScreenResolution.toDouble / 72
    2.19 +  def resolution_scale(i: Int): Int = (i.toDouble * resolution_scale()).round.toInt
    2.20 +
    2.21 +
    2.22    /* Java futures */
    2.23  
    2.24    def future_value[A](x: A) = new JFuture[A]