# HG changeset patch # User wenzelm # Date 1381581465 -7200 # Node ID e0fa4bd16c80bc48852c1e4cc82c44ecb527a5aa # Parent ffa4e0b1701e353dd7a23ee21867f941f42bedbe misc tuning; diff -r ffa4e0b1701e -r e0fa4bd16c80 src/Doc/JEdit/JEdit.thy --- a/src/Doc/JEdit/JEdit.thy Sat Oct 12 00:10:07 2013 +0200 +++ b/src/Doc/JEdit/JEdit.thy Sat Oct 12 14:37:45 2013 +0200 @@ -15,42 +15,42 @@ document-oriented approach to \emph{continuous proof processing} \cite{Wenzel:2011:CICM,Wenzel:2012}. Many concepts and system components are fit together in order to make this work. The main - building blocks are as follows: + building blocks are as follows. \begin{description} - \item [PIDE] is a general framework for Prover IDEs based on the - Isabelle/Scala. It is built around a concept of asynchronous - document processing, which is supported natively by the parallel - proof engine that is implemented in Isabelle/ML. The prover - discontinues the traditional TTY-based command loop in favor of - direct editing of formal source text. + \item [PIDE] is a general framework for Prover IDEs based on + Isabelle/Scala. It is built around a concept of parallel and + asynchronous document processing, which is supported natively by the + parallel proof engine that is implemented in Isabelle/ML. The prover + discontinues the traditional TTY-based command loop, and supports + direct editing of formal source text with rich formal markup for GUI + rendering. \item [Isabelle/ML] is the implementation and extension language of Isabelle, see also \cite{isabelle-implementation}. It is integrated - into the formal logical context and allows to manipulate logical - entities directly. Arbitrary add-on tools may be implemented for - object-logics such as Isabelle/HOL. + into the logical context of Isabelle/Isar and allows to manipulate + logical entities directly. Arbitrary add-on tools may be implemented + for object-logics such as Isabelle/HOL. \item [Isabelle/Scala] is the system programming language of Isabelle. It extends the pure logical environment of Isabelle/ML towards the ``real world'' of graphical user interfaces, text editors, IDE frameworks, web services etc. Special infrastructure - allows to transfer algebraic datatypes and formatted text easily - between ML and Scala, using asynchronous protocol commands. + allows to transfer algebraic datatypes values and formatted text + easily between ML and Scala, using asynchronous protocol commands. - \item [jEdit] is a sophisticated text - editor\footnote{\url{http://www.jedit.org}} implemented in Java. It - is easily extensible by plugins written in languages that work on - the JVM, e.g.\ Scala\footnote{\url{http://www.scala-lang.org/}}. + \item [jEdit] is a sophisticated text editor implemented in + Java.\footnote{\url{http://www.jedit.org}} It is easily extensible + by plugins written in languages that work on the JVM, e.g.\ + Scala\footnote{\url{http://www.scala-lang.org/}}. \item [Isabelle/jEdit] is the main example application of the PIDE - framework and the default user-interface for Isabelle. It is - targeted at beginners and experts alike. Technically, Isabelle/jEdit - combines a slightly modified version of the official jEdit code base - with a special plugin for Isabelle, which is then integrated as - standalone application for the main operating system platforms: - Linux, Windows, Mac OS X. + framework and the default user-interface for Isabelle. It targets + both beginners and experts. Technically, Isabelle/jEdit combines a + slightly modified version of the official jEdit code base with a + special plugin for Isabelle, integrated as standalone application + for the main operating system platforms: Linux, Windows, Mac OS X. \end{description} @@ -89,12 +89,13 @@ CONTROL} (Linux, Windows) or @{verbatim COMMAND} (Mac OS X) exposes additional formal content via tooltips and/or hyperlinks. - \item Dockable windows (e.g.\ \emph{Output}, \emph{Symbols}) are - managed separately by jEdit, which also allows multiple instances. - \item Formal output (in popups etc.) may be explored recursively, using the same techniques as in the editor source buffer. + \item Additional panels (e.g.\ \emph{Output}, \emph{Symbols}) are + organized by the Dockable Window Manager of jEdit, which also allows + multiple floating instances of each window class. + \item The prover process and source files are managed on the editor side. The prover operates on timeless and stateless document content via Isabelle/Scala. @@ -119,10 +120,10 @@ \emph{User's Guide} and \emph{Frequently Asked Questions} for this sophisticated text editor. - Most of the information is relevant for Isabelle/jEdit as well, but - one needs to keep in mind that defaults sometimes differ, and the - official jEdit documentation does not know about the Isabelle plugin - with its bias towards theory editing. + Most of this information about jEdit is relevant for Isabelle/jEdit + as well, but one needs to keep in mind that defaults sometimes + differ, and the official jEdit documentation does not know about the + Isabelle plugin with its special support for theory editing. *} @@ -131,12 +132,12 @@ text {* The \emph{Plugin Manager} of jEdit allows to augment editor functionality by JVM modules (jars) that are provided by the central plugin repository, or one of various mirror sites. The main - \emph{Isabelle} plugin that is bundled with Isabelle/jEdit needs to - remain active at all times! A few additional plugins are bundled + \emph{Isabelle} plugin is an integral part of Isabelle/jEdit needs + to remain active at all times! A few additional plugins are bundled with Isabelle/jEdit for convenience or out of necessity, notably \emph{Console} with its Isabelle/Scala sub-plugin and - \emph{SideKick} with some Isabelle-specific parsers for tree - structure. + \emph{SideKick} with some Isabelle-specific parsers for document + tree structure. Connecting to the plugin server infrastructure of the jEdit project allows to update bundled plugins or to add further @@ -152,32 +153,33 @@ subsection {* Options *} -text {* jEdit and Isabelle have separate management of persistent - options. Regular jEdit options are accessible via the dialogs for - \emph{Global Options} and \emph{Plugin Options}. This results in an - environment of name-value properties that is stored within the +text {* Both jEdit and Isabelle have distinctive management of + persistent options. Regular jEdit options are accessible via the + dialogs for \emph{Global Options} and \emph{Plugin Options}. This + results in an environment of properties that is stored within the \emph{settings directory} of jEdit; see also the menu \emph{Utilities / Settings Directory}. - In contrast, Isabelle system options are managed by Isabelle/Scala; - see also \cite{isabelle-sys}, especially the coverage of Isabelle - sessions and build. Options that are declared as \textbf{public} - are exposed to the \emph{Plugin Options} dialog of jEdit in its - section \emph{Isabelle / General}. This provides a view on Isabelle - options and persistent preferences in @{verbatim - "$ISABELLE_HOME_USER/etc/preferences"}, independently of the jEdit - properties in its settings directory. - - Isabelle options are loaded once on startup and saved on shutdown. - Editing the machine-generated @{verbatim "etc/preferences"} manually - while the application is running is likely to cause a lost-update! + Isabelle system options are managed by Isabelle/Scala; see also + \cite{isabelle-sys}, especially the coverage of sessions and + command-line tools like @{tool build} or @{tool options}. Isabelle + options that are declared as \textbf{public} are exposed to the + jEdit \emph{Plugin Options} dialog, in its section \emph{Isabelle / + General}. This provides a view on Isabelle options and persistent + preferences in @{verbatim "$ISABELLE_HOME_USER/etc/preferences"}, + independently of the jEdit properties in its settings directory. Some Isabelle options that are accessible in the Isabelle/jEdit Plugin Options dialog affect general parameters that are relevant outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or @{system_option parallel_proofs} for the Isabelle build tool \cite{isabelle-sys}. -*} + + \medskip Options are loaded once on startup and saved on shutdown of + Isabelle/jEdit. Editing the machine-generated files @{verbatim + "$ISABELLE_HOME_USER/jedit/properties"} or @{verbatim + "$ISABELLE_HOME_USER/etc/preferences"} manually while the + application is running is likely to cause a lost-update! *} subsection {* Keymaps *} @@ -191,30 +193,31 @@ This is relevant for Isabelle/jEdit due to various fine-tuning of default properties, and additional keyboard shortcuts for Isabelle specific functionality. Users may change their keymap later on, but - may need to copy important key bindings manually. + may need to copy Isabelle-specific key bindings manually. *} subsection {* Look-and-feel *} text {* jEdit is a Java/Swing application with some ambition to - support ``native'' platform look-and-feel, within the limits of what - Oracle as Java provider and major operating system vendors and - distributors allow. + support ``native'' look-and-feel on all platforms, within the limits + of what Oracle as Java provider and major operating system vendors + and distributors allow (see also \secref{sec:problems}). - Isabelle/jEdit uses platform-specific look-and-feel as follows: + Isabelle/jEdit enables platform-specific look-and-feel by default as + follows. \begin{description} \item[Linux] The platform-independent \emph{Nimbus} is used by default, but the classic \emph{Metal} also works. \emph{GTK+} works under the side-condition that the overall GTK theme is selected in a - Java/Swing friendly way: the success rate is @{text "\"} 50\%. + Java/Swing friendly way. \item[Windows] Regular \emph{Windows} is used by default, but platform-independent \emph{Nimbus} and \emph{Metal} also work. - \item[Mac OS X] standard \emph{Apple Aqua} is used by default. + \item[Mac OS X] Standard \emph{Apple Aqua} is used by default. Moreover the bundled \emph{MacOSX} plugin provides various functions that are expected from applications on that particular platform: quit from menu or dock, preferences menu, drag-and-drop of text @@ -224,11 +227,9 @@ \end{description} Users may experiment with different look-and-feels, but need to keep - in mind that this extra dimension of GUI functionality is unlikely - to work in arbitrary combinations. The \emph{GTK+} look-and-feel is + in mind that this extra variance of GUI functionality is unlikely to + work in arbitrary combinations. The \emph{GTK+} look-and-feel is particularly critical due to its additional dimension of ``themes''. - It is also important to ensure that the fonts of standard GUI - components use anti-aliasing as usual. After changing the look-and-feel in \emph{Global Options / Appearance}, it is advisable to restart Isabelle/jEdit in order to @@ -242,48 +243,35 @@ text {* jEdit maintains a collection of open \emph{text buffers} to store source files. Each buffer may be associated with any number - of \emph{text areas} as visible GUI representation of the content. - - Buffers are subject to a \emph{mode} that is determined from the - file type. Files with extension \texttt{.thy} are assigned to the - mode \emph{isabelle} and treated specifically as follows. - - \begin{itemize} + of visible \emph{text areas}. Buffers are subject to an + \emph{editor mode} that is determined from the file type. Files + with extension \texttt{.thy} are assigned to the mode + \emph{isabelle} and treated specifically. - \item Theory files are implicitly added to the formal document model - of Isabelle/jEdit, which maintains a family of versions of all - sources for the prover in the background. The \emph{Theories} panel + \medskip Isabelle theory files are automatically added to the formal + document model of Isabelle/Scala, which maintains a family of + versions of all sources for the prover. The \emph{Theories} panel provides an overview of the status of continuous checking of theory - sources. Unlike batch sessions \cite{isabelle-sys}, full theory - file names are used to identify theory nodes; this allows to - experiment with multiple (disjoint) Isabelle sessions - simultaneously. + sources. Unlike batch sessions \cite{isabelle-sys}, theory nodes + are identified by full path names; this allows to work with multiple + (disjoint) Isabelle sessions simultaneously within the same editor + session. - \item Certain events to open or update buffers containing theory - files cause Isabelle/jEdit to resolve dependencies of \emph{theory - imports}. The system will request to load further files into jEdit - editor buffers, which will eventually be added to the theory - document model for further checking. It is also possible to resolve - dependencies automatically, depending on the option @{system_option - jedit_auto_load}. + Certain events to open or update buffers with theory files cause + Isabelle/jEdit to resolve dependencies of \emph{theory imports}. + The system requests to load further files into jEdit editor buffers, + to be added to the theory document model for further checking. It + is also possible to resolve dependencies automatically, depending on + the option @{system_option jedit_auto_load}. - \item Physical rendering of jEdit buffer content within the visible - text areas is augmented by information from the formal document - model. Thus the prover can provide additional markup to help the - user understanding the meaning of the text, and to produce more text - with some add-on tools (e.g.\ information messages produced by - automated provers or disprovers in the background). - - \end{itemize} + \medskip The open text area views on theory buffers define the + visible \emph{perspective} of Isabelle/jEdit. This is taken as a + hint for document processing: the prover ensures that those parts of + a theory where the user is looking are checked, while other parts + that are presently not required are ignored. - The text area views on theory buffers define the visible part of the - \emph{perspective} of Isabelle/jEdit. This is taken as a hint for - document processing: the prover will ensure that those parts of a - theory where the user is looking are checked, while invisible parts - that are presently not required are left alone. - - The perspective can may changed by opening or closing text areas, or - scrolling the corresponding windows. It is also possible to + The perspective can be changed by opening or closing text areas + windows, or scrolling within some window. It is also possible to indicate theory nodes as \emph{required} for continuous checking in the \emph{Theories} panel. This means such nodes and all their imports are always processed, independently of the visibility @@ -292,14 +280,18 @@ \medskip Formal markup of checked theory content is turned into GUI rendering, based on a standard repertoire known from IDEs for programming languages: colors, icons, highlighting, squiggly - underline, tooltips, hyperlinks etc. There is some traditional - syntax-highlighting for the outer syntax of Isabelle/Isar, based on - static keyword tables. The coloring of inner syntax (term language - etc.) is based on dynamic information from the logical context of - the prover. + underline, tooltips, hyperlinks etc. For outer syntax of + Isabelle/Isar there is some traditional syntax-highlighting, based + on static keyword tables and tokenization within the editor. In + contrast, the painting of inner syntax (term language etc.) is + based on semantic information that is reported dynamically from the + logical context. Thus the prover can provide additional markup to + help the user understanding the meaning of the text, and to produce + more text with some add-on tools (e.g.\ information messages by + automated provers or disprovers running in the background). Such formally annotated text can be explored further by using the - @{verbatim CONTROL} modifier key on Linux or Windows, and @{verbatim + @{verbatim CONTROL} modifier key on Linux and Windows, or @{verbatim COMMAND} on Mac OS X. Hovering with the mouse while the modifier is pressed reveals \emph{tooltips} (grey box within the text with a yellow popup) and/or \emph{hyperlinks} (dark grey rectangle within @@ -315,48 +307,24 @@ text {* Isabelle sources consist of \emph{symbols} that extend plain ASCII and UTF-8 (for informal text) to allow infinitely many - mathematical symbols, without depending on particular encodings. + mathematical symbols within the formal sources. This works without + depending on particular encodings or varying Unicode standards + \cite{Wenzel:2011:CICM}. For the prover back-end, formal text consists of ASCII characters that are grouped according to some simple rules, e.g.\ as plain ``@{verbatim a}'' or symbolic ``@{verbatim "\"}''. - For the editor front-end, some well-known symbols are rendered as + For the editor front-end, a certain subset of symbols is rendered as Unicode glyphs, in order to show ``@{verbatim "\"}'' as actual ``@{text "\"}''. This symbol interpretation is specified by the Isabelle system distribution (in @{file - "$ISABELLE_HOME/etc/symbols"}) or the user (in @{verbatim + "$ISABELLE_HOME/etc/symbols"}) or by the user (in @{verbatim "$ISABELLE_HOME_USER/etc/symbols"}). - \medskip The appendix of \cite{isabelle-isar-ref} gives an overview - of the standard interpretation of finitely many symbols from the - infinite collection. Uninterpreted symbols are shown literally. - For example: - - \medskip - \begin{tabular}{l} - @{text "\"}, @{text "\"}, @{text "\"}, @{text "\"} \\ - @{text "\"}, @{text "\"}, @{text "\"}, @{text "\"}, @{text "\"}, @{text "\"}, @{text "\"} \\ - @{text "\"}, @{text "\"}, @{text "\"}, @{text "\"}, @{text "\"} \\ - @{text "\"}, @{text "\"}, @{text "\"}, @{text "\"} \\ - @{verbatim "\"}, @{verbatim "\"}, @{verbatim "\"}, @{text "\"} \\ - \end{tabular} - \medskip - - Correct rendering via Unicode requires a font that contains glyphs - for the corresponding codepoints. Many standard fonts lack that, so - Isabelle/jEdit uses the @{verbatim IsabelleText} by default, which - ensures that standard collection of Isabelle symbols are actually - seen on the screen (or printer). - - Note that a Java/Swing application can load additional fonts from - the file-system only if they are not installed as system font - already! This means an old version of @{verbatim IsabelleText} that - happens to be already present will prevent Isabelle/jEdit from using - its current bundled version. This might result in missing glyphs - (black rectangles), since @{verbatim IsabelleText} is occasionally - improved in its coverage over time. De-facto there is no need to - ``install'' that font on the system in the first place. + The appendix of \cite{isabelle-isar-ref} gives an overview of the + standard interpretation of finitely many symbols from the infinite + collection. Uninterpreted symbols are shown literally. \medskip Technically, the Unicode view on Isabelle symbols is an \emph{encoding} in Isabelle/jEdit, which is called @{verbatim @@ -369,16 +337,33 @@ UTF-8-Isabelle} helps to resolve such problems, potentially after repairing malformed parts of the text. + \medskip Correct rendering via Unicode requires a font that contains + glyphs for the corresponding codepoints. Most system fonts lack + that, so Isabelle/jEdit prefers its own application font @{verbatim + IsabelleText} by default, which ensures that standard collection of + Isabelle symbols are actually seen on the screen (or printer). + + Note that a Java/Swing application can load additional fonts only if + they are not installed as system font already! This means some old + version of @{verbatim IsabelleText} that happens to be already + present prevents Isabelle/jEdit from using its current bundled + version. This might result in missing glyphs (black rectangles), + since obsolete versions of @{verbatim IsabelleText} lack recent + improvements of Unicode glyph coverage. This problem can be avoided + by refraining to ``install'' any version of @{verbatim IsabelleText} + in the first place. + \medskip \paragraph{Input methods.} In principle, Isabelle/jEdit could delegate the problem to produce Isabelle symbols in their Unicode rendering to the underlying operating system and its - \emph{input methods}; jEdit also provides various ways to work with - \emph{abbreviations} to produce certain non-ASCII characters. Since - mathematical characters are far from mainstream use, various - specific Isabelle/jEdit input methods are required. + \emph{input methods}. Regular jEdit also provides various ways to + work with \emph{abbreviations} to produce certain non-ASCII + characters. Since none of these standard input methods work + satisfactorily for the mathematical characters required for + Isabelle, various specific Isabelle/jEdit mechanisms are provided. - Here are some practically relevant input methods for Isabelle - symbols: + Here is a summary for practically relevant input methods for + Isabelle symbols. \begin{enumerate} @@ -390,28 +375,28 @@ \item Copy / paste from decoded source files: text that is rendered as Unicode already may get re-used to produce further such text. This also works between different applications, e.g.\ Isabelle/jEdit - and some web browser, as long as the same Unicode view on actual - Isabelle symbols is used. + and some web browser or mail client, as long as the same Unicode + view on Isabelle symbols is used uniformly. - \item Copy / paste from prover output within Isabelle/jEdit: the - same principles as for text buffers apply. Note that copy in - Isabelle \emph{Output} works via the keyboard shortcut @{verbatim - "C+v"}, not the jEdit menu (which refers to the main text area). + \item Copy / paste from prover output within Isabelle/jEdit. The + same principles as for text buffers apply, but note that \emph{copy} + in Isabelle \emph{Output} works via the keyboard shortcut @{verbatim + "C+c"}, not the jEdit menu. \item Completion provided by Isabelle plugin (see \secref{sec:completion}). Isabelle symbols have a canonical name and optional abbreviations. This can be used with the text completion mechanism of Isabelle/jEdit, to replace a prefix of the - actual symbol @{verbatim "\"}, or its backslashed name @{verbatim - "\\"}@{verbatim "lambda"}, or its ASCII abbreviation @{verbatim - "%"}. + actual symbol like @{verbatim "\"}, or its backslashed name + @{verbatim "\\"}@{verbatim "lambda"}, or its ASCII abbreviation + @{verbatim "%"}. The following table is an extract of the information provided by the - standard @{verbatim "etc/symbols"} file: + standard @{file "$ISABELLE_HOME/etc/symbols"} file: \medskip \begin{tabular}{lll} - \textbf{symbol} & \textbf{abbreviation} & \textbf{backslash escape} \\\hline + \textbf{symbol} & \textbf{abbreviation} & \textbf{backslashed name} \\\hline @{text "\"} & @{verbatim "%"} & @{verbatim "\\lambda"} \\ @{text "\"} & @{verbatim "=>"} & @{verbatim "\\Rightarrow"} \\ @{text "\"} & @{verbatim "==>"} & @{verbatim "\\Longrightarrow"} \\ @@ -429,33 +414,28 @@ @{text "\"} & @{verbatim ":"} & @{verbatim "\\in"} \\ @{text "\"} & @{verbatim "~:"} & @{verbatim "\\notin"} \\ \end{tabular} + \medskip + + Note that the above abbreviations refer to the input method. The + logical notation provides ASCII alternatives that often coincide, + but deviate occasionally. Writing formal sources directly with + ASCII replacement notation like @{verbatim "!"} or @{verbatim "ALL"} + or @{verbatim "-->"} is considered very old fashioned in 2013! \end{enumerate} - Some further notes on symbol completion: - - \begin{itemize} - - \item The above abbreviations refer to the input method. The logical - notation provides ASCII alternatives that often coincide, but - deviate occasionally. - - \item Generic jEdit abbreviations or plugins perform similar source - replacement operations; this works for Isabelle as long as the - Unicode sequences coincide with the symbol mapping. - - \item Raw Unicode characters within prover source files should be + Raw Unicode characters within prover source files should be restricted to informal parts, e.g.\ to write text in non-latin alphabets. Mathematical symbols should be defined via the official rendering tables, to avoid problems with portability and longterm storage of formal text. - \end{itemize} - \paragraph{Control symbols.} There are some special control symbols - to modify the style of a \emph{single} symbol (without - nesting). Control symbols may be applied to a region of selected - text, either using the \emph{Symbols} panel or keyboard shortcuts. + to modify the style of a single symbol (without nesting). Control + symbols may be applied to a region of selected text, either using + the \emph{Symbols} panel or keyboard shortcuts; these editor + operations produce a separate control symbol for each symbol in the + text. \medskip \begin{tabular}{lll} @@ -507,18 +487,11 @@ *} -chapter {* Known problems and workarounds *} +chapter {* Known problems and workarounds \label{sec:problems} *} text {* \begin{itemize} - \item \textbf{Problem:} Keyboard shortcuts @{verbatim "C+PLUS"} and - @{verbatim "C+MINUS"} for adjusting the editor font size depend on - platform details and national keyboards. - - \textbf{Workaround:} Use numeric keypad or rebind keys in the - jEdit Shortcuts options dialog. - \item \textbf{Problem:} Lack of dependency management for auxiliary files that contribute to a theory (e.g.\ @{command ML_file}). @@ -532,28 +505,8 @@ \item \textbf{Problem:} No way to delete document nodes from the overall collection of theories. - \textbf{Workaround:} Restart whole Isabelle/jEdit session in worst-case - situation. - - \item \textbf{Problem:} Linux: some desktop environments with extreme - animation effects may disrupt Java 7 window placement and/or keyboard - focus. - - \textbf{Workaround:} Disable such effects. - - \item \textbf{Problem:} Linux: some X11 input methods such as IBus tend - to disrupt key event handling of Java/Swing. - - \textbf{Workaround:} Do not use input methods, reset the environment - variable @{verbatim XMODIFIERS} within Isabelle settings (default in - Isabelle2013-1). - - \item \textbf{Problem:} Linux: some X11 window managers that are not - ``re-parenting'' cause problems with additional windows opened by the Java - VM. This affects either historic or neo-minimalistic window managers like - ``@{verbatim awesome}'' or ``@{verbatim xmonad}''. - - \textbf{Workaround:} Use regular re-parenting window manager. + \textbf{Workaround:} Ignore unused files. Restart whole + Isabelle/jEdit session in worst-case situation. \item \textbf{Problem:} The Mac OS X keyboard shortcut @{verbatim "COMMAND+COMMA"} for Preferences is in conflict with the jEdit default @@ -562,11 +515,32 @@ \textbf{Workaround:} Remap in jEdit manually according to national keyboard, e.g.\ @{verbatim "COMMAND+SLASH"} on English ones. - \item \textbf{Problem:} Mac OS X: Java 7 is officially supported on Lion - and Mountain Lion, but not Snow Leopard. It usually works on the latter, - although with a small risk of instabilities. + \item \textbf{Problem:} Keyboard shortcuts @{verbatim "C+PLUS"} and + @{verbatim "C+MINUS"} for adjusting the editor font size depend on + platform details and national keyboards. + + \textbf{Workaround:} Use numeric keypad or rebind keys in the + jEdit Shortcuts options dialog. + + \item \textbf{Problem:} Some Linux / X11 input methods such as IBus + tend to disrupt key event handling of Java/Swing. - \textbf{Workaround:} Update to OS X Mountain Lion, or later. + \textbf{Workaround:} Do not use input methods, reset the environment + variable @{verbatim XMODIFIERS} within Isabelle settings (default in + Isabelle2013-1). + + \item \textbf{Problem:} Some Linux / X11 window managers that are + not ``re-parenting'' cause problems with additional windows opened + by the Java VM. This affects either historic or neo-minimalistic + window managers like @{verbatim awesome} or @{verbatim xmonad}. + + \textbf{Workaround:} Use regular re-parenting window manager. + + \item \textbf{Problem:} Recent forks of Linux / X11 window managers + and desktop environments (variants of Gnome) disrupt the handling of + menu popups and mouse positions of Java/AWT/Swing. + + \textbf{Workaround:} Use mainstream versions of Linux desktops. \end{itemize} *}