--- a/src/Doc/JEdit/JEdit.thy Sun Oct 18 21:30:01 2015 +0200
+++ b/src/Doc/JEdit/JEdit.thy Sun Oct 18 22:57:09 2015 +0200
@@ -9,11 +9,11 @@
section \<open>Concepts and terminology\<close>
text \<open>
- Isabelle/jEdit is a Prover IDE that integrates \emph{parallel proof
- checking} @{cite "Wenzel:2009" and "Wenzel:2013:ITP"} with
- \emph{asynchronous user interaction} @{cite "Wenzel:2010" and
+ Isabelle/jEdit is a Prover IDE that integrates \<^emph>\<open>parallel proof
+ checking\<close> @{cite "Wenzel:2009" and "Wenzel:2013:ITP"} with
+ \<^emph>\<open>asynchronous user interaction\<close> @{cite "Wenzel:2010" and
"Wenzel:2012:UITP-EPTCS" and "Wenzel:2014:ITP-PIDE" and "Wenzel:2014:UITP"},
- based on a document-oriented approach to \emph{continuous proof processing}
+ based on a document-oriented approach to \<^emph>\<open>continuous proof processing\<close>
@{cite "Wenzel:2011:CICM" and "Wenzel:2012"}. Many concepts and system
components are fit together in order to make this work. The main building
blocks are as follows.
@@ -72,12 +72,12 @@
Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some plugins for
the jEdit text editor, while preserving its general look-and-feel as far as
possible. The main plugin is called ``Isabelle'' and has its own menu
- \emph{Plugins~/ Isabelle} with access to several panels (see also
- \secref{sec:dockables}), as well as \emph{Plugins~/ Plugin Options~/
- Isabelle} (see also \secref{sec:options}).
+ \<^emph>\<open>Plugins~/ Isabelle\<close> with access to several panels (see also
+ \secref{sec:dockables}), as well as \<^emph>\<open>Plugins~/ Plugin Options~/
+ Isabelle\<close> (see also \secref{sec:options}).
The options allow to specify a logic session name --- the same selector is
- accessible in the \emph{Theories} panel (\secref{sec:theories}). On
+ accessible in the \<^emph>\<open>Theories\<close> panel (\secref{sec:theories}). On
application startup, the selected logic session image is provided
automatically by the Isabelle build tool @{cite "isabelle-system"}: if it is
absent or outdated wrt.\ its sources, the build process updates it before
@@ -109,13 +109,13 @@
subsection \<open>Documentation\<close>
text \<open>
- The \emph{Documentation} panel of Isabelle/jEdit provides access to the
+ The \<^emph>\<open>Documentation\<close> panel of Isabelle/jEdit provides access to the
standard Isabelle documentation: PDF files are opened by regular desktop
operations of the underlying platform. The section ``Original jEdit
- Documentation'' contains the original \emph{User's Guide} of this
+ Documentation'' contains the original \<^emph>\<open>User's Guide\<close> of this
sophisticated text editor. The same is accessible via the @{verbatim Help}
menu or @{verbatim F1} keyboard shortcut, using the built-in HTML viewer of
- Java/Swing. The latter also includes \emph{Frequently Asked Questions} and
+ Java/Swing. The latter also includes \<^emph>\<open>Frequently Asked Questions\<close> and
documentation of individual plugins.
Most of the information about generic jEdit is relevant for Isabelle/jEdit
@@ -129,7 +129,7 @@
subsection \<open>Plugins\<close>
text \<open>
- The \emph{Plugin Manager} of jEdit allows to augment editor functionality by
+ The \<^emph>\<open>Plugin Manager\<close> of jEdit allows to augment editor functionality by
JVM modules (jars) that are provided by the central plugin repository, which
is accessible via various mirror sites.
@@ -142,15 +142,15 @@
at a grand scale.
\<^medskip>
- The main \emph{Isabelle} plugin is an integral part of
+ The main \<^emph>\<open>Isabelle\<close> plugin is an integral part of
Isabelle/jEdit and 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
- (\secref{sec:scala-console}) and \emph{SideKick} with some Isabelle-specific
+ notably \<^emph>\<open>Console\<close> with its Isabelle/Scala sub-plugin
+ (\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close> with some Isabelle-specific
parsers for document tree structure (\secref{sec:sidekick}). The
- \emph{Navigator} plugin is particularly important for hyperlinks within the
+ \<^emph>\<open>Navigator\<close> plugin is particularly important for hyperlinks within the
formal document-model (\secref{sec:tooltips-hyperlinks}). Further plugins
- (e.g.\ \emph{ErrorList}, \emph{Code2HTML}) are included to saturate the
+ (e.g.\ \<^emph>\<open>ErrorList\<close>, \<^emph>\<open>Code2HTML\<close>) are included to saturate the
dependencies of bundled plugins, but have no particular use in
Isabelle/jEdit.
\<close>
@@ -161,8 +161,8 @@
text \<open>Both jEdit and Isabelle have distinctive management of
persistent options.
- Regular jEdit options are accessible via the dialogs \emph{Utilities~/
- Global Options} or \emph{Plugins~/ Plugin Options}, with a second chance to
+ Regular jEdit options are accessible via the dialogs \<^emph>\<open>Utilities~/
+ Global Options\<close> or \<^emph>\<open>Plugins~/ Plugin Options\<close>, with a second chance to
flip the two within the central options dialog. Changes are stored in
@{file_unchecked "$ISABELLE_HOME_USER/jedit/properties"} and
@{file_unchecked "$ISABELLE_HOME_USER/jedit/keymaps"}.
@@ -173,11 +173,11 @@
coverage of sessions and command-line tools like @{tool build} or @{tool
options}.
- Those Isabelle options that are declared as \textbf{public} are configurable
- in Isabelle/jEdit via \emph{Plugin Options~/ Isabelle~/ General}. Moreover,
+ Those Isabelle options that are declared as \<^bold>\<open>public\<close> are configurable
+ in Isabelle/jEdit via \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>. Moreover,
there are various options for rendering of document content, which are
- configurable via \emph{Plugin Options~/ Isabelle~/ Rendering}. Thus
- \emph{Plugin Options~/ Isabelle} in jEdit provides a view on a subset of
+ configurable via \<^emph>\<open>Plugin Options~/ Isabelle~/ Rendering\<close>. Thus
+ \<^emph>\<open>Plugin Options~/ Isabelle\<close> in jEdit provides a view on a subset of
Isabelle system options. Note that some of these options affect general
parameters that are relevant outside Isabelle/jEdit as well, e.g.\
@{system_option threads} or @{system_option parallel_proofs} for the
@@ -200,8 +200,8 @@
text \<open>Keyboard shortcuts used to be managed as jEdit properties in
the past, but recent versions (2013) have a separate concept of
- \emph{keymap} that is configurable via \emph{Global Options~/
- Shortcuts}. The @{verbatim imported} keymap is derived from the
+ \<^emph>\<open>keymap\<close> that is configurable via \<^emph>\<open>Global Options~/
+ Shortcuts\<close>. The @{verbatim imported} keymap is derived from the
initial environment of properties that is available at the first
start of the editor; afterwards the keymap file takes precedence.
@@ -251,7 +251,7 @@
The @{verbatim "-m"} option specifies additional print modes for the prover
process. Note that the system option @{system_option_ref jedit_print_mode}
- allows to do the same persistently (e.g.\ via the \emph{Plugin Options}
+ allows to do the same persistently (e.g.\ via the \<^emph>\<open>Plugin Options\<close>
dialog of Isabelle/jEdit), without requiring command-line invocation.
The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass additional
@@ -283,10 +283,10 @@
Isabelle/jEdit enables platform-specific look-and-feel by default as
follows.
- \<^descr>[Linux:] The platform-independent \emph{Nimbus} is used by
+ \<^descr>[Linux:] The platform-independent \<^emph>\<open>Nimbus\<close> is used by
default.
- \emph{GTK+} also works under the side-condition that the overall GTK theme
+ \<^emph>\<open>GTK+\<close> also works under the side-condition that the overall GTK theme
is selected in a Swing-friendly way.\footnote{GTK support in Java/Swing was
once marketed aggressively by Sun, but never quite finished. Today (2015) it
is lagging behind further development of Swing and GTK. The graphics
@@ -295,26 +295,26 @@
``4K'' or ``UHD'' models), because the rendering by the external library is
subject to global system settings for font scaling.}
- \<^descr>[Windows:] Regular \emph{Windows} is used by default, but
- \emph{Windows Classic} also works.
+ \<^descr>[Windows:] Regular \<^emph>\<open>Windows\<close> is used by default, but
+ \<^emph>\<open>Windows Classic\<close> also works.
- \<^descr>[Mac OS X:] Regular \emph{Mac OS X} is used by default.
+ \<^descr>[Mac OS X:] Regular \<^emph>\<open>Mac OS X\<close> is used by default.
- The bundled \emph{MacOSX} plugin provides various functions that are
+ The bundled \<^emph>\<open>MacOSX\<close> 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 files on the application,
full-screen mode for main editor windows. It is advisable to have the
- \emph{MacOSX} plugin enabled all the time on that platform.
+ \<^emph>\<open>MacOSX\<close> plugin enabled all the time on that platform.
Users may experiment with different look-and-feels, but need to keep
in mind that this extra variance of GUI functionality is unlikely to
work in arbitrary combinations. The platform-independent
- \emph{Nimbus} and \emph{Metal} should always work. The historic
- \emph{CDE/Motif} should be ignored.
+ \<^emph>\<open>Nimbus\<close> and \<^emph>\<open>Metal\<close> should always work. The historic
+ \<^emph>\<open>CDE/Motif\<close> should be ignored.
- After changing the look-and-feel in \emph{Global Options~/
- Appearance}, it is advisable to restart Isabelle/jEdit in order to
+ After changing the look-and-feel in \<^emph>\<open>Global Options~/
+ Appearance\<close>, it is advisable to restart Isabelle/jEdit in order to
take full effect.
\<close>
@@ -334,40 +334,40 @@
HD'' category). Subsequently there are further hints to improve on that.
\<^medskip>
- The \textbf{operating-system platform} usually provides some
+ The \<^bold>\<open>operating-system platform\<close> usually provides some
configuration for global scaling of text fonts, e.g.\ $120\%$--$250\%$ on
Windows. Changing that only has a partial effect on GUI rendering;
satisfactory display quality requires further adjustments.
\<^medskip>
- The Isabelle/jEdit \textbf{application} and its plugins provide
+ The Isabelle/jEdit \<^bold>\<open>application\<close> and its plugins provide
various font properties that are summarized below.
- \<^item> \emph{Global Options / Text Area / Text font}: the main text area
+ \<^item> \<^emph>\<open>Global Options / Text Area / Text font\<close>: the main text area
font, which is also used as reference point for various derived font sizes,
e.g.\ the Output panel (\secref{sec:output}).
- \<^item> \emph{Global Options / Gutter / Gutter font}: the font for the gutter
+ \<^item> \<^emph>\<open>Global Options / Gutter / Gutter font\<close>: the font for the gutter
area left of the main text area, e.g.\ relevant for display of line numbers
(disabled by default).
- \<^item> \emph{Global Options / Appearance / Button, menu and label font} as
- well as \emph{List and text field font}: this specifies the primary and
- secondary font for the old \emph{Metal} look-and-feel
+ \<^item> \<^emph>\<open>Global Options / Appearance / Button, menu and label font\<close> as
+ well as \<^emph>\<open>List and text field font\<close>: this specifies the primary and
+ secondary font for the old \<^emph>\<open>Metal\<close> look-and-feel
(\secref{sec:look-and-feel}), which happens to scale better than newer ones
- like \emph{Nimbus}.
+ like \<^emph>\<open>Nimbus\<close>.
- \<^item> \emph{Plugin Options / Isabelle / General / Reset Font Size}: the main
+ \<^item> \<^emph>\<open>Plugin Options / Isabelle / General / Reset Font Size\<close>: the main
text area font size for action @{action_ref "isabelle.reset-font-size"},
e.g.\ relevant for quick scaling like in major web browsers.
- \<^item> \emph{Plugin Options / Console / General / Font}: the console window
+ \<^item> \<^emph>\<open>Plugin Options / Console / General / Font\<close>: the console window
font, e.g.\ relevant for Isabelle/Scala command-line.
- In \figref{fig:isabelle-jedit-hdpi} the \emph{Metal} look-and-feel is
+ In \figref{fig:isabelle-jedit-hdpi} the \<^emph>\<open>Metal\<close> look-and-feel is
configured with custom fonts at 30 pixels, and the main text area and
- console at 36 pixels. Despite the old-fashioned appearance of \emph{Metal},
+ console at 36 pixels. Despite the old-fashioned appearance of \<^emph>\<open>Metal\<close>,
this leads to decent rendering quality on all platforms.
\begin{figure}[htb]
@@ -378,7 +378,7 @@
\label{fig:isabelle-jedit-hdpi}
\end{figure}
- On Linux, it is also possible to use \emph{GTK+} with a suitable theme and
+ On Linux, it is also possible to use \<^emph>\<open>GTK+\<close> with a suitable theme and
global font scaling. On Mac OS X, the default setup for ``Retina'' displays
should work adequately with the native look-and-feel.
\<close>
@@ -387,30 +387,30 @@
section \<open>Dockable windows \label{sec:dockables}\<close>
text \<open>
- In jEdit terminology, a \emph{view} is an editor window with one or more
- \emph{text areas} that show the content of one or more \emph{buffers}. A
- regular view may be surrounded by \emph{dockable windows} that show
- additional information in arbitrary format, not just text; a \emph{plain
- view} does not allow dockables. The \emph{dockable window manager} of jEdit
- organizes these dockable windows, either as \emph{floating} windows, or
- \emph{docked} panels within one of the four margins of the view. There may
+ In jEdit terminology, a \<^emph>\<open>view\<close> is an editor window with one or more
+ \<^emph>\<open>text areas\<close> that show the content of one or more \<^emph>\<open>buffers\<close>. A
+ regular view may be surrounded by \<^emph>\<open>dockable windows\<close> that show
+ additional information in arbitrary format, not just text; a \<^emph>\<open>plain
+ view\<close> does not allow dockables. The \<^emph>\<open>dockable window manager\<close> of jEdit
+ organizes these dockable windows, either as \<^emph>\<open>floating\<close> windows, or
+ \<^emph>\<open>docked\<close> panels within one of the four margins of the view. There may
be any number of floating instances of some dockable window, but at most one
- docked instance; jEdit actions that address \emph{the} dockable window of a
+ docked instance; jEdit actions that address \<^emph>\<open>the\<close> dockable window of a
particular kind refer to the unique docked instance.
Dockables are used routinely in jEdit for important functionality like
- \emph{HyperSearch Results} or the \emph{File System Browser}. Plugins often
+ \<^emph>\<open>HyperSearch Results\<close> or the \<^emph>\<open>File System Browser\<close>. Plugins often
provide a central dockable to access their key functionality, which may be
opened by the user on demand. The Isabelle/jEdit plugin takes this approach
to the extreme: its plugin menu provides the entry-points to many panels
that are managed as dockable windows. Some important panels are docked by
- default, e.g.\ \emph{Documentation}, \emph{Output}, \emph{Query}, but the
+ default, e.g.\ \<^emph>\<open>Documentation\<close>, \<^emph>\<open>Output\<close>, \<^emph>\<open>Query\<close>, but the
user can change this arrangement easily and persistently.
Compared to plain jEdit, dockable window management in Isabelle/jEdit is
slightly augmented according to the the following principles:
- \<^item> Floating windows are dependent on the main window as \emph{dialog} in
+ \<^item> Floating windows are dependent on the main window as \<^emph>\<open>dialog\<close> in
the sense of Java/AWT/Swing. Dialog windows always stay on top of the view,
which is particularly important in full-screen mode. The desktop environment
of the underlying platform may impose further policies on such dependent
@@ -419,24 +419,24 @@
\<^item> Keyboard focus of the main view vs.\ a dockable window is carefully
managed according to the intended semantics, as a panel mainly for output or
- input. For example, activating the \emph{Output} (\secref{sec:output}) panel
+ input. For example, activating the \<^emph>\<open>Output\<close> (\secref{sec:output}) panel
via the dockable window manager returns keyboard focus to the main text
- area, but for \emph{Query} (\secref{sec:query}) the focus is given to the
+ area, but for \<^emph>\<open>Query\<close> (\secref{sec:query}) the focus is given to the
main input field of that panel.
\<^item> Panels that provide their own text area for output have an additional
- dockable menu item \emph{Detach}. This produces an independent copy of the
- current output as a floating \emph{Info} window, which displays that content
+ dockable menu item \<^emph>\<open>Detach\<close>. This produces an independent copy of the
+ current output as a floating \<^emph>\<open>Info\<close> window, which displays that content
independently of ongoing changes of the PIDE document-model. Note that
Isabelle/jEdit popup windows (\secref{sec:tooltips-hyperlinks}) provide a
- similar \emph{Detach} operation as an icon.
+ similar \<^emph>\<open>Detach\<close> operation as an icon.
\<close>
section \<open>Isabelle symbols \label{sec:symbols}\<close>
text \<open>
- Isabelle sources consist of \emph{symbols} that extend plain ASCII to allow
+ Isabelle sources consist of \<^emph>\<open>symbols\<close> that extend plain ASCII to allow
infinitely many mathematical symbols within the formal sources. This works
without depending on particular encodings and varying Unicode
standards.\footnote{Raw Unicode characters within formal sources would
@@ -464,14 +464,14 @@
\<^medskip>
\paragraph{Encoding.} Technically, the Unicode view on Isabelle
- symbols is an \emph{encoding} called @{verbatim "UTF-8-Isabelle"} in jEdit
+ symbols is an \<^emph>\<open>encoding\<close> called @{verbatim "UTF-8-Isabelle"} in jEdit
(not in the underlying JVM). It is provided by the Isabelle/jEdit plugin and
enabled by default for all source files. Sometimes such defaults are reset
accidentally, or malformed UTF-8 sequences in the text force jEdit to fall
back on a different encoding like @{verbatim "ISO-8859-15"}. In that case,
verbatim ``@{verbatim "\<alpha>"}'' will be shown in the text buffer instead of its
- Unicode rendering ``@{text "\<alpha>"}''. The jEdit menu operation \emph{File~/
- Reload with Encoding~/ UTF-8-Isabelle} helps to resolve such problems (after
+ Unicode rendering ``@{text "\<alpha>"}''. The jEdit menu operation \<^emph>\<open>File~/
+ Reload with Encoding~/ UTF-8-Isabelle\<close> helps to resolve such problems (after
repairing malformed parts of the text).
\<^medskip>
@@ -496,8 +496,8 @@
\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}. Regular jEdit also provides various ways to
- work with \emph{abbreviations} to produce certain non-ASCII
+ \<^emph>\<open>input methods\<close>. Regular jEdit also provides various ways to
+ work with \<^emph>\<open>abbreviations\<close> 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.
@@ -505,10 +505,10 @@
This is a summary for practically relevant input methods for Isabelle
symbols.
- \<^enum> The \emph{Symbols} panel: some GUI buttons allow to insert
+ \<^enum> The \<^emph>\<open>Symbols\<close> panel: some GUI buttons allow to insert
certain symbols in the text buffer. There are also tooltips to
reveal the official Isabelle representation with some additional
- information about \emph{symbol abbreviations} (see below).
+ information about \<^emph>\<open>symbol abbreviations\<close> (see below).
\<^enum> Copy/paste from decoded source files: text that is rendered
as Unicode already can be re-used to produce further text. This
@@ -517,7 +517,7 @@
Isabelle symbols is used.
\<^enum> Copy/paste from prover output within Isabelle/jEdit. The same
- principles as for text buffers apply, but note that \emph{copy} in secondary
+ principles as for text buffers apply, but note that \<^emph>\<open>copy\<close> in secondary
Isabelle/jEdit windows works via the keyboard shortcuts @{verbatim "C+c"} or
@{verbatim "C+INSERT"}, while jEdit menu actions always refer to the primary
text area!
@@ -535,7 +535,7 @@
\<^medskip>
\begin{tabular}{lll}
- \textbf{symbol} & \textbf{name with backslash} & \textbf{abbreviation} \\\hline
+ \<^bold>\<open>symbol\<close> & \<^bold>\<open>name with backslash\<close> & \<^bold>\<open>abbreviation\<close> \\\hline
@{text "\<lambda>"} & @{verbatim "\\lambda"} & @{verbatim "%"} \\
@{text "\<Rightarrow>"} & @{verbatim "\\Rightarrow"} & @{verbatim "=>"} \\
@{text "\<Longrightarrow>"} & @{verbatim "\\Longrightarrow"} & @{verbatim "==>"} \\[0.5ex]
@@ -568,14 +568,14 @@
\paragraph{Control symbols.} There are some special control symbols
to modify the display 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 or
+ text, either using the \<^emph>\<open>Symbols\<close> panel or keyboard shortcuts or
jEdit actions. These editor operations produce a separate control
symbol for each symbol in the text, in order to make the whole text
appear in a certain style.
\<^medskip>
\begin{tabular}{llll}
- \textbf{style} & \textbf{symbol} & \textbf{shortcut} & \textbf{action} \\\hline
+ \<^bold>\<open>style\<close> & \<^bold>\<open>symbol\<close> & \<^bold>\<open>shortcut\<close> & \<^bold>\<open>action\<close> \\\hline
superscript & @{verbatim "\<^sup>"} & @{verbatim "C+e UP"} & @{action_ref "isabelle.control-sup"} \\
subscript & @{verbatim "\<^sub>"} & @{verbatim "C+e DOWN"} & @{action_ref "isabelle.control-sub"} \\
bold face & @{verbatim "\<^bold>"} & @{verbatim "C+e RIGHT"} & @{action_ref "isabelle.control-bold"} \\
@@ -591,7 +591,7 @@
section \<open>SideKick parsers \label{sec:sidekick}\<close>
text \<open>
- The \emph{SideKick} plugin provides some general services to display buffer
+ The \<^emph>\<open>SideKick\<close> plugin provides some general services to display buffer
structure in a tree view.
Isabelle/jEdit provides SideKick parsers for its main mode for theory files,
@@ -619,13 +619,13 @@
section \<open>Scala console \label{sec:scala-console}\<close>
text \<open>
- The \emph{Console} plugin manages various shells (command interpreters),
- e.g.\ \emph{BeanShell}, which is the official jEdit scripting language, and
- the cross-platform \emph{System} shell. Thus the console provides similar
+ The \<^emph>\<open>Console\<close> plugin manages various shells (command interpreters),
+ e.g.\ \<^emph>\<open>BeanShell\<close>, which is the official jEdit scripting language, and
+ the cross-platform \<^emph>\<open>System\<close> shell. Thus the console provides similar
functionality than the Emacs buffers @{verbatim "*scratch*"} and
@{verbatim "*shell*"}.
- Isabelle/jEdit extends the repertoire of the console by \emph{Scala}, which
+ Isabelle/jEdit extends the repertoire of the console by \<^emph>\<open>Scala\<close>, which
is the regular Scala toplevel loop running inside the same JVM process as
Isabelle/jEdit itself. This means the Scala command interpreter has access
to the JVM name space and state of the running Prover IDE application. The
@@ -647,7 +647,7 @@
text \<open>
File specifications in jEdit follow various formats and conventions
- according to \emph{Virtual File Systems}, which may be also provided by
+ according to \<^emph>\<open>Virtual File Systems\<close>, which may be also provided by
additional plugins. This allows to access remote files via the @{verbatim
"http:"} protocol prefix, for example. Isabelle/jEdit attempts to work with
the file-system model of jEdit as far as possible. In particular, theory
@@ -662,7 +662,7 @@
letters and network shares.
The Java notation for files needs to be distinguished from the one of
- Isabelle, which uses POSIX notation with forward slashes on \emph{all}
+ Isabelle, which uses POSIX notation with forward slashes on \<^emph>\<open>all\<close>
platforms.\footnote{Isabelle/ML on Windows uses Cygwin file-system access
and Unix-style path notation.} Moreover, environment variables from the
Isabelle process may be used freely, e.g.\ @{file
@@ -683,7 +683,7 @@
Isabelle/jEdit imitates @{verbatim "$ISABELLE_HOME"} and @{verbatim
"$ISABELLE_HOME_USER"} within the Java process environment, in order to
allow easy access to these important places from the editor. The file
- browser of jEdit also includes \emph{Favorites} for these two important
+ browser of jEdit also includes \<^emph>\<open>Favorites\<close> for these two important
locations.
\<^medskip>
@@ -718,15 +718,15 @@
subsection \<open>Editor buffers and document nodes \label{sec:buffer-node}\<close>
text \<open>
- As a regular text editor, jEdit maintains a collection of \emph{buffers} to
+ As a regular text editor, jEdit maintains a collection of \<^emph>\<open>buffers\<close> to
store text files; each buffer may be associated with any number of visible
- \emph{text areas}. Buffers are subject to an \emph{edit mode} that is
+ \<^emph>\<open>text areas\<close>. Buffers are subject to an \<^emph>\<open>edit mode\<close> that is
determined from the file name extension. The following modes are treated
specifically in Isabelle/jEdit:
\<^medskip>
\begin{tabular}{lll}
- \textbf{mode} & \textbf{file extension} & \textbf{content} \\\hline
+ \<^bold>\<open>mode\<close> & \<^bold>\<open>file extension\<close> & \<^bold>\<open>content\<close> \\\hline
@{verbatim "isabelle"} & @{verbatim ".thy"} & theory source \\
@{verbatim "isabelle-ml"} & @{verbatim ".ML"} & Isabelle/ML source \\
@{verbatim "sml"} & @{verbatim ".sml"} or @{verbatim ".sig"} & Standard ML source \\
@@ -734,15 +734,15 @@
\<^medskip>
All jEdit buffers are automatically added to the PIDE document-model as
- \emph{document nodes}. The overall document structure is defined by the
+ \<^emph>\<open>document nodes\<close>. The overall document structure is defined by the
theory nodes in two dimensions:
- \<^enum> via \textbf{theory imports} that are specified in the \emph{theory
- header} using concrete syntax of the @{command_ref theory} command
+ \<^enum> via \<^bold>\<open>theory imports\<close> that are specified in the \<^emph>\<open>theory
+ header\<close> using concrete syntax of the @{command_ref theory} command
@{cite "isabelle-isar-ref"};
- \<^enum> via \textbf{auxiliary files} that are loaded into a theory by special
- \emph{load commands}, notably @{command_ref ML_file} and @{command_ref
+ \<^enum> via \<^bold>\<open>auxiliary files\<close> that are loaded into a theory by special
+ \<^emph>\<open>load commands\<close>, notably @{command_ref ML_file} and @{command_ref
SML_file} @{cite "isabelle-isar-ref"}.
@@ -756,7 +756,7 @@
subsection \<open>Theories \label{sec:theories}\<close>
text \<open>
- The \emph{Theories} panel (see also \figref{fig:theories}) provides an
+ The \<^emph>\<open>Theories\<close> panel (see also \figref{fig:theories}) provides an
overview of the status of continuous checking of theory nodes within the
document model. Unlike batch sessions of @{tool build} @{cite
"isabelle-system"}, theory nodes are identified by full path names; this allows
@@ -780,17 +780,17 @@
@{system_option jedit_auto_load}.
\<^medskip>
- The visible \emph{perspective} of Isabelle/jEdit is defined by the
+ The visible \<^emph>\<open>perspective\<close> of Isabelle/jEdit is defined by the
collective view on theory buffers via open text areas. The perspective 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 perspective is changed by
opening or closing text area windows, or scrolling within a window.
- The \emph{Theories} panel provides some further options to influence
+ The \<^emph>\<open>Theories\<close> panel provides some further options to influence
the process of continuous checking: it may be switched off globally
to restrict the prover to superficial processing of command syntax.
- It is also possible to indicate theory nodes as \emph{required} for
+ It is also possible to indicate theory nodes as \<^emph>\<open>required\<close> for
continuous checking: this means such nodes and all their imports are
always processed independently of the visibility status (if
continuous checking is enabled). Big theory libraries that are
@@ -808,7 +808,7 @@
that is reported dynamically from the logical context. Thus the prover can
provide additional markup to help the user to understand the meaning of
formal text, and to produce more text with some add-on tools (e.g.\
- information messages with \emph{sendback} markup by automated provers or
+ information messages with \<^emph>\<open>sendback\<close> markup by automated provers or
disprovers in the background).
\<close>
@@ -870,7 +870,7 @@
section \<open>Output \label{sec:output}\<close>
text \<open>
- Prover output consists of \emph{markup} and \emph{messages}. Both are
+ Prover output consists of \<^emph>\<open>markup\<close> and \<^emph>\<open>messages\<close>. Both are
directly attached to the corresponding positions in the original source
text, and visualized in the text area, e.g.\ as text colours for free and
bound variables, or as squiggly underlines for warnings, errors etc.\ (see
@@ -900,14 +900,14 @@
the given window height. Mouse clicks on the overview area position the
cursor approximately to the corresponding line of text in the buffer.
- Another course-grained overview is provided by the \emph{Theories}
+ Another course-grained overview is provided by the \<^emph>\<open>Theories\<close>
panel, but without direct correspondence to text positions. A
double-click on one of the theory entries with their status overview
opens the corresponding text buffer, without changing the cursor
position.
\<^medskip>
- In addition, the \emph{Output} panel displays prover
+ In addition, the \<^emph>\<open>Output\<close> panel displays prover
messages that correspond to a given command, within a separate
window.
@@ -916,7 +916,7 @@
(in canonical order according to the internal execution of the command).
There are also control elements to modify the update policy of the output
wrt.\ continued editor movements. This is particularly useful with several
- independent instances of the \emph{Output} panel, which the Dockable Window
+ independent instances of the \<^emph>\<open>Output\<close> panel, which the Dockable Window
Manager of jEdit can handle conveniently.
Former users of the old TTY interaction model (e.g.\ Proof~General) might
@@ -929,7 +929,7 @@
situations by inspecting internal state of the prover.\footnote{In
that sense, unstructured tactic scripts depend on continuous
debugging with internal state inspection.} Consequently, some
- special messages for \emph{tracing} or \emph{proof state} only
+ special messages for \<^emph>\<open>tracing\<close> or \<^emph>\<open>proof state\<close> only
appear here, and are not attached to the original source.
\<^medskip>
@@ -943,16 +943,16 @@
section \<open>Query \label{sec:query}\<close>
text \<open>
- The \emph{Query} panel provides various GUI forms to request extra
+ The \<^emph>\<open>Query\<close> panel provides various GUI forms to request extra
information from the prover. In old times the user would have issued some
diagnostic command like @{command find_theorems} and inspected its output,
but this is now integrated into the Prover IDE.
- A \emph{Query} window provides some input fields and buttons for a
+ A \<^emph>\<open>Query\<close> window provides some input fields and buttons for a
particular query command, with output in a dedicated text area. There are
- various query modes: \emph{Find Theorems}, \emph{Find Constants},
- \emph{Print Context}, e.g.\ see \figref{fig:query}. As usual in jEdit,
- multiple \emph{Query} windows may be active at the same time: any number of
+ various query modes: \<^emph>\<open>Find Theorems\<close>, \<^emph>\<open>Find Constants\<close>,
+ \<^emph>\<open>Print Context\<close>, e.g.\ see \figref{fig:query}. As usual in jEdit,
+ multiple \<^emph>\<open>Query\<close> windows may be active at the same time: any number of
floating instances, but at most one docked instance (which is used by
default).
@@ -970,21 +970,21 @@
\<^item> The spinning wheel provides feedback about the status of a pending
query wrt.\ the evaluation of its context and its own operation.
- \<^item> The \emph{Apply} button attaches a fresh query invocation to the
+ \<^item> The \<^emph>\<open>Apply\<close> button attaches a fresh query invocation to the
current context of the command where the cursor is pointing in the text.
- \<^item> The \emph{Search} field allows to highlight query output according to
+ \<^item> The \<^emph>\<open>Search\<close> field allows to highlight query output according to
some regular expression, in the notation that is commonly used on the Java
platform.\footnote{@{url
"http://docs.oracle.com/javase/7/docs/api/java/util/regex/Pattern.html"}}
This may serve as an additional visual filter of the result.
- \<^item> The \emph{Zoom} box controls the font size of the output area.
+ \<^item> The \<^emph>\<open>Zoom\<close> box controls the font size of the output area.
All query operations are asynchronous: there is no need to wait for the
evaluation of the document for the query context, nor for the query
- operation itself. Query output may be detached as independent \emph{Info}
+ operation itself. Query output may be detached as independent \<^emph>\<open>Info\<close>
window, using a menu operation of the dockable window manager. The printed
result usually provides sufficient clues about the original query, with some
hyperlink to its context (via markup of its head line).
@@ -994,8 +994,8 @@
subsection \<open>Find theorems\<close>
text \<open>
- The \emph{Query} panel in \emph{Find Theorems} mode retrieves facts from the
- theory or proof context matching all of given criteria in the \emph{Find}
+ The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Theorems\<close> mode retrieves facts from the
+ theory or proof context matching all of given criteria in the \<^emph>\<open>Find\<close>
text field. A single criterium has the following syntax:
@{rail \<open>
@@ -1011,8 +1011,8 @@
subsection \<open>Find constants\<close>
text \<open>
- The \emph{Query} panel in \emph{Find Constants} mode prints all constants
- whose type meets all of the given criteria in the \emph{Find} text field.
+ The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Constants\<close> mode prints all constants
+ whose type meets all of the given criteria in the \<^emph>\<open>Find\<close> text field.
A single criterium has the following syntax:
@{rail \<open>
@@ -1028,7 +1028,7 @@
subsection \<open>Print context\<close>
text \<open>
- The \emph{Query} panel in \emph{Print Context} mode prints information from
+ The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Print Context\<close> mode prints information from
the theory or proof context, or proof state. See also the Isar commands
@{command_ref print_context}, @{command_ref print_cases}, @{command_ref
print_term_bindings}, @{command_ref print_theorems}, @{command_ref
@@ -1043,8 +1043,8 @@
information that can be explored further by using the @{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 a
- \emph{tooltip} (grey box over the text with a yellow popup) and/or a
- \emph{hyperlink} (black rectangle over the text with change of mouse
+ \<^emph>\<open>tooltip\<close> (grey box over the text with a yellow popup) and/or a
+ \<^emph>\<open>hyperlink\<close> (black rectangle over the text with change of mouse
pointer); see also \figref{fig:tooltip}.
\begin{figure}[htb]
@@ -1067,17 +1067,17 @@
\label{fig:nested-tooltips}
\end{figure}
- The tooltip popup window provides some controls to \emph{close} or
- \emph{detach} the window, turning it into a separate \emph{Info}
+ The tooltip popup window provides some controls to \<^emph>\<open>close\<close> or
+ \<^emph>\<open>detach\<close> the window, turning it into a separate \<^emph>\<open>Info\<close>
window managed by jEdit. The @{verbatim ESCAPE} key closes
- \emph{all} popups, which is particularly relevant when nested
+ \<^emph>\<open>all\<close> popups, which is particularly relevant when nested
tooltips are stacking up.
\<^medskip>
A black rectangle in the text indicates a hyperlink that may be
followed by a mouse click (while the @{verbatim CONTROL} or @{verbatim
COMMAND} modifier key is still pressed). Such jumps to other text locations
- are recorded by the \emph{Navigator} plugin, which is bundled with
+ are recorded by the \<^emph>\<open>Navigator\<close> plugin, which is bundled with
Isabelle/jEdit and enabled by default, including navigation arrows in the
main jEdit toolbar.
@@ -1091,25 +1091,25 @@
section \<open>Completion \label{sec:completion}\<close>
text \<open>
- Smart completion of partial input is the IDE functionality \emph{par
- excellance}. Isabelle/jEdit combines several sources of information to
+ Smart completion of partial input is the IDE functionality \<^emph>\<open>par
+ excellance\<close>. Isabelle/jEdit combines several sources of information to
achieve that. Despite its complexity, it should be possible to get some idea
how completion works by experimentation, based on the overview of completion
varieties in \secref{sec:completion-varieties}. The remaining subsections
explain concepts around completion more systematically.
\<^medskip>
- \emph{Explicit completion} is triggered by the action @{action_ref
+ \<^emph>\<open>Explicit completion\<close> is triggered by the action @{action_ref
"isabelle.complete"}, which is bound to the keyboard shortcut @{verbatim
"C+b"}, and thus overrides the jEdit default for @{action_ref
"complete-word"}.
- \emph{Implicit completion} hooks into the regular keyboard input stream of
+ \<^emph>\<open>Implicit completion\<close> hooks into the regular keyboard input stream of
the editor, with some event filtering and optional delays.
\<^medskip>
- Completion options may be configured in \emph{Plugin Options~/
- Isabelle~/ General~/ Completion}. These are explained in further detail
+ Completion options may be configured in \<^emph>\<open>Plugin Options~/
+ Isabelle~/ General~/ Completion\<close>. These are explained in further detail
below, whenever relevant. There is also a summary of options in
\secref{sec:completion-options}.
@@ -1133,7 +1133,7 @@
kinds and purposes. The completion mechanism supports this by the following
built-in templates:
- \<^descr> @{verbatim "`"} (single ASCII back-quote) supports \emph{quotations}
+ \<^descr> @{verbatim "`"} (single ASCII back-quote) supports \<^emph>\<open>quotations\<close>
via text cartouches. There are three selections, which are always presented
in the same order and do not depend on any context information. The default
choice produces a template ``@{text "\<open>\<box>\<close>"}'', where the box indicates the
@@ -1184,7 +1184,7 @@
\<^medskip>
\begin{tabular}{ll}
- \textbf{completion entry} & \textbf{example} \\\hline
+ \<^bold>\<open>completion entry\<close> & \<^bold>\<open>example\<close> \\\hline
literal symbol & @{verbatim "\<forall>"} \\
symbol name with backslash & @{verbatim "\\"}@{verbatim forall} \\
symbol abbreviation & @{verbatim "ALL"} or @{verbatim "!"} \\
@@ -1212,13 +1212,13 @@
text \<open>
This is genuine semantic completion, using information from the prover, so
- it requires some delay. A \emph{failed name-space lookup} produces an error
+ it requires some delay. A \<^emph>\<open>failed name-space lookup\<close> produces an error
message that is annotated with a list of alternative names that are legal.
The list of results is truncated according to the system option
@{system_option_ref completion_limit}. The completion mechanism takes this
into account when collecting information on the prover side.
- Already recognized names are \emph{not} completed further, but completion
+ Already recognized names are \<^emph>\<open>not\<close> completed further, but completion
may be extended by appending a suffix of underscores. This provokes a failed
lookup, and another completion attempt while ignoring the underscores. For
example, in a name space where @{verbatim "foo"} and @{verbatim "foobar"}
@@ -1240,7 +1240,7 @@
source text, e.g.\ for the argument of a load command
(\secref{sec:aux-files}), the completion mechanism explores the directory
content and offers the result as completion popup. Relative path
- specifications are understood wrt.\ the \emph{master directory} of the
+ specifications are understood wrt.\ the \<^emph>\<open>master directory\<close> of the
document node (\secref{sec:buffer-node}) of the enclosing editor buffer;
this requires a proper theory, not an auxiliary file.
@@ -1291,19 +1291,19 @@
document-model, the default context is given by the outer syntax of the
editor mode (see also \secref{sec:buffer-node}).
- The semantic \emph{language context} provides information about nested
+ The semantic \<^emph>\<open>language context\<close> provides information about nested
sub-languages of Isabelle: keywords are only completed for outer syntax,
symbols or antiquotations for languages that support them. E.g.\ there is no
symbol completion for ML source, but within ML strings, comments,
antiquotations.
- The prover may produce \emph{no completion} markup in exceptional
+ The prover may produce \<^emph>\<open>no completion\<close> markup in exceptional
situations, to tell that some language keywords should be excluded from
further completion attempts. For example, @{verbatim ":"} within accepted
Isar syntax looses its meaning as abbreviation for symbol @{text "\<in>"}.
\<^medskip>
- The completion context is \emph{ignored} for built-in templates and
+ The completion context is \<^emph>\<open>ignored\<close> for built-in templates and
symbols in their explicit form ``@{verbatim "\<foobar>"}''; see also
\secref{sec:completion-varieties}. This allows to complete within broken
input that escapes its normal semantic context, e.g.\ antiquotations or
@@ -1322,7 +1322,7 @@
"isabelle.complete"} with keyboard shortcut @{verbatim "C+b"}. This
overrides the shortcut for @{action_ref "complete-word"} in jEdit, but it is
possible to restore the original jEdit keyboard mapping of @{action
- "complete-word"} via \emph{Global Options~/ Shortcuts} and invent a
+ "complete-word"} via \<^emph>\<open>Global Options~/ Shortcuts\<close> and invent a
different one for @{action "isabelle.complete"}.
\<^descr>[Explicit spell-checker completion] works via @{action_ref
@@ -1358,7 +1358,7 @@
subsection \<open>Completion popup \label{sec:completion-popup}\<close>
text \<open>
- A \emph{completion popup} is a minimally invasive GUI component over the
+ A \<^emph>\<open>completion popup\<close> is a minimally invasive GUI component over the
text area that offers a selection of completion items to be inserted into
the text, e.g.\ by mouse clicks. Items are sorted dynamically, according to
the frequency of selection, with persistent history. The popup may interpret
@@ -1373,7 +1373,7 @@
\<^medskip>
\begin{tabular}{ll}
- \textbf{key} & \textbf{action} \\\hline
+ \<^bold>\<open>key\<close> & \<^bold>\<open>action\<close> \\\hline
@{verbatim "ENTER"} & select completion (if @{system_option jedit_completion_select_enter}) \\
@{verbatim "TAB"} & select completion (if @{system_option jedit_completion_select_tab}) \\
@{verbatim "ESCAPE"} & dismiss popup \\
@@ -1397,7 +1397,7 @@
replace text immediately in certain situations and depending on certain
options like @{system_option jedit_completion_immediate}. In any case,
insertion works uniformly, by imitating normal jEdit text insertion,
- depending on the state of the \emph{text selection}. Isabelle/jEdit tries to
+ depending on the state of the \<^emph>\<open>text selection\<close>. Isabelle/jEdit tries to
accommodate the most common forms of advanced selections in jEdit, but not
all combinations make sense. At least the following important cases are
well-defined:
@@ -1416,8 +1416,8 @@
Support for multiple selections is particularly useful for
- \emph{HyperSearch}: clicking on one of the items in the \emph{HyperSearch
- Results} window makes jEdit select all its occurrences in the corresponding
+ \<^emph>\<open>HyperSearch\<close>: clicking on one of the items in the \<^emph>\<open>HyperSearch
+ Results\<close> window makes jEdit select all its occurrences in the corresponding
line of text. Then explicit completion can be invoked via @{verbatim "C+b"},
e.g.\ to replace occurrences of @{verbatim "-->"} by @{text "\<longrightarrow>"}.
@@ -1435,8 +1435,8 @@
text \<open>
This is a summary of Isabelle/Scala system options that are relevant for
- completion. They may be configured in \emph{Plugin Options~/ Isabelle~/
- General} as usual.
+ completion. They may be configured in \<^emph>\<open>Plugin Options~/ Isabelle~/
+ General\<close> as usual.
\<^item> @{system_option_def completion_limit} specifies the maximum number of
items for various semantic completion operations (name-space entries etc.)
@@ -1491,7 +1491,7 @@
text \<open>
Continuous document processing works asynchronously in the background.
Visible document source that has been evaluated may get augmented by
- additional results of \emph{asynchronous print functions}. The canonical
+ additional results of \<^emph>\<open>asynchronous print functions\<close>. The canonical
example is proof state output, which is always enabled. More heavy-weight
print functions may be applied, in order to prove or disprove parts of the
formal text by other means.
@@ -1500,11 +1500,11 @@
on outermost goal statements (e.g.\ @{command lemma}, @{command
theorem}), independently of the state of the current proof attempt.
They work implicitly without any arguments. Results are output as
- \emph{information messages}, which are indicated in the text area by
+ \<^emph>\<open>information messages\<close>, which are indicated in the text area by
blue squiggles and a blue information sign in the gutter (see
\figref{fig:auto-tools}). The message content may be shown as for
other output (see also \secref{sec:output}). Some tools
- produce output with \emph{sendback} markup, which means that
+ produce output with \<^emph>\<open>sendback\<close> markup, which means that
clicking on certain parts of the output inserts that text into the
source in the proper place.
@@ -1519,8 +1519,8 @@
\<^medskip>
The following Isabelle system options control the behavior
of automatically tried tools (see also the jEdit dialog window
- \emph{Plugin Options~/ Isabelle~/ General~/ Automatically tried
- tools}):
+ \<^emph>\<open>Plugin Options~/ Isabelle~/ General~/ Automatically tried
+ tools\<close>):
\<^item> @{system_option_ref auto_methods} controls automatic use of a
combination of standard proof methods (@{method auto}, @{method
@@ -1544,7 +1544,7 @@
@{command_ref quickcheck}, which tests for counterexamples using a
series of assignments for free variables of a subgoal.
- This tool is \emph{enabled} by default. It requires little
+ This tool is \<^emph>\<open>enabled\<close> by default. It requires little
overhead, but is a bit weaker than @{command nitpick}.
\<^item> @{system_option_ref auto_sledgehammer} controls a significantly
@@ -1560,7 +1560,7 @@
can be solved directly by an existing theorem. This also helps to
detect duplicate lemmas.
- This tool is \emph{enabled} by default.
+ This tool is \<^emph>\<open>enabled\<close> by default.
Invocation of automatically tried tools is subject to some global
@@ -1589,7 +1589,7 @@
section \<open>Sledgehammer \label{sec:sledgehammer}\<close>
-text \<open>The \emph{Sledgehammer} panel (\figref{fig:sledgehammer})
+text \<open>The \<^emph>\<open>Sledgehammer\<close> panel (\figref{fig:sledgehammer})
provides a view on some independent execution of the Isar command
@{command_ref sledgehammer}, with process indicator (spinning wheel) and
GUI elements for important Sledgehammer arguments and options. Any
@@ -1605,14 +1605,14 @@
\label{fig:sledgehammer}
\end{figure}
- The \emph{Apply} button attaches a fresh invocation of @{command
+ The \<^emph>\<open>Apply\<close> button attaches a fresh invocation of @{command
sledgehammer} to the command where the cursor is pointing in the
text --- this should be some pending proof problem. Further buttons
- like \emph{Cancel} and \emph{Locate} help to manage the running
+ like \<^emph>\<open>Cancel\<close> and \<^emph>\<open>Locate\<close> help to manage the running
process.
Results appear incrementally in the output window of the panel.
- Proposed proof snippets are marked-up as \emph{sendback}, which
+ Proposed proof snippets are marked-up as \<^emph>\<open>sendback\<close>, which
means a single mouse click inserts the text into a suitable place of
the original source. Some manual editing may be required
nonetheless, say to remove earlier proof attempts.\<close>
@@ -1643,7 +1643,7 @@
\end{figure}
It is also possible to use text folding according to this structure, by
- adjusting \emph{Utilities / Buffer Options / Folding mode} of jEdit. The
+ adjusting \<^emph>\<open>Utilities / Buffer Options / Folding mode\<close> of jEdit. The
default mode @{verbatim isabelle} uses the structure of formal definitions,
statements, and proofs. The alternative mode @{verbatim sidekick} uses the
document structure of the SideKick parser, as explained above.\<close>
@@ -1659,7 +1659,7 @@
The document antiquotation @{text "@{cite}"} is described in @{cite
"isabelle-isar-ref"}. Within the Prover IDE it provides semantic markup for
tooltips, hyperlinks, and completion for Bib{\TeX} database entries.
- Isabelle/jEdit does \emph{not} know about the actual Bib{\TeX} environment
+ Isabelle/jEdit does \<^emph>\<open>not\<close> know about the actual Bib{\TeX} environment
used in {\LaTeX} batch-mode, but it can take citations from those @{verbatim
".bib"} files that happen to be open in the editor; see
\figref{fig:cite-completion}.
@@ -1701,7 +1701,7 @@
influences from the parallel environment that are outside the scope
of the current command transaction.
- The \emph{Timing} panel provides an overview of cumulative command
+ The \<^emph>\<open>Timing\<close> panel provides an overview of cumulative command
timings for each document node. Commands with elapsed time below
the given threshold are ignored in the grand total. Nodes are
sorted according to their overall timing. For the document node
@@ -1715,10 +1715,10 @@
modifier key as explained in \secref{sec:tooltips-hyperlinks}.
Actual display of timing depends on the global option
@{system_option_ref jedit_timing_threshold}, which can be configured in
- \emph{Plugin Options~/ Isabelle~/ General}.
+ \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>.
\<^medskip>
- The \emph{Monitor} panel visualizes various data collections about
+ The \<^emph>\<open>Monitor\<close> panel visualizes various data collections about
recent activity of the Isabelle/ML task farm and the underlying ML runtime
system. The display is continuously updated according to @{system_option_ref
editor_chart_delay}. Note that the painting of the chart takes considerable
@@ -1731,22 +1731,22 @@
section \<open>Low-level output\<close>
text \<open>Prover output is normally shown directly in the main text area
- or secondary \emph{Output} panels, as explained in
+ or secondary \<^emph>\<open>Output\<close> panels, as explained in
\secref{sec:output}.
Beyond this, it is occasionally useful to inspect low-level output
channels via some of the following additional panels:
- \<^item> \emph{Protocol} shows internal messages between the
+ \<^item> \<^emph>\<open>Protocol\<close> shows internal messages between the
Isabelle/Scala and Isabelle/ML side of the PIDE document editing protocol.
Recording of messages starts with the first activation of the
corresponding dockable window; earlier messages are lost.
Actual display of protocol messages causes considerable slowdown, so
- it is important to undock all \emph{Protocol} panels for production
+ it is important to undock all \<^emph>\<open>Protocol\<close> panels for production
work.
- \<^item> \emph{Raw Output} shows chunks of text from the @{verbatim
+ \<^item> \<^emph>\<open>Raw Output\<close> shows chunks of text from the @{verbatim
stdout} and @{verbatim stderr} channels of the prover process.
Recording of output starts with the first activation of the
corresponding dockable window; earlier output is lost.
@@ -1763,14 +1763,14 @@
within the document model (\secref{sec:output}). Unhandled Isabelle/ML
exceptions are printed by the system via @{ML Output.error_message}.
- \<^item> \emph{Syslog} shows system messages that might be relevant to diagnose
+ \<^item> \<^emph>\<open>Syslog\<close> shows system messages that might be relevant to diagnose
problems with the startup or shutdown phase of the prover process; this also
includes raw output on @{verbatim stderr}. Isabelle/ML also provides an
explicit @{ML Output.system_message} operation, which is occasionally useful
for diagnostic purposes within the system infrastructure itself.
A limited amount of syslog messages are buffered, independently of
- the docking state of the \emph{Syslog} panel. This allows to
+ the docking state of the \<^emph>\<open>Syslog\<close> panel. This allows to
diagnose serious problems with Isabelle/PIDE process management,
outside of the actual protocol layer.
@@ -1782,71 +1782,71 @@
chapter \<open>Known problems and workarounds \label{sec:problems}\<close>
text \<open>
- \<^item> \textbf{Problem:} Odd behavior of some diagnostic commands with
+ \<^item> \<^bold>\<open>Problem:\<close> Odd behavior of some diagnostic commands with
global side-effects, like writing a physical file.
- \textbf{Workaround:} Copy/paste complete command text from
+ \<^bold>\<open>Workaround:\<close> Copy/paste complete command text from
elsewhere, or disable continuous checking temporarily.
- \<^item> \textbf{Problem:} No direct support to remove document nodes from the
+ \<^item> \<^bold>\<open>Problem:\<close> No direct support to remove document nodes from the
collection of theories.
- \textbf{Workaround:} Clear the buffer content of unused files and close
- \emph{without} saving changes.
+ \<^bold>\<open>Workaround:\<close> Clear the buffer content of unused files and close
+ \<^emph>\<open>without\<close> saving changes.
- \<^item> \textbf{Problem:} Keyboard shortcuts @{verbatim "C+PLUS"} and
+ \<^item> \<^bold>\<open>Problem:\<close> Keyboard shortcuts @{verbatim "C+PLUS"} and
@{verbatim "C+MINUS"} for adjusting the editor font size depend on
platform details and national keyboards.
- \textbf{Workaround:} Rebind keys via \emph{Global Options~/
- Shortcuts}.
+ \<^bold>\<open>Workaround:\<close> Rebind keys via \<^emph>\<open>Global Options~/
+ Shortcuts\<close>.
- \<^item> \textbf{Problem:} The Mac OS X key sequence @{verbatim
- "COMMAND+COMMA"} for application \emph{Preferences} is in conflict with the
- jEdit default keyboard shortcut for \emph{Incremental Search Bar} (action
+ \<^item> \<^bold>\<open>Problem:\<close> The Mac OS X key sequence @{verbatim
+ "COMMAND+COMMA"} for application \<^emph>\<open>Preferences\<close> is in conflict with the
+ jEdit default keyboard shortcut for \<^emph>\<open>Incremental Search Bar\<close> (action
@{action_ref "quick-search"}).
- \textbf{Workaround:} Rebind key via \emph{Global Options~/
- Shortcuts} according to national keyboard, e.g.\ @{verbatim
+ \<^bold>\<open>Workaround:\<close> Rebind key via \<^emph>\<open>Global Options~/
+ Shortcuts\<close> according to national keyboard, e.g.\ @{verbatim
"COMMAND+SLASH"} on English ones.
- \<^item> \textbf{Problem:} Mac OS X system fonts sometimes lead to
+ \<^item> \<^bold>\<open>Problem:\<close> Mac OS X system fonts sometimes lead to
character drop-outs in the main text area.
- \textbf{Workaround:} Use the default @{verbatim IsabelleText} font.
+ \<^bold>\<open>Workaround:\<close> 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
+ \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus
tend to disrupt key event handling of Java/AWT/Swing.
- \textbf{Workaround:} Do not use X11 input methods. Note that environment
+ \<^bold>\<open>Workaround:\<close> Do not use X11 input methods. Note that environment
variable @{verbatim XMODIFIERS} is reset by default within Isabelle
settings.
- \<^item> \textbf{Problem:} Some Linux/X11 window managers that are
+ \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 window managers that are
not ``re-parenting'' cause problems with additional windows opened
by Java. This affects either historic or neo-minimalistic window
managers like @{verbatim awesome} or @{verbatim xmonad}.
- \textbf{Workaround:} Use a regular re-parenting X11 window manager.
+ \<^bold>\<open>Workaround:\<close> Use a regular re-parenting X11 window manager.
- \<^item> \textbf{Problem:} Various forks of Linux/X11 window managers and
+ \<^item> \<^bold>\<open>Problem:\<close> Various forks of Linux/X11 window managers and
desktop environments (like Gnome) disrupt the handling of menu popups and
mouse positions of Java/AWT/Swing.
- \textbf{Workaround:} Use mainstream versions of Linux desktops.
+ \<^bold>\<open>Workaround:\<close> Use mainstream versions of Linux desktops.
- \<^item> \textbf{Problem:} Native Windows look-and-feel with global font
+ \<^item> \<^bold>\<open>Problem:\<close> Native Windows look-and-feel with global font
scaling leads to bad GUI rendering of various tree views.
- \textbf{Workaround:} Use \emph{Metal} look-and-feel and re-adjust its
+ \<^bold>\<open>Workaround:\<close> Use \<^emph>\<open>Metal\<close> look-and-feel and re-adjust its
primary and secondary font as explained in \secref{sec:hdpi}.
- \<^item> \textbf{Problem:} Full-screen mode via jEdit action @{action_ref
+ \<^item> \<^bold>\<open>Problem:\<close> Full-screen mode via jEdit action @{action_ref
"toggle-full-screen"} (default keyboard 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
+ \<^bold>\<open>Workaround:\<close> Use native full-screen control of the window
manager (notably on Mac OS X).
\<close>