# 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} *}