# HG changeset patch
# User wenzelm
# Date 1358018014 -3600
# Node ID 4cd2d090be8f89c801563569964d64923a3e6d27
# Parent  70f7483df9cbf520ab9db6af04ef9f17bff9c909
tuned font size, notably for current HD displays;

diff -r 70f7483df9cb -r 4cd2d090be8f src/Pure/Tools/build_dialog.scala
--- a/src/Pure/Tools/build_dialog.scala	Sat Jan 12 19:53:24 2013 +0100
+++ b/src/Pure/Tools/build_dialog.scala	Sat Jan 12 20:13:34 2013 +0100
@@ -75,10 +75,10 @@
     /* text */
 
     val text = new TextArea {
-      font = new Font("SansSerif", Font.PLAIN, 14)
+      font = new Font("SansSerif", Font.PLAIN, Library.resolution_scale(10))
       editable = false
-      columns = 40
-      rows = 10
+      columns = 50
+      rows = 20
     }
 
     val progress = new Build.Progress
diff -r 70f7483df9cb -r 4cd2d090be8f src/Pure/library.scala
--- a/src/Pure/library.scala	Sat Jan 12 19:53:24 2013 +0100
+++ b/src/Pure/library.scala	Sat Jan 12 20:13:34 2013 +0100
@@ -11,7 +11,7 @@
 import java.lang.System
 import java.util.Locale
 import java.util.concurrent.{Future => JFuture, TimeUnit}
-import java.awt.Component
+import java.awt.{Component, Toolkit}
 import javax.swing.JOptionPane
 
 import scala.swing.{ComboBox, TextArea, ScrollPane}
@@ -200,6 +200,12 @@
   }
 
 
+  /* screen resolution */
+
+  def resolution_scale(): Double = Toolkit.getDefaultToolkit.getScreenResolution.toDouble / 72
+  def resolution_scale(i: Int): Int = (i.toDouble * resolution_scale()).round.toInt
+
+
   /* Java futures */
 
   def future_value[A](x: A) = new JFuture[A]