more on GTK;
authorwenzelm
Mon May 04 20:16:19 2015 +0200 (2015-05-04)
changeset 602562925c5552e25
parent 60255 0466bd194d74
child 60257 9ed816c033c5
more on GTK;
src/Doc/JEdit/JEdit.thy
     1.1 --- a/src/Doc/JEdit/JEdit.thy	Mon May 04 20:05:50 2015 +0200
     1.2 +++ b/src/Doc/JEdit/JEdit.thy	Mon May 04 20:16:19 2015 +0200
     1.3 @@ -285,11 +285,14 @@
     1.4    \item[Linux:] The platform-independent \emph{Nimbus} is used by
     1.5    default.
     1.6  
     1.7 -  \emph{GTK+} works under the side-condition that the overall GTK theme is
     1.8 -  selected in a Swing-friendly way.\footnote{GTK support in Java/Swing was
     1.9 -  once marketed aggressively by Sun, but never quite finished. Today (2013) it
    1.10 +  \emph{GTK+} also works under the side-condition that the overall GTK theme
    1.11 +  is selected in a Swing-friendly way.\footnote{GTK support in Java/Swing was
    1.12 +  once marketed aggressively by Sun, but never quite finished. Today (2015) it
    1.13    is lagging behind further development of Swing and GTK. The graphics
    1.14 -  rendering performance can be worse than for other Swing look-and-feels.}
    1.15 +  rendering performance can be worse than for other Swing look-and-feels.
    1.16 +  Nonetheless it has its uses for displays with very high resolution (such as
    1.17 +  ``4K'' or ``UHD'' models), because the rendering by the external library is
    1.18 +  subject to global system settings for font scaling.}
    1.19  
    1.20    \item[Windows:] Regular \emph{Windows} is used by default, but
    1.21    \emph{Windows Classic} also works.