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]