src/Doc/JEdit/JEdit.thy
changeset 69343 395c4fb15ea2
parent 68737 a8bef9ff7dc0
child 69597 ff784d5a5bfb
--- a/src/Doc/JEdit/JEdit.thy	Sat Nov 24 16:41:18 2018 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Sat Nov 24 18:56:44 2018 +0100
@@ -525,21 +525,20 @@
 text \<open>Correct rendering via Unicode requires a font that contains glyphs for
   the corresponding codepoints. There are also various unusual symbols with
   particular purpose in Isabelle, e.g.\ control symbols and very long arrows.
-  Isabelle/jEdit prefers its own application fonts \<^verbatim>\<open>IsabelleText\<close>, which
-  ensures that standard collection of Isabelle symbols is actually shown on
-  the screen (or printer) as expected.
+  Isabelle/jEdit prefers its own font collection \<^verbatim>\<open>Isabelle DejaVu\<close>, which
+  ensures that all standard Isabelle symbols are shown on the screen (or
+  printer) as expected.
 
   Note that a Java/AWT/Swing application can load additional fonts only if
-  they are not installed on the operating system already! Some outdated
-  version of \<^verbatim>\<open>IsabelleText\<close> that happens to be provided by the operating
-  system would prevent Isabelle/jEdit to use its bundled version. This could
-  lead to missing glyphs (black rectangles), when the system version of
-  \<^verbatim>\<open>IsabelleText\<close> is older than the application version. This problem can be
-  avoided by refraining to ``install'' any version of \<^verbatim>\<open>IsabelleText\<close> in the
-  first place, although it might be tempting to use the same font in other
-  applications.
+  they are not installed on the operating system already! Outdated versions of
+  Isabelle fonts that happen to be provided by the operating system prevent
+  Isabelle/jEdit to use its bundled version. This could lead to missing glyphs
+  (black rectangles), when the system version of a font is older than the
+  application version. This problem can be avoided by refraining to
+  ``install'' any version of \<^verbatim>\<open>IsabelleText\<close> in the first place, although it
+  might be tempting to use the same font in other applications.
 
-  HTML pages generated by Isabelle refer to the same \<^verbatim>\<open>IsabelleText\<close> font as a
+  HTML pages generated by Isabelle refer to the same Isabelle fonts as a
   server-side resource. Thus a web-browser can use that without requiring a
   locally installed copy.
 \<close>
@@ -2141,7 +2140,7 @@
   \<^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.
+  \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>Isabelle DejaVu\<close> fonts.
 
   \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key
   event handling of Java/AWT/Swing.