src/Doc/JEdit/JEdit.thy
changeset 54643 57aefb80b639
parent 54639 5adc68deb322
child 54655 9e8189a841f7
equal deleted inserted replaced
54642:bf2519f2bd01 54643:57aefb80b639
   225 
   225 
   226   \emph{GTK+} works under the side-condition that the overall GTK
   226   \emph{GTK+} works under the side-condition that the overall GTK
   227   theme is selected in a Swing-friendly way.\footnote{GTK support in
   227   theme is selected in a Swing-friendly way.\footnote{GTK support in
   228   Java/Swing was once marketed aggressively by Sun, but never quite
   228   Java/Swing was once marketed aggressively by Sun, but never quite
   229   finished, and is today (2013) lagging a bit behind further
   229   finished, and is today (2013) lagging a bit behind further
   230   development of Swing and GTK.}
   230   development of Swing and GTK.  The graphics rendering performance
       
   231   can be worse than for other Swing look-and-feels.}
   231 
   232 
   232   \item[Windows] Regular \emph{Windows} is used by default, but
   233   \item[Windows] Regular \emph{Windows} is used by default, but
   233   \emph{Windows Classic} also works.
   234   \emph{Windows Classic} also works.
   234 
   235 
   235   \item[Mac OS X] Regular \emph{Mac OS X} is used by default.
   236   \item[Mac OS X] Regular \emph{Mac OS X} is used by default.