# HG changeset patch
# User wenzelm
# Date 1446663158 -3600
# Node ID e717f152d2a81fa011743790306fae048af0ae2a
# Parent  320fa9d01e67d630743898b465d09b64ea5c3146
tuned whitespace;

diff -r 320fa9d01e67 -r e717f152d2a8 src/Doc/JEdit/JEdit.thy
--- a/src/Doc/JEdit/JEdit.thy	Wed Nov 04 18:35:50 2015 +0100
+++ b/src/Doc/JEdit/JEdit.thy	Wed Nov 04 19:52:38 2015 +0100
@@ -9,52 +9,50 @@
 section \<open>Concepts and terminology\<close>
 
 text \<open>
-  Isabelle/jEdit is a Prover IDE that integrates \<^emph>\<open>parallel proof
-  checking\<close> @{cite "Wenzel:2009" and "Wenzel:2013:ITP"} with
-  \<^emph>\<open>asynchronous user interaction\<close> @{cite "Wenzel:2010" and
-  "Wenzel:2012:UITP-EPTCS" and "Wenzel:2014:ITP-PIDE" and "Wenzel:2014:UITP"},
-  based on a document-oriented approach to \<^emph>\<open>continuous proof processing\<close>
-  @{cite "Wenzel:2011:CICM" and "Wenzel:2012"}. Many concepts and system
-  components are fit together in order to make this work. The main building
-  blocks are as follows.
+  Isabelle/jEdit is a Prover IDE that integrates \<^emph>\<open>parallel proof checking\<close>
+  @{cite "Wenzel:2009" and "Wenzel:2013:ITP"} with \<^emph>\<open>asynchronous user
+  interaction\<close> @{cite "Wenzel:2010" and "Wenzel:2012:UITP-EPTCS" and
+  "Wenzel:2014:ITP-PIDE" and "Wenzel:2014:UITP"}, based on a document-oriented
+  approach to \<^emph>\<open>continuous proof processing\<close> @{cite "Wenzel:2011:CICM" and
+  "Wenzel:2012"}. Many concepts and system components are fit together in
+  order to make this work. The main building blocks are as follows.
 
-  \<^descr>[PIDE] is a general framework for Prover IDEs based on Isabelle/Scala.
-  It is built around a concept of parallel and asynchronous document
-  processing, which is supported natively by the parallel proof engine that is
-  implemented in Isabelle/ML. The traditional prover command loop is given up;
-  instead there is direct support for editing of source text, with rich formal
-  markup for GUI rendering.
+    \<^descr>[PIDE] is a general framework for Prover IDEs based on Isabelle/Scala. It
+    is built around a concept of parallel and asynchronous document
+    processing, which is supported natively by the parallel proof engine that
+    is implemented in Isabelle/ML. The traditional prover command loop is
+    given up; instead there is direct support for editing of source text, with
+    rich formal markup for GUI rendering.
 
-  \<^descr>[Isabelle/ML] is the implementation and extension language of
-  Isabelle, see also @{cite "isabelle-implementation"}. It is integrated
-  into the logical context of Isabelle/Isar and allows to manipulate
-  logical entities directly. Arbitrary add-on tools may be implemented
-  for object-logics such as Isabelle/HOL.
+    \<^descr>[Isabelle/ML] is the implementation and extension language of Isabelle,
+    see also @{cite "isabelle-implementation"}. It is integrated into the
+    logical context of Isabelle/Isar and allows to manipulate logical entities
+    directly. Arbitrary add-on tools may be implemented for object-logics such
+    as Isabelle/HOL.
 
-  \<^descr>[Isabelle/Scala] is the system programming language of
-  Isabelle. It extends the pure logical environment of Isabelle/ML
-  towards the ``real world'' of graphical user interfaces, text
-  editors, IDE frameworks, web services etc.  Special infrastructure
-  allows to transfer algebraic datatypes and formatted text easily
-  between ML and Scala, using asynchronous protocol commands.
+    \<^descr>[Isabelle/Scala] is the system programming language of Isabelle. It
+    extends the pure logical environment of Isabelle/ML towards the ``real
+    world'' of graphical user interfaces, text editors, IDE frameworks, web
+    services etc. Special infrastructure allows to transfer algebraic
+    datatypes and formatted text easily between ML and Scala, using
+    asynchronous protocol commands.
 
-  \<^descr>[jEdit] is a sophisticated text editor implemented in
-  Java.\<^footnote>\<open>@{url "http://www.jedit.org"}\<close> It is easily extensible
-  by plugins written in languages that work on the JVM, e.g.\
-  Scala\<^footnote>\<open>@{url "http://www.scala-lang.org"}\<close>.
+    \<^descr>[jEdit] is a sophisticated text editor implemented in Java.\<^footnote>\<open>@{url
+    "http://www.jedit.org"}\<close> It is easily extensible by plugins written in
+    languages that work on the JVM, e.g.\ Scala\<^footnote>\<open>@{url
+    "http://www.scala-lang.org"}\<close>.
 
-  \<^descr>[Isabelle/jEdit] is the main example application of the PIDE
-  framework and the default user-interface for Isabelle. It targets
-  both beginners and experts. Technically, Isabelle/jEdit combines a
-  slightly modified version of the jEdit code base with a special
-  plugin for Isabelle, integrated as standalone application for the
-  main operating system platforms: Linux, Windows, Mac OS X.
+    \<^descr>[Isabelle/jEdit] is the main example application of the PIDE framework
+    and the default user-interface for Isabelle. It targets both beginners and
+    experts. Technically, Isabelle/jEdit combines a slightly modified version
+    of the jEdit code base with a special plugin for Isabelle, integrated as
+    standalone application for the main operating system platforms: Linux,
+    Windows, Mac OS X.
 
-
-  The subtle differences of Isabelle/ML versus Standard ML,
-  Isabelle/Scala versus Scala, Isabelle/jEdit versus jEdit need to be
-  taken into account when discussing any of these PIDE building blocks
-  in public forums, mailing lists, or even scientific publications.
+  The subtle differences of Isabelle/ML versus Standard ML, Isabelle/Scala
+  versus Scala, Isabelle/jEdit versus jEdit need to be taken into account when
+  discussing any of these PIDE building blocks in public forums, mailing
+  lists, or even scientific publications.
 \<close>
 
 
@@ -73,31 +71,31 @@
   the jEdit text editor, while preserving its general look-and-feel as far as
   possible. The main plugin is called ``Isabelle'' and has its own menu
   \<^emph>\<open>Plugins~/ Isabelle\<close> with access to several panels (see also
-  \secref{sec:dockables}), as well as \<^emph>\<open>Plugins~/ Plugin Options~/
-  Isabelle\<close> (see also \secref{sec:options}).
+  \secref{sec:dockables}), as well as \<^emph>\<open>Plugins~/ Plugin Options~/ Isabelle\<close>
+  (see also \secref{sec:options}).
 
   The options allow to specify a logic session name --- the same selector is
-  accessible in the \<^emph>\<open>Theories\<close> panel (\secref{sec:theories}). On
-  application startup, the selected logic session image is provided
-  automatically by the Isabelle build tool @{cite "isabelle-system"}: if it is
-  absent or outdated wrt.\ its sources, the build process updates it before
-  entering the Prover IDE.  Change of the logic session within Isabelle/jEdit
-  requires a restart of the whole application.
+  accessible in the \<^emph>\<open>Theories\<close> panel (\secref{sec:theories}). On application
+  startup, the selected logic session image is provided automatically by the
+  Isabelle build tool @{cite "isabelle-system"}: if it is absent or outdated
+  wrt.\ its sources, the build process updates it before 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
-  changes, taking the logical structure as a formal document into account (see
-  also \secref{sec:document-model}). The editor and the prover are connected
+  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
   checking of the formal text in parallel on multiple cores, and provides
   feedback via markup, which is rendered in the editor via colors, boxes,
   squiggly underlines, hyperlinks, popup windows, icons, clickable output etc.
 
-  Using the mouse together with the modifier key \<^verbatim>\<open>CONTROL\<close> (Linux,
-  Windows) or \<^verbatim>\<open>COMMAND\<close> (Mac OS X) exposes additional formal content
-  via tooltips and/or hyperlinks (see also \secref{sec:tooltips-hyperlinks}).
-  Output (in popups etc.) may be explored recursively, using the same
-  techniques as in the editor source buffer.
+  Using the mouse together with the modifier key \<^verbatim>\<open>CONTROL\<close> (Linux, Windows)
+  or \<^verbatim>\<open>COMMAND\<close> (Mac OS X) exposes additional formal content via tooltips
+  and/or hyperlinks (see also \secref{sec:tooltips-hyperlinks}). Output (in
+  popups etc.) may be explored recursively, using the same techniques as in
+  the editor source buffer.
 
   Thus the Prover IDE gives an impression of direct access to formal content
   of the prover within the editor, but in reality only certain aspects are
@@ -109,14 +107,13 @@
 subsection \<open>Documentation\<close>
 
 text \<open>
-  The \<^emph>\<open>Documentation\<close> panel of Isabelle/jEdit provides access to the
-  standard Isabelle documentation: PDF files are opened by regular desktop
-  operations of the underlying platform. The section ``Original jEdit
-  Documentation'' contains the original \<^emph>\<open>User's Guide\<close> of this
-  sophisticated text editor. The same is accessible via the \<^verbatim>\<open>Help\<close>
-  menu or \<^verbatim>\<open>F1\<close> keyboard shortcut, using the built-in HTML viewer of
-  Java/Swing. The latter also includes \<^emph>\<open>Frequently Asked Questions\<close> and
-  documentation of individual plugins.
+  The \<^emph>\<open>Documentation\<close> panel of Isabelle/jEdit provides access to the standard
+  Isabelle documentation: PDF files are opened by regular desktop operations
+  of the underlying platform. The section ``Original jEdit Documentation''
+  contains the original \<^emph>\<open>User's Guide\<close> of this sophisticated text editor. The
+  same is accessible via the \<^verbatim>\<open>Help\<close> menu or \<^verbatim>\<open>F1\<close> keyboard shortcut, using
+  the built-in HTML viewer of Java/Swing. The latter also includes
+  \<^emph>\<open>Frequently Asked Questions\<close> and documentation of individual plugins.
 
   Most of the information about generic jEdit is relevant for Isabelle/jEdit
   as well, but one needs to keep in mind that defaults sometimes differ, and
@@ -129,9 +126,9 @@
 subsection \<open>Plugins\<close>
 
 text \<open>
-  The \<^emph>\<open>Plugin Manager\<close> of jEdit allows to augment editor functionality by
-  JVM modules (jars) that are provided by the central plugin repository, which
-  is accessible via various mirror sites.
+  The \<^emph>\<open>Plugin Manager\<close> of jEdit allows to augment editor functionality by JVM
+  modules (jars) that are provided by the central plugin repository, which is
+  accessible via various mirror sites.
 
   Connecting to the plugin server-infrastructure of the jEdit project allows
   to update bundled plugins or to add further functionality. This needs to be
@@ -142,28 +139,27 @@
   at a grand scale.
 
   \<^medskip>
-  The main \<^emph>\<open>Isabelle\<close> plugin is an integral part of
-  Isabelle/jEdit and needs to remain active at all times! A few additional
-  plugins are bundled with Isabelle/jEdit for convenience or out of necessity,
-  notably \<^emph>\<open>Console\<close> with its Isabelle/Scala sub-plugin
-  (\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close> with some Isabelle-specific
-  parsers for document tree structure (\secref{sec:sidekick}). The
-  \<^emph>\<open>Navigator\<close> plugin is particularly important for hyperlinks within the
-  formal document-model (\secref{sec:tooltips-hyperlinks}). Further plugins
-  (e.g.\ \<^emph>\<open>ErrorList\<close>, \<^emph>\<open>Code2HTML\<close>) are included to saturate the
-  dependencies of bundled plugins, but have no particular use in
-  Isabelle/jEdit.
+  The main \<^emph>\<open>Isabelle\<close> plugin is an integral part of Isabelle/jEdit and needs
+  to remain active at all times! A few additional plugins are bundled with
+  Isabelle/jEdit for convenience or out of necessity, notably \<^emph>\<open>Console\<close> with
+  its Isabelle/Scala sub-plugin (\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close>
+  with some Isabelle-specific parsers for document tree structure
+  (\secref{sec:sidekick}). The \<^emph>\<open>Navigator\<close> plugin is particularly important
+  for hyperlinks within the formal document-model
+  (\secref{sec:tooltips-hyperlinks}). Further plugins (e.g.\ \<^emph>\<open>ErrorList\<close>,
+  \<^emph>\<open>Code2HTML\<close>) are included to saturate the dependencies of bundled plugins,
+  but have no particular use in Isabelle/jEdit.
 \<close>
 
 
 subsection \<open>Options \label{sec:options}\<close>
 
-text \<open>Both jEdit and Isabelle have distinctive management of
-  persistent options.
+text \<open>
+  Both jEdit and Isabelle have distinctive management of persistent options.
 
-  Regular jEdit options are accessible via the dialogs \<^emph>\<open>Utilities~/
-  Global Options\<close> or \<^emph>\<open>Plugins~/ Plugin Options\<close>, with a second chance to
-  flip the two within the central options dialog. Changes are stored in
+  Regular jEdit options are accessible via the dialogs \<^emph>\<open>Utilities~/ Global
+  Options\<close> or \<^emph>\<open>Plugins~/ Plugin Options\<close>, with a second chance to flip the
+  two within the central options dialog. Changes are stored in
   @{file_unchecked "$ISABELLE_HOME_USER/jedit/properties"} and
   @{file_unchecked "$ISABELLE_HOME_USER/jedit/keymaps"}.
 
@@ -173,17 +169,17 @@
   coverage of sessions and command-line tools like @{tool build} or @{tool
   options}.
 
-  Those Isabelle options that are declared as \<^bold>\<open>public\<close> are configurable
-  in Isabelle/jEdit via \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>. Moreover,
-  there are various options for rendering of document content, which are
-  configurable via \<^emph>\<open>Plugin Options~/ Isabelle~/ Rendering\<close>. Thus
-  \<^emph>\<open>Plugin Options~/ Isabelle\<close> in jEdit provides a view on a subset of
-  Isabelle system options. Note that some of these options affect general
-  parameters that are relevant outside Isabelle/jEdit as well, e.g.\
-  @{system_option threads} or @{system_option parallel_proofs} for the
-  Isabelle build tool @{cite "isabelle-system"}, but it is possible to use the
-  settings variable @{setting ISABELLE_BUILD_OPTIONS} to change defaults for
-  batch builds without affecting Isabelle/jEdit.
+  Those Isabelle options that are declared as \<^bold>\<open>public\<close> are configurable in
+  Isabelle/jEdit via \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>. Moreover, there
+  are various options for rendering of document content, which are
+  configurable via \<^emph>\<open>Plugin Options~/ Isabelle~/ Rendering\<close>. Thus \<^emph>\<open>Plugin
+  Options~/ Isabelle\<close> in jEdit provides a view on a subset of Isabelle system
+  options. Note that some of these options affect general parameters that are
+  relevant outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or
+  @{system_option parallel_proofs} for the Isabelle build tool @{cite
+  "isabelle-system"}, but it is possible to use the settings variable
+  @{setting ISABELLE_BUILD_OPTIONS} to change defaults for batch builds
+  without affecting Isabelle/jEdit.
 
   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.
@@ -193,24 +189,25 @@
   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
-  running is likely to cause surprise due to lost update!\<close>
+  running is likely to cause surprise due to lost update!
+\<close>
 
 
 subsection \<open>Keymaps\<close>
 
-text \<open>Keyboard shortcuts used to be managed as jEdit properties in
-  the past, but recent versions (2013) have a separate concept of
-  \<^emph>\<open>keymap\<close> that is configurable via \<^emph>\<open>Global Options~/
-  Shortcuts\<close>.  The \<^verbatim>\<open>imported\<close> keymap is derived from the
-  initial environment of properties that is available at the first
-  start of the editor; afterwards the keymap file takes precedence.
+text \<open>
+  Keyboard shortcuts used to be managed as jEdit properties in the past, but
+  recent versions (2013) have a separate concept of \<^emph>\<open>keymap\<close> that is
+  configurable via \<^emph>\<open>Global Options~/ Shortcuts\<close>. The \<^verbatim>\<open>imported\<close> keymap is
+  derived from the initial environment of properties that is available at the
+  first start of the editor; afterwards the keymap file takes precedence.
 
   This is relevant for Isabelle/jEdit due to various fine-tuning of default
   properties, and additional keyboard shortcuts for Isabelle-specific
   functionality. Users may change their keymap later, but need to copy some
   keyboard shortcuts manually (see also @{file_unchecked
-  "$ISABELLE_HOME_USER/jedit/keymaps"} versus \<^verbatim>\<open>shortcut\<close> properties
-  in @{file "$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props"}).
+  "$ISABELLE_HOME_USER/jedit/keymaps"} versus \<^verbatim>\<open>shortcut\<close> properties in @{file
+  "$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props"}).
 \<close>
 
 
@@ -239,33 +236,32 @@
   Start jEdit with Isabelle plugin setup and open FILES
   (default "$USER_HOME/Scratch.thy" or ":" for empty buffer).\<close>}
 
-  The \<^verbatim>\<open>-l\<close> option specifies the session name of the logic
-  image to be used for proof processing.  Additional session root
-  directories may be included via option \<^verbatim>\<open>-d\<close> to augment
-  that name space of @{tool build} @{cite "isabelle-system"}.
+  The \<^verbatim>\<open>-l\<close> option specifies the session name of the logic image to be used
+  for proof processing. Additional session root directories may be included
+  via option \<^verbatim>\<open>-d\<close> to augment that name space of @{tool build} @{cite
+  "isabelle-system"}.
 
-  By default, the specified image is checked and built on demand. The
-  \<^verbatim>\<open>-s\<close> option determines where to store the result session image
-  of @{tool build}. The \<^verbatim>\<open>-n\<close> option bypasses the implicit build
-  process for the selected session image.
+  By default, the specified image is checked and built on demand. The \<^verbatim>\<open>-s\<close>
+  option determines where to store the result session image of @{tool build}.
+  The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
+  session image.
 
-  The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover
-  process. Note that the system option @{system_option_ref jedit_print_mode}
-  allows to do the same persistently (e.g.\ via the \<^emph>\<open>Plugin Options\<close>
-  dialog of Isabelle/jEdit), without requiring command-line invocation.
+  The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover process.
+  Note that the system option @{system_option_ref jedit_print_mode} allows to
+  do the same persistently (e.g.\ via the \<^emph>\<open>Plugin Options\<close> dialog of
+  Isabelle/jEdit), without requiring command-line invocation.
 
-  The \<^verbatim>\<open>-J\<close> and \<^verbatim>\<open>-j\<close> options allow to pass additional
-  low-level options to the JVM or jEdit, respectively. The defaults are
-  provided by the Isabelle settings environment @{cite "isabelle-system"}, but
-  note that these only work for the command-line tool described here, and not
-  the regular application.
+  The \<^verbatim>\<open>-J\<close> and \<^verbatim>\<open>-j\<close> options allow to pass additional low-level options to
+  the JVM or jEdit, respectively. The defaults are provided by the Isabelle
+  settings environment @{cite "isabelle-system"}, but note that these only
+  work for the command-line tool described here, and not the regular
+  application.
 
-  The \<^verbatim>\<open>-b\<close> and \<^verbatim>\<open>-f\<close> options control the self-build
-  mechanism of Isabelle/jEdit. This is only relevant for building from
-  sources, which also requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component
-  from @{url "http://isabelle.in.tum.de/components"}. The official
-  Isabelle release already includes a pre-built version of Isabelle/jEdit.
-\<close>
+  The \<^verbatim>\<open>-b\<close> and \<^verbatim>\<open>-f\<close> options control the self-build mechanism of
+  Isabelle/jEdit. This is only relevant for building from sources, which also
+  requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component from @{url
+  "http://isabelle.in.tum.de/components"}. The official Isabelle release
+  already includes a pre-built version of Isabelle/jEdit. \<close>
 
 
 chapter \<open>Augmented jEdit functionality\<close>
@@ -283,39 +279,35 @@
   Isabelle/jEdit enables platform-specific look-and-feel by default as
   follows.
 
-  \<^descr>[Linux:] The platform-independent \<^emph>\<open>Metal\<close> is used by
-  default.
+    \<^descr>[Linux:] The platform-independent \<^emph>\<open>Metal\<close> is used by default.
 
-  \<^emph>\<open>GTK+\<close> also works under the side-condition that the overall GTK theme
-  is selected in a Swing-friendly way.\<^footnote>\<open>GTK support in Java/Swing was
-  once marketed aggressively by Sun, but never quite finished. Today (2015) it
-  is lagging behind further development of Swing and GTK. The graphics
-  rendering performance can be worse than for other Swing look-and-feels.
-  Nonetheless it has its uses for displays with very high resolution (such as
-  ``4K'' or ``UHD'' models), because the rendering by the external library is
-  subject to global system settings for font scaling.\<close>
+    \<^emph>\<open>GTK+\<close> also works under the side-condition that the overall GTK theme is
+    selected in a Swing-friendly way.\<^footnote>\<open>GTK support in Java/Swing was once
+    marketed aggressively by Sun, but never quite finished. Today (2015) it is
+    lagging behind further development of Swing and GTK. The graphics
+    rendering performance can be worse than for other Swing look-and-feels.
+    Nonetheless it has its uses for displays with very high resolution (such
+    as ``4K'' or ``UHD'' models), because the rendering by the external
+    library is subject to global system settings for font scaling.\<close>
 
-  \<^descr>[Windows:] Regular \<^emph>\<open>Windows\<close> is used by default, but
-  \<^emph>\<open>Windows Classic\<close> also works.
-
-  \<^descr>[Mac OS X:] Regular \<^emph>\<open>Mac OS X\<close> is used by default.
+    \<^descr>[Windows:] Regular \<^emph>\<open>Windows\<close> is used by default, but \<^emph>\<open>Windows Classic\<close>
+    also works.
 
-  The bundled \<^emph>\<open>MacOSX\<close> plugin provides various functions that are
-  expected from applications on that particular platform: quit from menu or
-  dock, preferences menu, drag-and-drop of text files on the application,
-  full-screen mode for main editor windows. It is advisable to have the
-  \<^emph>\<open>MacOSX\<close> plugin enabled all the time on that platform.
+    \<^descr>[Mac OS X:] Regular \<^emph>\<open>Mac OS X\<close> is used by default.
 
+    The bundled \<^emph>\<open>MacOSX\<close> plugin provides various functions that are expected
+    from applications on that particular platform: quit from menu or dock,
+    preferences menu, drag-and-drop of text files on the application,
+    full-screen mode for main editor windows. It is advisable to have the
+    \<^emph>\<open>MacOSX\<close> plugin enabled all the time on that platform.
 
-  Users may experiment with different look-and-feels, but need to keep
-  in mind that this extra variance of GUI functionality is unlikely to
-  work in arbitrary combinations.  The platform-independent
-  \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close> should always work.  The historic
-  \<^emph>\<open>CDE/Motif\<close> should be ignored.
+  Users may experiment with different look-and-feels, but need to keep in mind
+  that this extra variance of GUI functionality is unlikely to work in
+  arbitrary combinations. The platform-independent \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close>
+  should always work. The historic \<^emph>\<open>CDE/Motif\<close> should be ignored.
 
-  After changing the look-and-feel in \<^emph>\<open>Global Options~/
-  Appearance\<close>, it is advisable to restart Isabelle/jEdit in order to
-  take full effect.
+  After changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close>, it is
+  advisable to restart Isabelle/jEdit in order to take full effect.
 \<close>
 
 
@@ -326,49 +318,47 @@
   were considered ``high resolution'' and bitmap fonts with 12 or 14 pixels as
   adequate for text rendering. Today (2015), we routinely see ``Full HD''
   monitors at $1920 \times 1080$ pixels, and occasionally ``Ultra HD'' at
-  $3840 \times 2160$ or more, but GUI rendering did not really progress
-  beyond the old standards.
+  $3840 \times 2160$ or more, but GUI rendering did not really progress beyond
+  the old standards.
 
   Isabelle/jEdit defaults are a compromise for reasonable out-of-the box
   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 \<^bold>\<open>operating-system platform\<close> usually provides some
-  configuration for global scaling of text fonts, e.g.\ $120\%$--$250\%$ on
-  Windows. Changing that only has a partial effect on GUI rendering;
-  satisfactory display quality requires further adjustments.
+  The \<^bold>\<open>operating-system platform\<close> usually provides some configuration for
+  global scaling of text fonts, e.g.\ $120\%$--$250\%$ on Windows. Changing
+  that only has a partial effect on GUI rendering; satisfactory display
+  quality requires further adjustments.
 
   \<^medskip>
-  The Isabelle/jEdit \<^bold>\<open>application\<close> and its plugins provide
-  various font properties that are summarized below.
+  The Isabelle/jEdit \<^bold>\<open>application\<close> and its plugins provide various font
+  properties that are summarized below.
 
-  \<^item> \<^emph>\<open>Global Options / Text Area / Text font\<close>: the main text area
-  font, which is also used as reference point for various derived font sizes,
-  e.g.\ the Output panel (\secref{sec:output}).
+    \<^item> \<^emph>\<open>Global Options / Text Area / Text font\<close>: the main text area font,
+    which is also used as reference point for various derived font sizes,
+    e.g.\ the Output panel (\secref{sec:output}).
 
-  \<^item> \<^emph>\<open>Global Options / Gutter / Gutter font\<close>: the font for the gutter
-  area left of the main text area, e.g.\ relevant for display of line numbers
-  (disabled by default).
+    \<^item> \<^emph>\<open>Global Options / Gutter / Gutter font\<close>: the font for the gutter area
+    left of the main text area, e.g.\ relevant for display of line numbers
+    (disabled by default).
 
-  \<^item> \<^emph>\<open>Global Options / Appearance / Button, menu and label font\<close> as
-  well as \<^emph>\<open>List and text field font\<close>: this specifies the primary and
-  secondary font for the traditional \<^emph>\<open>Metal\<close> look-and-feel
-  (\secref{sec:look-and-feel}), which happens to scale better than newer ones
-  like \<^emph>\<open>Nimbus\<close>.
+    \<^item> \<^emph>\<open>Global Options / Appearance / Button, menu and label font\<close> as well as
+    \<^emph>\<open>List and text field font\<close>: this specifies the primary and secondary font
+    for the traditional \<^emph>\<open>Metal\<close> look-and-feel (\secref{sec:look-and-feel}),
+    which happens to scale better than newer ones like \<^emph>\<open>Nimbus\<close>.
 
-  \<^item> \<^emph>\<open>Plugin Options / Isabelle / General / Reset Font Size\<close>: the main
-  text area font size for action @{action_ref "isabelle.reset-font-size"},
-  e.g.\ relevant for quick scaling like in major web browsers.
+    \<^item> \<^emph>\<open>Plugin Options / Isabelle / General / Reset Font Size\<close>: the main text
+    area font size for action @{action_ref "isabelle.reset-font-size"}, e.g.\
+    relevant for quick scaling like in major web browsers.
 
-  \<^item> \<^emph>\<open>Plugin Options / Console / General / Font\<close>: the console window
-  font, e.g.\ relevant for Isabelle/Scala command-line.
-
+    \<^item> \<^emph>\<open>Plugin Options / Console / General / Font\<close>: the console window font,
+    e.g.\ relevant for Isabelle/Scala command-line.
 
-  In \figref{fig:isabelle-jedit-hdpi} the \<^emph>\<open>Metal\<close> look-and-feel is
-  configured with custom fonts at 30 pixels, and the main text area and
-  console at 36 pixels. Despite the old-fashioned appearance of \<^emph>\<open>Metal\<close>,
-  this leads to decent rendering quality on all platforms.
+  In \figref{fig:isabelle-jedit-hdpi} the \<^emph>\<open>Metal\<close> look-and-feel is configured
+  with custom fonts at 30 pixels, and the main text area and console at 36
+  pixels. Despite the old-fashioned appearance of \<^emph>\<open>Metal\<close>, this leads to
+  decent rendering quality on all platforms.
 
   \begin{figure}[htb]
   \begin{center}
@@ -387,25 +377,25 @@
 section \<open>Dockable windows \label{sec:dockables}\<close>
 
 text \<open>
-  In jEdit terminology, a \<^emph>\<open>view\<close> is an editor window with one or more
-  \<^emph>\<open>text areas\<close> that show the content of one or more \<^emph>\<open>buffers\<close>. A
-  regular view may be surrounded by \<^emph>\<open>dockable windows\<close> that show
-  additional information in arbitrary format, not just text; a \<^emph>\<open>plain
-  view\<close> does not allow dockables. The \<^emph>\<open>dockable window manager\<close> of jEdit
-  organizes these dockable windows, either as \<^emph>\<open>floating\<close> windows, or
-  \<^emph>\<open>docked\<close> panels within one of the four margins of the view. There may
-  be any number of floating instances of some dockable window, but at most one
-  docked instance; jEdit actions that address \<^emph>\<open>the\<close> dockable window of a
-  particular kind refer to the unique docked instance.
+  In jEdit terminology, a \<^emph>\<open>view\<close> is an editor window with one or more \<^emph>\<open>text
+  areas\<close> that show the content of one or more \<^emph>\<open>buffers\<close>. A regular view may
+  be surrounded by \<^emph>\<open>dockable windows\<close> that show additional information in
+  arbitrary format, not just text; a \<^emph>\<open>plain view\<close> does not allow dockables.
+  The \<^emph>\<open>dockable window manager\<close> of jEdit organizes these dockable windows,
+  either as \<^emph>\<open>floating\<close> windows, or \<^emph>\<open>docked\<close> panels within one of the four
+  margins of the view. There may be any number of floating instances of some
+  dockable window, but at most one docked instance; jEdit actions that address
+  \<^emph>\<open>the\<close> dockable window of a particular kind refer to the unique docked
+  instance.
 
   Dockables are used routinely in jEdit for important functionality like
-  \<^emph>\<open>HyperSearch Results\<close> or the \<^emph>\<open>File System Browser\<close>. Plugins often
-  provide a central dockable to access their key functionality, which may be
-  opened by the user on demand. The Isabelle/jEdit plugin takes this approach
-  to the extreme: its plugin menu provides the entry-points to many panels
-  that are managed as dockable windows. Some important panels are docked by
-  default, e.g.\ \<^emph>\<open>Documentation\<close>, \<^emph>\<open>Output\<close>, \<^emph>\<open>Query\<close>, but the
-  user can change this arrangement easily and persistently.
+  \<^emph>\<open>HyperSearch Results\<close> or the \<^emph>\<open>File System Browser\<close>. Plugins often provide
+  a central dockable to access their key functionality, which may be opened by
+  the user on demand. The Isabelle/jEdit plugin takes this approach to the
+  extreme: its plugin menu provides the entry-points to many panels that are
+  managed as dockable windows. Some important panels are docked by default,
+  e.g.\ \<^emph>\<open>Documentation\<close>, \<^emph>\<open>Output\<close>, \<^emph>\<open>Query\<close>, but the user can change this
+  arrangement easily and persistently.
 
   Compared to plain jEdit, dockable window management in Isabelle/jEdit is
   slightly augmented according to the the following principles:
@@ -439,19 +429,18 @@
   Isabelle sources consist of \<^emph>\<open>symbols\<close> that extend plain ASCII to allow
   infinitely many mathematical symbols within the formal sources. This works
   without depending on particular encodings and varying Unicode
-  standards.\<^footnote>\<open>Raw Unicode characters within formal sources would
-  compromise portability and reliability in the face of changing
-  interpretation of special features of Unicode, such as Combining Characters
-  or Bi-directional Text.\<close> See also @{cite "Wenzel:2011:CICM"}.
+  standards.\<^footnote>\<open>Raw Unicode characters within formal sources would compromise
+  portability and reliability in the face of changing interpretation of
+  special features of Unicode, such as Combining Characters or Bi-directional
+  Text.\<close> See also @{cite "Wenzel:2011:CICM"}.
 
   For the prover back-end, formal text consists of ASCII characters that are
-  grouped according to some simple rules, e.g.\ as plain ``\<^verbatim>\<open>a\<close>'' or
-  symbolic ``\<^verbatim>\<open>\<alpha>\<close>''. For the editor front-end, a certain subset of
-  symbols is rendered physically via Unicode glyphs, in order to show
-  ``\<^verbatim>\<open>\<alpha>\<close>'' as ``\<open>\<alpha>\<close>'', for example. This symbol
-  interpretation is specified by the Isabelle system distribution in @{file
-  "$ISABELLE_HOME/etc/symbols"} and may be augmented by the user in
-  @{file_unchecked "$ISABELLE_HOME_USER/etc/symbols"}.
+  grouped according to some simple rules, e.g.\ as plain ``\<^verbatim>\<open>a\<close>'' or symbolic
+  ``\<^verbatim>\<open>\<alpha>\<close>''. For the editor front-end, a certain subset of symbols is rendered
+  physically via Unicode glyphs, in order to show ``\<^verbatim>\<open>\<alpha>\<close>'' as ``\<open>\<alpha>\<close>'', for
+  example. This symbol interpretation is specified by the Isabelle system
+  distribution in @{file "$ISABELLE_HOME/etc/symbols"} and may be augmented by
+  the user in @{file_unchecked "$ISABELLE_HOME_USER/etc/symbols"}.
 
   The appendix of @{cite "isabelle-isar-ref"} gives an overview of the
   standard interpretation of finitely many symbols from the infinite
@@ -484,13 +473,13 @@
 
   Note that a Java/AWT/Swing application can load additional fonts only if
   they are not installed on the operating system already! Some outdated
-  version of \<^verbatim>\<open>IsabelleText\<close> that happens to be provided by the
-  operating system would prevent Isabelle/jEdit to use its bundled version.
-  This could lead to missing glyphs (black rectangles), when the system
-  version of \<^verbatim>\<open>IsabelleText\<close> is older than the application version.
-  This problem can be avoided by refraining to ``install'' any version of
-  \<^verbatim>\<open>IsabelleText\<close> in the first place, although it is occasionally
-  tempting to use the same font in other applications.
+  version of \<^verbatim>\<open>IsabelleText\<close> that happens to be provided by the operating
+  system would prevent Isabelle/jEdit to use its bundled version. This could
+  lead to missing glyphs (black rectangles), when the system version of
+  \<^verbatim>\<open>IsabelleText\<close> is older than the application version. This problem can be
+  avoided by refraining to ``install'' any version of \<^verbatim>\<open>IsabelleText\<close> in the
+  first place, although it is occasionally tempting to use the same font in
+  other applications.
 \<close>
 
 paragraph \<open>Input methods.\<close>
@@ -548,17 +537,16 @@
     \<open>\<notin>\<close> & \<^verbatim>\<open>\notin\<close> & \<^verbatim>\<open>~:\<close> \\
   \end{tabular}
   \<^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
-  Isabelle source that use ASCII replacement notation like \<^verbatim>\<open>!\<close> or
-  \<^verbatim>\<open>ALL\<close> directly in the text.
+  Isabelle source that use ASCII replacement notation like \<^verbatim>\<open>!\<close> or \<^verbatim>\<open>ALL\<close>
+  directly in the text.
 
   On the other hand, coincidence of symbol abbreviations with ASCII
-  replacement syntax syntax helps to update old theory sources via
-  explicit completion (see also \<^verbatim>\<open>C+b\<close> explained in
-  \secref{sec:completion}).
+  replacement syntax syntax helps to update old theory sources via explicit
+  completion (see also \<^verbatim>\<open>C+b\<close> explained in \secref{sec:completion}).
 \<close>
 
 paragraph \<open>Control symbols.\<close>
@@ -596,8 +584,7 @@
 
   Isabelle/jEdit provides SideKick parsers for its main mode for theory files,
   as well as some minor modes for the \<^verbatim>\<open>NEWS\<close> file (see
-  \figref{fig:sidekick}), session \<^verbatim>\<open>ROOT\<close> files, and system
-  \<^verbatim>\<open>options\<close>.
+  \figref{fig:sidekick}), session \<^verbatim>\<open>ROOT\<close> files, and system \<^verbatim>\<open>options\<close>.
 
   \begin{figure}[htb]
   \begin{center}
@@ -607,35 +594,33 @@
   \label{fig:sidekick}
   \end{figure}
 
-  Moreover, the special SideKick parser \<^verbatim>\<open>isabelle-markup\<close>
-  provides access to the full (uninterpreted) markup tree of the PIDE
-  document model of the current buffer.  This is occasionally useful
-  for informative purposes, but the amount of displayed information
-  might cause problems for large buffers, both for the human and the
-  machine.
+  Moreover, the special SideKick parser \<^verbatim>\<open>isabelle-markup\<close> provides access to
+  the full (uninterpreted) markup tree of the PIDE document model of the
+  current buffer. This is occasionally useful for informative purposes, but
+  the amount of displayed information might cause problems for large buffers,
+  both for the human and the machine.
 \<close>
 
 
 section \<open>Scala console \label{sec:scala-console}\<close>
 
 text \<open>
-  The \<^emph>\<open>Console\<close> plugin manages various shells (command interpreters),
-  e.g.\ \<^emph>\<open>BeanShell\<close>, which is the official jEdit scripting language, and
-  the cross-platform \<^emph>\<open>System\<close> shell. Thus the console provides similar
-  functionality than the Emacs buffers \<^verbatim>\<open>*scratch*\<close> and
-  \<^verbatim>\<open>*shell*\<close>.
+  The \<^emph>\<open>Console\<close> plugin manages various shells (command interpreters), e.g.\
+  \<^emph>\<open>BeanShell\<close>, which is the official jEdit scripting language, and the
+  cross-platform \<^emph>\<open>System\<close> shell. Thus the console provides similar
+  functionality than the Emacs buffers \<^verbatim>\<open>*scratch*\<close> and \<^verbatim>\<open>*shell*\<close>.
 
-  Isabelle/jEdit extends the repertoire of the console by \<^emph>\<open>Scala\<close>, which
-  is the regular Scala toplevel loop running inside the same JVM process as
+  Isabelle/jEdit extends the repertoire of the console by \<^emph>\<open>Scala\<close>, which is
+  the regular Scala toplevel loop running inside the same JVM process as
   Isabelle/jEdit itself. This means the Scala command interpreter has access
   to the JVM name space and state of the running Prover IDE application. The
   default environment imports the full content of packages \<^verbatim>\<open>isabelle\<close> and
   \<^verbatim>\<open>isabelle.jedit\<close>.
 
-  For example, \<^verbatim>\<open>PIDE\<close> refers to the Isabelle/jEdit plugin object,
-  and \<^verbatim>\<open>view\<close> to the current editor view of jEdit. The Scala
-  expression \<^verbatim>\<open>PIDE.snapshot(view)\<close> makes a PIDE document snapshot
-  of the current buffer within the current editor view.
+  For example, \<^verbatim>\<open>PIDE\<close> refers to the Isabelle/jEdit plugin object, and \<^verbatim>\<open>view\<close>
+  to the current editor view of jEdit. The Scala expression
+  \<^verbatim>\<open>PIDE.snapshot(view)\<close> makes a PIDE document snapshot of the current buffer
+  within the current editor view.
 
   This helps to explore Isabelle/Scala functionality interactively. Some care
   is required to avoid interference with the internals of the running
@@ -649,10 +634,10 @@
   File specifications in jEdit follow various formats and conventions
   according to \<^emph>\<open>Virtual File Systems\<close>, which may be also provided by
   additional plugins. This allows to access remote files via the \<^verbatim>\<open>http:\<close>
-  protocol prefix, for example. Isabelle/jEdit attempts to work with
-  the file-system model of jEdit as far as possible. In particular, theory
-  sources are passed directly from the editor to the prover, without
-  indirection via physical files.
+  protocol prefix, for example. Isabelle/jEdit attempts to work with the
+  file-system model of jEdit as far as possible. In particular, theory sources
+  are passed directly from the editor to the prover, without indirection via
+  physical files.
 
   Despite the flexibility of URLs in jEdit, local files are particularly
   important and are accessible without protocol prefix. Here the path notation
@@ -663,12 +648,11 @@
 
   The Java notation for files needs to be distinguished from the one of
   Isabelle, which uses POSIX notation with forward slashes on \<^emph>\<open>all\<close>
-  platforms.\<^footnote>\<open>Isabelle/ML on Windows uses Cygwin file-system access
-  and Unix-style path notation.\<close> Moreover, environment variables from the
-  Isabelle process may be used freely, e.g.\ @{file
-  "$ISABELLE_HOME/etc/symbols"} or @{file_unchecked "$POLYML_HOME/README"}.
-  There are special shortcuts: @{file "~"} for @{file "$USER_HOME"} and @{file
-  "~~"} for @{file "$ISABELLE_HOME"}.
+  platforms.\<^footnote>\<open>Isabelle/ML on Windows uses Cygwin file-system access and
+  Unix-style path notation.\<close> Moreover, environment variables from the Isabelle
+  process may be used freely, e.g.\ @{file "$ISABELLE_HOME/etc/symbols"} or
+  @{file_unchecked "$POLYML_HOME/README"}. 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
@@ -681,20 +665,19 @@
   (\secref{sec:command-line}).
 
   Isabelle/jEdit imitates \<^verbatim>\<open>$ISABELLE_HOME\<close> and \<^verbatim>\<open>$ISABELLE_HOME_USER\<close> within
-  the Java process environment, in order to
-  allow easy access to these important places from the editor. The file
-  browser of jEdit also includes \<^emph>\<open>Favorites\<close> for these two important
-  locations.
+  the Java process environment, in order to allow easy access to these
+  important places from the editor. The file browser of jEdit also includes
+  \<^emph>\<open>Favorites\<close> for these two important locations.
 
   \<^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.
+  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.
 
   Formally checked paths in prover input are subject to completion
-  (\secref{sec:completion}): partial specifications are resolved via
-  directory content and possible completions are offered in a popup.
+  (\secref{sec:completion}): partial specifications are resolved via directory
+  content and possible completions are offered in a popup.
 \<close>
 
 
@@ -720,9 +703,9 @@
 text \<open>
   As a regular text editor, jEdit maintains a collection of \<^emph>\<open>buffers\<close> to
   store text files; each buffer may be associated with any number of visible
-  \<^emph>\<open>text areas\<close>. Buffers are subject to an \<^emph>\<open>edit mode\<close> that is
-  determined from the file name extension. The following modes are treated
-  specifically in Isabelle/jEdit:
+  \<^emph>\<open>text areas\<close>. Buffers are subject to an \<^emph>\<open>edit mode\<close> that is determined
+  from the file name extension. The following modes are treated specifically
+  in Isabelle/jEdit:
 
   \<^medskip>
   \begin{tabular}{lll}
@@ -734,17 +717,16 @@
   \<^medskip>
 
   All jEdit buffers are automatically added to the PIDE document-model as
-  \<^emph>\<open>document nodes\<close>. The overall document structure is defined by the
-  theory nodes in two dimensions:
+  \<^emph>\<open>document nodes\<close>. The overall document structure is defined by the theory
+  nodes in two dimensions:
 
-  \<^enum> via \<^bold>\<open>theory imports\<close> that are specified in the \<^emph>\<open>theory
-  header\<close> using concrete syntax of the @{command_ref theory} command
-  @{cite "isabelle-isar-ref"};
+    \<^enum> via \<^bold>\<open>theory imports\<close> that are specified in the \<^emph>\<open>theory header\<close> using
+    concrete syntax of the @{command_ref theory} command @{cite
+    "isabelle-isar-ref"};
 
-  \<^enum> via \<^bold>\<open>auxiliary files\<close> that are loaded into a theory by special
-  \<^emph>\<open>load commands\<close>, notably @{command_ref ML_file} and @{command_ref
-  SML_file} @{cite "isabelle-isar-ref"}.
-
+    \<^enum> via \<^bold>\<open>auxiliary files\<close> that are loaded into a theory by special \<^emph>\<open>load
+    commands\<close>, notably @{command_ref ML_file} and @{command_ref SML_file}
+    @{cite "isabelle-isar-ref"}.
 
   In any case, source files are managed by the PIDE infrastructure: the
   physical file-system only plays a subordinate role. The relevant version of
@@ -756,12 +738,12 @@
 subsection \<open>Theories \label{sec:theories}\<close>
 
 text \<open>
-  The \<^emph>\<open>Theories\<close> panel (see also \figref{fig:theories}) provides an
-  overview of the status of continuous checking of theory nodes within the
-  document model. Unlike batch sessions of @{tool build} @{cite
-  "isabelle-system"}, theory nodes are identified by full path names; this allows
-  to work with multiple (disjoint) Isabelle sessions simultaneously within the
-  same editor session.
+  The \<^emph>\<open>Theories\<close> panel (see also \figref{fig:theories}) provides an overview
+  of the status of continuous checking of theory nodes within the document
+  model. Unlike batch sessions of @{tool build} @{cite "isabelle-system"},
+  theory nodes are identified by full path names; this allows to work with
+  multiple (disjoint) Isabelle sessions simultaneously within the same editor
+  session.
 
   \begin{figure}[htb]
   \begin{center}
@@ -780,38 +762,36 @@
   @{system_option jedit_auto_load}.
 
   \<^medskip>
-  The visible \<^emph>\<open>perspective\<close> of Isabelle/jEdit is defined by the
-  collective view on theory buffers via open text areas. The perspective is
-  taken as a hint for document processing: the prover ensures that those parts
-  of a theory where the user is looking are checked, while other parts that
-  are presently not required are ignored. The perspective is changed by
-  opening or closing text area windows, or scrolling within a window.
+  The visible \<^emph>\<open>perspective\<close> of Isabelle/jEdit is defined by the collective
+  view on theory buffers via open text areas. The perspective is taken as a
+  hint for document processing: the prover ensures that those parts of a
+  theory where the user is looking are checked, while other parts that are
+  presently not required are ignored. The perspective is changed by opening or
+  closing text area windows, or scrolling within a window.
 
-  The \<^emph>\<open>Theories\<close> panel provides some further options to influence
-  the process of continuous checking: it may be switched off globally
-  to restrict the prover to superficial processing of command syntax.
-  It is also possible to indicate theory nodes as \<^emph>\<open>required\<close> for
-  continuous checking: this means such nodes and all their imports are
-  always processed independently of the visibility status (if
-  continuous checking is enabled).  Big theory libraries that are
-  marked as required can have significant impact on performance,
+  The \<^emph>\<open>Theories\<close> panel provides some further options to influence the process
+  of continuous checking: it may be switched off globally to restrict the
+  prover to superficial processing of command syntax. It is also possible to
+  indicate theory nodes as \<^emph>\<open>required\<close> for continuous checking: this means
+  such nodes and all their imports are always processed independently of the
+  visibility status (if continuous checking is enabled). Big theory libraries
+  that are marked as required can have significant impact on performance,
   though.
 
   \<^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
-  syntax-highlighting via static keywords and tokenization within the editor;
-  this buffer syntax is determined from theory imports. In contrast, the
-  painting of inner syntax (term language etc.)\ uses semantic information
-  that is reported dynamically from the logical context. Thus the prover can
-  provide additional markup to help the user to understand the meaning of
-  formal text, and to produce more text with some add-on tools (e.g.\
-  information messages with \<^emph>\<open>sendback\<close> markup by automated provers or
-  disprovers in the background).
+  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 syntax-highlighting
+  via static keywords and tokenization within the editor; this buffer syntax
+  is determined from theory imports. In contrast, the painting of inner syntax
+  (term language etc.)\ uses semantic information that is reported dynamically
+  from the logical context. Thus the prover can provide additional markup to
+  help the user to understand the meaning of formal text, and to produce more
+  text with some add-on tools (e.g.\ information messages with \<^emph>\<open>sendback\<close>
+  markup by automated provers or disprovers in the background).
+\<close>
 
-\<close>
 
 subsection \<open>Auxiliary files \label{sec:aux-files}\<close>
 
@@ -826,14 +806,13 @@
   treated as changes of the corresponding load command.
 
   \<^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
-  Isabelle/HOL may be edited conveniently in the Prover IDE on small machines
-  with only 8\,GB of main memory. Using \<^verbatim>\<open>Pure\<close> as logic session
-  image, the exploration may start at the top @{file
-  "$ISABELLE_HOME/src/HOL/Main.thy"} or the bottom @{file
+  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 Isabelle/HOL may be
+  edited conveniently in the Prover IDE on small machines with only 8\,GB of
+  main memory. Using \<^verbatim>\<open>Pure\<close> as logic session image, the exploration may start
+  at the top @{file "$ISABELLE_HOME/src/HOL/Main.thy"} or the bottom @{file
   "$ISABELLE_HOME/src/HOL/HOL.thy"}, for example.
 
   Initially, before an auxiliary file is opened in the editor, the prover
@@ -853,30 +832,30 @@
   morally unsupported and might lead to confusion.
 
   \<^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}).
+  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}).
 
   Warnings, errors, and other useful markup is attached directly to the
   positions in the auxiliary file buffer, in the manner of other well-known
   IDEs. By using the load command @{command SML_file} as explained in @{file
   "$ISABELLE_HOME/src/Tools/SML/Examples.thy"}, Isabelle/jEdit may be used as
   fully-featured IDE for Standard ML, independently of theory or proof
-  development: the required theory merely serves as some kind of project
-  file for a collection of SML source modules.
+  development: the required theory merely serves as some kind of project file
+  for a collection of SML source modules.
 \<close>
 
 
 section \<open>Output \label{sec:output}\<close>
 
 text \<open>
-  Prover output consists of \<^emph>\<open>markup\<close> and \<^emph>\<open>messages\<close>. Both are
-  directly attached to the corresponding positions in the original source
-  text, and visualized in the text area, e.g.\ as text colours for free and
-  bound variables, or as squiggly underlines for warnings, errors etc.\ (see
-  also \figref{fig:output}). In the latter case, the corresponding messages
-  are shown by hovering with the mouse over the highlighted text --- although
-  in many situations the user should already get some clue by looking at the
+  Prover output consists of \<^emph>\<open>markup\<close> and \<^emph>\<open>messages\<close>. Both are directly
+  attached to the corresponding positions in the original source text, and
+  visualized in the text area, e.g.\ as text colours for free and bound
+  variables, or as squiggly underlines for warnings, errors etc.\ (see also
+  \figref{fig:output}). In the latter case, the corresponding messages are
+  shown by hovering with the mouse over the highlighted text --- although in
+  many situations the user should already get some clue by looking at the
   position of the text highlighting, without the text itself.
 
   \begin{figure}[htb]
@@ -888,11 +867,10 @@
   \label{fig:output}
   \end{figure}
 
-  The ``gutter area'' on the left-hand-side of the text area uses
-  icons to provide a summary of the messages within the adjacent
-  line of text.  Message priorities are used to prefer errors over
-  warnings, warnings over information messages, but plain output is
-  ignored.
+  The ``gutter area'' on the left-hand-side of the text area uses icons to
+  provide a summary of the messages within the adjacent line of text. Message
+  priorities are used to prefer errors over warnings, warnings over
+  information messages, but plain output is ignored.
 
   The ``overview area'' on the right-hand-side of the text area uses similar
   information to paint small rectangles for the overall status of the whole
@@ -900,16 +878,14 @@
   the given window height. Mouse clicks on the overview area position the
   cursor approximately to the corresponding line of text in the buffer.
 
-  Another course-grained overview is provided by the \<^emph>\<open>Theories\<close>
-  panel, but without direct correspondence to text positions.  A
-  double-click on one of the theory entries with their status overview
-  opens the corresponding text buffer, without changing the cursor
-  position.
+  Another course-grained overview is provided by the \<^emph>\<open>Theories\<close> panel, but
+  without direct correspondence to text positions. A double-click on one of
+  the theory entries with their status overview opens the corresponding text
+  buffer, without changing the cursor position.
 
   \<^medskip>
-  In addition, the \<^emph>\<open>Output\<close> panel displays prover
-  messages that correspond to a given command, within a separate
-  window.
+  In addition, the \<^emph>\<open>Output\<close> panel displays prover messages that correspond to
+  a given command, within a separate window.
 
   The cursor position in the presently active text area determines the prover
   command whose cumulative message output is appended and shown in that window
@@ -925,36 +901,34 @@
   possible to do meaningful proof editing within the primary text area and its
   markup, while using secondary output windows only rarely.
 
-  The main purpose of the output window is to ``debug'' unclear
-  situations by inspecting internal state of the prover.\<^footnote>\<open>In
-  that sense, unstructured tactic scripts depend on continuous
-  debugging with internal state inspection.\<close> Consequently, some
-  special messages for \<^emph>\<open>tracing\<close> or \<^emph>\<open>proof state\<close> only
+  The main purpose of the output window is to ``debug'' unclear situations by
+  inspecting internal state of the prover.\<^footnote>\<open>In that sense, unstructured tactic
+  scripts depend on continuous debugging with internal state inspection.\<close>
+  Consequently, some special messages for \<^emph>\<open>tracing\<close> or \<^emph>\<open>proof state\<close> only
   appear here, and are not attached to the original source.
 
   \<^medskip>
-  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
-  \secref{sec:sledgehammer}).\<close>
+  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 \secref{sec:sledgehammer}).
+\<close>
 
 
 section \<open>Query \label{sec:query}\<close>
 
 text \<open>
-  The \<^emph>\<open>Query\<close> panel provides various GUI forms to request extra
-  information from the prover. In old times the user would have issued some
-  diagnostic command like @{command find_theorems} and inspected its output,
-  but this is now integrated into the Prover IDE.
+  The \<^emph>\<open>Query\<close> panel provides various GUI forms to request extra information
+  from the prover. In old times the user would have issued some diagnostic
+  command like @{command find_theorems} and inspected its output, but this is
+  now integrated into the Prover IDE.
 
-  A \<^emph>\<open>Query\<close> window provides some input fields and buttons for a
-  particular query command, with output in a dedicated text area. There are
-  various query modes: \<^emph>\<open>Find Theorems\<close>, \<^emph>\<open>Find Constants\<close>,
-  \<^emph>\<open>Print Context\<close>, e.g.\ see \figref{fig:query}. As usual in jEdit,
-  multiple \<^emph>\<open>Query\<close> windows may be active at the same time: any number of
-  floating instances, but at most one docked instance (which is used by
-  default).
+  A \<^emph>\<open>Query\<close> window provides some input fields and buttons for a particular
+  query command, with output in a dedicated text area. There are various query
+  modes: \<^emph>\<open>Find Theorems\<close>, \<^emph>\<open>Find Constants\<close>, \<^emph>\<open>Print Context\<close>, e.g.\ see
+  \figref{fig:query}. As usual in jEdit, multiple \<^emph>\<open>Query\<close> windows may be
+  active at the same time: any number of floating instances, but at most one
+  docked instance (which is used by default).
 
   \begin{figure}[htb]
   \begin{center}
@@ -967,20 +941,19 @@
   \<^medskip>
   The following GUI elements are common to all query modes:
 
-  \<^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 spinning wheel provides feedback about the status of a pending query
+    wrt.\ the evaluation of its context and its own operation.
 
-  \<^item> The \<^emph>\<open>Apply\<close> button attaches a fresh query invocation to the
-  current context of the command where the cursor is pointing in the text.
+    \<^item> The \<^emph>\<open>Apply\<close> button attaches a fresh query invocation to the current
+    context of the command where the cursor is pointing in the text.
 
-  \<^item> The \<^emph>\<open>Search\<close> field allows to highlight query output according to
-  some regular expression, in the notation that is commonly used on the Java
-  platform.\<^footnote>\<open>@{url
-  "https://docs.oracle.com/javase/8/docs/api/java/util/regex/Pattern.html"}\<close>
-  This may serve as an additional visual filter of the result.
+    \<^item> The \<^emph>\<open>Search\<close> field allows to highlight query output according to some
+    regular expression, in the notation that is commonly used on the Java
+    platform.\<^footnote>\<open>@{url
+    "https://docs.oracle.com/javase/8/docs/api/java/util/regex/Pattern.html"}\<close>
+    This may serve as an additional visual filter of the result.
 
-  \<^item> The \<^emph>\<open>Zoom\<close> box controls the font size of the output area.
-
+    \<^item> The \<^emph>\<open>Zoom\<close> box controls the font size of the output area.
 
   All query operations are asynchronous: there is no need to wait for the
   evaluation of the document for the query context, nor for the query
@@ -994,26 +967,26 @@
 subsection \<open>Find theorems\<close>
 
 text \<open>
-  The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Theorems\<close> mode retrieves facts from the
-  theory or proof context matching all of given criteria in the \<^emph>\<open>Find\<close>
-  text field. A single criterium has the following syntax:
+  The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Theorems\<close> mode retrieves facts from the theory
+  or proof context matching all of given criteria in the \<^emph>\<open>Find\<close> text field. A
+  single criterium has the following syntax:
 
   @{rail \<open>
     ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
       'solves' | 'simp' ':' @{syntax term} | @{syntax term})
   \<close>}
 
-  See also the Isar command @{command_ref find_theorems} in
-  @{cite "isabelle-isar-ref"}.
+  See also the Isar command @{command_ref find_theorems} in @{cite
+  "isabelle-isar-ref"}.
 \<close>
 
 
 subsection \<open>Find constants\<close>
 
 text \<open>
-  The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Constants\<close> mode prints all constants
-  whose type meets all of the given criteria in the \<^emph>\<open>Find\<close> text field.
-  A single criterium has the following syntax:
+  The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Constants\<close> mode prints all constants whose type
+  meets all of the given criteria in the \<^emph>\<open>Find\<close> text field. A single
+  criterium has the following syntax:
 
   @{rail \<open>
     ('-'?)
@@ -1028,8 +1001,8 @@
 subsection \<open>Print context\<close>
 
 text \<open>
-  The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Print Context\<close> mode prints information from
-  the theory or proof context, or proof state. See also the Isar commands
+  The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Print Context\<close> mode prints information from the
+  theory or proof context, or proof state. See also the Isar commands
   @{command_ref print_context}, @{command_ref print_cases}, @{command_ref
   print_term_bindings}, @{command_ref print_theorems}, @{command_ref
   print_state} described in @{cite "isabelle-isar-ref"}.
@@ -1040,12 +1013,11 @@
 
 text \<open>
   Formally processed text (prover input or output) contains rich markup
-  information that can be explored further by using the \<^verbatim>\<open>CONTROL\<close>
-  modifier key on Linux and Windows, or \<^verbatim>\<open>COMMAND\<close> on Mac OS X.
-  Hovering with the mouse while the modifier is pressed reveals a
-  \<^emph>\<open>tooltip\<close> (grey box over the text with a yellow popup) and/or a
-  \<^emph>\<open>hyperlink\<close> (black rectangle over the text with change of mouse
-  pointer); see also \figref{fig:tooltip}.
+  information that can be explored further by using the \<^verbatim>\<open>CONTROL\<close> modifier
+  key on Linux and Windows, or \<^verbatim>\<open>COMMAND\<close> on Mac OS X. Hovering with the mouse
+  while the modifier is pressed reveals a \<^emph>\<open>tooltip\<close> (grey box over the text
+  with a yellow popup) and/or a \<^emph>\<open>hyperlink\<close> (black rectangle over the text
+  with change of mouse pointer); see also \figref{fig:tooltip}.
 
   \begin{figure}[htb]
   \begin{center}
@@ -1055,9 +1027,9 @@
   \label{fig:tooltip}
   \end{figure}
 
-  Tooltip popups use the same rendering mechanisms as the main text
-  area, and further tooltips and/or hyperlinks may be exposed
-  recursively by the same mechanism; see \figref{fig:nested-tooltips}.
+  Tooltip popups use the same rendering mechanisms as the main text area, and
+  further tooltips and/or hyperlinks may be exposed recursively by the same
+  mechanism; see \figref{fig:nested-tooltips}.
 
   \begin{figure}[htb]
   \begin{center}
@@ -1067,25 +1039,24 @@
   \label{fig:nested-tooltips}
   \end{figure}
 
-  The tooltip popup window provides some controls to \<^emph>\<open>close\<close> or
-  \<^emph>\<open>detach\<close> the window, turning it into a separate \<^emph>\<open>Info\<close>
-  window managed by jEdit.  The \<^verbatim>\<open>ESCAPE\<close> key closes
-  \<^emph>\<open>all\<close> popups, which is particularly relevant when nested
-  tooltips are stacking up.
+  The tooltip popup window provides some controls to \<^emph>\<open>close\<close> or \<^emph>\<open>detach\<close> the
+  window, turning it into a separate \<^emph>\<open>Info\<close> window managed by jEdit. The
+  \<^verbatim>\<open>ESCAPE\<close> key closes \<^emph>\<open>all\<close> popups, which is particularly relevant when
+  nested tooltips are stacking up.
 
   \<^medskip>
-  A black rectangle in the text indicates a hyperlink that may be
-  followed by a mouse click (while the \<^verbatim>\<open>CONTROL\<close> or \<^verbatim>\<open>COMMAND\<close> modifier
-  key is still pressed). Such jumps to other text locations
-  are recorded by the \<^emph>\<open>Navigator\<close> plugin, which is bundled with
-  Isabelle/jEdit and enabled by default, including navigation arrows in the
-  main jEdit toolbar.
+  A black rectangle in the text indicates a hyperlink that may be followed by
+  a mouse click (while the \<^verbatim>\<open>CONTROL\<close> or \<^verbatim>\<open>COMMAND\<close> modifier key is still
+  pressed). Such jumps to other text locations are recorded by the
+  \<^emph>\<open>Navigator\<close> plugin, which is bundled with Isabelle/jEdit and enabled by
+  default, including navigation arrows in the main jEdit toolbar.
 
-  Also note that the link target may be a file that is itself not
-  subject to formal document processing of the editor session and thus
-  prevents further exploration: the chain of hyperlinks may end in
-  some source file of the underlying logic image, or within the
-  ML bootstrap sources of Isabelle/Pure.\<close>
+  Also note that the link target may be a file that is itself not subject to
+  formal document processing of the editor session and thus prevents further
+  exploration: the chain of hyperlinks may end in some source file of the
+  underlying logic image, or within the ML bootstrap sources of
+  Isabelle/Pure.
+\<close>
 
 
 section \<open>Completion \label{sec:completion}\<close>
@@ -1100,16 +1071,16 @@
 
   \<^medskip>
   \<^emph>\<open>Explicit completion\<close> is triggered by the action @{action_ref
-  "isabelle.complete"}, which is bound to the keyboard shortcut \<^verbatim>\<open>C+b\<close>,
-  and thus overrides the jEdit default for @{action_ref "complete-word"}.
+  "isabelle.complete"}, which is bound to the keyboard shortcut \<^verbatim>\<open>C+b\<close>, and
+  thus overrides the jEdit default for @{action_ref "complete-word"}.
 
-  \<^emph>\<open>Implicit completion\<close> hooks into the regular keyboard input stream of
-  the editor, with some event filtering and optional delays.
+  \<^emph>\<open>Implicit completion\<close> hooks into the regular keyboard input stream of the
+  editor, with some event filtering and optional delays.
 
   \<^medskip>
-  Completion options may be configured in \<^emph>\<open>Plugin Options~/
-  Isabelle~/ General~/ Completion\<close>. These are explained in further detail
-  below, whenever relevant. There is also a summary of options in
+  Completion options may be configured in \<^emph>\<open>Plugin Options~/ Isabelle~/
+  General~/ Completion\<close>. These are explained in further detail below, whenever
+  relevant. There is also a summary of options in
   \secref{sec:completion-options}.
 
   The asynchronous nature of PIDE interaction means that information from the
@@ -1132,19 +1103,17 @@
   kinds and purposes. The completion mechanism supports this by the following
   built-in templates:
 
-  \<^descr> \<^verbatim>\<open>`\<close> (single ASCII back-quote) supports \<^emph>\<open>quotations\<close>
-  via text cartouches. There are three selections, which are always presented
-  in the same order and do not depend on any context information. The default
-  choice produces a template ``\<open>\<open>\<box>\<close>\<close>'', where the box indicates the
-  cursor position after insertion; the other choices help to repair the block
-  structure of unbalanced text cartouches.
+    \<^descr> \<^verbatim>\<open>`\<close> (single ASCII back-quote) supports \<^emph>\<open>quotations\<close> via text
+    cartouches. There are three selections, which are always presented in the
+    same order and do not depend on any context information. The default
+    choice produces a template ``\<open>\<open>\<box>\<close>\<close>'', where the box indicates the cursor
+    position after insertion; the other choices help to repair the block
+    structure of unbalanced text cartouches.
 
-  \<^descr> \<^verbatim>\<open>@{\<close> is completed to the template ``\<open>@{\<box>}\<close>'',
-  where the box indicates the cursor position after insertion. Here it is
-  convenient to use the wildcard ``\<^verbatim>\<open>__\<close>'' or a more specific name
-  prefix to let semantic completion of name-space entries propose
-  antiquotation names.
-
+    \<^descr> \<^verbatim>\<open>@{\<close> is completed to the template ``\<open>@{\<box>}\<close>'', where the box indicates
+    the cursor position after insertion. Here it is convenient to use the
+    wildcard ``\<^verbatim>\<open>__\<close>'' or a more specific name prefix to let semantic
+    completion of name-space entries propose antiquotation names.
 
   With some practice, input of quoted sub-languages and antiquotations of
   embedded languages should work fluently. Note that national keyboard layouts
@@ -1193,10 +1162,9 @@
   When inserted into the text, the above examples all produce the same Unicode
   rendering \<open>\<forall>\<close> of the underlying symbol \<^verbatim>\<open>\<forall>\<close>.
 
-  A symbol abbreviation that is a plain word, like \<^verbatim>\<open>ALL\<close>, is
-  treated like a syntax keyword. Non-word abbreviations like \<^verbatim>\<open>-->\<close>
-  are inserted more aggressively, except for single-character abbreviations
-  like \<^verbatim>\<open>!\<close> above.
+  A symbol abbreviation that is a plain word, like \<^verbatim>\<open>ALL\<close>, is treated like a
+  syntax keyword. Non-word abbreviations like \<^verbatim>\<open>-->\<close> are inserted more
+  aggressively, except for single-character abbreviations like \<^verbatim>\<open>!\<close> above.
 
   \<^medskip>
   Symbol completion depends on the semantic language context
@@ -1217,17 +1185,17 @@
   @{system_option_ref completion_limit}. The completion mechanism takes this
   into account when collecting information on the prover side.
 
-  Already recognized names are \<^emph>\<open>not\<close> completed further, but completion
-  may be extended by appending a suffix of underscores. This provokes a failed
+  Already recognized names are \<^emph>\<open>not\<close> completed further, but completion may be
+  extended by appending a suffix of underscores. This provokes a failed
   lookup, and another completion attempt while ignoring the underscores. For
-  example, in a name space where \<^verbatim>\<open>foo\<close> and \<^verbatim>\<open>foobar\<close>
-  are known, the input \<^verbatim>\<open>foo\<close> remains unchanged, but \<^verbatim>\<open>foo_\<close> may be completed
-  to \<^verbatim>\<open>foo\<close> or \<^verbatim>\<open>foobar\<close>.
+  example, in a name space where \<^verbatim>\<open>foo\<close> and \<^verbatim>\<open>foobar\<close> are known, the input
+  \<^verbatim>\<open>foo\<close> remains unchanged, but \<^verbatim>\<open>foo_\<close> may be completed to \<^verbatim>\<open>foo\<close> or
+  \<^verbatim>\<open>foobar\<close>.
 
-  The special identifier ``\<^verbatim>\<open>__\<close>'' serves as a wild-card for
-  arbitrary completion: it exposes the name-space content to the completion
-  mechanism (truncated according to @{system_option completion_limit}). This
-  is occasionally useful to explore an unknown name-space, e.g.\ in some
+  The special identifier ``\<^verbatim>\<open>__\<close>'' serves as a wild-card for arbitrary
+  completion: it exposes the name-space content to the completion mechanism
+  (truncated according to @{system_option completion_limit}). This is
+  occasionally useful to explore an unknown name-space, e.g.\ in some
   template.
 \<close>
 
@@ -1239,9 +1207,9 @@
   source text, e.g.\ for the argument of a load command
   (\secref{sec:aux-files}), the completion mechanism explores the directory
   content and offers the result as completion popup. Relative path
-  specifications are understood wrt.\ the \<^emph>\<open>master directory\<close> of the
-  document node (\secref{sec:buffer-node}) of the enclosing editor buffer;
-  this requires a proper theory, not an auxiliary file.
+  specifications are understood wrt.\ the \<^emph>\<open>master directory\<close> of the document
+  node (\secref{sec:buffer-node}) of the enclosing editor buffer; this
+  requires a proper theory, not an auxiliary file.
 
   A suffix of slashes may be used to continue the exploration of an already
   recognized directory name.
@@ -1274,10 +1242,10 @@
   default keyboard shortcut \<^verbatim>\<open>C+b\<close>.
 
   \<^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.
+  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.
 \<close>
 
 
@@ -1296,14 +1264,14 @@
   symbol completion for ML source, but within ML strings, comments,
   antiquotations.
 
-  The prover may produce \<^emph>\<open>no completion\<close> markup in exceptional
-  situations, to tell that some language keywords should be excluded from
-  further completion attempts. For example, \<^verbatim>\<open>:\<close> within accepted
-  Isar syntax looses its meaning as abbreviation for symbol \<open>\<in>\<close>.
+  The prover may produce \<^emph>\<open>no completion\<close> markup in exceptional situations, to
+  tell that some language keywords should be excluded from further completion
+  attempts. For example, \<^verbatim>\<open>:\<close> within accepted Isar syntax looses its meaning
+  as abbreviation for symbol \<open>\<in>\<close>.
 
   \<^medskip>
-  The completion context is \<^emph>\<open>ignored\<close> for built-in templates and
-  symbols in their explicit form ``\<^verbatim>\<open>\<foobar>\<close>''; see also
+  The completion context is \<^emph>\<open>ignored\<close> for built-in templates and symbols in
+  their explicit form ``\<^verbatim>\<open>\<foobar>\<close>''; see also
   \secref{sec:completion-varieties}. This allows to complete within broken
   input that escapes its normal semantic context, e.g.\ antiquotations or
   string literals in ML, which do not allow arbitrary backslash sequences.
@@ -1317,56 +1285,55 @@
   optional delay after keyboard input according to @{system_option
   jedit_completion_delay}.
 
-  \<^descr>[Explicit completion] works via action @{action_ref
-  "isabelle.complete"} with keyboard shortcut \<^verbatim>\<open>C+b\<close>. This
-  overrides the shortcut for @{action_ref "complete-word"} in jEdit, but it is
-  possible to restore the original jEdit keyboard mapping of @{action
-  "complete-word"} via \<^emph>\<open>Global Options~/ Shortcuts\<close> and invent a
-  different one for @{action "isabelle.complete"}.
+  \<^descr>[Explicit completion] works via action @{action_ref "isabelle.complete"}
+  with keyboard shortcut \<^verbatim>\<open>C+b\<close>. This overrides the shortcut for @{action_ref
+  "complete-word"} in jEdit, but it is possible to restore the original jEdit
+  keyboard mapping of @{action "complete-word"} via \<^emph>\<open>Global Options~/
+  Shortcuts\<close> and invent a different one for @{action "isabelle.complete"}.
 
   \<^descr>[Explicit spell-checker completion] works via @{action_ref
   "isabelle.complete-word"}, which is exposed in the jEdit context menu, if
   the mouse points to a word that the spell-checker can complete.
 
-  \<^descr>[Implicit completion] works via regular keyboard input of the editor.
-  It depends on further side-conditions:
+  \<^descr>[Implicit completion] works via regular keyboard input of the editor. It
+  depends on further side-conditions:
 
-    \<^enum> The system option @{system_option_ref jedit_completion} needs to
-    be enabled (default).
+    \<^enum> The system option @{system_option_ref jedit_completion} needs to be
+    enabled (default).
 
-    \<^enum> Completion of syntax keywords requires at least 3 relevant
-    characters in the text.
+    \<^enum> Completion of syntax keywords requires at least 3 relevant characters in
+    the text.
 
-    \<^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
+    \<^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}).
 
     \<^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}).
+    jedit_completion_delay}. This aggressive mode of completion is restricted
+    to Isabelle symbols and their abbreviations (\secref{sec:symbols}).
 
-    \<^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}.
+    \<^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}.
 \<close>
 
 
 subsection \<open>Completion popup \label{sec:completion-popup}\<close>
 
 text \<open>
-  A \<^emph>\<open>completion popup\<close> is a minimally invasive GUI component over the
-  text area that offers a selection of completion items to be inserted into
-  the text, e.g.\ by mouse clicks. Items are sorted dynamically, according to
-  the frequency of selection, with persistent history. The popup may interpret
-  special keys \<^verbatim>\<open>ENTER\<close>, \<^verbatim>\<open>TAB\<close>, \<^verbatim>\<open>ESCAPE\<close>,
-  \<^verbatim>\<open>UP\<close>, \<^verbatim>\<open>DOWN\<close>, \<^verbatim>\<open>PAGE_UP\<close>, \<^verbatim>\<open>PAGE_DOWN\<close>, but all other key events are
-  passed to the underlying text area.
-  This allows to ignore unwanted completions most of the time and continue
-  typing quickly. Thus the popup serves as a mechanism of confirmation of
-  proposed items, but the default is to continue without completion.
+  A \<^emph>\<open>completion popup\<close> is a minimally invasive GUI component over the text
+  area that offers a selection of completion items to be inserted into the
+  text, e.g.\ by mouse clicks. Items are sorted dynamically, according to the
+  frequency of selection, with persistent history. The popup may interpret
+  special keys \<^verbatim>\<open>ENTER\<close>, \<^verbatim>\<open>TAB\<close>, \<^verbatim>\<open>ESCAPE\<close>, \<^verbatim>\<open>UP\<close>, \<^verbatim>\<open>DOWN\<close>, \<^verbatim>\<open>PAGE_UP\<close>,
+  \<^verbatim>\<open>PAGE_DOWN\<close>, but all other key events are passed to the underlying text
+  area. This allows to ignore unwanted completions most of the time and
+  continue typing quickly. Thus the popup serves as a mechanism of
+  confirmation of proposed items, but the default is to continue without
+  completion.
 
   The meaning of special keys is as follows:
 
@@ -1383,9 +1350,9 @@
   \end{tabular}
   \<^medskip>
 
-  Movement within the popup is only active for multiple items.
-  Otherwise the corresponding key event retains its standard meaning
-  within the underlying text area.
+  Movement within the popup is only active for multiple items. Otherwise the
+  corresponding key event retains its standard meaning within the underlying
+  text area.
 \<close>
 
 
@@ -1401,32 +1368,31 @@
   all combinations make sense. At least the following important cases are
   well-defined:
 
-  \<^descr>[No selection.] The original is removed and the replacement inserted,
-  depending on the caret position.
+    \<^descr>[No selection.] The original is removed and the replacement inserted,
+    depending on the caret position.
 
-  \<^descr>[Rectangular selection of zero width.] This special case is treated by
-  jEdit as ``tall caret'' and insertion of completion imitates its normal
-  behaviour: separate copies of the replacement are inserted for each line of
-  the selection.
+    \<^descr>[Rectangular selection of zero width.] This special case is treated by
+    jEdit as ``tall caret'' and insertion of completion imitates its normal
+    behaviour: separate copies of the replacement are inserted for each line
+    of the selection.
 
-  \<^descr>[Other rectangular selection or multiple selections.] Here the original
-  is removed and the replacement is inserted for each line (or segment) of the
-  selection.
-
+    \<^descr>[Other rectangular selection or multiple selections.] Here the original
+    is removed and the replacement is inserted for each line (or segment) of
+    the selection.
 
-  Support for multiple selections is particularly useful for
-  \<^emph>\<open>HyperSearch\<close>: clicking on one of the items in the \<^emph>\<open>HyperSearch
-  Results\<close> window makes jEdit select all its occurrences in the corresponding
-  line of text. Then explicit completion can be invoked via \<^verbatim>\<open>C+b\<close>,
-  e.g.\ to replace occurrences of \<^verbatim>\<open>-->\<close> by \<open>\<longrightarrow>\<close>.
+  Support for multiple selections is particularly useful for \<^emph>\<open>HyperSearch\<close>:
+  clicking on one of the items in the \<^emph>\<open>HyperSearch Results\<close> window makes
+  jEdit select all its occurrences in the corresponding line of text. Then
+  explicit completion can be invoked via \<^verbatim>\<open>C+b\<close>, e.g.\ to replace occurrences
+  of \<^verbatim>\<open>-->\<close> by \<open>\<longrightarrow>\<close>.
 
   \<^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
-  @{action undo} is selected: \<^verbatim>\<open>ESCAPE\<close> is required to reset the
-  selection and to continue typing more text.
+  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 @{action undo}
+  is selected: \<^verbatim>\<open>ESCAPE\<close> is required to reset the selection and to continue
+  typing more text.
 \<close>
 
 
@@ -1434,8 +1400,8 @@
 
 text \<open>
   This is a summary of Isabelle/Scala system options that are relevant for
-  completion. They may be configured in \<^emph>\<open>Plugin Options~/ Isabelle~/
-  General\<close> as usual.
+  completion. They may be configured in \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>
+  as usual.
 
   \<^item> @{system_option_def completion_limit} specifies the maximum number of
   items for various semantic completion operations (name-space entries etc.)
@@ -1444,10 +1410,10 @@
   regular jEdit key events (\secref{sec:completion-input}): it allows to
   disable implicit completion altogether.
 
-  \<^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_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
   language context provided by the prover should be used at all. Disabling
@@ -1459,17 +1425,17 @@
   jedit_completion_immediate} determine the handling of keyboard events for
   implicit completion (\secref{sec:completion-input}).
 
-  A @{system_option jedit_completion_delay}~\<^verbatim>\<open>> 0\<close> postpones the
-  processing of key events, until after the user has stopped typing for the
-  given time span, but @{system_option jedit_completion_immediate}~\<^verbatim>\<open>"= true\<close>
-  means that abbreviations of Isabelle symbols are handled nonetheless.
+  A @{system_option jedit_completion_delay}~\<^verbatim>\<open>> 0\<close> postpones the processing of
+  key events, until after the user has stopped typing for the given time span,
+  but @{system_option jedit_completion_immediate}~\<^verbatim>\<open>"= true\<close> means that
+  abbreviations of Isabelle symbols are handled nonetheless.
 
   \<^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
-  spell-checker operations: it allows to disable that mechanism altogether.
+  \<^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
   dictionary, taken from the colon-separated list in the settings variable
@@ -1478,9 +1444,9 @@
   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
-  comma-separated list of markup elements that delimit words in the source
-  that is subject to spell-checking, including various forms of comments.
+  \<^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.
 \<close>
 
 
@@ -1489,22 +1455,21 @@
 text \<open>
   Continuous document processing works asynchronously in the background.
   Visible document source that has been evaluated may get augmented by
-  additional results of \<^emph>\<open>asynchronous print functions\<close>. The canonical
-  example is proof state output, which is always enabled. More heavy-weight
-  print functions may be applied, in order to prove or disprove parts of the
-  formal text by other means.
+  additional results of \<^emph>\<open>asynchronous print functions\<close>. The canonical example
+  is proof state output, which is always enabled. More heavy-weight print
+  functions may be applied, in order to prove or disprove parts of the formal
+  text by other means.
 
-  Isabelle/HOL provides various automatically tried tools that operate
-  on outermost goal statements (e.g.\ @{command lemma}, @{command
-  theorem}), independently of the state of the current proof attempt.
-  They work implicitly without any arguments.  Results are output as
-  \<^emph>\<open>information messages\<close>, which are indicated in the text area by
-  blue squiggles and a blue information sign in the gutter (see
-  \figref{fig:auto-tools}).  The message content may be shown as for
-  other output (see also \secref{sec:output}).  Some tools
-  produce output with \<^emph>\<open>sendback\<close> markup, which means that
-  clicking on certain parts of the output inserts that text into the
-  source in the proper place.
+  Isabelle/HOL provides various automatically tried tools that operate on
+  outermost goal statements (e.g.\ @{command lemma}, @{command theorem}),
+  independently of the state of the current proof attempt. They work
+  implicitly without any arguments. Results are output as \<^emph>\<open>information
+  messages\<close>, which are indicated in the text area by blue squiggles and a blue
+  information sign in the gutter (see \figref{fig:auto-tools}). The message
+  content may be shown as for other output (see also \secref{sec:output}).
+  Some tools produce output with \<^emph>\<open>sendback\<close> markup, which means that clicking
+  on certain parts of the output inserts that text into the source in the
+  proper place.
 
   \begin{figure}[htb]
   \begin{center}
@@ -1515,85 +1480,81 @@
   \end{figure}
 
   \<^medskip>
-  The following Isabelle system options control the behavior
-  of automatically tried tools (see also the jEdit dialog window
-  \<^emph>\<open>Plugin Options~/ Isabelle~/ General~/ Automatically tried
-  tools\<close>):
+  The following Isabelle system options control the behavior of automatically
+  tried tools (see also the jEdit dialog window \<^emph>\<open>Plugin Options~/ Isabelle~/
+  General~/ Automatically tried tools\<close>):
 
-  \<^item> @{system_option_ref auto_methods} controls automatic use of a
-  combination of standard proof methods (@{method auto}, @{method
-  simp}, @{method blast}, etc.).  This corresponds to the Isar command
-  @{command_ref "try0"} @{cite "isabelle-isar-ref"}.
+  \<^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"}.
 
   The tool is disabled by default, since unparameterized invocation of
-  standard proof methods often consumes substantial CPU resources
-  without leading to success.
+  standard proof methods often consumes substantial CPU resources without
+  leading to success.
 
-  \<^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"}.
+  \<^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"}.
 
-  This tool is disabled by default, due to the extra overhead of
-  invoking an external Java process for each attempt to disprove a
-  subgoal.
+  This tool is disabled by default, due to the extra overhead of invoking an
+  external Java process for each attempt to disprove a subgoal.
 
   \<^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.
+  @{command_ref quickcheck}, which tests for counterexamples using a series of
+  assignments for free variables of a subgoal.
 
-  This tool is \<^emph>\<open>enabled\<close> by default.  It requires little
-  overhead, but is a bit weaker than @{command nitpick}.
+  This tool is \<^emph>\<open>enabled\<close> by default. It requires little overhead, but is a
+  bit weaker than @{command nitpick}.
 
-  \<^item> @{system_option_ref auto_sledgehammer} controls a significantly
-  reduced version of @{command_ref sledgehammer}, which attempts to prove
-  a subgoal using external automatic provers. See also the
-  Sledgehammer manual @{cite "isabelle-sledgehammer"}.
+  \<^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"}.
 
-  This tool is disabled by default, due to the relatively heavy nature
-  of Sledgehammer.
+  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
-  @{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.
+  @{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.
 
   This tool is \<^emph>\<open>enabled\<close> by default.
 
 
-  Invocation of automatically tried tools is subject to some global
-  policies of parallel execution, which may be configured as follows:
+  Invocation of automatically tried tools is subject to some global policies
+  of parallel execution, which may be configured as follows:
 
-  \<^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_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
-  start delay (in seconds) for automatically tried tools, after the
-  main command evaluation is finished.
+  \<^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.
 
 
-  Each tool is submitted independently to the pool of parallel
-  execution tasks in Isabelle/ML, using hardwired priorities according
-  to its relative ``heaviness''.  The main stages of evaluation and
-  printing of proof states take precedence, but an already running
-  tool is not canceled and may thus reduce reactivity of proof
-  document processing.
+  Each tool is submitted independently to the pool of parallel execution tasks
+  in Isabelle/ML, using hardwired priorities according to its relative
+  ``heaviness''. The main stages of evaluation and printing of proof states
+  take precedence, but an already running tool is not canceled and may thus
+  reduce reactivity of proof document processing.
 
-  Users should experiment how the available CPU resources (number of
-  cores) are best invested to get additional feedback from prover in
-  the background, by using a selection of weaker or stronger tools.
+  Users should experiment how the available CPU resources (number of cores)
+  are best invested to get additional feedback from prover in the background,
+  by using a selection of weaker or stronger tools.
 \<close>
 
 
 section \<open>Sledgehammer \label{sec:sledgehammer}\<close>
 
-text \<open>The \<^emph>\<open>Sledgehammer\<close> panel (\figref{fig:sledgehammer})
-  provides a view on some independent execution of the Isar command
-  @{command_ref sledgehammer}, with process indicator (spinning wheel) and
-  GUI elements for important Sledgehammer arguments and options.  Any
-  number of Sledgehammer panels may be active, according to the
-  standard policies of Dockable Window Management in jEdit.  Closing
-  such windows also cancels the corresponding prover tasks.
+text \<open>
+  The \<^emph>\<open>Sledgehammer\<close> panel (\figref{fig:sledgehammer}) provides a view on
+  some independent execution of the Isar command @{command_ref sledgehammer},
+  with process indicator (spinning wheel) and GUI elements for important
+  Sledgehammer arguments and options. Any number of Sledgehammer panels may be
+  active, according to the standard policies of Dockable Window Management in
+  jEdit. Closing such windows also cancels the corresponding prover tasks.
 
   \begin{figure}[htb]
   \begin{center}
@@ -1603,34 +1564,37 @@
   \label{fig:sledgehammer}
   \end{figure}
 
-  The \<^emph>\<open>Apply\<close> button attaches a fresh invocation of @{command
-  sledgehammer} to the command where the cursor is pointing in the
-  text --- this should be some pending proof problem.  Further buttons
-  like \<^emph>\<open>Cancel\<close> and \<^emph>\<open>Locate\<close> help to manage the running
-  process.
+  The \<^emph>\<open>Apply\<close> button attaches a fresh invocation of @{command sledgehammer}
+  to the command where the cursor is pointing in the text --- this should be
+  some pending proof problem. Further buttons like \<^emph>\<open>Cancel\<close> and \<^emph>\<open>Locate\<close>
+  help to manage the running process.
 
-  Results appear incrementally in the output window of the panel.
-  Proposed proof snippets are marked-up as \<^emph>\<open>sendback\<close>, which
-  means a single mouse click inserts the text into a suitable place of
-  the original source.  Some manual editing may be required
-  nonetheless, say to remove earlier proof attempts.\<close>
+  Results appear incrementally in the output window of the panel. Proposed
+  proof snippets are marked-up as \<^emph>\<open>sendback\<close>, which means a single mouse
+  click inserts the text into a suitable place of the original source. Some
+  manual editing may be required nonetheless, say to remove earlier proof
+  attempts.
+\<close>
 
 
 chapter \<open>Isabelle document preparation\<close>
 
-text \<open>The ultimate purpose of Isabelle is to produce nicely rendered documents
+text \<open>
+  The ultimate purpose of Isabelle is to produce nicely rendered documents
   with the Isabelle document preparation system, which is based on {\LaTeX};
   see also @{cite "isabelle-system" and "isabelle-isar-ref"}. Isabelle/jEdit
-  provides some additional support for document editing.\<close>
+  provides some additional support for document editing.
+\<close>
 
 
 section \<open>Document outline\<close>
 
-text \<open>Theory sources may contain document markup commands, such as
-  @{command_ref chapter}, @{command_ref section}, @{command subsection}. The
-  Isabelle SideKick parser (\secref{sec:sidekick}) represents this document
-  outline as structured tree view, with formal statements and proofs nested
-  inside; see \figref{fig:sidekick-document}.
+text \<open>
+  Theory sources may contain document markup commands, such as @{command_ref
+  chapter}, @{command_ref section}, @{command subsection}. The Isabelle
+  SideKick parser (\secref{sec:sidekick}) represents this document outline as
+  structured tree view, with formal statements and proofs nested inside; see
+  \figref{fig:sidekick-document}.
 
   \begin{figure}[htb]
   \begin{center}
@@ -1641,25 +1605,27 @@
   \end{figure}
 
   It is also possible to use text folding according to this structure, by
-  adjusting \<^emph>\<open>Utilities / Buffer Options / Folding mode\<close> of jEdit. The
-  default mode \<^verbatim>\<open>isabelle\<close> uses the structure of formal definitions,
-  statements, and proofs. The alternative mode \<^verbatim>\<open>sidekick\<close> uses the
-  document structure of the SideKick parser, as explained above.\<close>
+  adjusting \<^emph>\<open>Utilities / Buffer Options / Folding mode\<close> of jEdit. The default
+  mode \<^verbatim>\<open>isabelle\<close> uses the structure of formal definitions, statements, and
+  proofs. The alternative mode \<^verbatim>\<open>sidekick\<close> uses the document structure of the
+  SideKick parser, as explained above.
+\<close>
 
 
 section \<open>Citations and Bib{\TeX} entries\<close>
 
-text \<open>Citations are managed by {\LaTeX} and Bib{\TeX} in \<^verbatim>\<open>.bib\<close>
-  files. The Isabelle session build process and the @{tool latex} tool @{cite
+text \<open>
+  Citations are managed by {\LaTeX} and Bib{\TeX} in \<^verbatim>\<open>.bib\<close> files. The
+  Isabelle session build process and the @{tool latex} tool @{cite
   "isabelle-system"} are smart enough to assemble the result, based on the
   session directory layout.
 
   The document antiquotation \<open>@{cite}\<close> is described in @{cite
   "isabelle-isar-ref"}. Within the Prover IDE it provides semantic markup for
   tooltips, hyperlinks, and completion for Bib{\TeX} database entries.
-  Isabelle/jEdit does \<^emph>\<open>not\<close> know about the actual Bib{\TeX} environment
-  used in {\LaTeX} batch-mode, but it can take citations from those \<^verbatim>\<open>.bib\<close>
-  files that happen to be open in the editor; see \figref{fig:cite-completion}.
+  Isabelle/jEdit does \<^emph>\<open>not\<close> know about the actual Bib{\TeX} environment used
+  in {\LaTeX} batch-mode, but it can take citations from those \<^verbatim>\<open>.bib\<close> files
+  that happen to be open in the editor; see \figref{fig:cite-completion}.
 
   \begin{figure}[htb]
   \begin{center}
@@ -1669,9 +1635,9 @@
   \label{fig:cite-completion}
   \end{figure}
 
-  Isabelle/jEdit also provides some support for editing \<^verbatim>\<open>.bib\<close>
-  files themselves. There is syntax highlighting based on entry types
-  (according to standard Bib{\TeX} styles), a context-menu to compose entries
+  Isabelle/jEdit also provides some support for editing \<^verbatim>\<open>.bib\<close> files
+  themselves. There is syntax highlighting based on entry types (according to
+  standard Bib{\TeX} styles), a context-menu to compose entries
   systematically, and a SideKick tree view of the overall content; see
   \figref{fig:bibtex-mode}.
 
@@ -1689,35 +1655,33 @@
 
 section \<open>Timing\<close>
 
-text \<open>Managed evaluation of commands within PIDE documents includes
-  timing information, which consists of elapsed (wall-clock) time, CPU
-  time, and GC (garbage collection) time.  Note that in a
-  multithreaded system it is difficult to measure execution time
-  precisely: elapsed time is closer to the real requirements of
-  runtime resources than CPU or GC time, which are both subject to
-  influences from the parallel environment that are outside the scope
-  of the current command transaction.
+text \<open>
+  Managed evaluation of commands within PIDE documents includes timing
+  information, which consists of elapsed (wall-clock) time, CPU time, and GC
+  (garbage collection) time. Note that in a multithreaded system it is
+  difficult to measure execution time precisely: elapsed time is closer to the
+  real requirements of runtime resources than CPU or GC time, which are both
+  subject to influences from the parallel environment that are outside the
+  scope of the current command transaction.
 
-  The \<^emph>\<open>Timing\<close> panel provides an overview of cumulative command
-  timings for each document node.  Commands with elapsed time below
-  the given threshold are ignored in the grand total.  Nodes are
-  sorted according to their overall timing.  For the document node
-  that corresponds to the current buffer, individual command timings
-  are shown as well.  A double-click on a theory node or command moves
-  the editor focus to that particular source position.
+  The \<^emph>\<open>Timing\<close> panel provides an overview of cumulative command timings for
+  each document node. Commands with elapsed time below the given threshold are
+  ignored in the grand total. Nodes are sorted according to their overall
+  timing. For the document node that corresponds to the current buffer,
+  individual command timings are shown as well. A double-click on a theory
+  node or command moves the editor focus to that particular source position.
 
-  It is also possible to reveal individual timing information via some
-  tooltip for the corresponding command keyword, using the technique
-  of mouse hovering with \<^verbatim>\<open>CONTROL\<close>/\<^verbatim>\<open>COMMAND\<close>
-  modifier key as explained in \secref{sec:tooltips-hyperlinks}.
-  Actual display of timing depends on the global option
-  @{system_option_ref jedit_timing_threshold}, which can be configured in
-  \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>.
+  It is also possible to reveal individual timing information via some tooltip
+  for the corresponding command keyword, using the technique of mouse hovering
+  with \<^verbatim>\<open>CONTROL\<close>~/ \<^verbatim>\<open>COMMAND\<close> modifier key as explained in
+  \secref{sec:tooltips-hyperlinks}. Actual display of timing depends on the
+  global option @{system_option_ref jedit_timing_threshold}, which can be
+  configured in \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>.
 
   \<^medskip>
-  The \<^emph>\<open>Monitor\<close> panel visualizes various data collections about
-  recent activity of the Isabelle/ML task farm and the underlying ML runtime
-  system. The display is continuously updated according to @{system_option_ref
+  The \<^emph>\<open>Monitor\<close> panel visualizes various data collections about recent
+  activity of the Isabelle/ML task farm and the underlying ML runtime system.
+  The display is continuously updated according to @{system_option_ref
   editor_chart_delay}. Note that the painting of the chart takes considerable
   runtime itself --- on the Java Virtual Machine that runs Isabelle/Scala, not
   Isabelle/ML. Internally, the Isabelle/Scala module \<^verbatim>\<open>isabelle.ML_Statistics\<close>
@@ -1727,32 +1691,30 @@
 
 section \<open>Low-level output\<close>
 
-text \<open>Prover output is normally shown directly in the main text area
-  or secondary \<^emph>\<open>Output\<close> panels, as explained in
-  \secref{sec:output}.
+text \<open>
+  Prover output is normally shown directly in the main text area or secondary
+  \<^emph>\<open>Output\<close> panels, as explained in \secref{sec:output}.
 
-  Beyond this, it is occasionally useful to inspect low-level output
-  channels via some of the following additional panels:
+  Beyond this, it is occasionally useful to inspect low-level output channels
+  via some of the following additional panels:
 
-  \<^item> \<^emph>\<open>Protocol\<close> shows internal messages between the
-  Isabelle/Scala and Isabelle/ML side of the PIDE document editing protocol.
-  Recording of messages starts with the first activation of the
-  corresponding dockable window; earlier messages are lost.
+  \<^item> \<^emph>\<open>Protocol\<close> shows internal messages between the Isabelle/Scala and
+  Isabelle/ML side of the PIDE document editing protocol. Recording of
+  messages starts with the first activation of the corresponding dockable
+  window; earlier messages are lost.
 
-  Actual display of protocol messages causes considerable slowdown, so
-  it is important to undock all \<^emph>\<open>Protocol\<close> panels for production
-  work.
+  Actual display of protocol messages causes considerable slowdown, so it is
+  important to undock all \<^emph>\<open>Protocol\<close> panels for production work.
 
   \<^item> \<^emph>\<open>Raw Output\<close> shows chunks of text from the \<^verbatim>\<open>stdout\<close> and \<^verbatim>\<open>stderr\<close>
-  channels of the prover process.
-  Recording of output starts with the first activation of the
-  corresponding dockable window; earlier output is lost.
+  channels of the prover process. Recording of output starts with the first
+  activation of the corresponding dockable window; earlier output is lost.
 
-  The implicit stateful nature of physical I/O channels makes it
-  difficult to relate raw output to the actual command from where it
-  was originating.  Parallel execution may add to the confusion.
-  Peeking at physical process I/O is only the last resort to diagnose
-  problems with tools that are not PIDE compliant.
+  The implicit stateful nature of physical I/O channels makes it difficult to
+  relate raw output to the actual command from where it was originating.
+  Parallel execution may add to the confusion. Peeking at physical process I/O
+  is only the last resort to diagnose problems with tools that are not PIDE
+  compliant.
 
   Under normal circumstances, prover output always works via managed message
   channels (corresponding to @{ML writeln}, @{ML warning}, @{ML
@@ -1762,50 +1724,45 @@
 
   \<^item> \<^emph>\<open>Syslog\<close> shows system messages that might be relevant to diagnose
   problems with the startup or shutdown phase of the prover process; this also
-  includes raw output on \<^verbatim>\<open>stderr\<close>. Isabelle/ML also provides an
-  explicit @{ML Output.system_message} operation, which is occasionally useful
-  for diagnostic purposes within the system infrastructure itself.
+  includes raw output on \<^verbatim>\<open>stderr\<close>. Isabelle/ML also provides an explicit @{ML
+  Output.system_message} operation, which is occasionally useful for
+  diagnostic purposes within the system infrastructure itself.
 
-  A limited amount of syslog messages are buffered, independently of
-  the docking state of the \<^emph>\<open>Syslog\<close> panel.  This allows to
-  diagnose serious problems with Isabelle/PIDE process management,
-  outside of the actual protocol layer.
+  A limited amount of syslog messages are buffered, independently of the
+  docking state of the \<^emph>\<open>Syslog\<close> panel. This allows to diagnose serious
+  problems with Isabelle/PIDE process management, outside of the actual
+  protocol layer.
 
-  Under normal situations, such low-level system output can be
-  ignored.
+  Under normal situations, such low-level system output can be ignored.
 \<close>
 
 
 chapter \<open>Known problems and workarounds \label{sec:problems}\<close>
 
 text \<open>
-  \<^item> \<^bold>\<open>Problem:\<close> Odd behavior of some diagnostic commands with
-  global side-effects, like writing a physical file.
+  \<^item> \<^bold>\<open>Problem:\<close> Odd behavior of some diagnostic commands with global
+  side-effects, like writing a physical file.
 
-  \<^bold>\<open>Workaround:\<close> Copy/paste complete command text from
-  elsewhere, or disable continuous checking temporarily.
-
-  \<^item> \<^bold>\<open>Problem:\<close> No direct support to remove document nodes from the
-  collection of theories.
+  \<^bold>\<open>Workaround:\<close> Copy/paste complete command text from elsewhere, or disable
+  continuous checking temporarily.
 
-  \<^bold>\<open>Workaround:\<close> Clear the buffer content of unused files and close
-  \<^emph>\<open>without\<close> saving changes.
+  \<^item> \<^bold>\<open>Problem:\<close> No direct support to remove document nodes from the collection
+  of theories.
 
-  \<^item> \<^bold>\<open>Problem:\<close> Keyboard shortcuts \<^verbatim>\<open>C+PLUS\<close> and
-  \<^verbatim>\<open>C+MINUS\<close> for adjusting the editor font size depend on
-  platform details and national keyboards.
+  \<^bold>\<open>Workaround:\<close> Clear the buffer content of unused files and close \<^emph>\<open>without\<close>
+  saving changes.
 
-  \<^bold>\<open>Workaround:\<close> Rebind keys via \<^emph>\<open>Global Options~/
-  Shortcuts\<close>.
+  \<^item> \<^bold>\<open>Problem:\<close> Keyboard shortcuts \<^verbatim>\<open>C+PLUS\<close> and \<^verbatim>\<open>C+MINUS\<close> for adjusting the
+  editor font size depend on platform details and national keyboards.
+
+  \<^bold>\<open>Workaround:\<close> Rebind keys via \<^emph>\<open>Global Options~/ Shortcuts\<close>.
 
   \<^item> \<^bold>\<open>Problem:\<close> The Mac OS X key sequence \<^verbatim>\<open>COMMAND+COMMA\<close> for application
-  \<^emph>\<open>Preferences\<close> is in conflict with the
-  jEdit default keyboard shortcut for \<^emph>\<open>Incremental Search Bar\<close> (action
-  @{action_ref "quick-search"}).
+  \<^emph>\<open>Preferences\<close> is in conflict with the jEdit default keyboard shortcut for
+  \<^emph>\<open>Incremental Search Bar\<close> (action @{action_ref "quick-search"}).
 
-  \<^bold>\<open>Workaround:\<close> Rebind key via \<^emph>\<open>Global Options~/
-  Shortcuts\<close> according to national keyboard, e.g.\ \<^verbatim>\<open>COMMAND+SLASH\<close>
-  on English ones.
+  \<^bold>\<open>Workaround:\<close> Rebind key via \<^emph>\<open>Global Options~/ Shortcuts\<close> according to
+  national keyboard, e.g.\ \<^verbatim>\<open>COMMAND+SLASH\<close> on English ones.
 
   \<^item> \<^bold>\<open>Problem:\<close> On Mac OS X with native Apple look-and-feel, some exotic
   national keyboards may cause a conflict of menu accelerator keys with
@@ -1815,44 +1772,42 @@
   \<^bold>\<open>Workaround:\<close> Disable the native Apple menu bar via Java runtime option
   \<^verbatim>\<open>-Dapple.laf.useScreenMenuBar=false\<close>.
 
-  \<^item> \<^bold>\<open>Problem:\<close> Mac OS X system fonts sometimes lead to
-  character drop-outs in the main text area.
+  \<^item> \<^bold>\<open>Problem:\<close> Mac OS X system fonts sometimes lead to character drop-outs in
+  the main text area.
 
-  \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>IsabelleText\<close> font.
-  (Do not install that font on the system.)
-
-  \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus
-  tend to disrupt key event handling of Java/AWT/Swing.
+  \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>IsabelleText\<close> font. (Do not install that
+  font on the system.)
 
-  \<^bold>\<open>Workaround:\<close> Do not use X11 input methods. Note that environment
-  variable \<^verbatim>\<open>XMODIFIERS\<close> is reset by default within Isabelle
-  settings.
+  \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key
+  event handling of Java/AWT/Swing.
 
-  \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 window managers that are
-  not ``re-parenting'' cause problems with additional windows opened
-  by Java. This affects either historic or neo-minimalistic window
-  managers like \<^verbatim>\<open>awesome\<close> or \<^verbatim>\<open>xmonad\<close>.
+  \<^bold>\<open>Workaround:\<close> Do not use X11 input methods. Note that environment variable
+  \<^verbatim>\<open>XMODIFIERS\<close> is reset by default within Isabelle settings.
+
+  \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 window managers that are not ``re-parenting''
+  cause problems with additional windows opened by Java. This affects either
+  historic or neo-minimalistic window managers like \<^verbatim>\<open>awesome\<close> or \<^verbatim>\<open>xmonad\<close>.
 
   \<^bold>\<open>Workaround:\<close> Use a regular re-parenting X11 window manager.
 
-  \<^item> \<^bold>\<open>Problem:\<close> Various forks of Linux/X11 window managers and
-  desktop environments (like Gnome) disrupt the handling of menu popups and
-  mouse positions of Java/AWT/Swing.
+  \<^item> \<^bold>\<open>Problem:\<close> Various forks of Linux/X11 window managers and desktop
+  environments (like Gnome) disrupt the handling of menu popups and mouse
+  positions of Java/AWT/Swing.
 
   \<^bold>\<open>Workaround:\<close> Use mainstream versions of Linux desktops.
 
-  \<^item> \<^bold>\<open>Problem:\<close> Native Windows look-and-feel with global font
-  scaling leads to bad GUI rendering of various tree views.
+  \<^item> \<^bold>\<open>Problem:\<close> Native Windows look-and-feel with global font scaling leads to
+  bad GUI rendering of various tree views.
 
-  \<^bold>\<open>Workaround:\<close> Use \<^emph>\<open>Metal\<close> look-and-feel and re-adjust its
-  primary and secondary font as explained in \secref{sec:hdpi}.
+  \<^bold>\<open>Workaround:\<close> Use \<^emph>\<open>Metal\<close> look-and-feel and re-adjust its primary and
+  secondary font as explained in \secref{sec:hdpi}.
 
   \<^item> \<^bold>\<open>Problem:\<close> Full-screen mode via jEdit action @{action_ref
-  "toggle-full-screen"} (default keyboard shortcut \<^verbatim>\<open>F11\<close>) works on
-  Windows, but not on Mac OS X or various Linux/X11 window managers.
+  "toggle-full-screen"} (default keyboard shortcut \<^verbatim>\<open>F11\<close>) works on Windows,
+  but not on Mac OS X or various Linux/X11 window managers.
 
-  \<^bold>\<open>Workaround:\<close> Use native full-screen control of the window
-  manager (notably on Mac OS X).
+  \<^bold>\<open>Workaround:\<close> Use native full-screen control of the window manager (notably
+  on Mac OS X).
 \<close>
 
 end
\ No newline at end of file