# HG changeset patch
# User wenzelm
# Date 1554582398 -7200
# Node ID b718a64d0d09896b9258a14ea2ead0b0313e5929
# Parent  6b0e4ba2062c600f24aa288946daf7d5ce561f59
notes about old Java 8 font rendering for low-quality displays;

diff -r 6b0e4ba2062c -r b718a64d0d09 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Sat Apr 06 22:09:41 2019 +0200
+++ b/src/Doc/JEdit/JEdit.thy	Sat Apr 06 22:26:38 2019 +0200
@@ -2108,6 +2108,17 @@
 chapter \<open>Known problems and workarounds \label{sec:problems}\<close>
 
 text \<open>
+  \<^item> \<^bold>\<open>Problem:\<close> Font-rendering in Java 11 (OpenJDK) is worse than Java 8
+  (by Oracle) on low-quality displays.
+
+  \<^bold>\<open>Workaround:\<close> Find an old copy of Java 8 from Oracle (which has
+  ``end-of-live'' status since Jan-2019) and refer to its main directory via
+  @{setting "ISABELLE_JDK_HOME"}\<^verbatim>\<open>="..."\<close> in
+  \<^path>\<open>$ISABELLE_HOME_USER/etc/settings\<close>. Also add
+  \<^verbatim>\<open>isabelle_fonts_hints=false\<close> to
+  \<^path>\<open>$ISABELLE_HOME_USER/etc/preferences\<close> to avoid problems of the old
+  font renderer with hinting.
+
   \<^item> \<^bold>\<open>Problem:\<close> Keyboard shortcuts \<^verbatim>\<open>C+PLUS\<close> and \<^verbatim>\<open>C+MINUS\<close> for adjusting the
   editor font size depend on platform details and national keyboards.