back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
authorwenzelm
Sat Oct 31 14:38:48 2015 +0100 (2015-10-31)
changeset 6152982fc5a6231a2
parent 61528 053f7083b3eb
child 61530 aa1ece0bce62
back to traditional Metal as default, and thus evade current problems with Nimbus scrollbar slider;
NEWS
src/Doc/JEdit/JEdit.thy
src/Pure/GUI/gui.scala
src/Tools/jEdit/src/jEdit.props
     1.1 --- a/NEWS	Sat Oct 31 14:16:29 2015 +0100
     1.2 +++ b/NEWS	Sat Oct 31 14:38:48 2015 +0100
     1.3 @@ -66,6 +66,10 @@
     1.4  uniformly, and allow the dummy file argument ":" to open an empty buffer
     1.5  instead.
     1.6  
     1.7 +* The default look-and-feel for Linux is the traditional "Metal", which
     1.8 +works better with GUI scaling for very high-resolution displays (e.g.
     1.9 +4K). Moreover, it is generally more robust than "Nimbus".
    1.10 +
    1.11  
    1.12  *** Document preparation ***
    1.13  
     2.1 --- a/src/Doc/JEdit/JEdit.thy	Sat Oct 31 14:16:29 2015 +0100
     2.2 +++ b/src/Doc/JEdit/JEdit.thy	Sat Oct 31 14:38:48 2015 +0100
     2.3 @@ -283,7 +283,7 @@
     2.4    Isabelle/jEdit enables platform-specific look-and-feel by default as
     2.5    follows.
     2.6  
     2.7 -  \<^descr>[Linux:] The platform-independent \<^emph>\<open>Nimbus\<close> is used by
     2.8 +  \<^descr>[Linux:] The platform-independent \<^emph>\<open>Metal\<close> is used by
     2.9    default.
    2.10  
    2.11    \<^emph>\<open>GTK+\<close> also works under the side-condition that the overall GTK theme
    2.12 @@ -310,7 +310,7 @@
    2.13    Users may experiment with different look-and-feels, but need to keep
    2.14    in mind that this extra variance of GUI functionality is unlikely to
    2.15    work in arbitrary combinations.  The platform-independent
    2.16 -  \<^emph>\<open>Nimbus\<close> and \<^emph>\<open>Metal\<close> should always work.  The historic
    2.17 +  \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close> should always work.  The historic
    2.18    \<^emph>\<open>CDE/Motif\<close> should be ignored.
    2.19  
    2.20    After changing the look-and-feel in \<^emph>\<open>Global Options~/
    2.21 @@ -353,7 +353,7 @@
    2.22  
    2.23    \<^item> \<^emph>\<open>Global Options / Appearance / Button, menu and label font\<close> as
    2.24    well as \<^emph>\<open>List and text field font\<close>: this specifies the primary and
    2.25 -  secondary font for the old \<^emph>\<open>Metal\<close> look-and-feel
    2.26 +  secondary font for the traditional \<^emph>\<open>Metal\<close> look-and-feel
    2.27    (\secref{sec:look-and-feel}), which happens to scale better than newer ones
    2.28    like \<^emph>\<open>Nimbus\<close>.
    2.29  
     3.1 --- a/src/Pure/GUI/gui.scala	Sat Oct 31 14:16:29 2015 +0100
     3.2 +++ b/src/Pure/GUI/gui.scala	Sat Oct 31 14:38:48 2015 +0100
     3.3 @@ -34,8 +34,7 @@
     3.4        if (Platform.is_windows || Platform.is_macos)
     3.5          UIManager.getSystemLookAndFeelClassName()
     3.6        else
     3.7 -        find_laf("Nimbus") getOrElse
     3.8 -          UIManager.getCrossPlatformLookAndFeelClassName()
     3.9 +        UIManager.getCrossPlatformLookAndFeelClassName()
    3.10      }
    3.11  
    3.12    def init_laf(): Unit = UIManager.setLookAndFeel(get_laf())
     4.1 --- a/src/Tools/jEdit/src/jEdit.props	Sat Oct 31 14:16:29 2015 +0100
     4.2 +++ b/src/Tools/jEdit/src/jEdit.props	Sat Oct 31 14:38:48 2015 +0100
     4.3 @@ -240,7 +240,7 @@
     4.4  line-end.shortcut=END
     4.5  line-home.shortcut=HOME
     4.6  logo.icon.medium=32x32/apps/isabelle.gif
     4.7 -lookAndFeel=javax.swing.plaf.nimbus.NimbusLookAndFeel
     4.8 +lookAndFeel=javax.swing.plaf.metal.MetalLookAndFeel
     4.9  match-bracket.shortcut2=C+9
    4.10  navigator.showOnToolbar=true
    4.11  next-bracket.shortcut2=C+e C+9