back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;

--- a/NEWS	Sat Oct 31 14:16:29 2015 +0100
+++ b/NEWS	Sat Oct 31 14:38:48 2015 +0100
@@ -66,6 +66,10 @@
 uniformly, and allow the dummy file argument ":" to open an empty buffer
 instead.
 
+* The default look-and-feel for Linux is the traditional "Metal", which
+works better with GUI scaling for very high-resolution displays (e.g.
+4K). Moreover, it is generally more robust than "Nimbus".
+
 
 *** Document preparation ***
 

--- a/src/Doc/JEdit/JEdit.thy	Sat Oct 31 14:16:29 2015 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sat Oct 31 14:38:48 2015 +0100
@@ -283,7 +283,7 @@
   Isabelle/jEdit enables platform-specific look-and-feel by default as
   follows.
 
-  \<^descr>[Linux:] The platform-independent \<^emph>\<open>Nimbus\<close> is used by
+  \<^descr>[Linux:] The platform-independent \<^emph>\<open>Metal\<close> is used by
   default.
 
   \<^emph>\<open>GTK+\<close> also works under the side-condition that the overall GTK theme
@@ -310,7 +310,7 @@
   Users may experiment with different look-and-feels, but need to keep
   in mind that this extra variance of GUI functionality is unlikely to
   work in arbitrary combinations.  The platform-independent
-  \<^emph>\<open>Nimbus\<close> and \<^emph>\<open>Metal\<close> should always work.  The historic
+  \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close> should always work.  The historic
   \<^emph>\<open>CDE/Motif\<close> should be ignored.
 
   After changing the look-and-feel in \<^emph>\<open>Global Options~/
@@ -353,7 +353,7 @@
 
   \<^item> \<^emph>\<open>Global Options / Appearance / Button, menu and label font\<close> as
   well as \<^emph>\<open>List and text field font\<close>: this specifies the primary and
-  secondary font for the old \<^emph>\<open>Metal\<close> look-and-feel
+  secondary font for the traditional \<^emph>\<open>Metal\<close> look-and-feel
   (\secref{sec:look-and-feel}), which happens to scale better than newer ones
   like \<^emph>\<open>Nimbus\<close>.
 

--- a/src/Pure/GUI/gui.scala	Sat Oct 31 14:16:29 2015 +0100
+++ b/src/Pure/GUI/gui.scala	Sat Oct 31 14:38:48 2015 +0100
@@ -34,8 +34,7 @@
       if (Platform.is_windows || Platform.is_macos)
         UIManager.getSystemLookAndFeelClassName()
       else
-        find_laf("Nimbus") getOrElse
-          UIManager.getCrossPlatformLookAndFeelClassName()
+        UIManager.getCrossPlatformLookAndFeelClassName()
     }
 
   def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())

--- a/src/Tools/jEdit/src/jEdit.props	Sat Oct 31 14:16:29 2015 +0100
+++ b/src/Tools/jEdit/src/jEdit.props	Sat Oct 31 14:38:48 2015 +0100
@@ -240,7 +240,7 @@
 line-end.shortcut=END
 line-home.shortcut=HOME
 logo.icon.medium=32x32/apps/isabelle.gif
-lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel
+lookAndFeel=javax.swing.plaf.metal.MetalLookAndFeel
 match-bracket.shortcut2=C+9
 navigator.showOnToolbar=true
 next-bracket.shortcut2=C+e C+9