# HG changeset patch
# User wenzelm
# Date 1273505852 -7200
# Node ID b7a62e7dec00978217d349c72cee9ec725b6262a
# Parent  55025bd6605f2670b034e060de98b509d00d771f
more convenient look-and-feel setup;

diff -r 55025bd6605f -r b7a62e7dec00 src/Pure/System/gui_setup.scala
--- a/src/Pure/System/gui_setup.scala	Mon May 10 17:29:19 2010 +0200
+++ b/src/Pure/System/gui_setup.scala	Mon May 10 17:37:32 2010 +0200
@@ -6,8 +6,6 @@
 
 package isabelle
 
-import javax.swing.UIManager
-
 import scala.swing._
 import scala.swing.event._
 
@@ -16,7 +14,7 @@
 {
   def startup(args: Array[String]) =
   {
-    UIManager.setLookAndFeel(Platform.look_and_feel)
+    Platform.init_laf()
     top.pack()
     top.visible = true
   }
diff -r 55025bd6605f -r b7a62e7dec00 src/Pure/System/platform.scala
--- a/src/Pure/System/platform.scala	Mon May 10 17:29:19 2010 +0200
+++ b/src/Pure/System/platform.scala	Mon May 10 17:37:32 2010 +0200
@@ -58,12 +58,14 @@
   private def find_laf(name: String): Option[String] =
     UIManager.getInstalledLookAndFeels().find(_.getName == name).map(_.getClassName)
 
-  def look_and_feel(): String =
+  def get_laf(): String =
   {
     if (is_windows || is_macos) UIManager.getSystemLookAndFeelClassName()
     else
       find_laf("Nimbus") orElse find_laf("GTK+") getOrElse
       UIManager.getCrossPlatformLookAndFeelClassName()
   }
+
+  def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
 }