more on Mac OS X with Retina display;
Fri, 05 Feb 2016 10:21:38 +0100
changeset 62265 dfb70abaa3f0
parent 62264 340f98836fd9
child 62266 f4baefee5776
more on Mac OS X with Retina display;
--- 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.