1 (*:wrap=hard:maxLineLen=78:*)
7 chapter {* Introduction *}
9 section {* Concepts and terminology *}
11 text {* Isabelle/jEdit is a Prover IDE that integrates \emph{parallel
12 proof checking} \cite{Wenzel:2009,Wenzel:2013:ITP} with
13 \emph{asynchronous user interaction}
14 \cite{Wenzel:2010,Wenzel:2012:UITP-EPTCS}, based on a
15 document-oriented approach to \emph{continuous proof processing}
16 \cite{Wenzel:2011:CICM,Wenzel:2012}. Many concepts and system
17 components are fit together in order to make this work. The main
18 building blocks are as follows.
22 \item [PIDE] is a general framework for Prover IDEs based on
23 Isabelle/Scala. It is built around a concept of parallel and
24 asynchronous document processing, which is supported natively by the
25 parallel proof engine that is implemented in Isabelle/ML. The prover
26 discontinues the traditional TTY-based command loop, and supports
27 direct editing of formal source text with rich formal markup for GUI
30 \item [Isabelle/ML] is the implementation and extension language of
31 Isabelle, see also \cite{isabelle-implementation}. It is integrated
32 into the logical context of Isabelle/Isar and allows to manipulate
33 logical entities directly. Arbitrary add-on tools may be implemented
34 for object-logics such as Isabelle/HOL.
36 \item [Isabelle/Scala] is the system programming language of
37 Isabelle. It extends the pure logical environment of Isabelle/ML
38 towards the ``real world'' of graphical user interfaces, text
39 editors, IDE frameworks, web services etc. Special infrastructure
40 allows to transfer algebraic datatype values and formatted text
41 easily between ML and Scala, using asynchronous protocol commands.
43 \item [jEdit] is a sophisticated text editor implemented in
44 Java.\footnote{\url{http://www.jedit.org}} It is easily extensible
45 by plugins written in languages that work on the JVM, e.g.\
46 Scala\footnote{\url{http://www.scala-lang.org/}}.
48 \item [Isabelle/jEdit] is the main example application of the PIDE
49 framework and the default user-interface for Isabelle. It targets
50 both beginners and experts. Technically, Isabelle/jEdit combines a
51 slightly modified version of the official jEdit code base with a
52 special plugin for Isabelle, integrated as standalone application
53 for the main operating system platforms: Linux, Windows, Mac OS X.
57 The subtle differences of Isabelle/ML versus Standard ML,
58 Isabelle/Scala versus Scala, Isabelle/jEdit versus jEdit need to be
59 taken into account when discussing any of these PIDE building blocks
60 in public forums, mailing lists, or even scientific publications.
64 section {* The Isabelle/jEdit Prover IDE *}
69 \includegraphics[width=\textwidth]{isabelle-jedit}
71 \caption{The Isabelle/jEdit Prover IDE}
74 Isabelle/jEdit consists of some plugins for the well-known jEdit
75 text editor \url{http://www.jedit.org}, according to the following
80 \item The original jEdit look-and-feel is generally preserved,
81 although some default properties are changed to accommodate Isabelle
82 (e.g.\ the text area font).
84 \item Formal Isabelle/Isar text is checked asynchronously while
85 editing. The user is in full command of the editor, and the prover
86 refrains from locking portions of the buffer.
88 \item Prover feedback works via colors, boxes, squiggly underline,
89 hyperlinks, popup windows, icons, clickable output --- all based on
90 semantic markup produced by Isabelle in the background.
92 \item Using the mouse together with the modifier key @{verbatim
93 CONTROL} (Linux, Windows) or @{verbatim COMMAND} (Mac OS X) exposes
94 additional formal content via tooltips and/or hyperlinks.
96 \item Formal output (in popups etc.) may be explored recursively,
97 using the same techniques as in the editor source buffer.
99 \item Additional panels (e.g.\ \emph{Output}, \emph{Symbols}) are
100 organized by the Dockable Window Manager of jEdit, which also allows
101 multiple floating instances of each window class.
103 \item The prover process and source files are managed on the editor
104 side. The prover operates on timeless and stateless document
105 content as provided via Isabelle/Scala.
107 \item Plugin options of jEdit (for the \emph{Isabelle} plugin) give
108 access to a selection of Isabelle/Scala options and its persistent
109 preferences, usually with immediate effect on the prover back-end or
112 \item The logic image of the prover session may be specified within
113 Isabelle/jEdit. The new image is provided automatically by the
114 Isabelle build tool after restart of the application.
120 subsection {* Documentation *}
122 text {* Regular jEdit documentation is accessible via its @{verbatim
123 Help} menu or @{verbatim F1} keyboard shortcut. This includes a full
124 \emph{User's Guide} and \emph{Frequently Asked Questions} for this
125 sophisticated text editor.
127 Most of this information about jEdit is relevant for Isabelle/jEdit
128 as well, but one needs to keep in mind that defaults sometimes
129 differ, and the official jEdit documentation does not know about the
130 Isabelle plugin with its special support for theory editing.
134 subsection {* Plugins *}
136 text {* The \emph{Plugin Manager} of jEdit allows to augment editor
137 functionality by JVM modules (jars) that are provided by the central
138 plugin repository, which is accessible by various mirror sites.
140 Connecting to the plugin server infrastructure of the jEdit project
141 allows to update bundled plugins or to add further functionality.
142 This needs to be done with the usual care for such an open bazaar of
143 contributions. Arbitrary combinations of add-on features are apt to
144 cause problems. It is advisable to start with the default
145 configuration of Isabelle/jEdit and develop some understanding how
146 it is supposed to work, before loading additional plugins at a grand
149 \medskip The main \emph{Isabelle} plugin is an integral part of
150 Isabelle/jEdit and needs to remain active at all times! A few
151 additional plugins are bundled with Isabelle/jEdit for convenience
152 or out of necessity, notably \emph{Console} with its Isabelle/Scala
153 sub-plugin and \emph{SideKick} with some Isabelle-specific parsers
154 for document tree structure. The \emph{ErrorList} plugin is
155 required by \emph{SideKick}, but not used specifically in
159 subsection {* Options *}
161 text {* Both jEdit and Isabelle have distinctive management of
164 Regular jEdit options are accessible via the dialogs for
165 \emph{Global Options} and \emph{Plugin Options}. Changed properties
166 are stored eventually in @{verbatim
167 "$ISABELLE_HOME_USER/jedit/properties"}. In contrast, Isabelle
168 system options are managed by Isabelle/Scala and changes stored in
169 @{verbatim "$ISABELLE_HOME_USER/etc/preferences"}, independently of
170 the jEdit properties. See also \cite{isabelle-sys}, especially the
171 coverage of sessions and command-line tools like @{tool build} or
174 Those Isabelle options that are declared as \textbf{public} are
175 configurable in jEdit via \emph{Plugin Options / Isabelle /
176 General}. Moreover, there are various options for rendering of
177 document content, which are configurable via \emph{Plugin Options /
178 Isabelle / Rendering}. Thus \emph{Plugin Options / Isabelle} in
179 jEdit provides a view on certain Isabelle options. Note that some
180 of these options affect general parameters that are relevant outside
181 Isabelle/jEdit as well, e.g.\ @{system_option threads} or
182 @{system_option parallel_proofs} for the Isabelle build tool
185 \medskip All options are loaded on startup and saved on shutdown of
186 Isabelle/jEdit. Editing the machine-generated files @{verbatim
187 "$ISABELLE_HOME_USER/jedit/properties"} or @{verbatim
188 "$ISABELLE_HOME_USER/etc/preferences"} manually while the
189 application is running is likely to cause surprise due to lost
193 subsection {* Keymaps *}
195 text {* Keyboard shortcuts used to be managed as jEdit properties in
196 the past, but recent versions (2013) have a separate concept of
197 \emph{keymap} that is configurable via \emph{Global Options /
198 Shortcuts}. The @{verbatim imported} keymap is derived from the
199 initial environment of properties that is available at the first
200 start of the editor; afterwards the keymap file takes precedence.
202 This is relevant for Isabelle/jEdit due to various fine-tuning of
203 default properties, and additional keyboard shortcuts for Isabelle
204 specific functionality. Users may change their keymap, but need to
205 copy Isabelle-specific key bindings manually. *}
208 subsection {* Look-and-feel *}
210 text {* jEdit is a Java/AWT/Swing application with some ambition to
211 support ``native'' look-and-feel on all platforms, within the limits
212 of what Oracle as Java provider and major operating system
213 distributors allow (see also \secref{sec:problems}).
215 Isabelle/jEdit enables platform-specific look-and-feel by default as
220 \item[Linux] The platform-independent \emph{Nimbus} is used by
221 default, but the classic \emph{Metal} also works. \emph{GTK+} works
222 under the side-condition that the overall GTK theme is selected in a
223 Swing-friendly way.\footnote{GTK support in Java/Swing was once
224 marketed aggressively by Sun, but never quite finished, and is today
225 (2013) lagging a bit behind further development of Swing and GTK.}
227 \item[Windows] Regular \emph{Windows} is used by default, but
228 platform-independent \emph{Nimbus} and \emph{Metal} also work.
230 \item[Mac OS X] Regular \emph{Mac OS X} is used by default, but
231 platform-independent \emph{Nimbus} and \emph{Metal} also work.
232 Moreover the bundled \emph{MacOSX} plugin provides various functions
233 that are expected from applications on that particular platform:
234 quit from menu or dock, preferences menu, drag-and-drop of text
235 files on the application, full-screen mode for main editor windows
240 Users may experiment with different look-and-feels, but need to keep
241 in mind that this extra variance of GUI functionality is unlikely to
242 work in arbitrary combinations. The historic \emph{CDE/Motif} is
243 better avoided. After changing the look-and-feel in \emph{Global
244 Options / Appearance}, it is advisable to restart Isabelle/jEdit in
245 order to take full effect. *}
248 chapter {* Prover IDE functionality *}
250 section {* Text buffers and theories *}
252 text {* As regular text editor, jEdit maintains a collection of open
253 \emph{text buffers} to store source files; each buffer may be
254 associated with any number of visible \emph{text areas}. Buffers
255 are subject to an \emph{edit mode} that is determined from the file
256 type. Files with extension \texttt{.thy} are assigned to the mode
257 \emph{isabelle} and treated specifically.
259 \medskip Isabelle theory files are automatically added to the formal
260 document model of Isabelle/Scala, which maintains a family of
261 versions of all sources for the prover. The \emph{Theories} panel
262 provides an overview of the status of continuous checking of theory
263 sources. Unlike batch sessions \cite{isabelle-sys}, theory nodes
264 are identified by full path names; this allows to work with multiple
265 (disjoint) Isabelle sessions simultaneously within the same editor
268 Certain events to open or update buffers with theory files cause
269 Isabelle/jEdit to resolve dependencies of \emph{theory imports}.
270 The system requests to load additional files into editor buffers, in
271 order to be included in the theory document model for further
272 checking. It is also possible to resolve dependencies
273 automatically, depending on \emph{Plugin Options / Isabelle /
274 General / Auto load} (Isabelle system option @{system_option
277 \medskip The open text area views on theory buffers define the
278 visible \emph{perspective} of Isabelle/jEdit. This is taken as a
279 hint for document processing: the prover ensures that those parts of
280 a theory where the user is looking are checked, while other parts
281 that are presently not required are ignored. The perspective is
282 changed by opening or closing text area windows, or scrolling within
285 The \emph{Theories} panel provides some further options to influence
286 the process of continuous checking: it may be switched off globally
287 to restrict the prover to superficial processing of command syntax.
288 It is also possible to indicate theory nodes as \emph{required} for
289 continuous checking: this means such nodes and all their imports are
290 always processed independently of the visibility status (if
291 continuous checking is enabled). Big theory libraries that are
292 marked as required can have significant impact on performance,
295 \medskip Formal markup of checked theory content is turned into GUI
296 rendering, based on a standard repertoire known from IDEs for
297 programming languages: colors, icons, highlighting, squiggly
298 underline, tooltips, hyperlinks etc. For outer syntax of
299 Isabelle/Isar there is some traditional syntax-highlighting via
300 static keyword tables and tokenization within the editor. In
301 contrast, the painting of inner syntax (term language etc.)\ uses
302 semantic information that is reported dynamically from the logical
303 context. Thus the prover can provide additional markup to help the
304 user to understand the meaning of formal text, and to produce more
305 text with some add-on tools (e.g.\ information messages by automated
306 provers or disprovers running in the background).
308 Such annotated text can be explored further by using the @{verbatim
309 CONTROL} modifier key on Linux and Windows, or @{verbatim COMMAND}
310 on Mac OS X. Hovering with the mouse while the modifier is pressed
311 reveals a \emph{tooltip} (grey box over the text with a yellow
312 popup) and/or a \emph{hyperlink} (black rectangle over the text);
313 see \figref{fig:tooltip}.
317 \includegraphics[scale=0.3]{popup1}
319 \caption{Tooltip and hyperlink for some formal entity.}
323 Tooltip popups use the same rendering principles as the main text
324 area, and further tooltips and/or hyperlinks may be exposed
325 recursively by the same mechanism; see
326 \figref{fig:nested-tooltips}.
330 \includegraphics[scale=0.3]{popup2}
332 \caption{Nested tooltips over formal entities.}
333 \label{fig:nested-tooltips}
336 The tooltip popup window provides some controls to \emph{close} or
337 \emph{detach} the window, turning it into a separate \emph{Info}
338 dockable window managed by jEdit. The @{verbatim ESCAPE} key closes
339 \emph{all} popups, which is particularly relevant for nested
340 tooltips stacking up. *}
343 section {* Isabelle symbols and fonts *}
345 text {* Isabelle sources consist of \emph{symbols} that extend plain
346 ASCII to allow infinitely many mathematical symbols within the
347 formal sources. This works without depending on particular
348 encodings or varying Unicode standards \cite{Wenzel:2011:CICM}.
350 For the prover back-end, formal text consists of ASCII characters
351 that are grouped according to some simple rules, e.g.\ as plain
352 ``@{verbatim a}'' or symbolic ``@{verbatim "\<alpha>"}''.
354 For the editor front-end, a certain subset of symbols is rendered as
355 Unicode glyphs, in order to show ``@{verbatim "\<alpha>"}'' as ``@{text
356 "\<alpha>"}'', for example. This symbol interpretation is specified by the
357 Isabelle system distribution (@{file "$ISABELLE_HOME/etc/symbols"})
358 or by the user (@{verbatim "$ISABELLE_HOME_USER/etc/symbols"}).
360 The appendix of \cite{isabelle-isar-ref} gives an overview of the
361 standard interpretation of finitely many symbols from the infinite
362 collection. Uninterpreted symbols are shown literally, e.g.\
363 ``@{verbatim "\<foobar>"}''.
365 \medskip Technically, the Unicode view on Isabelle symbols is an
366 \emph{encoding} in Isabelle/jEdit, which is called @{verbatim
367 "UTF-8-Isabelle"} and enabled by default. Sometimes such defaults
368 are reset accidentally, or malformed UTF-8 sequences in the text
369 force jEdit to fall back on a different encoding like @{verbatim
370 "ISO-8859-15"}. In that case, verbatim ``@{verbatim "\<alpha>"}'' will be
371 shown in the text buffer instead of its Unicode rendering ``@{text
372 "\<alpha>"}''. The jEdit menu operation \emph{File / Reload with Encoding
373 / UTF-8-Isabelle} helps to resolve such problems, potentially after
374 repairing malformed parts of the text.
376 \medskip Correct rendering via Unicode requires a font that contains
377 glyphs for the corresponding codepoints. Most system fonts lack
378 that, so Isabelle/jEdit prefers its own application font @{verbatim
379 IsabelleText}, which ensures that standard collection of Isabelle
380 symbols are actually seen on the screen (or printer).
382 Note that a Java/AWT/Swing application can load additional fonts
383 only if they are not installed as system font already! This means
384 some old version of @{verbatim IsabelleText} that happens to be
385 already present prevents Isabelle/jEdit from using its current
386 bundled version. This might result in missing glyphs (black
387 rectangles), since obsolete versions of @{verbatim IsabelleText}
388 lack recent improvements of Unicode glyph coverage. This problem
389 can be avoided by refraining to ``install'' any version of
390 @{verbatim IsabelleText} in the first place.
392 \medskip \paragraph{Input methods.} In principle, Isabelle/jEdit
393 could delegate the problem to produce Isabelle symbols in their
394 Unicode rendering to the underlying operating system and its
395 \emph{input methods}. Regular jEdit also provides various ways to
396 work with \emph{abbreviations} to produce certain non-ASCII
397 characters. Since none of these standard input methods work
398 satisfactorily for the mathematical characters required for
399 Isabelle, various specific Isabelle/jEdit mechanisms are provided.
401 Here is a summary for practically relevant input methods for
406 \item The \emph{Symbols} panel with some GUI buttons to insert
407 certain symbols in the text buffer. There are also tooltips to
408 reveal to official Isabelle representation with some additional
409 information about \emph{symbol abbreviations} (see below).
411 \item Copy / paste from decoded source files: text that is rendered
412 as Unicode already can be re-used to produce further such text.
413 This also works between different applications, e.g.\ Isabelle/jEdit
414 and some web browser or mail client, as long as the same Unicode
415 view on Isabelle symbols is used uniformly.
417 \item Copy / paste from prover output within Isabelle/jEdit. The
418 same principles as for text buffers apply, but note that \emph{copy}
419 in Isabelle \emph{Output} works via the keyboard shortcut @{verbatim
420 "C+c"}, not jEdit menu actions.
422 \item Completion provided by Isabelle plugin (see
423 \secref{sec:completion}). Isabelle symbols have a canonical name
424 and optional abbreviations. This can be used with the text
425 completion mechanism of Isabelle/jEdit, to replace a prefix of the
426 actual symbol like @{verbatim "\<lambda>"}, or its backslashed name
427 @{verbatim "\\"}@{verbatim "lambda"}, or its ASCII abbreviation
428 @{verbatim "%"} by the Unicode rendering.
430 The following table is an extract of the information provided by the
431 standard @{file "$ISABELLE_HOME/etc/symbols"} file:
435 \textbf{symbol} & \textbf{abbreviation} & \textbf{backslashed name} \\\hline
436 @{text "\<lambda>"} & @{verbatim "%"} & @{verbatim "\\lambda"} \\
437 @{text "\<Rightarrow>"} & @{verbatim "=>"} & @{verbatim "\\Rightarrow"} \\
438 @{text "\<Longrightarrow>"} & @{verbatim "==>"} & @{verbatim "\\Longrightarrow"} \\
440 @{text "\<And>"} & @{verbatim "!!"} & @{verbatim "\\And"} \\
441 @{text "\<equiv>"} & @{verbatim "=="} & @{verbatim "\\equiv"} \\
443 @{text "\<forall>"} & @{verbatim "!"} & @{verbatim "\\forall"} \\
444 @{text "\<exists>"} & @{verbatim "?"} & @{verbatim "\\exists"} \\
445 @{text "\<longrightarrow>"} & @{verbatim "-->"} & @{verbatim "\\longrightarrow"} \\
446 @{text "\<and>"} & @{verbatim "&"} & @{verbatim "\\and"} \\
447 @{text "\<or>"} & @{verbatim "|"} & @{verbatim "\\or"} \\
448 @{text "\<not>"} & @{verbatim "~"} & @{verbatim "\\not"} \\
449 @{text "\<noteq>"} & @{verbatim "~="} & @{verbatim "\\noteq"} \\
450 @{text "\<in>"} & @{verbatim ":"} & @{verbatim "\\in"} \\
451 @{text "\<notin>"} & @{verbatim "~:"} & @{verbatim "\\notin"} \\
455 Note that the above abbreviations refer to the input method. The
456 logical notation provides ASCII alternatives that often coincide,
457 but deviate occasionally. Writing formal sources directly with
458 ASCII replacement notation like @{verbatim "!"} or @{verbatim "ALL"}
459 is considered old-fashioned in 2013!
463 Raw Unicode characters within prover source files should be
464 restricted to informal parts, e.g.\ to write text in non-latin
465 alphabets. Mathematical symbols should be defined via the official
466 rendering tables, to avoid problems with portability and long-term
467 storage of formal text.
469 \paragraph{Control symbols.} There are some special control symbols
470 to modify the style of a single symbol (without nesting). Control
471 symbols may be applied to a region of selected text, either using
472 the \emph{Symbols} panel or keyboard shortcuts; these editor
473 operations produce a separate control symbol for each symbol in the
474 text, in order to make the whole text appear in a certain style.
478 \textbf{symbol} & style & keyboard shortcut \\\hline
479 @{verbatim "\<^sup>"} & superscript & @{verbatim "C+e UP"} \\
480 @{verbatim "\<^sub>"} & subscript & @{verbatim "C+e DOWN"} \\
481 @{verbatim "\<^bold>"} & bold face & @{verbatim "C+e RIGHT"} \\
482 & reset & @{verbatim "C+e LEFT"} \\
485 It is also possible to complete on @{verbatim "\\"}@{verbatim sup},
486 @{verbatim "\\"}@{verbatim sub}, @{verbatim "\\"}@{verbatim bold} as
491 section {* Text completion \label{sec:completion} *}
494 Text completion works via some light-weight GUI popup, which is triggered by
495 keyboard events during the normal editing process in the main jEdit text
496 area and a few additional text fields. The popup interprets special keys:
497 @{verbatim TAB}, @{verbatim ESCAPE}, @{verbatim UP}, @{verbatim DOWN},
498 @{verbatim PAGE_UP}, @{verbatim PAGE_DOWN}. All other key events are passed
499 to the jEdit text area --- this allows to ignore unwanted completions most
500 of the time and continue typing quickly.
502 Various Isabelle plugin options control the popup behavior and immediate
503 insertion into buffer.
505 Isabelle Symbols are completed in backslashed forms, e.g.\ @{verbatim
506 "\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the Isabelle
507 symbol @{text "\<forall>"} in its Unicode rendering. Alternatively, symbol
508 abbreviations may be used as specified in @{file
509 "$ISABELLE_HOME/etc/symbols"}.
511 \emph{Explicit completion} works via standard jEdit shortcut @{verbatim
512 "C+b"}, which is remapped to action @{verbatim "isabelle.complete"}, with a
513 fall-back on regular @{verbatim "complete-word"} for non-Isabelle buffers.
515 \emph{Implicit completion} works via keyboard input on text area, with popup
516 or immediate insertion into buffer. Plain words require at least 3
517 characters to be completed.
519 \emph{Immediate completion} means the (unique) replacement text is inserted
520 into the buffer without popup. This mode ignores plain words and requires
521 more than one characters for symbol abbreviations. Otherwise it falls back
526 chapter {* Known problems and workarounds \label{sec:problems} *}
531 \item \textbf{Problem:} Lack of dependency management for auxiliary files
532 that contribute to a theory (e.g.\ @{command ML_file}).
534 \textbf{Workaround:} Re-load files manually within the prover, by
535 editing corresponding command in the text.
537 \item \textbf{Problem:} Odd behavior of some diagnostic commands with
538 global side-effects, like writing a physical file.
540 \textbf{Workaround:} Avoid such commands.
542 \item \textbf{Problem:} No way to delete document nodes from the overall
543 collection of theories.
545 \textbf{Workaround:} Ignore unused files. Restart whole
546 Isabelle/jEdit session in worst-case situation.
548 \item \textbf{Problem:} Keyboard shortcuts @{verbatim "C+PLUS"} and
549 @{verbatim "C+MINUS"} for adjusting the editor font size depend on
550 platform details and national keyboards.
552 \textbf{Workaround:} Use numeric keypad or rebind keys in the
553 jEdit Shortcuts options dialog.
555 \item \textbf{Problem:} The Mac OS X keyboard shortcut @{verbatim
556 "COMMAND+COMMA"} for application \emph{Preferences} is in conflict
557 with the jEdit default shortcut for \emph{Incremental Search Bar}
558 (action @{verbatim "quick-search"}).
560 \textbf{Workaround:} Remap in jEdit manually according to national
561 keyboard, e.g.\ @{verbatim "COMMAND+SLASH"} on English ones.
563 \item \textbf{Problem:} Mac OS X system fonts sometimes lead to
564 character drop-outs in the main text area.
566 \textbf{Workaround:} Use the default @{verbatim IsabelleText} font.
567 (Do not install that font on the system.)
569 \item \textbf{Problem:} Some Linux / X11 input methods such as IBus
570 tend to disrupt key event handling of Java/AWT/Swing.
572 \textbf{Workaround:} Do not use input methods, reset the environment
573 variable @{verbatim XMODIFIERS} within Isabelle settings (default in
576 \item \textbf{Problem:} Some Linux / X11 window managers that are
577 not ``re-parenting'' cause problems with additional windows opened
578 by Java. This affects either historic or neo-minimalistic window
579 managers like @{verbatim awesome} or @{verbatim xmonad}.
581 \textbf{Workaround:} Use regular re-parenting window manager.
583 \item \textbf{Problem:} Recent forks of Linux / X11 window managers
584 and desktop environments (variants of Gnome) disrupt the handling of
585 menu popups and mouse positions of Java/AWT/Swing.
587 \textbf{Workaround:} Use mainstream versions of Linux desktops.
589 \item \textbf{Problem:} Full-screen mode via jEdit action @{verbatim
590 "toggle-full-screen"} (default shortcut @{verbatim F11}) works on
591 Windows, but not on Mac OS X or various Linux / X11 window managers.
593 \textbf{Workaround:} Use native full-screen control of the window
594 manager, if available (notably on Mac OS X).
596 \item \textbf{Problem:} Full-screen mode and dockable windows in
597 \emph{floating} state may lead to confusion about window placement
598 (depending on platform characteristics).
600 \textbf{Workaround:} Avoid this combination.