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 datatypes 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 regular jEdit
59 need to be taken into account when discussing any of these PIDE
60 building blocks on public forums, mailing lists, or even scientific
65 section {* The Isabelle/jEdit Prover IDE *}
68 \includegraphics[width=\textwidth]{isabelle-jedit}
70 Isabelle/jEdit consists of some plugins for the well-known jEdit
71 text editor \url{http://www.jedit.org}, according to the following
76 \item The original jEdit look-and-feel is generally preserved,
77 although some default properties have been changed to accommodate
78 Isabelle (e.g.\ the text area font).
80 \item Formal Isabelle/Isar text is checked asynchronously while
81 editing. The user is in full command of the editor, and the prover
82 refrains from locking portions of the buffer.
84 \item Prover feedback works via colors, boxes, squiggly underline,
85 hyperlinks, popup windows, icons, clickable output, all based on
86 semantic markup produced by Isabelle in the background.
88 \item Using the mouse together with the modifier key @{verbatim
89 CONTROL} (Linux, Windows) or @{verbatim COMMAND} (Mac OS X) exposes
90 additional formal content via tooltips and/or hyperlinks.
92 \item Formal output (in popups etc.) may be explored recursively,
93 using the same techniques as in the editor source buffer.
95 \item Additional panels (e.g.\ \emph{Output}, \emph{Symbols}) are
96 organized by the Dockable Window Manager of jEdit, which also allows
97 multiple floating instances of each window class.
99 \item The prover process and source files are managed on the editor
100 side. The prover operates on timeless and stateless document
101 content via Isabelle/Scala.
103 \item Plugin options of jEdit (for the \emph{Isabelle} plugin) give
104 access to a selection of Isabelle/Scala options and its persistence
105 preferences, usually with immediate effect on the prover back-end or
108 \item The logic image of the prover session may be specified within
109 Isabelle/jEdit, but this requires restart. The new image is provided
110 automatically by the Isabelle build tool.
116 subsection {* Documentation *}
118 text {* Regular jEdit documentation is accessible via its @{verbatim
119 Help} menu or @{verbatim F1} keyboard shortcut. This includes a full
120 \emph{User's Guide} and \emph{Frequently Asked Questions} for this
121 sophisticated text editor.
123 Most of this information about jEdit is relevant for Isabelle/jEdit
124 as well, but one needs to keep in mind that defaults sometimes
125 differ, and the official jEdit documentation does not know about the
126 Isabelle plugin with its special support for theory editing.
130 subsection {* Plugins *}
132 text {* The \emph{Plugin Manager} of jEdit allows to augment editor
133 functionality by JVM modules (jars) that are provided by the central
134 plugin repository, or one of various mirror sites. The main
135 \emph{Isabelle} plugin is an integral part of Isabelle/jEdit needs
136 to remain active at all times! A few additional plugins are bundled
137 with Isabelle/jEdit for convenience or out of necessity, notably
138 \emph{Console} with its Isabelle/Scala sub-plugin and
139 \emph{SideKick} with some Isabelle-specific parsers for document
142 Connecting to the plugin server infrastructure of the jEdit project
143 allows to update bundled plugins or to add further
144 functionality. This needs to be done with the usual care for such an
145 open bazaar, with contributions of very mixed quality. Arbitrary
146 combinations of add-on features are apt to cause problems.
148 It is advisable to start with the default configuration of
149 Isabelle/jEdit and develop some understanding how it is supposed to
150 work, before loading additional plugins at a grand scale.
154 subsection {* Options *}
156 text {* Both jEdit and Isabelle have distinctive management of
157 persistent options. Regular jEdit options are accessible via the
158 dialogs for \emph{Global Options} and \emph{Plugin Options}. This
159 results in an environment of properties that is stored within the
160 \emph{settings directory} of jEdit; see also the menu
161 \emph{Utilities / Settings Directory}.
163 Isabelle system options are managed by Isabelle/Scala; see also
164 \cite{isabelle-sys}, especially the coverage of sessions and
165 command-line tools like @{tool build} or @{tool options}. Isabelle
166 options that are declared as \textbf{public} are exposed to the
167 jEdit \emph{Plugin Options} dialog, in its section \emph{Isabelle /
168 General}. This provides a view on Isabelle options and persistent
169 preferences in @{verbatim "$ISABELLE_HOME_USER/etc/preferences"},
170 independently of the jEdit properties in its settings directory.
172 Some Isabelle options that are accessible in the Isabelle/jEdit
173 Plugin Options dialog affect general parameters that are relevant
174 outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or
175 @{system_option parallel_proofs} for the Isabelle build tool
178 \medskip Options are loaded once on startup and saved on shutdown of
179 Isabelle/jEdit. Editing the machine-generated files @{verbatim
180 "$ISABELLE_HOME_USER/jedit/properties"} or @{verbatim
181 "$ISABELLE_HOME_USER/etc/preferences"} manually while the
182 application is running is likely to cause a lost-update! *}
185 subsection {* Keymaps *}
187 text {* Keyboard shortcuts used to be managed as jEdit properties in
188 the past, but recent versions (2013) have a separate concept of
189 \emph{keymap}. The ``imported'' keymap is produced initially from
190 the environment of properties that is available at the first start
193 This is relevant for Isabelle/jEdit due to various fine-tuning of
194 default properties, and additional keyboard shortcuts for Isabelle
195 specific functionality. Users may change their keymap later on, but
196 may need to copy Isabelle-specific key bindings manually.
200 subsection {* Look-and-feel *}
202 text {* jEdit is a Java/Swing application with some ambition to
203 support ``native'' look-and-feel on all platforms, within the limits
204 of what Oracle as Java provider and major operating system vendors
205 and distributors allow (see also \secref{sec:problems}).
207 Isabelle/jEdit enables platform-specific look-and-feel by default as
212 \item[Linux] The platform-independent \emph{Nimbus} is used by
213 default, but the classic \emph{Metal} also works. \emph{GTK+} works
214 under the side-condition that the overall GTK theme is selected in a
215 Java/Swing friendly way.
217 \item[Windows] Regular \emph{Windows} is used by default, but
218 platform-independent \emph{Nimbus} and \emph{Metal} also work.
220 \item[Mac OS X] Standard \emph{Apple Aqua} is used by default.
221 Moreover the bundled \emph{MacOSX} plugin provides various functions
222 that are expected from applications on that particular platform:
223 quit from menu or dock, preferences menu, drag-and-drop of text
224 files on the application, full-screen mode for main editor windows
229 Users may experiment with different look-and-feels, but need to keep
230 in mind that this extra variance of GUI functionality is unlikely to
231 work in arbitrary combinations. The \emph{GTK+} look-and-feel is
232 particularly critical due to its additional dimension of ``themes''.
234 After changing the look-and-feel in \emph{Global Options /
235 Appearance}, it is advisable to restart Isabelle/jEdit in order to
240 chapter {* Prover IDE functionality *}
242 section {* Buffers and theories *}
244 text {* jEdit maintains a collection of open \emph{text buffers} to
245 store source files. Each buffer may be associated with any number
246 of visible \emph{text areas}. Buffers are subject to an
247 \emph{editor mode} that is determined from the file type. Files
248 with extension \texttt{.thy} are assigned to the mode
249 \emph{isabelle} and treated specifically.
251 \medskip Isabelle theory files are automatically added to the formal
252 document model of Isabelle/Scala, which maintains a family of
253 versions of all sources for the prover. The \emph{Theories} panel
254 provides an overview of the status of continuous checking of theory
255 sources. Unlike batch sessions \cite{isabelle-sys}, theory nodes
256 are identified by full path names; this allows to work with multiple
257 (disjoint) Isabelle sessions simultaneously within the same editor
260 Certain events to open or update buffers with theory files cause
261 Isabelle/jEdit to resolve dependencies of \emph{theory imports}.
262 The system requests to load further files into jEdit editor buffers,
263 to be added to the theory document model for further checking. It
264 is also possible to resolve dependencies automatically, depending on
265 the option @{system_option jedit_auto_load}.
267 \medskip The open text area views on theory buffers define the
268 visible \emph{perspective} of Isabelle/jEdit. This is taken as a
269 hint for document processing: the prover ensures that those parts of
270 a theory where the user is looking are checked, while other parts
271 that are presently not required are ignored.
273 The perspective can be changed by opening or closing text areas
274 windows, or scrolling within some window. It is also possible to
275 indicate theory nodes as \emph{required} for continuous checking in
276 the \emph{Theories} panel. This means such nodes and all their
277 imports are always processed, independently of the visibility
278 status. This can have significant impact on performance, though.
280 \medskip Formal markup of checked theory content is turned into GUI
281 rendering, based on a standard repertoire known from IDEs for
282 programming languages: colors, icons, highlighting, squiggly
283 underline, tooltips, hyperlinks etc. For outer syntax of
284 Isabelle/Isar there is some traditional syntax-highlighting, based
285 on static keyword tables and tokenization within the editor. In
286 contrast, the painting of inner syntax (term language etc.) is
287 based on semantic information that is reported dynamically from the
288 logical context. Thus the prover can provide additional markup to
289 help the user understanding the meaning of the text, and to produce
290 more text with some add-on tools (e.g.\ information messages by
291 automated provers or disprovers running in the background).
293 Such formally annotated text can be explored further by using the
294 @{verbatim CONTROL} modifier key on Linux and Windows, or @{verbatim
295 COMMAND} on Mac OS X. Hovering with the mouse while the modifier is
296 pressed reveals \emph{tooltips} (grey box within the text with a
297 yellow popup) and/or \emph{hyperlinks} (dark grey rectangle within
298 the text). Tooltip popups use the same rendering principles as the
299 main text area, and further tooltips and/or hyperlinks may be
300 exposed recursively by the same mechanism.
302 %FIXME screenshot of term "x = x" with typing/sorting
306 section {* Isabelle symbols and fonts *}
308 text {* Isabelle sources consist of \emph{symbols} that extend plain
309 ASCII and UTF-8 (for informal text) to allow infinitely many
310 mathematical symbols within the formal sources. This works without
311 depending on particular encodings or varying Unicode standards
312 \cite{Wenzel:2011:CICM}.
314 For the prover back-end, formal text consists of ASCII characters
315 that are grouped according to some simple rules, e.g.\ as plain
316 ``@{verbatim a}'' or symbolic ``@{verbatim "\<alpha>"}''.
318 For the editor front-end, a certain subset of symbols is rendered as
319 Unicode glyphs, in order to show ``@{verbatim "\<alpha>"}'' as actual
320 ``@{text "\<alpha>"}''. This symbol interpretation is specified by the
321 Isabelle system distribution (in @{file
322 "$ISABELLE_HOME/etc/symbols"}) or by the user (in @{verbatim
323 "$ISABELLE_HOME_USER/etc/symbols"}).
325 The appendix of \cite{isabelle-isar-ref} gives an overview of the
326 standard interpretation of finitely many symbols from the infinite
327 collection. Uninterpreted symbols are shown literally.
329 \medskip Technically, the Unicode view on Isabelle symbols is an
330 \emph{encoding} in Isabelle/jEdit, which is called @{verbatim
331 "UTF-8-Isabelle"} and enabled by default. Sometimes such defaults
332 are reset accidentally, or malformed UTF-8 sequences in the text
333 force jEdit to fall back on a different encoding like @{verbatim
334 "ISO-8859-15"}. In the latter case, raw @{verbatim "\<alpha>"} will be
335 shown in the text buffer instead of its Unicode rendering @{text
336 "\<alpha>"}. The jEdit menu operation \emph{File / Reload with Encoding /
337 UTF-8-Isabelle} helps to resolve such problems, potentially after
338 repairing malformed parts of the text.
340 \medskip Correct rendering via Unicode requires a font that contains
341 glyphs for the corresponding codepoints. Most system fonts lack
342 that, so Isabelle/jEdit prefers its own application font @{verbatim
343 IsabelleText} by default, which ensures that standard collection of
344 Isabelle symbols are actually seen on the screen (or printer).
346 Note that a Java/Swing application can load additional fonts only if
347 they are not installed as system font already! This means some old
348 version of @{verbatim IsabelleText} that happens to be already
349 present prevents Isabelle/jEdit from using its current bundled
350 version. This might result in missing glyphs (black rectangles),
351 since obsolete versions of @{verbatim IsabelleText} lack recent
352 improvements of Unicode glyph coverage. This problem can be avoided
353 by refraining to ``install'' any version of @{verbatim IsabelleText}
356 \medskip \paragraph{Input methods.} In principle, Isabelle/jEdit
357 could delegate the problem to produce Isabelle symbols in their
358 Unicode rendering to the underlying operating system and its
359 \emph{input methods}. Regular jEdit also provides various ways to
360 work with \emph{abbreviations} to produce certain non-ASCII
361 characters. Since none of these standard input methods work
362 satisfactorily for the mathematical characters required for
363 Isabelle, various specific Isabelle/jEdit mechanisms are provided.
365 Here is a summary for practically relevant input methods for
370 \item The \emph{Symbols} panel with some GUI buttoms to insert
371 certain symbols in the text buffer. There are also tooltips to
372 reveal to official Isabelle representation with some additional
373 information about \emph{symbol abbreviations} (see below).
375 \item Copy / paste from decoded source files: text that is rendered
376 as Unicode already may get re-used to produce further such text.
377 This also works between different applications, e.g.\ Isabelle/jEdit
378 and some web browser or mail client, as long as the same Unicode
379 view on Isabelle symbols is used uniformly.
381 \item Copy / paste from prover output within Isabelle/jEdit. The
382 same principles as for text buffers apply, but note that \emph{copy}
383 in Isabelle \emph{Output} works via the keyboard shortcut @{verbatim
384 "C+c"}, not the jEdit menu.
386 \item Completion provided by Isabelle plugin (see
387 \secref{sec:completion}). Isabelle symbols have a canonical name
388 and optional abbreviations. This can be used with the text
389 completion mechanism of Isabelle/jEdit, to replace a prefix of the
390 actual symbol like @{verbatim "\<lambda>"}, or its backslashed name
391 @{verbatim "\\"}@{verbatim "lambda"}, or its ASCII abbreviation
394 The following table is an extract of the information provided by the
395 standard @{file "$ISABELLE_HOME/etc/symbols"} file:
399 \textbf{symbol} & \textbf{abbreviation} & \textbf{backslashed name} \\\hline
400 @{text "\<lambda>"} & @{verbatim "%"} & @{verbatim "\\lambda"} \\
401 @{text "\<Rightarrow>"} & @{verbatim "=>"} & @{verbatim "\\Rightarrow"} \\
402 @{text "\<Longrightarrow>"} & @{verbatim "==>"} & @{verbatim "\\Longrightarrow"} \\
404 @{text "\<And>"} & @{verbatim "!!"} & @{verbatim "\\And"} \\
405 @{text "\<equiv>"} & @{verbatim "=="} & @{verbatim "\\equiv"} \\
407 @{text "\<forall>"} & @{verbatim "!"} & @{verbatim "\\forall"} \\
408 @{text "\<exists>"} & @{verbatim "?"} & @{verbatim "\\exists"} \\
409 @{text "\<longrightarrow>"} & @{verbatim "-->"} & @{verbatim "\\longrightarrow"} \\
410 @{text "\<and>"} & @{verbatim "&"} & @{verbatim "\\and"} \\
411 @{text "\<or>"} & @{verbatim "|"} & @{verbatim "\\or"} \\
412 @{text "\<not>"} & @{verbatim "~"} & @{verbatim "\\not"} \\
413 @{text "\<noteq>"} & @{verbatim "~="} & @{verbatim "\\noteq"} \\
414 @{text "\<in>"} & @{verbatim ":"} & @{verbatim "\\in"} \\
415 @{text "\<notin>"} & @{verbatim "~:"} & @{verbatim "\\notin"} \\
419 Note that the above abbreviations refer to the input method. The
420 logical notation provides ASCII alternatives that often coincide,
421 but deviate occasionally. Writing formal sources directly with
422 ASCII replacement notation like @{verbatim "!"} or @{verbatim "ALL"}
423 or @{verbatim "-->"} is considered very old fashioned in 2013!
427 Raw Unicode characters within prover source files should be
428 restricted to informal parts, e.g.\ to write text in non-latin
429 alphabets. Mathematical symbols should be defined via the official
430 rendering tables, to avoid problems with portability and longterm
431 storage of formal text.
433 \paragraph{Control symbols.} There are some special control symbols
434 to modify the style of a single symbol (without nesting). Control
435 symbols may be applied to a region of selected text, either using
436 the \emph{Symbols} panel or keyboard shortcuts; these editor
437 operations produce a separate control symbol for each symbol in the
442 \textbf{symbol} & style & keyboard shortcut \\\hline
443 @{verbatim "\<^sup>"} & superscript & @{verbatim "C+e UP"} \\
444 @{verbatim "\<^sub>"} & subscript & @{verbatim "C+e DOWN"} \\
445 @{verbatim "\<^bold>"} & bold face & @{verbatim "C+e RIGHT"} \\
446 & reset & @{verbatim "C+e LEFT"} \\
449 It is also possible to complete on @{verbatim "\\"}@{verbatim sup},
450 @{verbatim "\\"}@{verbatim sub}, @{verbatim "\\"}@{verbatim bold} as
455 section {* Text completion \label{sec:completion} *}
458 Text completion works via some light-weight GUI popup, which is triggered by
459 keyboard events during the normal editing process in the main jEdit text
460 area and a few additional text fields. The popup interprets special keys:
461 @{verbatim TAB}, @{verbatim ESCAPE}, @{verbatim UP}, @{verbatim DOWN},
462 @{verbatim PAGE_UP}, @{verbatim PAGE_DOWN}. All other key events are passed
463 to the jEdit text area --- this allows to ignore unwanted completions most
464 of the time and continue typing quickly.
466 Various Isabelle plugin options control the popup behavior and immediate
467 insertion into buffer.
469 Isabelle Symbols are completed in backslashed forms, e.g.\ @{verbatim
470 "\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the Isabelle
471 symbol @{text "\<forall>"} in its Unicode rendering. Alternatively, symbol
472 abbreviations may be used as specified in @{file
473 "$ISABELLE_HOME/etc/symbols"}.
475 \emph{Explicit completion} works via standard jEdit shortcut @{verbatim
476 "C+b"}, which is remapped to action @{verbatim "isabelle.complete"}, with a
477 fall-back on regular @{verbatim "complete-word"} for non-Isabelle buffers.
479 \emph{Implicit completion} works via keyboard input on text area, with popup
480 or immediate insertion into buffer. Plain words require at least 3
481 characters to be completed.
483 \emph{Immediate completion} means the (unique) replacement text is inserted
484 into the buffer without popup. This mode ignores plain words and requires
485 more than one characters for symbol abbreviations. Otherwise it falls back
490 chapter {* Known problems and workarounds \label{sec:problems} *}
495 \item \textbf{Problem:} Lack of dependency management for auxiliary files
496 that contribute to a theory (e.g.\ @{command ML_file}).
498 \textbf{Workaround:} Re-load files manually within the prover.
500 \item \textbf{Problem:} Odd behavior of some diagnostic commands with
501 global side-effects, like writing a physical file.
503 \textbf{Workaround:} Avoid such commands.
505 \item \textbf{Problem:} No way to delete document nodes from the overall
506 collection of theories.
508 \textbf{Workaround:} Ignore unused files. Restart whole
509 Isabelle/jEdit session in worst-case situation.
511 \item \textbf{Problem:} The Mac OS X keyboard shortcut @{verbatim
512 "COMMAND+COMMA"} for Preferences is in conflict with the jEdit default
513 binding for @{verbatim "quick-search"}.
515 \textbf{Workaround:} Remap in jEdit manually according to national
516 keyboard, e.g.\ @{verbatim "COMMAND+SLASH"} on English ones.
518 \item \textbf{Problem:} Keyboard shortcuts @{verbatim "C+PLUS"} and
519 @{verbatim "C+MINUS"} for adjusting the editor font size depend on
520 platform details and national keyboards.
522 \textbf{Workaround:} Use numeric keypad or rebind keys in the
523 jEdit Shortcuts options dialog.
525 \item \textbf{Problem:} Some Linux / X11 input methods such as IBus
526 tend to disrupt key event handling of Java/Swing.
528 \textbf{Workaround:} Do not use input methods, reset the environment
529 variable @{verbatim XMODIFIERS} within Isabelle settings (default in
532 \item \textbf{Problem:} Some Linux / X11 window managers that are
533 not ``re-parenting'' cause problems with additional windows opened
534 by the Java VM. This affects either historic or neo-minimalistic
535 window managers like @{verbatim awesome} or @{verbatim xmonad}.
537 \textbf{Workaround:} Use regular re-parenting window manager.
539 \item \textbf{Problem:} Recent forks of Linux / X11 window managers
540 and desktop environments (variants of Gnome) disrupt the handling of
541 menu popups and mouse positions of Java/AWT/Swing.
543 \textbf{Workaround:} Use mainstream versions of Linux desktops.