# HG changeset patch # User wenzelm # Date 1444675340 -7200 # Node ID 55e73b352287d2a2c3bb01c00dc09f97937dffc0 # Parent 0d2d399c90a41456d4b784450d01e7b2aa4d3737 more symbols; diff -r 0d2d399c90a4 -r 55e73b352287 src/Doc/JEdit/JEdit.thy --- 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 "\"} & @{verbatim "\\lambda"} & @{verbatim "%"} \\ @@ -558,8 +566,8 @@ @{text "\"} & @{verbatim "\\in"} & @{verbatim ":"} \\ @{text "\"} & @{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.\ @@ -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 "\"} \\ 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 "\"} of the underlying symbol @{verbatim "\"}. @@ -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 "\"}. - \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 "\"}''; 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 "\"}. - \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 \ \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.