src/Pure/GUI/gui.scala
changeset 69113 0012f3a08f42
parent 67835 c8e4ee2b5482
child 69343 395c4fb15ea2
equal deleted inserted replaced
69112:5b749aa452c6 69113:0012f3a08f42
    53     val dummy_button = new JButton
    53     val dummy_button = new JButton
    54     def apply(id: Int): Unit =
    54     def apply(id: Int): Unit =
    55       component.setFocusTraversalKeys(id, dummy_button.getFocusTraversalKeys(id))
    55       component.setFocusTraversalKeys(id, dummy_button.getFocusTraversalKeys(id))
    56     apply(KeyboardFocusManager.FORWARD_TRAVERSAL_KEYS)
    56     apply(KeyboardFocusManager.FORWARD_TRAVERSAL_KEYS)
    57     apply(KeyboardFocusManager.BACKWARD_TRAVERSAL_KEYS)
    57     apply(KeyboardFocusManager.BACKWARD_TRAVERSAL_KEYS)
    58   }
       
    59 
       
    60 
       
    61   /* X11 window manager */
       
    62 
       
    63   def window_manager(): Option[String] =
       
    64   {
       
    65     if (Platform.is_windows || Platform.is_macos) None
       
    66     else
       
    67       try {
       
    68         val wm =
       
    69           Untyped.method(Class.forName("sun.awt.X11.XWM", true, ClassLoader.getSystemClassLoader),
       
    70             "getWM").invoke(null)
       
    71         if (wm == null) None
       
    72         else Some(wm.toString)
       
    73       }
       
    74       catch {
       
    75         case _: ClassNotFoundException => None
       
    76         case _: NoSuchMethodException => None
       
    77       }
       
    78   }
    58   }
    79 
    59 
    80 
    60 
    81   /* simple dialogs */
    61   /* simple dialogs */
    82 
    62