diff -r 0466bd194d74 -r 2925c5552e25 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Mon May 04 20:05:50 2015 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Mon May 04 20:16:19 2015 +0200
@@ -285,11 +285,14 @@
   \item[Linux:] The platform-independent \emph{Nimbus} is used by
   default.
 
-  \emph{GTK+} works under the side-condition that the overall GTK theme is
-  selected in a Swing-friendly way.\footnote{GTK support in Java/Swing was
-  once marketed aggressively by Sun, but never quite finished. Today (2013) it
+  \emph{GTK+} also works under the side-condition that the overall GTK theme
+  is selected in a Swing-friendly way.\footnote{GTK support in Java/Swing was
+  once marketed aggressively by Sun, but never quite finished. Today (2015) it
   is lagging behind further development of Swing and GTK. The graphics
-  rendering performance can be worse than for other Swing look-and-feels.}
+  rendering performance can be worse than for other Swing look-and-feels.
+  Nonetheless it has its uses for displays with very high resolution (such as
+  ``4K'' or ``UHD'' models), because the rendering by the external library is
+  subject to global system settings for font scaling.}
 
   \item[Windows:] Regular \emph{Windows} is used by default, but
   \emph{Windows Classic} also works.