# HG changeset patch
# User wenzelm
# Date 1538565605 -7200
# Node ID 163626ddaa1968642a1622301989741b3943763e
# Parent  a3efc22181a882f9821d2d0f17ad4b083444365d# Parent  0012f3a08f4239551dde1b9ad2cb47d458300cff
merged

diff -r a3efc22181a8 -r 163626ddaa19 src/Pure/GUI/gui.scala
--- a/src/Pure/GUI/gui.scala	Wed Oct 03 10:42:00 2018 +0100
+++ b/src/Pure/GUI/gui.scala	Wed Oct 03 13:20:05 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)
diff -r a3efc22181a8 -r 163626ddaa19 src/Pure/System/platform.scala
--- a/src/Pure/System/platform.scala	Wed Oct 03 10:42:00 2018 +0100
+++ b/src/Pure/System/platform.scala	Wed Oct 03 13:20:05 2018 +0200
@@ -1,35 +1,29 @@
 /*  Title:      Pure/System/platform.scala
     Author:     Makarius
 
-Raw platform identification.
+System platform identification.
 */
 
 package isabelle
 
 
-import scala.util.matching.Regex
-
-
 object Platform
 {
-  /* main OS variants */
+  /* platform family */
 
   val is_linux = System.getProperty("os.name", "") == "Linux"
   val is_macos = System.getProperty("os.name", "") == "Mac OS X"
   val is_windows = System.getProperty("os.name", "").startsWith("Windows")
 
 
-  /* Platform identifiers */
+  /* platform identifiers */
 
-  private val Solaris = new Regex("SunOS|Solaris")
-  private val Linux = new Regex("Linux")
-  private val Darwin = new Regex("Mac OS X")
-  private val Windows = new Regex("Windows.*")
+  private val Linux = """Linux""".r
+  private val Darwin = """Mac OS X""".r
+  private val Windows = """Windows.*""".r
 
-  private val X86 = new Regex("i.86|x86")
-  private val X86_64 = new Regex("amd64|x86_64")
-  private val Sparc = new Regex("sparc")
-  private val PPC = new Regex("PowerPC|ppc")
+  private val X86 = """i.86|x86""".r
+  private val X86_64 = """amd64|x86_64""".r
 
   lazy val jvm_platform: String =
   {
@@ -37,13 +31,10 @@
       System.getProperty("os.arch", "") match {
         case X86() => "x86"
         case X86_64() => "x86_64"
-        case Sparc() => "sparc"
-        case PPC() => "ppc"
         case _ => error("Failed to determine CPU architecture")
       }
     val os =
       System.getProperty("os.name", "") match {
-        case Solaris() => "solaris"
         case Linux() => "linux"
         case Darwin() => "darwin"
         case Windows() => "windows"
@@ -55,7 +46,7 @@
 
   /* JVM version */
 
-  private val Version = new Regex("""1\.(\d+)\.0_(\d+)""")
+  private val Version = """1\.(\d+)\.0_(\d+)""".r
   lazy val jvm_version =
     System.getProperty("java.version") match {
       case Version(a, b) => a + "u" + b