# HG changeset patch
# User wenzelm
# Date 1365091608 -7200
# Node ID 4e49bba9772d055c9cddce24f422406adaa532fb
# Parent  949e2cf02a3df7c0be902d4cd48bc8cbb78b34f6
tuned signature -- concentrate GUI tools;

diff -r 949e2cf02a3d -r 4e49bba9772d src/Pure/System/gui_setup.scala
--- a/src/Pure/System/gui_setup.scala	Thu Apr 04 17:58:47 2013 +0200
+++ b/src/Pure/System/gui_setup.scala	Thu Apr 04 18:06:48 2013 +0200
@@ -17,7 +17,7 @@
 {
   def startup(args: Array[String]) =
   {
-    Platform.init_laf()
+    GUI.init_laf()
     top.pack()
     top.visible = true
   }
diff -r 949e2cf02a3d -r 4e49bba9772d src/Pure/System/platform.scala
--- a/src/Pure/System/platform.scala	Thu Apr 04 17:58:47 2013 +0200
+++ b/src/Pure/System/platform.scala	Thu Apr 04 18:06:48 2013 +0200
@@ -8,7 +8,6 @@
 package isabelle
 
 import java.lang.System
-import javax.swing.UIManager
 
 import scala.util.matching.Regex
 
@@ -58,21 +57,5 @@
   /* JVM name */
 
   val jvm_name: String = System.getProperty("java.vm.name")
-
-
-  /* Swing look-and-feel */
-
-  private def find_laf(name: String): Option[String] =
-    UIManager.getInstalledLookAndFeels().find(_.getName == name).map(_.getClassName)
-
-  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())
 }
 
diff -r 949e2cf02a3d -r 4e49bba9772d src/Pure/Tools/build_dialog.scala
--- a/src/Pure/Tools/build_dialog.scala	Thu Apr 04 17:58:47 2013 +0200
+++ b/src/Pure/Tools/build_dialog.scala	Thu Apr 04 18:06:48 2013 +0200
@@ -18,7 +18,7 @@
 {
   def main(args: Array[String]) =
   {
-    Platform.init_laf()
+    GUI.init_laf()
     try {
       args.toList match {
         case
diff -r 949e2cf02a3d -r 4e49bba9772d src/Pure/Tools/main.scala
--- a/src/Pure/Tools/main.scala	Thu Apr 04 17:58:47 2013 +0200
+++ b/src/Pure/Tools/main.scala	Thu Apr 04 18:06:48 2013 +0200
@@ -15,7 +15,7 @@
   {
     val (out, rc) =
       try {
-        Platform.init_laf()
+        GUI.init_laf()
         Isabelle_System.init()
         Isabelle_System.isabelle_tool("jedit", ("-s" :: args.toList): _*)
       }
diff -r 949e2cf02a3d -r 4e49bba9772d src/Tools/Graphview/src/graphview.scala
--- a/src/Tools/Graphview/src/graphview.scala	Thu Apr 04 17:58:47 2013 +0200
+++ b/src/Tools/Graphview/src/graphview.scala	Thu Apr 04 18:06:48 2013 +0200
@@ -22,7 +22,7 @@
     // FIXME avoid I/O etc. on Swing thread
     val graph: Model.Graph =
       try {
-        Platform.init_laf()
+        GUI.init_laf()
         Isabelle_System.init()
         Isabelle_Font.install_fonts()
         ToolTipManager.sharedInstance.setDismissDelay(1000*60*60)
diff -r 949e2cf02a3d -r 4e49bba9772d src/Tools/jEdit/src/jedit_main.scala
--- a/src/Tools/jEdit/src/jedit_main.scala	Thu Apr 04 17:58:47 2013 +0200
+++ b/src/Tools/jEdit/src/jedit_main.scala	Thu Apr 04 18:06:48 2013 +0200
@@ -17,7 +17,7 @@
 {
   def main(args: Array[String])
   {
-    Platform.init_laf()
+    GUI.init_laf()
     Isabelle_System.init()
 
     System.setProperty("jedit.home",