notes about old Java 8 font rendering for low-quality displays;
authorwenzelm
Sat, 06 Apr 2019 22:26:38 +0200
changeset 70256 b718a64d0d09
parent 70255 6b0e4ba2062c
child 70257 8df39b286ecb
child 70258 ee0b8e06b01c
notes about old Java 8 font rendering for low-quality displays;
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.