equal
deleted
inserted
replaced
475 tooltips are stacking up. |
475 tooltips are stacking up. |
476 |
476 |
477 \medskip A black rectangle in the text indicates a hyperlink that |
477 \medskip A black rectangle in the text indicates a hyperlink that |
478 may be followed by a mouse click (while the @{verbatim CONTROL} or |
478 may be followed by a mouse click (while the @{verbatim CONTROL} or |
479 @{verbatim COMMAND} modifier key is still pressed). Presently |
479 @{verbatim COMMAND} modifier key is still pressed). Presently |
480 (Isabelle2013-1) there is no systematic navigation within the |
480 (Isabelle2013-2) there is no systematic navigation within the |
481 editor to return to the original location. |
481 editor to return to the original location. |
482 |
482 |
483 Also note that the link target may be a file that is itself not |
483 Also note that the link target may be a file that is itself not |
484 subject to formal document processing of the editor session and thus |
484 subject to formal document processing of the editor session and thus |
485 prevents further exploration: the chain of hyperlinks may end in |
485 prevents further exploration: the chain of hyperlinks may end in |
1107 \item \textbf{Problem:} Some Linux / X11 input methods such as IBus |
1107 \item \textbf{Problem:} Some Linux / X11 input methods such as IBus |
1108 tend to disrupt key event handling of Java/AWT/Swing. |
1108 tend to disrupt key event handling of Java/AWT/Swing. |
1109 |
1109 |
1110 \textbf{Workaround:} Do not use input methods, reset the environment |
1110 \textbf{Workaround:} Do not use input methods, reset the environment |
1111 variable @{verbatim XMODIFIERS} within Isabelle settings (default in |
1111 variable @{verbatim XMODIFIERS} within Isabelle settings (default in |
1112 Isabelle2013-1). |
1112 Isabelle2013-2). |
1113 |
1113 |
1114 \item \textbf{Problem:} Some Linux / X11 window managers that are |
1114 \item \textbf{Problem:} Some Linux / X11 window managers that are |
1115 not ``re-parenting'' cause problems with additional windows opened |
1115 not ``re-parenting'' cause problems with additional windows opened |
1116 by Java. This affects either historic or neo-minimalistic window |
1116 by Java. This affects either historic or neo-minimalistic window |
1117 managers like @{verbatim awesome} or @{verbatim xmonad}. |
1117 managers like @{verbatim awesome} or @{verbatim xmonad}. |