# HG changeset patch
# User wenzelm
# Date 1454664098 -3600
# Node ID dfb70abaa3f07f70b70cb2e3c4f659b7f93ba278
# Parent  340f98836fd9503527d85ec984f4249bcb0fd0ff
more on Mac OS X with Retina display;

diff -r 340f98836fd9 -r dfb70abaa3f0 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Thu Feb 04 21:53:06 2016 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Fri Feb 05 10:21:38 2016 +0100
@@ -1995,8 +1995,16 @@
   \<^item> \<^bold>\<open>Problem:\<close> Mac OS X system fonts sometimes lead to character drop-outs in
   the main text area.
 
-  \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>IsabelleText\<close> font. (Do not install that
-  font on the system.)
+  \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>IsabelleText\<close> font.
+
+  \<^item> \<^bold>\<open>Problem:\<close> Mac OS X with Retina display has problems to determine the
+  font metrics of \<^verbatim>\<open>IsabelleText\<close> accurately, notably in plain Swing text
+  fields (e.g.\ in the \<^emph>\<open>Search and Replace\<close> dialog).
+
+  \<^bold>\<open>Workaround:\<close> Install \<^verbatim>\<open>IsabelleText\<close> and \<^verbatim>\<open>IsabelleTextBold\<close> on the system
+  with \<^emph>\<open>Font Book\<close>, despite the warnings in \secref{sec:symbols} against
+  that! The \<^verbatim>\<open>.ttf\<close> font files reside in some directory @{file_unchecked
+  "$ISABELLE_HOME/contrib/isabelle_fonts-XYZ"}.
 
   \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key
   event handling of Java/AWT/Swing.