src/Pure/GUI/gui.scala
changeset 59201 702e0971d617
parent 59183 ec83638b6bfb
child 59230 cae3ef2897f2
--- a/src/Pure/GUI/gui.scala	Tue Dec 30 10:38:10 2014 +0100
+++ b/src/Pure/GUI/gui.scala	Tue Dec 30 11:50:34 2014 +0100
@@ -25,14 +25,19 @@
 {
   /* Swing look-and-feel */
 
+  def find_laf(name: String): Option[String] =
+    UIManager.getInstalledLookAndFeels().
+      find(c => c.getName == name || c.getClassName == name).
+      map(_.getClassName)
+
   def get_laf(): String =
-  {
-    if (Platform.is_windows || Platform.is_macos)
-      UIManager.getSystemLookAndFeelClassName()
-    else
-      UIManager.getInstalledLookAndFeels().find(_.getName == "Nimbus").map(_.getClassName)
-        .getOrElse(UIManager.getCrossPlatformLookAndFeelClassName())
-  }
+    find_laf(System.getProperty("isabelle.laf")) getOrElse {
+      if (Platform.is_windows || Platform.is_macos)
+        UIManager.getSystemLookAndFeelClassName()
+      else
+        find_laf("Nimbus") getOrElse
+          UIManager.getCrossPlatformLookAndFeelClassName()
+    }
 
   def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
 
@@ -161,12 +166,6 @@
     else "<html>" + HTML.encode(text) + "</html>"
 
 
-  /* screen resolution */
-
-  def resolution_scale(): Double = Toolkit.getDefaultToolkit.getScreenResolution.toDouble / 72
-  def resolution_scale(i: Int): Int = (i.toDouble * resolution_scale()).round.toInt
-
-
   /* icon */
 
   def isabelle_icon(): ImageIcon =