src/Doc/JEdit/JEdit.thy
changeset 69343 395c4fb15ea2
parent 68737 a8bef9ff7dc0
child 69597 ff784d5a5bfb
equal deleted inserted replaced
69342:fa981730b964 69343:395c4fb15ea2
   523 
   523 
   524 paragraph \<open>Font.\<close>
   524 paragraph \<open>Font.\<close>
   525 text \<open>Correct rendering via Unicode requires a font that contains glyphs for
   525 text \<open>Correct rendering via Unicode requires a font that contains glyphs for
   526   the corresponding codepoints. There are also various unusual symbols with
   526   the corresponding codepoints. There are also various unusual symbols with
   527   particular purpose in Isabelle, e.g.\ control symbols and very long arrows.
   527   particular purpose in Isabelle, e.g.\ control symbols and very long arrows.
   528   Isabelle/jEdit prefers its own application fonts \<^verbatim>\<open>IsabelleText\<close>, which
   528   Isabelle/jEdit prefers its own font collection \<^verbatim>\<open>Isabelle DejaVu\<close>, which
   529   ensures that standard collection of Isabelle symbols is actually shown on
   529   ensures that all standard Isabelle symbols are shown on the screen (or
   530   the screen (or printer) as expected.
   530   printer) as expected.
   531 
   531 
   532   Note that a Java/AWT/Swing application can load additional fonts only if
   532   Note that a Java/AWT/Swing application can load additional fonts only if
   533   they are not installed on the operating system already! Some outdated
   533   they are not installed on the operating system already! Outdated versions of
   534   version of \<^verbatim>\<open>IsabelleText\<close> that happens to be provided by the operating
   534   Isabelle fonts that happen to be provided by the operating system prevent
   535   system would prevent Isabelle/jEdit to use its bundled version. This could
   535   Isabelle/jEdit to use its bundled version. This could lead to missing glyphs
   536   lead to missing glyphs (black rectangles), when the system version of
   536   (black rectangles), when the system version of a font is older than the
   537   \<^verbatim>\<open>IsabelleText\<close> is older than the application version. This problem can be
   537   application version. This problem can be avoided by refraining to
   538   avoided by refraining to ``install'' any version of \<^verbatim>\<open>IsabelleText\<close> in the
   538   ``install'' any version of \<^verbatim>\<open>IsabelleText\<close> in the first place, although it
   539   first place, although it might be tempting to use the same font in other
   539   might be tempting to use the same font in other applications.
   540   applications.
   540 
   541 
   541   HTML pages generated by Isabelle refer to the same Isabelle fonts as a
   542   HTML pages generated by Isabelle refer to the same \<^verbatim>\<open>IsabelleText\<close> font as a
       
   543   server-side resource. Thus a web-browser can use that without requiring a
   542   server-side resource. Thus a web-browser can use that without requiring a
   544   locally installed copy.
   543   locally installed copy.
   545 \<close>
   544 \<close>
   546 
   545 
   547 paragraph \<open>Input methods.\<close>
   546 paragraph \<open>Input methods.\<close>
  2139   \<^verbatim>\<open>-Dapple.laf.useScreenMenuBar=false\<close>.
  2138   \<^verbatim>\<open>-Dapple.laf.useScreenMenuBar=false\<close>.
  2140 
  2139 
  2141   \<^item> \<^bold>\<open>Problem:\<close> Mac OS X system fonts sometimes lead to character drop-outs in
  2140   \<^item> \<^bold>\<open>Problem:\<close> Mac OS X system fonts sometimes lead to character drop-outs in
  2142   the main text area.
  2141   the main text area.
  2143 
  2142 
  2144   \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>IsabelleText\<close> font.
  2143   \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>Isabelle DejaVu\<close> fonts.
  2145 
  2144 
  2146   \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key
  2145   \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key
  2147   event handling of Java/AWT/Swing.
  2146   event handling of Java/AWT/Swing.
  2148 
  2147 
  2149   \<^bold>\<open>Workaround:\<close> Do not use X11 input methods. Note that environment variable
  2148   \<^bold>\<open>Workaround:\<close> Do not use X11 input methods. Note that environment variable