--- a/src/Doc/JEdit/JEdit.thy Mon Oct 12 20:31:34 2015 +0200
+++ b/src/Doc/JEdit/JEdit.thy Mon Oct 12 20:42:20 2015 +0200
@@ -87,7 +87,8 @@
entering the Prover IDE. Change of the logic session within Isabelle/jEdit
requires a restart of the whole application.
- \medskip The main job of the Prover IDE is to manage sources and their
+ \<^medskip>
+ The main job of the Prover IDE is to manage sources and their
changes, taking the logical structure as a formal document into account (see
also \secref{sec:document-model}). The editor and the prover are connected
asynchronously in a lock-free manner. The prover is free to organize the
@@ -143,7 +144,8 @@
understanding how it is supposed to work, before loading additional plugins
at a grand scale.
- \medskip The main \emph{Isabelle} plugin is an integral part of
+ \<^medskip>
+ The main \emph{Isabelle} 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
@@ -189,7 +191,8 @@
The jEdit action @{action_def isabelle.options} opens the options dialog for
the Isabelle plugin; it can be mapped to editor GUI elements as usual.
- \medskip Options are usually loaded on startup and saved on shutdown of
+ \<^medskip>
+ Options are usually loaded on startup and saved on shutdown of
Isabelle/jEdit. Editing the machine-generated @{file_unchecked
"$ISABELLE_HOME_USER/jedit/properties"} or @{file_unchecked
"$ISABELLE_HOME_USER/etc/preferences"} manually while the application is
@@ -336,35 +339,37 @@
results on common platforms and medium resolution displays (e.g.\ the ``Full
HD'' category). Subsequently there are further hints to improve on that.
- \medskip The \textbf{operating-system platform} usually provides some
+ \<^medskip>
+ The \textbf{operating-system platform} 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
+ \<^medskip>
+ The Isabelle/jEdit \textbf{application} and its plugins provide
various font properties that are summarized below.
\begin{itemize}
- \item \emph{Global Options / Text Area / Text font}: the main text area
+ \<^item> \emph{Global Options / Text Area / Text font}: 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{Global Options / Gutter / Gutter font}: 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
+ \<^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
(\secref{sec:look-and-feel}), which happens to scale better than newer ones
like \emph{Nimbus}.
- \item \emph{Plugin Options / Isabelle / General / Reset Font Size}: the main
+ \<^item> \emph{Plugin Options / Isabelle / General / Reset Font Size}: 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{Plugin Options / Console / General / Font}: the console window
font, e.g.\ relevant for Isabelle/Scala command-line.
\end{itemize}
@@ -416,21 +421,21 @@
\begin{itemize}
- \item Floating windows are dependent on the main window as \emph{dialog} in
+ \<^item> Floating windows are dependent on the main window as \emph{dialog} 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
dialogs, in contrast to fully independent windows, e.g.\ some window
management functions may be missing.
- \item Keyboard focus of the main view vs.\ a dockable window is carefully
+ \<^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
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
main input field of that panel.
- \item Panels that provide their own text area for output have an additional
+ \<^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
independently of ongoing changes of the PIDE document-model. Note that
@@ -470,7 +475,8 @@
should be restricted to informal parts, e.g.\ to write text in non-latin
alphabets in comments.
- \medskip \paragraph{Encoding.} Technically, the Unicode view on Isabelle
+ \<^medskip>
+ \paragraph{Encoding.} Technically, the Unicode view on Isabelle
symbols is an \emph{encoding} 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
@@ -481,7 +487,8 @@
Reload with Encoding~/ UTF-8-Isabelle} helps to resolve such problems (after
repairing malformed parts of the text).
- \medskip \paragraph{Font.} Correct rendering via Unicode requires a
+ \<^medskip>
+ \paragraph{Font.} 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}, which ensures that
@@ -498,7 +505,8 @@
@{verbatim IsabelleText} in the first place, although it is occasionally
tempting to use the same font in other applications.
- \medskip \paragraph{Input methods.} In principle, Isabelle/jEdit
+ \<^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}. Regular jEdit also provides various ways to
@@ -512,24 +520,24 @@
\begin{enumerate}
- \item The \emph{Symbols} panel: some GUI buttons allow to insert
+ \<^enum> The \emph{Symbols} 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).
- \item Copy/paste from decoded source files: text that is rendered
+ \<^enum> Copy/paste from decoded source files: text that is rendered
as Unicode already can be re-used to produce further text. This
also works between different applications, e.g.\ Isabelle/jEdit and
some web browser or mail client, as long as the same Unicode view on
Isabelle symbols is used.
- \item Copy/paste from prover output within Isabelle/jEdit. The same
+ \<^enum> Copy/paste from prover output within Isabelle/jEdit. The same
principles as for text buffers apply, but note that \emph{copy} 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!
- \item Completion provided by Isabelle plugin (see
+ \<^enum> 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
@@ -540,7 +548,7 @@
The following table is an extract of the information provided by the
standard @{file "$ISABELLE_HOME/etc/symbols"} file:
- \medskip
+ \<^medskip>
\begin{tabular}{lll}
\textbf{symbol} & \textbf{name with backslash} & \textbf{abbreviation} \\\hline
@{text "\<lambda>"} & @{verbatim "\\lambda"} & @{verbatim "%"} \\
@@ -558,8 +566,8 @@
@{text "\<in>"} & @{verbatim "\\in"} & @{verbatim ":"} \\
@{text "\<notin>"} & @{verbatim "\\notin"} & @{verbatim "~:"} \\
\end{tabular}
- \medskip
-
+ \<^medskip>
+
Note that the above abbreviations refer to the input method. The logical
notation provides ASCII alternatives that often coincide, but sometimes
deviate. This occasionally causes user confusion with very old-fashioned
@@ -581,7 +589,7 @@
symbol for each symbol in the text, in order to make the whole text
appear in a certain style.
- \medskip
+ \<^medskip>
\begin{tabular}{llll}
\textbf{style} & \textbf{symbol} & \textbf{shortcut} & \textbf{action} \\\hline
superscript & @{verbatim "\<^sup>"} & @{verbatim "C+e UP"} & @{action_ref "isabelle.control-sup"} \\
@@ -589,8 +597,8 @@
bold face & @{verbatim "\<^bold>"} & @{verbatim "C+e RIGHT"} & @{action_ref "isabelle.control-bold"} \\
reset & & @{verbatim "C+e LEFT"} & @{action_ref "isabelle.control-reset"} \\
\end{tabular}
- \medskip
-
+ \<^medskip>
+
To produce a single control symbol, it is also possible to complete
on @{verbatim "\\"}@{verbatim sup}, @{verbatim "\\"}@{verbatim sub},
@{verbatim "\\"}@{verbatim bold} as for regular symbols.\<close>
@@ -678,7 +686,8 @@
There are special shortcuts: @{file "~"} for @{file "$USER_HOME"} and @{file
"~~"} for @{file "$ISABELLE_HOME"}.
- \medskip Since jEdit happens to support environment variables within file
+ \<^medskip>
+ Since jEdit happens to support environment variables within file
specifications as well, it is natural to use similar notation within the
editor, e.g.\ in the file-browser. This does not work in full generality,
though, due to the bias of jEdit towards platform-specific notation and of
@@ -693,7 +702,8 @@
browser of jEdit also includes \emph{Favorites} for these two important
locations.
- \medskip Path specifications in prover input or output usually include
+ \<^medskip>
+ Path specifications in prover input or output usually include
formal markup that turns it into a hyperlink (see also
\secref{sec:tooltips-hyperlinks}). This allows to open the corresponding
file in the text editor, independently of the path notation.
@@ -730,14 +740,14 @@
determined from the file name extension. The following modes are treated
specifically in Isabelle/jEdit:
- \medskip
+ \<^medskip>
\begin{tabular}{lll}
\textbf{mode} & \textbf{file extension} & \textbf{content} \\\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 \\
\end{tabular}
- \medskip
+ \<^medskip>
All jEdit buffers are automatically added to the PIDE document-model as
\emph{document nodes}. The overall document structure is defined by the
@@ -745,11 +755,11 @@
\begin{enumerate}
- \item via \textbf{theory imports} that are specified in the \emph{theory
+ \<^enum> via \textbf{theory imports} that are specified in the \emph{theory
header} using concrete syntax of the @{command_ref theory} command
@{cite "isabelle-isar-ref"};
- \item via \textbf{auxiliary files} that are loaded into a theory by special
+ \<^enum> via \textbf{auxiliary files} that are loaded into a theory by special
\emph{load commands}, notably @{command_ref ML_file} and @{command_ref
SML_file} @{cite "isabelle-isar-ref"}.
@@ -788,7 +798,8 @@
resolve dependencies automatically, according to the system option
@{system_option jedit_auto_load}.
- \medskip The visible \emph{perspective} of Isabelle/jEdit is defined by the
+ \<^medskip>
+ The visible \emph{perspective} 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
@@ -805,7 +816,8 @@
marked as required can have significant impact on performance,
though.
- \medskip Formal markup of checked theory content is turned into GUI
+ \<^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 underlines, tooltips,
hyperlinks etc. For outer syntax of Isabelle/Isar there is some traditional
@@ -832,7 +844,8 @@
update and process it accordingly: changes of auxiliary file content are
treated as changes of the corresponding load command.
- \medskip As a concession to the massive amount of ML files in Isabelle/HOL
+ \<^medskip>
+ As a concession to the massive amount of ML files in Isabelle/HOL
itself, the content of auxiliary files is only added to the PIDE
document-model on demand, the first time when opened explicitly in the
editor. There are further tricks to manage markup of ML files, such that
@@ -858,7 +871,8 @@
multiple load commands is associated to an arbitrary one: this situation is
morally unsupported and might lead to confusion.
- \medskip Output that refers to an auxiliary file is combined with that of
+ \<^medskip>
+ Output that refers to an auxiliary file is combined with that of
the corresponding load command, and shown whenever the file or the command
are active (see also \secref{sec:output}).
@@ -911,7 +925,8 @@
opens the corresponding text buffer, without changing the cursor
position.
- \medskip In addition, the \emph{Output} panel displays prover
+ \<^medskip>
+ In addition, the \emph{Output} panel displays prover
messages that correspond to a given command, within a separate
window.
@@ -936,7 +951,8 @@
special messages for \emph{tracing} or \emph{proof state} only
appear here, and are not attached to the original source.
- \medskip In any case, prover messages also contain markup that may
+ \<^medskip>
+ In any case, prover messages also contain markup that may
be explored recursively via tooltips or hyperlinks (see
\secref{sec:tooltips-hyperlinks}), or clicked directly to initiate
certain actions (see \secref{sec:auto-tools} and
@@ -967,22 +983,23 @@
\label{fig:query}
\end{figure}
- \medskip The following GUI elements are common to all query modes:
+ \<^medskip>
+ The following GUI elements are common to all query modes:
\begin{itemize}
- \item The spinning wheel provides feedback about the status of a pending
+ \<^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{Apply} 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{Search} 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{Zoom} box controls the font size of the output area.
\end{itemize}
@@ -1077,7 +1094,8 @@
\emph{all} popups, which is particularly relevant when nested
tooltips are stacking up.
- \medskip A black rectangle in the text indicates a hyperlink that may be
+ \<^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
@@ -1101,7 +1119,8 @@
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
+ \<^medskip>
+ \emph{Explicit completion} 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"}.
@@ -1109,7 +1128,8 @@
\emph{Implicit completion} 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~/
+ \<^medskip>
+ Completion options may be configured in \emph{Plugin Options~/
Isabelle~/ General~/ Completion}. These are explained in further detail
below, whenever relevant. There is also a summary of options in
\secref{sec:completion-options}.
@@ -1186,14 +1206,14 @@
@{file_unchecked "$ISABELLE_HOME_USER/etc/symbols"} for each symbol
specification as follows:
- \medskip
+ \<^medskip>
\begin{tabular}{ll}
\textbf{completion entry} & \textbf{example} \\\hline
literal symbol & @{verbatim "\<forall>"} \\
symbol name with backslash & @{verbatim "\\"}@{verbatim forall} \\
symbol abbreviation & @{verbatim "ALL"} or @{verbatim "!"} \\
\end{tabular}
- \medskip
+ \<^medskip>
When inserted into the text, the above examples all produce the same Unicode
rendering @{text "\<forall>"} of the underlying symbol @{verbatim "\<forall>"}.
@@ -1203,7 +1223,8 @@
are inserted more aggressively, except for single-character abbreviations
like @{verbatim "!"} above.
- \medskip Symbol completion depends on the semantic language context
+ \<^medskip>
+ Symbol completion depends on the semantic language context
(\secref{sec:completion-context}), to enable or disable that aspect for a
particular sub-language of Isabelle. For example, symbol completion is
suppressed within document source to avoid confusion with {\LaTeX} macros
@@ -1263,7 +1284,7 @@
the user that some action may be taken. The jEdit context menu provides
various actions, as far as applicable:
- \medskip
+ \<^medskip>
\begin{tabular}{l}
@{action_ref "isabelle.complete-word"} \\
@{action_ref "isabelle.exclude-word"} \\
@@ -1271,13 +1292,14 @@
@{action_ref "isabelle.include-word"} \\
@{action_ref "isabelle.include-word-permanently"} \\
\end{tabular}
- \medskip
+ \<^medskip>
Instead of the specific @{action_ref "isabelle.complete-word"}, it is also
possible to use the generic @{action_ref "isabelle.complete"} with its
default keyboard shortcut @{verbatim "C+b"}.
- \medskip Dictionary lookup uses some educated guesses about lower-case,
+ \<^medskip>
+ Dictionary lookup uses some educated guesses about lower-case,
upper-case, and capitalized words. This is oriented on common use in
English, where this aspect is not decisive for proper spelling, in contrast
to German, for example.
@@ -1304,7 +1326,8 @@
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
+ \<^medskip>
+ The completion context is \emph{ignored} 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
@@ -1337,24 +1360,24 @@
\begin{enumerate}
- \item The system option @{system_option_ref jedit_completion} needs to
+ \<^enum> The system option @{system_option_ref jedit_completion} needs to
be enabled (default).
- \item Completion of syntax keywords requires at least 3 relevant
+ \<^enum> Completion of syntax keywords requires at least 3 relevant
characters in the text.
- \item The system option @{system_option_ref jedit_completion_delay}
+ \<^enum> The system option @{system_option_ref jedit_completion_delay}
determines an additional delay (0.5 by default), before opening a completion
popup. The delay gives the prover a chance to provide semantic completion
information, notably the context (\secref{sec:completion-context}).
- \item The system option @{system_option_ref jedit_completion_immediate}
+ \<^enum> The system option @{system_option_ref jedit_completion_immediate}
(enabled by default) controls whether replacement text should be inserted
immediately without popup, regardless of @{system_option
jedit_completion_delay}. This aggressive mode of completion is restricted to
Isabelle symbols and their abbreviations (\secref{sec:symbols}).
- \item Completion of symbol abbreviations with only one relevant
+ \<^enum> Completion of symbol abbreviations with only one relevant
character in the text always enforces an explicit popup,
regardless of @{system_option_ref jedit_completion_immediate}.
@@ -1380,7 +1403,7 @@
The meaning of special keys is as follows:
- \medskip
+ \<^medskip>
\begin{tabular}{ll}
\textbf{key} & \textbf{action} \\\hline
@{verbatim "ENTER"} & select completion (if @{system_option jedit_completion_select_enter}) \\
@@ -1391,7 +1414,7 @@
@{verbatim "PAGE_UP"} & move up one page of items \\
@{verbatim "PAGE_DOWN"} & move down one page of items \\
\end{tabular}
- \medskip
+ \<^medskip>
Movement within the popup is only active for multiple items.
Otherwise the corresponding key event retains its standard meaning
@@ -1433,7 +1456,8 @@
line of text. Then explicit completion can be invoked via @{verbatim "C+b"},
e.g.\ to replace occurrences of @{verbatim "-->"} by @{text "\<longrightarrow>"}.
- \medskip Insertion works by removing and inserting pieces of text from the
+ \<^medskip>
+ Insertion works by removing and inserting pieces of text from the
buffer. This counts as one atomic operation on the jEdit history. Thus
unintended completions may be reverted by the regular @{action undo} action
of jEdit. According to normal jEdit policies, the recovered text after
@@ -1451,25 +1475,25 @@
\begin{itemize}
- \item @{system_option_def completion_limit} specifies the maximum number of
+ \<^item> @{system_option_def completion_limit} specifies the maximum number of
items for various semantic completion operations (name-space entries etc.)
- \item @{system_option_def jedit_completion} guards implicit completion via
+ \<^item> @{system_option_def jedit_completion} guards implicit completion via
regular jEdit key events (\secref{sec:completion-input}): it allows to
disable implicit completion altogether.
- \item @{system_option_def jedit_completion_select_enter} and
+ \<^item> @{system_option_def jedit_completion_select_enter} and
@{system_option_def jedit_completion_select_tab} enable keys to select a
completion item from the popup (\secref{sec:completion-popup}). Note that a
regular mouse click on the list of items is always possible.
- \item @{system_option_def jedit_completion_context} specifies whether the
+ \<^item> @{system_option_def jedit_completion_context} specifies whether the
language context provided by the prover should be used at all. Disabling
that option makes completion less ``semantic''. Note that incomplete or
severely broken input may cause some disagreement of the prover and the user
about the intended language context.
- \item @{system_option_def jedit_completion_delay} and @{system_option_def
+ \<^item> @{system_option_def jedit_completion_delay} and @{system_option_def
jedit_completion_immediate} determine the handling of keyboard events for
implicit completion (\secref{sec:completion-input}).
@@ -1479,21 +1503,21 @@
"= true"} means that abbreviations of Isabelle symbols are handled
nonetheless.
- \item @{system_option_def jedit_completion_path_ignore} specifies ``glob''
+ \<^item> @{system_option_def jedit_completion_path_ignore} specifies ``glob''
patterns to ignore in file-system path completion (separated by colons),
e.g.\ backup files ending with tilde.
- \item @{system_option_def spell_checker} is a global guard for all
+ \<^item> @{system_option_def spell_checker} is a global guard for all
spell-checker operations: it allows to disable that mechanism altogether.
- \item @{system_option_def spell_checker_dictionary} determines the current
+ \<^item> @{system_option_def spell_checker_dictionary} determines the current
dictionary, taken from the colon-separated list in the settings variable
@{setting_def JORTHO_DICTIONARIES}. There are jEdit actions to specify local
updates to a dictionary, by including or excluding words. The result of
permanent dictionary updates is stored in the directory @{file_unchecked
"$ISABELLE_HOME_USER/dictionaries"}, in a separate file for each dictionary.
- \item @{system_option_def spell_checker_elements} specifies a
+ \<^item> @{system_option_def spell_checker_elements} specifies a
comma-separated list of markup elements that delimit words in the source
that is subject to spell-checking, including various forms of comments.
@@ -1531,14 +1555,15 @@
\label{fig:auto-tools}
\end{figure}
- \medskip The following Isabelle system options control the behavior
+ \<^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}):
\begin{itemize}
- \item @{system_option_ref auto_methods} controls automatic use of a
+ \<^item> @{system_option_ref auto_methods} controls automatic use of a
combination of standard proof methods (@{method auto}, @{method
simp}, @{method blast}, etc.). This corresponds to the Isar command
@{command_ref "try0"} @{cite "isabelle-isar-ref"}.
@@ -1547,7 +1572,7 @@
standard proof methods often consumes substantial CPU resources
without leading to success.
- \item @{system_option_ref auto_nitpick} controls a slightly reduced
+ \<^item> @{system_option_ref auto_nitpick} controls a slightly reduced
version of @{command_ref nitpick}, which tests for counterexamples using
first-order relational logic. See also the Nitpick manual
@{cite "isabelle-nitpick"}.
@@ -1556,14 +1581,14 @@
invoking an external Java process for each attempt to disprove a
subgoal.
- \item @{system_option_ref auto_quickcheck} controls automatic use of
+ \<^item> @{system_option_ref auto_quickcheck} controls automatic use of
@{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
overhead, but is a bit weaker than @{command nitpick}.
- \item @{system_option_ref auto_sledgehammer} controls a significantly
+ \<^item> @{system_option_ref auto_sledgehammer} controls a significantly
reduced version of @{command_ref sledgehammer}, which attempts to prove
a subgoal using external automatic provers. See also the
Sledgehammer manual @{cite "isabelle-sledgehammer"}.
@@ -1571,7 +1596,7 @@
This tool is disabled by default, due to the relatively heavy nature
of Sledgehammer.
- \item @{system_option_ref auto_solve_direct} controls automatic use of
+ \<^item> @{system_option_ref auto_solve_direct} controls automatic use of
@{command_ref solve_direct}, which checks whether the current subgoals
can be solved directly by an existing theorem. This also helps to
detect duplicate lemmas.
@@ -1585,10 +1610,10 @@
\begin{itemize}
- \item @{system_option_ref auto_time_limit} (default 2.0) determines the
+ \<^item> @{system_option_ref auto_time_limit} (default 2.0) determines the
timeout (in seconds) for each tool execution.
- \item @{system_option_ref auto_time_start} (default 1.0) determines the
+ \<^item> @{system_option_ref auto_time_start} (default 1.0) determines the
start delay (in seconds) for automatically tried tools, after the
main command evaluation is finished.
@@ -1737,7 +1762,8 @@
@{system_option_ref jedit_timing_threshold}, which can be configured in
\emph{Plugin Options~/ Isabelle~/ General}.
- \medskip The \emph{Monitor} panel visualizes various data collections about
+ \<^medskip>
+ The \emph{Monitor} 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
@@ -1758,7 +1784,7 @@
\begin{itemize}
- \item \emph{Protocol} shows internal messages between the
+ \<^item> \emph{Protocol} 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.
@@ -1767,7 +1793,7 @@
it is important to undock all \emph{Protocol} panels for production
work.
- \item \emph{Raw Output} shows chunks of text from the @{verbatim
+ \<^item> \emph{Raw Output} 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.
@@ -1784,7 +1810,7 @@
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{Syslog} 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
@@ -1807,26 +1833,26 @@
text \<open>
\begin{itemize}
- \item \textbf{Problem:} Odd behavior of some diagnostic commands with
+ \<^item> \textbf{Problem:} Odd behavior of some diagnostic commands with
global side-effects, like writing a physical file.
\textbf{Workaround:} 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> \textbf{Problem:} 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.
- \item \textbf{Problem:} Keyboard shortcuts @{verbatim "C+PLUS"} and
+ \<^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:} Rebind keys via \emph{Global Options~/
Shortcuts}.
- \item \textbf{Problem:} The Mac OS X key sequence @{verbatim
+ \<^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
@{action_ref "quick-search"}).
@@ -1835,39 +1861,39 @@
Shortcuts} according to national keyboard, e.g.\ @{verbatim
"COMMAND+SLASH"} on English ones.
- \item \textbf{Problem:} Mac OS X system fonts sometimes lead to
+ \<^item> \textbf{Problem:} Mac OS X system fonts sometimes lead to
character drop-outs in the main text area.
\textbf{Workaround:} 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> \textbf{Problem:} 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
variable @{verbatim XMODIFIERS} is reset by default within Isabelle
settings.
- \item \textbf{Problem:} Some Linux/X11 window managers that are
+ \<^item> \textbf{Problem:} 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.
- \item \textbf{Problem:} Various forks of Linux/X11 window managers and
+ \<^item> \textbf{Problem:} 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.
- \item \textbf{Problem:} Native Windows look-and-feel with global font
+ \<^item> \textbf{Problem:} 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
primary and secondary font as explained in \secref{sec:hdpi}.
- \item \textbf{Problem:} Full-screen mode via jEdit action @{action_ref
+ \<^item> \textbf{Problem:} 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.