# HG changeset patch
# User wenzelm
# Date 1383072355 -3600
# Node ID fd5ddf2bce76e35162cdcd87f46c4ef121316939
# Parent  923690bfb81853fc87923de7faaa0a0cf79083cb
more on problems and workarounds;

diff -r 923690bfb818 -r fd5ddf2bce76 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Tue Oct 29 18:20:20 2013 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Tue Oct 29 19:45:55 2013 +0100
@@ -543,12 +543,19 @@
   jEdit Shortcuts options dialog.
 
   \item \textbf{Problem:} The Mac OS X keyboard shortcut @{verbatim
-  "COMMAND+COMMA"} for Preferences is in conflict with the jEdit default
-  binding for @{verbatim "quick-search"}.
+  "COMMAND+COMMA"} for application \emph{Preferences} is in conflict
+  with the jEdit default shortcut for \emph{Incremental Search Bar}
+  (action @{verbatim "quick-search"}).
 
   \textbf{Workaround:} Remap in jEdit manually according to national
   keyboard, e.g.\ @{verbatim "COMMAND+SLASH"} on English ones.
 
+  \item \textbf{Problem:} Mac OS X system fonts sometimes lead to
+  character drop-outs in the main text area.
+
+  \textbf{Workaround:} Use the default @{verbatim IsabelleText} font.
+  (Do not install that font on the system.)
+
   \item \textbf{Problem:} Some Linux / X11 input methods such as IBus
   tend to disrupt key event handling of Java/AWT/Swing.
 
@@ -569,6 +576,19 @@
 
   \textbf{Workaround:} Use mainstream versions of Linux desktops.
 
+  \item \textbf{Problem:} Full-screen mode via jEdit action @{verbatim
+  "toggle-full-screen"} (default shortcut @{verbatim F11}) works on
+  Windows, but not on Mac OS X or various Linux / X11 window managers.
+
+  \textbf{Workaround:} Use native full-screen control of the window
+  manager, if available (notably on Mac OS X).
+
+  \item \textbf{Problem:} Full-screen mode and dockable windows in
+  \emph{floating} state may lead to confusion about window placement
+  (depending on platform characteristics).
+
+  \textbf{Workaround:} Avoid this combination.
+
   \end{itemize}
 *}