1 (*:wrap=hard:maxLineLen=78:*)
7 chapter {* Introduction *}
9 section {* Concepts and terminology *}
11 text {* Isabelle/jEdit is a Prover IDE that integrates \emph{parallel
12 proof checking} \cite{Wenzel:2009,Wenzel:2013:ITP} with
13 \emph{asynchronous user interaction}
14 \cite{Wenzel:2010,Wenzel:2012:UITP-EPTCS}, based on a
15 document-oriented approach to \emph{continuous proof processing}
16 \cite{Wenzel:2011:CICM,Wenzel:2012}. Many concepts and system
17 components are fit together in order to make this work. The main
18 building blocks are as follows.
22 \item [PIDE] is a general framework for Prover IDEs based on
23 Isabelle/Scala. It is built around a concept of parallel and
24 asynchronous document processing, which is supported natively by the
25 parallel proof engine that is implemented in Isabelle/ML. The prover
26 discontinues the traditional TTY-based command loop, and supports
27 direct editing of formal source text with rich formal markup for GUI
30 \item [Isabelle/ML] is the implementation and extension language of
31 Isabelle, see also \cite{isabelle-implementation}. It is integrated
32 into the logical context of Isabelle/Isar and allows to manipulate
33 logical entities directly. Arbitrary add-on tools may be implemented
34 for object-logics such as Isabelle/HOL.
36 \item [Isabelle/Scala] is the system programming language of
37 Isabelle. It extends the pure logical environment of Isabelle/ML
38 towards the ``real world'' of graphical user interfaces, text
39 editors, IDE frameworks, web services etc. Special infrastructure
40 allows to transfer algebraic datatype values and formatted text
41 easily between ML and Scala, using asynchronous protocol commands.
43 \item [jEdit] is a sophisticated text editor implemented in
44 Java.\footnote{\url{http://www.jedit.org}} It is easily extensible
45 by plugins written in languages that work on the JVM, e.g.\
46 Scala\footnote{\url{http://www.scala-lang.org/}}.
48 \item [Isabelle/jEdit] is the main example application of the PIDE
49 framework and the default user-interface for Isabelle. It targets
50 both beginners and experts. Technically, Isabelle/jEdit combines a
51 slightly modified version of the official jEdit code base with a
52 special plugin for Isabelle, integrated as standalone application
53 for the main operating system platforms: Linux, Windows, Mac OS X.
57 The subtle differences of Isabelle/ML versus Standard ML,
58 Isabelle/Scala versus Scala, Isabelle/jEdit versus jEdit need to be
59 taken into account when discussing any of these PIDE building blocks
60 in public forums, mailing lists, or even scientific publications.
64 section {* The Isabelle/jEdit Prover IDE *}
69 \includegraphics[width=\textwidth]{isabelle-jedit}
71 \caption{The Isabelle/jEdit Prover IDE}
72 \label{fig:isabelle-jedit}
75 Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some
76 plugins for the well-known jEdit text editor
77 \url{http://www.jedit.org}, according to the following principles.
81 \item The original jEdit look-and-feel is generally preserved,
82 although some default properties are changed to accommodate Isabelle
83 (e.g.\ the text area font).
85 \item Formal Isabelle/Isar text is checked asynchronously while
86 editing. The user is in full command of the editor, and the prover
87 refrains from locking portions of the buffer.
89 \item Prover feedback works via colors, boxes, squiggly underline,
90 hyperlinks, popup windows, icons, clickable output --- all based on
91 semantic markup produced by Isabelle in the background.
93 \item Using the mouse together with the modifier key @{verbatim
94 CONTROL} (Linux, Windows) or @{verbatim COMMAND} (Mac OS X) exposes
95 additional formal content via tooltips and/or hyperlinks.
97 \item Formal output (in popups etc.) may be explored recursively,
98 using the same techniques as in the editor source buffer.
100 \item Additional panels (e.g.\ \emph{Output}, \emph{Symbols}) are
101 organized by the Dockable Window Manager of jEdit, which also allows
102 multiple floating instances of each window class.
104 \item The prover process and source files are managed on the editor
105 side. The prover operates on timeless and stateless document
106 content as provided via Isabelle/Scala.
108 \item Plugin options of jEdit (for the \emph{Isabelle} plugin) give
109 access to a selection of Isabelle/Scala options and its persistent
110 preferences, usually with immediate effect on the prover back-end or
113 \item The logic image of the prover session may be specified within
114 Isabelle/jEdit. The new image is provided automatically by the
115 Isabelle build tool after restart of the application.
121 subsection {* Documentation *}
123 text {* Regular jEdit documentation is accessible via its @{verbatim
124 Help} menu or @{verbatim F1} keyboard shortcut. This includes a full
125 \emph{User's Guide} and \emph{Frequently Asked Questions} for this
126 sophisticated text editor.
128 Most of this information about jEdit is relevant for Isabelle/jEdit
129 as well, but one needs to keep in mind that defaults sometimes
130 differ, and the official jEdit documentation does not know about the
131 Isabelle plugin with its special support for theory editing.
135 subsection {* Plugins *}
137 text {* The \emph{Plugin Manager} of jEdit allows to augment editor
138 functionality by JVM modules (jars) that are provided by the central
139 plugin repository, which is accessible by various mirror sites.
141 Connecting to the plugin server infrastructure of the jEdit project
142 allows to update bundled plugins or to add further functionality.
143 This needs to be done with the usual care for such an open bazaar of
144 contributions. Arbitrary combinations of add-on features are apt to
145 cause problems. It is advisable to start with the default
146 configuration of Isabelle/jEdit and develop some understanding how
147 it is supposed to work, before loading additional plugins at a grand
150 \medskip The main \emph{Isabelle} plugin is an integral part of
151 Isabelle/jEdit and needs to remain active at all times! A few
152 additional plugins are bundled with Isabelle/jEdit for convenience
153 or out of necessity, notably \emph{Console} with its Isabelle/Scala
154 sub-plugin and \emph{SideKick} with some Isabelle-specific parsers
155 for document tree structure. The \emph{ErrorList} plugin is
156 required by \emph{SideKick}, but not used specifically in
160 subsection {* Options *}
162 text {* Both jEdit and Isabelle have distinctive management of
165 Regular jEdit options are accessible via the dialogs for
166 \emph{Global Options} and \emph{Plugin Options}. Changed properties
167 are stored eventually in @{verbatim
168 "$ISABELLE_HOME_USER/jedit/properties"}. In contrast, Isabelle
169 system options are managed by Isabelle/Scala and changes stored in
170 @{verbatim "$ISABELLE_HOME_USER/etc/preferences"}, independently of
171 the jEdit properties. See also \cite{isabelle-sys}, especially the
172 coverage of sessions and command-line tools like @{tool build} or
175 Those Isabelle options that are declared as \textbf{public} are
176 configurable in jEdit via \emph{Plugin Options / Isabelle /
177 General}. Moreover, there are various options for rendering of
178 document content, which are configurable via \emph{Plugin Options /
179 Isabelle / Rendering}. Thus \emph{Plugin Options / Isabelle} in
180 jEdit provides a view on certain Isabelle options. Note that some
181 of these options affect general parameters that are relevant outside
182 Isabelle/jEdit as well, e.g.\ @{system_option threads} or
183 @{system_option parallel_proofs} for the Isabelle build tool
186 \medskip All options are loaded on startup and saved on shutdown of
187 Isabelle/jEdit. Editing the machine-generated files @{verbatim
188 "$ISABELLE_HOME_USER/jedit/properties"} or @{verbatim
189 "$ISABELLE_HOME_USER/etc/preferences"} manually while the
190 application is running is likely to cause surprise due to lost
194 subsection {* Keymaps *}
196 text {* Keyboard shortcuts used to be managed as jEdit properties in
197 the past, but recent versions (2013) have a separate concept of
198 \emph{keymap} that is configurable via \emph{Global Options /
199 Shortcuts}. The @{verbatim imported} keymap is derived from the
200 initial environment of properties that is available at the first
201 start of the editor; afterwards the keymap file takes precedence.
203 This is relevant for Isabelle/jEdit due to various fine-tuning of
204 default properties, and additional keyboard shortcuts for Isabelle
205 specific functionality. Users may change their keymap, but need to
206 copy Isabelle-specific key bindings manually. *}
209 subsection {* Look-and-feel *}
211 text {* jEdit is a Java/AWT/Swing application with some ambition to
212 support ``native'' look-and-feel on all platforms, within the limits
213 of what Oracle as Java provider and major operating system
214 distributors allow (see also \secref{sec:problems}).
216 Isabelle/jEdit enables platform-specific look-and-feel by default as
221 \item[Linux] The platform-independent \emph{Nimbus} is used by
222 default, but the classic \emph{Metal} also works. \emph{GTK+} works
223 under the side-condition that the overall GTK theme is selected in a
224 Swing-friendly way.\footnote{GTK support in Java/Swing was once
225 marketed aggressively by Sun, but never quite finished, and is today
226 (2013) lagging a bit behind further development of Swing and GTK.}
228 \item[Windows] Regular \emph{Windows} is used by default, but
229 platform-independent \emph{Nimbus} and \emph{Metal} also work.
231 \item[Mac OS X] Regular \emph{Mac OS X} is used by default, but
232 platform-independent \emph{Nimbus} and \emph{Metal} also work.
233 Moreover the bundled \emph{MacOSX} plugin provides various functions
234 that are expected from applications on that particular platform:
235 quit from menu or dock, preferences menu, drag-and-drop of text
236 files on the application, full-screen mode for main editor windows
241 Users may experiment with different look-and-feels, but need to keep
242 in mind that this extra variance of GUI functionality is unlikely to
243 work in arbitrary combinations. The historic \emph{CDE/Motif} is
244 better avoided. After changing the look-and-feel in \emph{Global
245 Options / Appearance}, it is advisable to restart Isabelle/jEdit in
246 order to take full effect. *}
249 subsection {* File-system access *}
251 text {* File specifications in jEdit follow various formats and
252 conventions according to \emph{Virtual File Systems}, which may be
253 also provided by additional plugins. This allows to access remote
254 files via the @{verbatim "http:"} protocol prefix, for example.
255 Isabelle/jEdit attempts to work with the file-system access model of
256 jEdit as far as possible. In particular, theory sources are passed
257 directly from the editor to the prover, without indirection via
260 Despite the flexibility of URLs in jEdit, local files are
261 particularly important and are accessible without protocol prefix.
262 Here the path notation is that of the Java Virtual Machine on the
263 underlying platform. On Windows the preferred form uses
264 backslashes, but happens to accept Unix/POSIX forward slashes, too.
265 Further differences arise due to drive letters and network shares.
267 The Java notation for files needs to be distinguished from the one
268 of Isabelle, which uses POSIX notation with forward slashes on
269 \emph{all} platforms.\footnote{Isabelle on Windows uses Cygwin
270 file-system access.} Moreover, environment variables from the
271 Isabelle process may be used freely, e.g.\ @{file
272 "$ISABELLE_HOME/etc/symbols"} or @{file
273 "$ISABELLE_JDK_HOME/README.html"}. There are special shortcuts:
274 @{verbatim "~"} for @{file "$USER_HOME"}, and @{verbatim "~~"} for
275 @{file "$ISABELLE_HOME"}.
277 \medskip Since jEdit happens to support environment variables within
278 file specifications as well, it is natural to use similar notation
279 within the editor, e.g.\ in the file-browser. This does not work in
280 full generality, though, due to the bias of jEdit towards
281 platform-specific notation and of Isabelle towards POSIX. Moreover,
282 the Isabelle settings environment is not yet active when starting
283 Isabelle/jEdit via its standard application wrapper (in contrast to
284 @{verbatim "isabelle jedit"} run from the command line).
286 For convenience, Isabelle/jEdit imitates at least @{verbatim
287 "$ISABELLE_HOME"} and @{verbatim "$ISABELLE_HOME_USER"} within the
288 Java process environment, in order to allow easy access to these
289 important places from the editor.
291 Moreover note that path specifications in prover input or output
292 usually include formal markup that turns it into a hyperlink (see
293 also \secref{sec:tooltips-hyperlinks}). This allows to open the
294 corresponding file in the text editor, independently of the path
298 chapter {* Prover IDE functionality *}
300 section {* Text buffers and theories \label{sec:buffers-theories} *}
302 text {* As regular text editor, jEdit maintains a collection of open
303 \emph{text buffers} to store source files; each buffer may be
304 associated with any number of visible \emph{text areas}. Buffers
305 are subject to an \emph{edit mode} that is determined from the file
306 type. Files with extension \texttt{.thy} are assigned to the mode
307 \emph{isabelle} and treated specifically.
309 \medskip Isabelle theory files are automatically added to the formal
310 document model of Isabelle/Scala, which maintains a family of
311 versions of all sources for the prover. The \emph{Theories} panel
312 provides an overview of the status of continuous checking of theory
313 sources. Unlike batch sessions \cite{isabelle-sys}, theory nodes
314 are identified by full path names; this allows to work with multiple
315 (disjoint) Isabelle sessions simultaneously within the same editor
318 Certain events to open or update buffers with theory files cause
319 Isabelle/jEdit to resolve dependencies of \emph{theory imports}.
320 The system requests to load additional files into editor buffers, in
321 order to be included in the theory document model for further
322 checking. It is also possible to resolve dependencies
323 automatically, depending on \emph{Plugin Options / Isabelle /
324 General / Auto load} (Isabelle system option @{system_option
327 \medskip The open text area views on theory buffers define the
328 visible \emph{perspective} of Isabelle/jEdit. This is taken as a
329 hint for document processing: the prover ensures that those parts of
330 a theory where the user is looking are checked, while other parts
331 that are presently not required are ignored. The perspective is
332 changed by opening or closing text area windows, or scrolling within
335 The \emph{Theories} panel provides some further options to influence
336 the process of continuous checking: it may be switched off globally
337 to restrict the prover to superficial processing of command syntax.
338 It is also possible to indicate theory nodes as \emph{required} for
339 continuous checking: this means such nodes and all their imports are
340 always processed independently of the visibility status (if
341 continuous checking is enabled). Big theory libraries that are
342 marked as required can have significant impact on performance,
345 \medskip Formal markup of checked theory content is turned into GUI
346 rendering, based on a standard repertoire known from IDEs for
347 programming languages: colors, icons, highlighting, squiggly
348 underline, tooltips, hyperlinks etc. For outer syntax of
349 Isabelle/Isar there is some traditional syntax-highlighting via
350 static keyword tables and tokenization within the editor. In
351 contrast, the painting of inner syntax (term language etc.)\ uses
352 semantic information that is reported dynamically from the logical
353 context. Thus the prover can provide additional markup to help the
354 user to understand the meaning of formal text, and to produce more
355 text with some add-on tools (e.g.\ information messages by automated
356 provers or disprovers running in the background).
360 section {* Prover output \label{sec:prover-output} *}
362 text {* Prover output consists of \emph{markup} and \emph{messages}.
363 Both are directly attached to the corresponding positions in the
364 original source text, and visualized in the text area, e.g.\ as text
365 colours for free and bound variables, or as squiggly underline for
366 warnings, errors etc.\ (see also \figref{fig:output}). In the
367 latter case, the corresponding messages are shown by hovering with
368 the mouse over the highlighted text --- although in many situations
369 the user should already get some clue by looking at the text
374 \includegraphics[scale=0.3]{output}
376 \caption{Multiple views on prover output: gutter area, text area
377 with popup, overview area, Theories panel, Output panel}
381 The ``gutter area'' on the left-hand-side of the text area uses
382 icons to provide a summary of the messages within the corresponding
383 line of text. Message priorities are used to prefer errors over
384 warnings, warnings over information messages etc. Plain output is
387 The ``overview area'' on the right-hand-side of the text area uses
388 similar information to paint small rectangles for the overall status
389 of the whole text buffer. The graphics is scaled to fit the logical
390 buffer length into the given window height. Mouse clicks on the
391 overview area position the cursor approximately to the corresponding
392 line of text in the buffer.
394 Another course-grained overview is provided by the \emph{Theories}
395 panel (\secref{sec:buffers-theories}), but without direct
396 correspondence to text positions. A double-click on one of the
397 theory entries with their status overview opens the corresponding
398 text buffer, without changing the cursor position.
400 \medskip In addition, the \emph{Output} panel displays prover
401 messages that correspond to a given command, within a separate
404 The cursor position in the presently active text area determines the
405 prover commands whose cumulative message output is appended an shown
406 in that window (in canonical order according to the processing of
407 the command). There are also control elements to modify the update
408 policy of the output wrt.\ continued editor movements. This is
409 particularly useful with several independent instances of the
410 \emph{Output} panel, which the Dockable Window Manager of jEdit can
413 Former users of the old TTY interaction model (e.g.\ Proof~General)
414 might find a separate window for prover messages familiar, but it is
415 important to understand that the main Prover IDE feedback happens
416 elsewhere. It is possible to do meaningful proof editing
417 efficiently while using the secondary window only rarely.
419 The main purpose of the output window is to ``debug'' unclear
420 situations by inspecting internal state of the prover.\footnote{In
421 that sense, unstructured tactic scripts depend on continuous
422 debugging with internal state inspection.} Consequently, some
423 special messages for \emph{tracing} or \emph{proof state} only
424 appear here, and are not attached to the original source.
426 \medskip In any case, prover messages also contain markup that may
427 be explored recursively via tooltips or hyperlinks (see
428 \secref{sec:tooltips-hyperlinks}), or clicked directly to initiate
429 certain actions (see \secref{sec:auto-tools} and
430 \secref{sec:sledgehammer}). *}
433 section {* Tooltips and hyperlinks \label{sec:tooltips-hyperlinks} *}
435 text {* Formally processed text (prover input or output) contains rich
436 markup information that can be explored further by using the
437 @{verbatim CONTROL} modifier key on Linux and Windows, or @{verbatim
438 COMMAND} on Mac OS X. Hovering with the mouse while the modifier is
439 pressed reveals a \emph{tooltip} (grey box over the text with a
440 yellow popup) and/or a \emph{hyperlink} (black rectangle over the
441 text); see also \figref{fig:tooltip}.
445 \includegraphics[scale=0.5]{popup1}
447 \caption{Tooltip and hyperlink for some formal entity}
451 Tooltip popups use the same rendering principles as the main text
452 area, and further tooltips and/or hyperlinks may be exposed
453 recursively by the same mechanism; see \figref{fig:nested-tooltips}.
457 \includegraphics[scale=0.5]{popup2}
459 \caption{Nested tooltips over formal entities}
460 \label{fig:nested-tooltips}
463 The tooltip popup window provides some controls to \emph{close} or
464 \emph{detach} the window, turning it into a separate \emph{Info}
465 dockable window managed by jEdit. The @{verbatim ESCAPE} key closes
466 \emph{all} popups, which is particularly relevant when nested
467 tooltips are stacking up.
469 \medskip A black rectangle in the text indicates a hyperlink that
470 may be followed by a mouse click (while the @{verbatim CONTROL} or
471 @{verbatim COMMAND} modifier key is still pressed). Presently (2013)
472 there is no systematic way to return to the original location within
475 Also note that the link target may be a file that is itself not
476 subject to formal document processing of the editor session and thus
477 prevents further exploration: the chain of hyperlinks may end in
478 some source file of the underlying logic image, even within the
479 Isabelle/ML bootstrap sources of Isabelle/Pure, where the formal
480 markup is less detailed. *}
483 section {* Isabelle symbols *}
485 text {* Isabelle sources consist of \emph{symbols} that extend plain
486 ASCII to allow infinitely many mathematical symbols within the
487 formal sources. This works without depending on particular
488 encodings or varying Unicode standards
489 \cite{Wenzel:2011:CICM}.\footnote{Raw Unicode characters within
490 formal sources would compromise portability and reliability in the
491 face of changing interpretation of various unexpected features of
494 For the prover back-end, formal text consists of ASCII characters
495 that are grouped according to some simple rules, e.g.\ as plain
496 ``@{verbatim a}'' or symbolic ``@{verbatim "\<alpha>"}''.
498 For the editor front-end, a certain subset of symbols is rendered
499 physically via Unicode glyphs, in order to show ``@{verbatim "\<alpha>"}''
500 as ``@{text "\<alpha>"}'', for example. This symbol interpretation is
501 specified by the Isabelle system distribution in @{file
502 "$ISABELLE_HOME/etc/symbols"} and may be augmented by the user in
503 @{verbatim "$ISABELLE_HOME_USER/etc/symbols"}.
505 The appendix of \cite{isabelle-isar-ref} gives an overview of the
506 standard interpretation of finitely many symbols from the infinite
507 collection. Uninterpreted symbols are displayed literally, e.g.\
508 ``@{verbatim "\<foobar>"}''. Overlap of Unicode characters used in
509 symbol interpretation with informal ones that might appear e.g.\ in
510 comments needs to be avoided!
512 \medskip \paragraph{Encoding.} Technically, the Unicode view on
513 Isabelle symbols is an \emph{encoding} in jEdit (not in the
514 underlying JVM) that is called @{verbatim "UTF-8-Isabelle"}. It is
515 provided by the Isabelle/jEdit plugin and enabled by default for all
516 source files. Sometimes such defaults are reset accidentally, or
517 malformed UTF-8 sequences in the text force jEdit to fall back on a
518 different encoding like @{verbatim "ISO-8859-15"}. In that case,
519 verbatim ``@{verbatim "\<alpha>"}'' will be shown in the text buffer
520 instead of its Unicode rendering ``@{text "\<alpha>"}''. The jEdit menu
521 operation \emph{File / Reload with Encoding / UTF-8-Isabelle} helps
522 to resolve such problems, potentially after repairing malformed
525 \medskip \paragraph{Font.} Correct rendering via Unicode requires a
526 font that contains glyphs for the corresponding codepoints. Most
527 system fonts lack that, so Isabelle/jEdit prefers its own
528 application font @{verbatim IsabelleText}, which ensures that
529 standard collection of Isabelle symbols are actually seen on the
532 Note that a Java/AWT/Swing application can load additional fonts
533 only if they are not installed as system font already! This means
534 some old version of @{verbatim IsabelleText} that happens to be
535 already present prevents Isabelle/jEdit from using its current
536 bundled version. This results in missing glyphs (black rectangles),
537 when some obsolete version of @{verbatim IsabelleText} is used by
538 accident. This problem can be avoided by refraining to ``install''
539 any version of @{verbatim IsabelleText} in the first place.
541 \medskip \paragraph{Input methods.} In principle, Isabelle/jEdit
542 could delegate the problem to produce Isabelle symbols in their
543 Unicode rendering to the underlying operating system and its
544 \emph{input methods}. Regular jEdit also provides various ways to
545 work with \emph{abbreviations} to produce certain non-ASCII
546 characters. Since none of these standard input methods work
547 satisfactorily for the mathematical characters required for
548 Isabelle, various specific Isabelle/jEdit mechanisms are provided.
550 Here is a summary for practically relevant input methods for
555 \item The \emph{Symbols} panel with some GUI buttons to insert
556 certain symbols in the text buffer. There are also tooltips to
557 reveal to official Isabelle representation with some additional
558 information about \emph{symbol abbreviations} (see below).
560 \item Copy / paste from decoded source files: text that is rendered
561 as Unicode already can be re-used to produce further text. This
562 also works between different applications, e.g.\ Isabelle/jEdit and
563 some web browser or mail client, as long as the same Unicode view on
564 Isabelle symbols is used uniformly.
566 \item Copy / paste from prover output within Isabelle/jEdit. The
567 same principles as for text buffers apply, but note that \emph{copy}
568 in secondary Isabelle/jEdit windows works via the keyboard shortcut
569 @{verbatim "C+c"}. The jEdit menu actions always refer to the
572 \item Completion provided by Isabelle plugin (see
573 \secref{sec:completion}). Isabelle symbols have a canonical name
574 and optional abbreviations. This can be used with the text
575 completion mechanism of Isabelle/jEdit, to replace a prefix of the
576 actual symbol like @{verbatim "\<lambda>"}, or its backslashed name
577 @{verbatim "\\"}@{verbatim "lambda"}, or its ASCII abbreviation
578 @{verbatim "%"} by the Unicode rendering.
580 The following table is an extract of the information provided by the
581 standard @{file "$ISABELLE_HOME/etc/symbols"} file:
585 \textbf{symbol} & \textbf{abbreviation} & \textbf{backslashed name} \\\hline
586 @{text "\<lambda>"} & @{verbatim "%"} & @{verbatim "\\lambda"} \\
587 @{text "\<Rightarrow>"} & @{verbatim "=>"} & @{verbatim "\\Rightarrow"} \\
588 @{text "\<Longrightarrow>"} & @{verbatim "==>"} & @{verbatim "\\Longrightarrow"} \\
590 @{text "\<And>"} & @{verbatim "!!"} & @{verbatim "\\And"} \\
591 @{text "\<equiv>"} & @{verbatim "=="} & @{verbatim "\\equiv"} \\
593 @{text "\<forall>"} & @{verbatim "!"} & @{verbatim "\\forall"} \\
594 @{text "\<exists>"} & @{verbatim "?"} & @{verbatim "\\exists"} \\
595 @{text "\<longrightarrow>"} & @{verbatim "-->"} & @{verbatim "\\longrightarrow"} \\
596 @{text "\<and>"} & @{verbatim "&"} & @{verbatim "\\and"} \\
597 @{text "\<or>"} & @{verbatim "|"} & @{verbatim "\\or"} \\
598 @{text "\<not>"} & @{verbatim "~"} & @{verbatim "\\not"} \\
599 @{text "\<noteq>"} & @{verbatim "~="} & @{verbatim "\\noteq"} \\
600 @{text "\<in>"} & @{verbatim ":"} & @{verbatim "\\in"} \\
601 @{text "\<notin>"} & @{verbatim "~:"} & @{verbatim "\\notin"} \\
605 Note that the above abbreviations refer to the input method. The
606 logical notation provides ASCII alternatives that often coincide,
607 but deviate occasionally. This occasionally causes user confusion
608 with very old-fashioned Isabelle source that use ASCII replacement
609 notation like @{verbatim "!"} or @{verbatim "ALL"} directly.
613 Raw Unicode characters within prover source files should be
614 restricted to informal parts, e.g.\ to write text in non-latin
615 alphabets. Mathematical symbols should be defined via the official
616 rendering tables, to avoid problems with portability and long-term
617 storage of formal text.
619 \paragraph{Control symbols.} There are some special control symbols
620 to modify the style of a single symbol (without nesting). Control
621 symbols may be applied to a region of selected text, either using
622 the \emph{Symbols} panel or keyboard shortcuts or jEdit actions.
623 These editor operations produce a separate control symbol for each
624 symbol in the text, in order to make the whole text appear in a
628 \begin{tabular}{llll}
629 style & \textbf{symbol} & shortcut & action \\\hline
630 superscript & @{verbatim "\<^sup>"} & @{verbatim "C+e UP"} & @{verbatim "isabelle.control-sup"} \\
631 subscript & @{verbatim "\<^sub>"} & @{verbatim "C+e DOWN"} & @{verbatim "isabelle.control-sub"} \\
632 bold face & @{verbatim "\<^bold>"} & @{verbatim "C+e RIGHT"} & @{verbatim "isabelle.control-bold"} \\
633 reset & & @{verbatim "C+e LEFT"} & @{verbatim "isabelle.control-reset"} \\
637 To produce a single control symbol, it is also possible to complete
638 on @{verbatim "\\"}@{verbatim sup}, @{verbatim "\\"}@{verbatim sub},
639 @{verbatim "\\"}@{verbatim bold} as for regular symbols. *}
642 section {* Text completion \label{sec:completion} *}
645 Text completion works via some light-weight GUI popup, which is triggered by
646 keyboard events during the normal editing process in the main jEdit text
647 area and a few additional text fields. The popup interprets special keys:
648 @{verbatim TAB}, @{verbatim ESCAPE}, @{verbatim UP}, @{verbatim DOWN},
649 @{verbatim PAGE_UP}, @{verbatim PAGE_DOWN}. All other key events are passed
650 to the jEdit text area --- this allows to ignore unwanted completions most
651 of the time and continue typing quickly.
653 Various Isabelle plugin options control the popup behavior and immediate
654 insertion into buffer.
656 Isabelle Symbols are completed in backslashed forms, e.g.\ @{verbatim
657 "\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the Isabelle
658 symbol @{text "\<forall>"} in its Unicode rendering. Alternatively, symbol
659 abbreviations may be used as specified in @{file
660 "$ISABELLE_HOME/etc/symbols"}.
662 \emph{Explicit completion} works via standard jEdit shortcut @{verbatim
663 "C+b"}, which is remapped to action @{verbatim "isabelle.complete"}, with a
664 fall-back on regular @{verbatim "complete-word"} for non-Isabelle buffers.
666 \emph{Implicit completion} works via keyboard input on text area, with popup
667 or immediate insertion into buffer. Plain words require at least 3
668 characters to be completed.
670 \emph{Immediate completion} means the (unique) replacement text is inserted
671 into the buffer without popup. This mode ignores plain words and requires
672 more than one characters for symbol abbreviations. Otherwise it falls back
677 section {* Automatically tried tools \label{sec:auto-tools} *}
679 text {* Continuous document processing works asynchronously in the
680 background. Visible document source that has been evaluated already
681 may get augmented by additional results of \emph{asynchronous print
682 functions}. The canonical example is proof state output, which is
683 always enabled. More heavy-weight print functions may be applied,
684 in order to prove or disprove parts of the formal text by other
687 Isabelle/HOL provides various automatically tried tools that operate
688 on outermost goal statements (e.g.\ @{command lemma}, @{command
689 theorem}), independently of the state of the current proof attempt.
690 They work implicitly without any arguments. Results are output as
691 \emph{information messages}, which are indicated in the text area by
692 blue squiggles and a blue information sign in the gutter (see
693 \figref{fig:auto-tools}). The message content may be shown as for
694 any other message, see also \secref{sec:prover-output}. Some tools
695 produce output with \emph{sendback} markup, which means that
696 clicking on certain parts of the output inserts that text into the
697 source in the proper place.
701 \includegraphics[scale=0.5]{auto-tools}
703 \caption{Results of automatically tried tools}
704 \label{fig:auto-tools}
707 \medskip The following Isabelle system options control the behaviour
708 of automatically tried tools (see also the jEdit dialog window
709 \emph{Plugin Options / Isabelle / General / Automatically tried
714 \item @{system_option auto_methods} controls automatic use of a
715 combination of standard proof methods (@{method auto}, @{method
716 simp}, @{method blast}, etc.). This corresponds to the command
719 The tool is disabled by default, since unparameterized invocation of
720 standard proof methods often consumes substantial CPU resources
721 without leading to success.
723 \item @{system_option auto_nitpick} controls a slightly reduced
724 version of @{command nitpick}, which tests for counterexamples using
725 first-order relational logic. See also the Nitpick manual
726 \cite{isabelle-nitpick}.
728 This tool is disabled by default, due to the extra overhead of
729 invoking an external Java process for each attempt to disprove a
732 \item @{system_option auto_quickcheck} controls automatic use of
733 @{command quickcheck}, which tests for counterexamples using a
734 series of assignments for free variables of a subgoal.
736 This tool is \emph{enabled} by default. It requires little
737 overhead, but is a bit weaker than @{command nitpick}.
739 \item @{system_option auto_sledgehammer} controls a significantly
740 reduced version of @{command sledgehammer}, which attempts to prove
741 a subgoal using external automatic provers. See also the
742 Sledgehammer manual \cite{isabelle-sledgehammer}.
744 This tool is disabled by default, due to the relatively heavy nature
747 \item @{system_option auto_solve_direct} controls automatic use of
748 @{command solve_direct}, which checks whether the current subgoals
749 can be solved directly by an existing theorem. This also helps to
750 detect duplicate lemmas.
752 This tool is \emph{enabled} by default.
756 Invocation of automatically tried tools is subject to some global
757 policies of parallel execution, which may be configured as follows:
761 \item @{system_option auto_time_limit} (default 2.0) determines the
762 timeout (in seconds) for each tool execution individually.
764 \item @{system_option auto_time_start} (default 1.0) determines the
765 start delay (in seconds) for automatically tried tools, after the
766 main command evaluation is finished.
770 Each tool is submitted independently to the pool of parallel
771 execution tasks in Isabelle/ML, using hardwired priorities according
772 to its relative ``heaviness''. The main stages of evaluation and
773 printing of proof states take precedence, but an already running
774 tool is not canceled and may thus reduce reactivity of proof
777 Users should experiment how the available CPU resources (number of
778 cores) are best invested to get additional feedback from prover in
779 the background, by using weaker or stronger tools. *}
782 section {* Sledgehammer \label{sec:sledgehammer} *}
784 text {* The \emph{Sledgehammer} panel (\figref{fig:sledgehammer})
785 provides a view on some independent execution of @{command
786 sledgehammer}, with process indicator (spinning wheel) and GUI
787 elements for important Sledgehammer arguments and options. Any
788 number of Sledgehammer panels may be active, according to the
789 standard policies of Dockable Window Management in jEdit. Closing a
790 window also cancels the corresponding prover tasks.
794 \includegraphics[scale=0.3]{sledgehammer}
796 \caption{An instance of the Sledgehammer panel}
797 \label{fig:sledgehammer}
800 The \emph{Apply} button attaches a fresh invocation of @{command
801 sledgehammer} to the command where the cursor is pointing in the
802 text --- this should be some pending proof problem. Further buttons
803 like \emph{Cancel} and \emph{Locate} help to manage the running
806 Results appear incrementally in the output window of the panel.
807 Proposed proof snippets are marked up as \emph{sendback}, which
808 means a single mouse click inserts the text into a suitable place of
809 the original source. Some manual editing may be required
810 nonetheless, say to remove earlier proof attempts. *}
813 section {* Find theorems *}
815 text {* The \emph{Find} panel (\figref{fig:find}) provides an
816 independent view for @{command find_theorems}. The main text field
817 accepts search criteria according to the syntax @{syntax
818 thmcriterium} given in \cite{isabelle-isar-ref}. Further options of
819 @{command find_theorems} are available via GUI elements.
823 \includegraphics[scale=0.3]{find}
825 \caption{An instance of the Find panel}
829 The \emph{Apply} button attaches a fresh invocation of @{command
830 find_theorems} to the current context of the command where the
831 cursor is pointing in the text, unless an alternative theory context
832 (from the underlying logic image) is specified explicitly. *}
835 chapter {* Known problems and workarounds \label{sec:problems} *}
840 \item \textbf{Problem:} Lack of dependency management for auxiliary files
841 that contribute to a theory (e.g.\ @{command ML_file}).
843 \textbf{Workaround:} Re-load files manually within the prover, by
844 editing corresponding command in the text.
846 \item \textbf{Problem:} Odd behavior of some diagnostic commands with
847 global side-effects, like writing a physical file.
849 \textbf{Workaround:} Avoid such commands.
851 \item \textbf{Problem:} No way to delete document nodes from the overall
852 collection of theories.
854 \textbf{Workaround:} Ignore unused files. Restart whole
855 Isabelle/jEdit session in worst-case situation.
857 \item \textbf{Problem:} Keyboard shortcuts @{verbatim "C+PLUS"} and
858 @{verbatim "C+MINUS"} for adjusting the editor font size depend on
859 platform details and national keyboards.
861 \textbf{Workaround:} Use numeric keypad or rebind keys in the
862 jEdit Shortcuts options dialog.
864 \item \textbf{Problem:} The Mac OS X keyboard shortcut @{verbatim
865 "COMMAND+COMMA"} for application \emph{Preferences} is in conflict
866 with the jEdit default shortcut for \emph{Incremental Search Bar}
867 (action @{verbatim "quick-search"}).
869 \textbf{Workaround:} Remap in jEdit manually according to national
870 keyboard, e.g.\ @{verbatim "COMMAND+SLASH"} on English ones.
872 \item \textbf{Problem:} Mac OS X system fonts sometimes lead to
873 character drop-outs in the main text area.
875 \textbf{Workaround:} Use the default @{verbatim IsabelleText} font.
876 (Do not install that font on the system.)
878 \item \textbf{Problem:} Some Linux / X11 input methods such as IBus
879 tend to disrupt key event handling of Java/AWT/Swing.
881 \textbf{Workaround:} Do not use input methods, reset the environment
882 variable @{verbatim XMODIFIERS} within Isabelle settings (default in
885 \item \textbf{Problem:} Some Linux / X11 window managers that are
886 not ``re-parenting'' cause problems with additional windows opened
887 by Java. This affects either historic or neo-minimalistic window
888 managers like @{verbatim awesome} or @{verbatim xmonad}.
890 \textbf{Workaround:} Use regular re-parenting window manager.
892 \item \textbf{Problem:} Recent forks of Linux / X11 window managers
893 and desktop environments (variants of Gnome) disrupt the handling of
894 menu popups and mouse positions of Java/AWT/Swing.
896 \textbf{Workaround:} Use mainstream versions of Linux desktops.
898 \item \textbf{Problem:} Full-screen mode via jEdit action @{verbatim
899 "toggle-full-screen"} (default shortcut @{verbatim F11}) works on
900 Windows, but not on Mac OS X or various Linux / X11 window managers.
902 \textbf{Workaround:} Use native full-screen control of the window
903 manager, if available (notably on Mac OS X).
905 \item \textbf{Problem:} Full-screen mode and dockable windows in
906 \emph{floating} state may lead to confusion about window placement
907 (depending on platform characteristics).
909 \textbf{Workaround:} Avoid this combination.