src/Pure/GUI/gui.scala
changeset 54965 a8af7a9c38d1
parent 54962 993aab23894c
child 56622 891d1b8b64fb
equal deleted inserted replaced
54964:bbf2ef613b8c 54965:a8af7a9c38d1
    41 
    41 
    42   /* X11 window manager */
    42   /* X11 window manager */
    43 
    43 
    44   def window_manager(): Option[String] =
    44   def window_manager(): Option[String] =
    45   {
    45   {
    46     try {
    46     if (Platform.is_windows || Platform.is_macos) None
    47       val XWM = Class.forName("sun.awt.X11.XWM", true, ClassLoader.getSystemClassLoader)
    47     else
    48       val getWM = XWM.getDeclaredMethod("getWM")
    48       try {
    49       getWM.setAccessible(true)
    49         val XWM = Class.forName("sun.awt.X11.XWM", true, ClassLoader.getSystemClassLoader)
    50       getWM.invoke(null) match {
    50         val getWM = XWM.getDeclaredMethod("getWM")
    51         case null => None
    51         getWM.setAccessible(true)
    52         case wm => Some(wm.toString)
    52         getWM.invoke(null) match {
    53       }
    53           case null => None
    54     }
    54           case wm => Some(wm.toString)
    55     catch {
    55         }
    56       case _: ClassNotFoundException => None
    56       }
    57       case _: NoSuchMethodException => None
    57       catch {
    58     }
    58         case _: ClassNotFoundException => None
       
    59         case _: NoSuchMethodException => None
       
    60       }
    59   }
    61   }
    60 
    62 
    61 
    63 
    62   /* simple dialogs */
    64   /* simple dialogs */
    63 
    65