--- 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 "\<approx>"} 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 "\<alpha>"}''.
- 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 "\<alpha>"}'' as actual
``@{text "\<alpha>"}''. 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 "\<alpha>"}, @{text "\<beta>"}, @{text "\<gamma>"}, @{text "\<dots>"} \\
- @{text "\<forall>"}, @{text "\<exists>"}, @{text "\<or>"}, @{text "\<and>"}, @{text "\<longrightarrow>"}, @{text "\<longleftrightarrow>"}, @{text "\<dots>"} \\
- @{text "\<le>"}, @{text "\<ge>"}, @{text "\<sqinter>"}, @{text "\<squnion>"}, @{text "\<dots>"} \\
- @{text "\<aleph>"}, @{text "\<triangle>"}, @{text "\<nabla>"}, @{text "\<dots>"} \\
- @{verbatim "\<foo>"}, @{verbatim "\<bar>"}, @{verbatim "\<baz>"}, @{text "\<dots>"} \\
- \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 "\<lambda>"}, or its backslashed name @{verbatim
- "\\"}@{verbatim "lambda"}, or its ASCII abbreviation @{verbatim
- "%"}.
+ actual symbol like @{verbatim "\<lambda>"}, 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 "\<lambda>"} & @{verbatim "%"} & @{verbatim "\\lambda"} \\
@{text "\<Rightarrow>"} & @{verbatim "=>"} & @{verbatim "\\Rightarrow"} \\
@{text "\<Longrightarrow>"} & @{verbatim "==>"} & @{verbatim "\\Longrightarrow"} \\
@@ -429,33 +414,28 @@
@{text "\<in>"} & @{verbatim ":"} & @{verbatim "\\in"} \\
@{text "\<notin>"} & @{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}
*}