more on problems and workarounds;
Tue, 29 Oct 2013 19:45:55 +0100
changeset 54349 fd5ddf2bce76
parent 54348 923690bfb818
child 54350 b0cdb4b10d20
more on problems and workarounds;
--- 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.