unused -- avoid illegal access in Java 11;
authorwenzelm
Wed, 03 Oct 2018 12:28:09 +0200
changeset 69113 0012f3a08f42
parent 69112 5b749aa452c6
child 69114 163626ddaa19
unused -- avoid illegal access in Java 11;
src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Wed Oct 03 12:27:39 2018 +0200
+++ b/src/Pure/GUI/gui.scala	Wed Oct 03 12:28:09 2018 +0200
@@ -58,26 +58,6 @@
   }
 
 
-  /* X11 window manager */
-
-  def window_manager(): Option[String] =
-  {
-    if (Platform.is_windows || Platform.is_macos) None
-    else
-      try {
-        val wm =
-          Untyped.method(Class.forName("sun.awt.X11.XWM", true, ClassLoader.getSystemClassLoader),
-            "getWM").invoke(null)
-        if (wm == null) None
-        else Some(wm.toString)
-      }
-      catch {
-        case _: ClassNotFoundException => None
-        case _: NoSuchMethodException => None
-      }
-  }
-
-
   /* simple dialogs */
 
   def scrollable_text(raw_txt: String, width: Int = 60, height: Int = 20, editable: Boolean = false)