src/Doc/JEdit/JEdit.thy
author wenzelm
Thu Nov 02 10:16:22 2017 +0100 (17 months ago)
changeset 66987 352b23c97ac8
parent 66977 fa79f18eadc7
child 66988 7f8c1dd7576a
permissions -rw-r--r--
support focus_session, for much faster startup of Isabelle/jEdit;
more options for "isabelle jedit";
     1 (*:maxLineLen=78:*)
     2 
     3 theory JEdit
     4 imports Base
     5 begin
     6 
     7 chapter \<open>Introduction\<close>
     8 
     9 section \<open>Concepts and terminology\<close>
    10 
    11 text \<open>
    12   Isabelle/jEdit is a Prover IDE that integrates \<^emph>\<open>parallel proof checking\<close>
    13   @{cite "Wenzel:2009" and "Wenzel:2013:ITP"} with \<^emph>\<open>asynchronous user
    14   interaction\<close> @{cite "Wenzel:2010" and "Wenzel:2012:UITP-EPTCS" and
    15   "Wenzel:2014:ITP-PIDE" and "Wenzel:2014:UITP"}, based on a document-oriented
    16   approach to \<^emph>\<open>continuous proof processing\<close> @{cite "Wenzel:2011:CICM" and
    17   "Wenzel:2012"}. Many concepts and system components are fit together in
    18   order to make this work. The main building blocks are as follows.
    19 
    20     \<^descr>[Isabelle/ML] is the implementation and extension language of Isabelle,
    21     see also @{cite "isabelle-implementation"}. It is integrated into the
    22     logical context of Isabelle/Isar and allows to manipulate logical entities
    23     directly. Arbitrary add-on tools may be implemented for object-logics such
    24     as Isabelle/HOL.
    25 
    26     \<^descr>[Isabelle/Scala] is the system programming language of Isabelle. It
    27     extends the pure logical environment of Isabelle/ML towards the outer
    28     world of graphical user interfaces, text editors, IDE frameworks, web
    29     services, SSH servers, SQL databases etc. Special infrastructure allows to
    30     transfer algebraic datatypes and formatted text easily between ML and
    31     Scala, using asynchronous protocol commands.
    32 
    33     \<^descr>[PIDE] is a general framework for Prover IDEs based on Isabelle/Scala. It
    34     is built around a concept of parallel and asynchronous document
    35     processing, which is supported natively by the parallel proof engine that
    36     is implemented in Isabelle/ML. The traditional prover command loop is
    37     given up; instead there is direct support for editing of source text, with
    38     rich formal markup for GUI rendering.
    39 
    40     \<^descr>[jEdit] is a sophisticated text editor\<^footnote>\<open>\<^url>\<open>http://www.jedit.org\<close>\<close>
    41     implemented in Java\<^footnote>\<open>\<^url>\<open>http://www.java.com\<close>\<close>. It is easily extensible by
    42     plugins written in any language that works on the JVM. In the context of
    43     Isabelle this is always Scala\<^footnote>\<open>\<^url>\<open>http://www.scala-lang.org\<close>\<close>.
    44 
    45     \<^descr>[Isabelle/jEdit] is the main application of the PIDE framework and the
    46     default user-interface for Isabelle. It targets both beginners and
    47     experts. Technically, Isabelle/jEdit consists of the original jEdit code
    48     base with minimal patches and a special plugin for Isabelle. This is
    49     integrated as a desktop application for the main operating system
    50     families: Linux, Windows, Mac OS X.
    51 
    52   End-users of Isabelle download and run a standalone application that exposes
    53   jEdit as a text editor on the surface. Thus there is occasionally a tendency
    54   to apply the name ``jEdit'' to any of the Isabelle Prover IDE aspects,
    55   without proper differentiation. When discussing these PIDE building blocks
    56   in public forums, mailing lists, or even scientific publications, it is
    57   particularly important to distinguish Isabelle/ML versus Standard ML,
    58   Isabelle/Scala versus Scala, Isabelle/jEdit versus jEdit.
    59 \<close>
    60 
    61 
    62 section \<open>The Isabelle/jEdit Prover IDE\<close>
    63 
    64 text \<open>
    65   \begin{figure}[!htb]
    66   \begin{center}
    67   \includegraphics[scale=0.333]{isabelle-jedit}
    68   \end{center}
    69   \caption{The Isabelle/jEdit Prover IDE}
    70   \label{fig:isabelle-jedit}
    71   \end{figure}
    72 
    73   Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some plugins for
    74   the jEdit text editor, while preserving its general look-and-feel as far as
    75   possible. The main plugin is called ``Isabelle'' and has its own menu
    76   \<^emph>\<open>Plugins~/ Isabelle\<close> with access to several panels (see also
    77   \secref{sec:dockables}), as well as \<^emph>\<open>Plugins~/ Plugin Options~/ Isabelle\<close>
    78   (see also \secref{sec:options}).
    79 
    80   The options allow to specify a logic session name, but the same selector is
    81   also accessible in the \<^emph>\<open>Theories\<close> panel (\secref{sec:theories}). After
    82   startup of the Isabelle plugin, the selected logic session image is provided
    83   automatically by the Isabelle build tool @{cite "isabelle-system"}: if it is
    84   absent or outdated wrt.\ its sources, the build process updates it within
    85   the running text editor. Prover IDE functionality is fully activated after
    86   successful termination of the build process. A failure may require changing
    87   some options and restart of the Isabelle plugin or application. Changing the
    88   logic session, or the underlying ML system platform (32\,bit versus 64\,bit)
    89   requires a restart of the whole application to take effect.
    90 
    91   \<^medskip>
    92   The main job of the Prover IDE is to manage sources and their changes,
    93   taking the logical structure as a formal document into account (see also
    94   \secref{sec:document-model}). The editor and the prover are connected
    95   asynchronously in a lock-free manner. The prover is free to organize the
    96   checking of the formal text in parallel on multiple cores, and provides
    97   feedback via markup, which is rendered in the editor via colors, boxes,
    98   squiggly underlines, hyperlinks, popup windows, icons, clickable output etc.
    99 
   100   Using the mouse together with the modifier key \<^verbatim>\<open>CONTROL\<close> (Linux, Windows)
   101   or \<^verbatim>\<open>COMMAND\<close> (Mac OS X) exposes formal content via tooltips and/or
   102   hyperlinks (see also \secref{sec:tooltips-hyperlinks}). Output (in popups
   103   etc.) may be explored recursively, using the same techniques as in the
   104   editor source buffer.
   105 
   106   Thus the Prover IDE gives an impression of direct access to formal content
   107   of the prover within the editor, but in reality only certain aspects are
   108   exposed, according to the possibilities of the prover and its add-on tools.
   109 \<close>
   110 
   111 
   112 subsection \<open>Documentation\<close>
   113 
   114 text \<open>
   115   The \<^emph>\<open>Documentation\<close> panel of Isabelle/jEdit provides access to some example
   116   theory files and the standard Isabelle documentation. PDF files are opened
   117   by regular desktop operations of the underlying platform. The section
   118   ``Original jEdit Documentation'' contains the original \<^emph>\<open>User's Guide\<close> of
   119   this sophisticated text editor. The same is accessible via the \<^verbatim>\<open>Help\<close> menu
   120   or \<^verbatim>\<open>F1\<close> keyboard shortcut, using the built-in HTML viewer of Java/Swing.
   121   The latter also includes \<^emph>\<open>Frequently Asked Questions\<close> and documentation of
   122   individual plugins.
   123 
   124   Most of the information about jEdit is relevant for Isabelle/jEdit as well,
   125   but users need to keep in mind that defaults sometimes differ, and the
   126   official jEdit documentation does not know about the Isabelle plugin with
   127   its support for continuous checking of formal source text: jEdit is a plain
   128   text editor, but Isabelle/jEdit is a Prover IDE.
   129 \<close>
   130 
   131 
   132 subsection \<open>Plugins\<close>
   133 
   134 text \<open>
   135   The \<^emph>\<open>Plugin Manager\<close> of jEdit allows to augment editor functionality by JVM
   136   modules (jars) that are provided by the central plugin repository, which is
   137   accessible via various mirror sites.
   138 
   139   Connecting to the plugin server-infrastructure of the jEdit project allows
   140   to update bundled plugins or to add further functionality. This needs to be
   141   done with the usual care for such an open bazaar of contributions. Arbitrary
   142   combinations of add-on features are apt to cause problems. It is advisable
   143   to start with the default configuration of Isabelle/jEdit and develop some
   144   sense how it is meant to work, before loading too many other plugins.
   145 
   146   \<^medskip>
   147   The \<^emph>\<open>Isabelle\<close> plugin is responsible for the main Prover IDE functionality
   148   of Isabelle/jEdit: it manages the prover session in the background. A few
   149   additional plugins are bundled with Isabelle/jEdit for convenience or out of
   150   necessity, notably \<^emph>\<open>Console\<close> with its \<^emph>\<open>Scala\<close> sub-plugin
   151   (\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close> with some Isabelle-specific
   152   parsers for document tree structure (\secref{sec:sidekick}). The
   153   \<^emph>\<open>Navigator\<close> plugin is particularly important for hyperlinks within the
   154   formal document-model (\secref{sec:tooltips-hyperlinks}). Further plugins
   155   (e.g.\ \<^emph>\<open>ErrorList\<close>, \<^emph>\<open>Code2HTML\<close>) are included to saturate the dependencies
   156   of bundled plugins, but have no particular use in Isabelle/jEdit.
   157 \<close>
   158 
   159 
   160 subsection \<open>Options \label{sec:options}\<close>
   161 
   162 text \<open>
   163   Both jEdit and Isabelle have distinctive management of persistent options.
   164 
   165   Regular jEdit options are accessible via the dialogs \<^emph>\<open>Utilities~/ Global
   166   Options\<close> or \<^emph>\<open>Plugins~/ Plugin Options\<close>, with a second chance to flip the
   167   two within the central options dialog. Changes are stored in @{path
   168   "$JEDIT_SETTINGS/properties"} and @{path "$JEDIT_SETTINGS/keymaps"}.
   169 
   170   Isabelle system options are managed by Isabelle/Scala and changes are stored
   171   in @{path "$ISABELLE_HOME_USER/etc/preferences"}, independently of
   172   other jEdit properties. See also @{cite "isabelle-system"}, especially the
   173   coverage of sessions and command-line tools like @{tool build} or @{tool
   174   options}.
   175 
   176   Those Isabelle options that are declared as \<^verbatim>\<open>public\<close> are configurable in
   177   Isabelle/jEdit via \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>. Moreover, there
   178   are various options for rendering document content, which are configurable
   179   via \<^emph>\<open>Plugin Options~/ Isabelle~/ Rendering\<close>. Thus \<^emph>\<open>Plugin Options~/
   180   Isabelle\<close> in jEdit provides a view on a subset of Isabelle system options.
   181   Note that some of these options affect general parameters that are relevant
   182   outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or
   183   @{system_option parallel_proofs} for the Isabelle build tool @{cite
   184   "isabelle-system"}, but it is possible to use the settings variable
   185   @{setting ISABELLE_BUILD_OPTIONS} to change defaults for batch builds
   186   without affecting the Prover IDE.
   187 
   188   The jEdit action @{action_def isabelle.options} opens the options dialog for
   189   the Isabelle plugin; it can be mapped to editor GUI elements as usual.
   190 
   191   \<^medskip>
   192   Options are usually loaded on startup and saved on shutdown of
   193   Isabelle/jEdit. Editing the generated @{path "$JEDIT_SETTINGS/properties"}
   194   or @{path "$ISABELLE_HOME_USER/etc/preferences"} manually while the
   195   application is running may cause surprise due to lost updates!
   196 \<close>
   197 
   198 
   199 subsection \<open>Keymaps\<close>
   200 
   201 text \<open>
   202   Keyboard shortcuts are managed as a separate concept of \<^emph>\<open>keymap\<close> that is
   203   configurable via \<^emph>\<open>Global Options~/ Shortcuts\<close>. The \<^verbatim>\<open>imported\<close> keymap is
   204   derived from the initial environment of properties that is available at the
   205   first start of the editor; afterwards the keymap file takes precedence and
   206   is no longer affected by change of default properties.
   207 
   208   Users may change their keymap later, but this may lead to conflicts with
   209   \<^verbatim>\<open>shortcut\<close> properties in \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>.
   210 
   211   The action @{action_def "isabelle.keymap-merge"} helps to resolve pending
   212   Isabelle keymap changes that are in conflict with the current jEdit keymap;
   213   while non-conflicting changes are applied implicitly. This action is
   214   automatically invoked on Isabelle/jEdit startup.
   215 \<close>
   216 
   217 
   218 section \<open>Command-line invocation \label{sec:command-line}\<close>
   219 
   220 text \<open>
   221   Isabelle/jEdit is normally invoked as a single-instance desktop application,
   222   based on platform-specific executables for Linux, Windows, Mac OS X.
   223 
   224   It is also possible to invoke the Prover IDE on the command-line, with some
   225   extra options and environment settings. The command-line usage of @{tool_def
   226   jedit} is as follows:
   227   @{verbatim [display]
   228 \<open>Usage: isabelle jedit [OPTIONS] [FILES ...]
   229 
   230   Options are:
   231     -B           use base session image, with theories from other sessions
   232     -F           focus on selected logic session: ignore unrelated theories
   233     -D NAME=X    set JVM system property
   234     -J OPTION    add JVM runtime option
   235                  (default $JEDIT_JAVA_SYSTEM_OPTIONS $JEDIT_JAVA_OPTIONS)
   236     -P           use parent session image
   237     -R           open ROOT entry of logic session
   238     -S NAME      edit specified logic session, same as -B -F -R -l NAME
   239     -b           build only
   240     -d DIR       include session directory
   241     -f           fresh build
   242     -j OPTION    add jEdit runtime option
   243                  (default $JEDIT_OPTIONS)
   244     -l NAME      logic image name
   245     -m MODE      add print mode for output
   246     -n           no build of session image on startup
   247     -p CMD       ML process command prefix (process policy)
   248     -s           system build mode for session image
   249 
   250   Start jEdit with Isabelle plugin setup and open FILES
   251   (default "$USER_HOME/Scratch.thy" or ":" for empty buffer).\<close>}
   252 
   253   The \<^verbatim>\<open>-l\<close> option specifies the session name of the logic image to be used
   254   for proof processing. Additional session root directories may be included
   255   via option \<^verbatim>\<open>-d\<close> to augment the session name space (see also @{cite
   256   "isabelle-system"}).
   257 
   258   By default, the specified image is checked and built on demand. The \<^verbatim>\<open>-s\<close>
   259   option determines where to store the result session image of @{tool build}.
   260   The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
   261   session image.
   262 
   263   Option \<^verbatim>\<open>-B\<close> and \<^verbatim>\<open>-P\<close> are mutually exclusive and modify the meaning of
   264   option \<^verbatim>\<open>-l\<close> as follows: \<^verbatim>\<open>-B\<close> prepares a logic image on the spot, based on
   265   the required theory imports from other sessions, or the parent session image
   266   if all required theories are already present there. \<^verbatim>\<open>-P\<close> opens the parent
   267   session image directly.
   268 
   269   Option \<^verbatim>\<open>-F\<close> focuses on the specified logic session, as resulting from
   270   options \<^verbatim>\<open>-l\<close>, \<^verbatim>\<open>-B\<close>, \<^verbatim>\<open>-P\<close>. The accessible name space of theories is
   271   restricted to sessions that are connected to this session.
   272 
   273   Option \<^verbatim>\<open>-R\<close> opens the ROOT entry of the specified logic session in the
   274   editor. Option \<^verbatim>\<open>-S\<close> sets up the development environment to edit the
   275   specified session: it abbreviates \<^verbatim>\<open>-B\<close> \<^verbatim>\<open>-F\<close> \<^verbatim>\<open>-R\<close> \<^verbatim>\<open>-l\<close>.
   276 
   277   The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover process.
   278   Note that the system option @{system_option_ref jedit_print_mode} allows to
   279   do the same persistently (e.g.\ via the \<^emph>\<open>Plugin Options\<close> dialog of
   280   Isabelle/jEdit), without requiring command-line invocation.
   281 
   282   The \<^verbatim>\<open>-J\<close> and \<^verbatim>\<open>-j\<close> options pass additional low-level options to the JVM or
   283   jEdit, respectively. The defaults are provided by the Isabelle settings
   284   environment @{cite "isabelle-system"}, but note that these only work for the
   285   command-line tool described here, and not the regular application.
   286 
   287   The \<^verbatim>\<open>-D\<close> option allows to define JVM system properties; this is passed
   288   directly to the underlying \<^verbatim>\<open>java\<close> process.
   289 
   290   The \<^verbatim>\<open>-b\<close> and \<^verbatim>\<open>-f\<close> options control the self-build mechanism of
   291   Isabelle/jEdit. This is only relevant for building from sources, which also
   292   requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component from
   293   \<^url>\<open>http://isabelle.in.tum.de/components\<close>. The official Isabelle release
   294   already includes a pre-built version of Isabelle/jEdit.
   295 
   296   \<^bigskip>
   297   It is also possible to connect to an already running Isabelle/jEdit process
   298   via @{tool_def jedit_client}:
   299   @{verbatim [display]
   300 \<open>Usage: isabelle jedit_client [OPTIONS] [FILES ...]
   301 
   302   Options are:
   303     -c           only check presence of server
   304     -n           only report server name
   305     -s NAME      server name (default Isabelle)
   306 
   307   Connect to already running Isabelle/jEdit instance and open FILES\<close>}
   308 
   309   The \<^verbatim>\<open>-c\<close> option merely checks the presence of the server, producing a
   310   process return code accordingly.
   311 
   312   The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a
   313   different server name. The default server name is the official distribution
   314   name (e.g.\ \<^verbatim>\<open>Isabelle2017\<close>). Thus @{tool jedit_client} can connect to the
   315   Isabelle desktop application without further options.
   316 
   317   The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system
   318   option @{system_option_ref ML_process_policy} for ML processes started by
   319   the Prover IDE, e.g. to control CPU affinity on multiprocessor systems.
   320 
   321   The JVM system property \<^verbatim>\<open>isabelle.jedit_server\<close> provides a different server
   322   name, e.g.\ use \<^verbatim>\<open>isabelle jedit -Disabelle.jedit_server=\<close>\<open>name\<close> and
   323   \<^verbatim>\<open>isabelle jedit_client -s\<close>~\<open>name\<close> to connect later on.
   324 \<close>
   325 
   326 
   327 section \<open>GUI rendering\<close>
   328 
   329 subsection \<open>Look-and-feel \label{sec:look-and-feel}\<close>
   330 
   331 text \<open>
   332   jEdit is a Java/AWT/Swing application with the ambition to support
   333   ``native'' look-and-feel on all platforms, within the limits of what Oracle
   334   as Java provider and major operating system distributors allow (see also
   335   \secref{sec:problems}).
   336 
   337   Isabelle/jEdit enables platform-specific look-and-feel by default as
   338   follows.
   339 
   340     \<^descr>[Linux:] The platform-independent \<^emph>\<open>Metal\<close> is used by default.
   341 
   342     The Linux-specific \<^emph>\<open>GTK+\<close> often works as well, but the overall GTK theme
   343     and options need to be selected to suite Java/AWT/Swing. Note that Java
   344     Virtual Machine has no direct influence of GTK rendering.
   345 
   346     \<^descr>[Windows:] Regular \<^emph>\<open>Windows\<close> is used by default.
   347 
   348     \<^descr>[Mac OS X:] Regular \<^emph>\<open>Mac OS X\<close> is used by default.
   349 
   350     The bundled \<^emph>\<open>MacOSX\<close> plugin provides various functions that are expected
   351     from applications on that particular platform: quit from menu or dock,
   352     preferences menu, drag-and-drop of text files on the application,
   353     full-screen mode for main editor windows. It is advisable to have the
   354     \<^emph>\<open>MacOSX\<close> plugin enabled all the time on that platform.
   355 
   356   Users may experiment with different Swing look-and-feels, but need to keep
   357   in mind that this extra variance of GUI functionality often causes problems.
   358   The platform-independent \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close> should always work on all
   359   platforms, although they are technically and stylistically outdated. The
   360   historic \<^emph>\<open>CDE/Motif\<close> should be ignored.
   361 
   362   Changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close> may update the
   363   GUI only partially: proper restart of Isabelle/jEdit is usually required.
   364 \<close>
   365 
   366 
   367 subsection \<open>Displays with very high resolution \label{sec:hdpi}\<close>
   368 
   369 text \<open>
   370   In distant past, displays with $1024 \times 768$ or $1280 \times 1024$
   371   pixels were considered ``high resolution'' and bitmap fonts with 12 or 14
   372   pixels as adequate for text rendering. In 2017, we routinely see much higher
   373   resolutions, e.g. ``Full HD'' at $1920 \times 1080$ pixels or ``Ultra HD'' /
   374   ``4K'' at $3840 \times 2160$.
   375 
   376   GUI frameworks are usually lagging behind, with hard-wired icon sizes and
   377   tiny fonts. Java and jEdit do provide reasonable support for very high
   378   resolution, but this requires manual adjustments as described below.
   379 
   380   \<^medskip>
   381   The \<^bold>\<open>operating-system\<close> usually provides some configuration for global
   382   scaling of text fonts, e.g.\ $120\%$--$250\%$ on Windows. This impacts
   383   regular GUI elements, when used with native look-and-feel: Linux \<^emph>\<open>GTK+\<close>,
   384   \<^emph>\<open>Windows\<close>, \<^emph>\<open>Mac OS X\<close>, respectively. Alternatively, it is possible to use
   385   the platform-independent \<^emph>\<open>Metal\<close> look-and-feel and readjust its main font
   386   sizes via jEdit options explained below. The Isabelle/jEdit \<^bold>\<open>application\<close>
   387   provides further options to adjust font sizes in particular GUI elements.
   388   Here is a summary of all relevant font properties:
   389 
   390     \<^item> \<^emph>\<open>Global Options / Text Area / Text font\<close>: the main text area font,
   391     which is also used as reference point for various derived font sizes,
   392     e.g.\ the \<^emph>\<open>Output\<close> (\secref{sec:output}) and \<^emph>\<open>State\<close>
   393     (\secref{sec:state-output}) panels.
   394 
   395     \<^item> \<^emph>\<open>Global Options / Gutter / Gutter font\<close>: the font for the gutter area
   396     left of the main text area, e.g.\ relevant for display of line numbers
   397     (disabled by default).
   398 
   399     \<^item> \<^emph>\<open>Global Options / Appearance / Button, menu and label font\<close> as well as
   400     \<^emph>\<open>List and text field font\<close>: this specifies the primary and secondary font
   401     for the \<^emph>\<open>Metal\<close> look-and-feel (\secref{sec:look-and-feel}).
   402 
   403     \<^item> \<^emph>\<open>Plugin Options / Isabelle / General / Reset Font Size\<close>: the main text
   404     area font size for action @{action_ref "isabelle.reset-font-size"}, e.g.\
   405     relevant for quick scaling like in common web browsers.
   406 
   407     \<^item> \<^emph>\<open>Plugin Options / Console / General / Font\<close>: the console window font,
   408     e.g.\ relevant for Isabelle/Scala command-line.
   409 
   410   In \figref{fig:isabelle-jedit-hdpi} the \<^emph>\<open>Metal\<close> look-and-feel is configured
   411   with custom fonts at 30 pixels, and the main text area and console at 36
   412   pixels. This leads to decent rendering quality, despite the old-fashioned
   413   appearance of \<^emph>\<open>Metal\<close>.
   414 
   415   \begin{figure}[!htb]
   416   \begin{center}
   417   \includegraphics[width=\textwidth]{isabelle-jedit-hdpi}
   418   \end{center}
   419   \caption{Metal look-and-feel with custom fonts for very high resolution}
   420   \label{fig:isabelle-jedit-hdpi}
   421   \end{figure}
   422 \<close>
   423 
   424 
   425 chapter \<open>Augmented jEdit functionality\<close>
   426 
   427 section \<open>Dockable windows \label{sec:dockables}\<close>
   428 
   429 text \<open>
   430   In jEdit terminology, a \<^emph>\<open>view\<close> is an editor window with one or more \<^emph>\<open>text
   431   areas\<close> that show the content of one or more \<^emph>\<open>buffers\<close>. A regular view may
   432   be surrounded by \<^emph>\<open>dockable windows\<close> that show additional information in
   433   arbitrary format, not just text; a \<^emph>\<open>plain view\<close> does not allow dockables.
   434   The \<^emph>\<open>dockable window manager\<close> of jEdit organizes these dockable windows,
   435   either as \<^emph>\<open>floating\<close> windows, or \<^emph>\<open>docked\<close> panels within one of the four
   436   margins of the view. There may be any number of floating instances of some
   437   dockable window, but at most one docked instance; jEdit actions that address
   438   \<^emph>\<open>the\<close> dockable window of a particular kind refer to the unique docked
   439   instance.
   440 
   441   Dockables are used routinely in jEdit for important functionality like
   442   \<^emph>\<open>HyperSearch Results\<close> or the \<^emph>\<open>File System Browser\<close>. Plugins often provide
   443   a central dockable to access their main functionality, which may be opened
   444   by the user on demand. The Isabelle/jEdit plugin takes this approach to the
   445   extreme: its plugin menu provides the entry-points to many panels that are
   446   managed as dockable windows. Some important panels are docked by default,
   447   e.g.\ \<^emph>\<open>Documentation\<close>, \<^emph>\<open>State\<close>, \<^emph>\<open>Theories\<close> \<^emph>\<open>Output\<close>, \<^emph>\<open>Query\<close>. The user
   448   can change this arrangement easily and persistently.
   449 
   450   Compared to plain jEdit, dockable window management in Isabelle/jEdit is
   451   slightly augmented according to the the following principles:
   452 
   453   \<^item> Floating windows are dependent on the main window as \<^emph>\<open>dialog\<close> in
   454   the sense of Java/AWT/Swing. Dialog windows always stay on top of the view,
   455   which is particularly important in full-screen mode. The desktop environment
   456   of the underlying platform may impose further policies on such dependent
   457   dialogs, in contrast to fully independent windows, e.g.\ some window
   458   management functions may be missing.
   459 
   460   \<^item> Keyboard focus of the main view vs.\ a dockable window is carefully
   461   managed according to the intended semantics, as a panel mainly for output or
   462   input. For example, activating the \<^emph>\<open>Output\<close> (\secref{sec:output}) or State
   463   (\secref{sec:state-output}) panel via the dockable window manager returns
   464   keyboard focus to the main text area, but for \<^emph>\<open>Query\<close> (\secref{sec:query})
   465   or \<^emph>\<open>Sledgehammer\<close> \secref{sec:sledgehammer} the focus is given to the main
   466   input field of that panel.
   467 
   468   \<^item> Panels that provide their own text area for output have an additional
   469   dockable menu item \<^emph>\<open>Detach\<close>. This produces an independent copy of the
   470   current output as a floating \<^emph>\<open>Info\<close> window, which displays that content
   471   independently of ongoing changes of the PIDE document-model. Note that
   472   Isabelle/jEdit popup windows (\secref{sec:tooltips-hyperlinks}) provide a
   473   similar \<^emph>\<open>Detach\<close> operation as an icon.
   474 \<close>
   475 
   476 
   477 section \<open>Isabelle symbols \label{sec:symbols}\<close>
   478 
   479 text \<open>
   480   Isabelle sources consist of \<^emph>\<open>symbols\<close> that extend plain ASCII to allow
   481   infinitely many mathematical symbols within the formal sources. This works
   482   without depending on particular encodings and varying Unicode
   483   standards.\<^footnote>\<open>Raw Unicode characters within formal sources would compromise
   484   portability and reliability in the face of changing interpretation of
   485   special features of Unicode, such as Combining Characters or Bi-directional
   486   Text.\<close> See @{cite "Wenzel:2011:CICM"}.
   487 
   488   For the prover back-end, formal text consists of ASCII characters that are
   489   grouped according to some simple rules, e.g.\ as plain ``\<^verbatim>\<open>a\<close>'' or symbolic
   490   ``\<^verbatim>\<open>\<alpha>\<close>''. For the editor front-end, a certain subset of symbols is rendered
   491   physically via Unicode glyphs, in order to show ``\<^verbatim>\<open>\<alpha>\<close>'' as ``\<open>\<alpha>\<close>'', for
   492   example. This symbol interpretation is specified by the Isabelle system
   493   distribution in \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and may be augmented by the
   494   user in @{path "$ISABELLE_HOME_USER/etc/symbols"}.
   495 
   496   The appendix of @{cite "isabelle-isar-ref"} gives an overview of the
   497   standard interpretation of finitely many symbols from the infinite
   498   collection. Uninterpreted symbols are displayed literally, e.g.\
   499   ``\<^verbatim>\<open>\<foobar>\<close>''. Overlap of Unicode characters used in symbol
   500   interpretation with informal ones (which might appear e.g.\ in comments)
   501   needs to be avoided. Raw Unicode characters within prover source files
   502   should be restricted to informal parts, e.g.\ to write text in non-latin
   503   alphabets in comments.
   504 \<close>
   505 
   506 paragraph \<open>Encoding.\<close>
   507 text \<open>Technically, the Unicode interpretation of Isabelle symbols is an
   508   \<^emph>\<open>encoding\<close> called \<^verbatim>\<open>UTF-8-Isabelle\<close> in jEdit (\<^emph>\<open>not\<close> in the underlying
   509   JVM). It is provided by the Isabelle Base plugin and enabled by default for
   510   all source files in Isabelle/jEdit. Sometimes such defaults are reset
   511   accidentally, or malformed UTF-8 sequences in the text force jEdit to fall
   512   back on a different encoding like \<^verbatim>\<open>ISO-8859-15\<close>. In that case, verbatim
   513   ``\<^verbatim>\<open>\<alpha>\<close>'' will be shown in the text buffer instead of its Unicode rendering
   514   ``\<open>\<alpha>\<close>''. The jEdit menu operation \<^emph>\<open>File~/ Reload with Encoding~/
   515   UTF-8-Isabelle\<close> helps to resolve such problems (after repairing malformed
   516   parts of the text). \<close>
   517 
   518 paragraph \<open>Font.\<close>
   519 text \<open>Correct rendering via Unicode requires a font that contains glyphs for
   520   the corresponding codepoints. There are also various unusual symbols with
   521   particular purpose in Isabelle, e.g.\ control symbols and very long arrows.
   522   Isabelle/jEdit prefers its own application fonts \<^verbatim>\<open>IsabelleText\<close>, which
   523   ensures that standard collection of Isabelle symbols is actually shown on
   524   the screen (or printer) as expected.
   525 
   526   Note that a Java/AWT/Swing application can load additional fonts only if
   527   they are not installed on the operating system already! Some outdated
   528   version of \<^verbatim>\<open>IsabelleText\<close> that happens to be provided by the operating
   529   system would prevent Isabelle/jEdit to use its bundled version. This could
   530   lead to missing glyphs (black rectangles), when the system version of
   531   \<^verbatim>\<open>IsabelleText\<close> is older than the application version. This problem can be
   532   avoided by refraining to ``install'' any version of \<^verbatim>\<open>IsabelleText\<close> in the
   533   first place, although it might be tempting to use the same font in other
   534   applications.
   535 
   536   HTML pages generated by Isabelle refer to the same \<^verbatim>\<open>IsabelleText\<close> font as a
   537   server-side resource. Thus a web-browser can use that without requiring a
   538   locally installed copy.
   539 \<close>
   540 
   541 paragraph \<open>Input methods.\<close>
   542 text \<open>In principle, Isabelle/jEdit could delegate the problem to produce
   543   Isabelle symbols in their Unicode rendering to the underlying operating
   544   system and its \<^emph>\<open>input methods\<close>. Regular jEdit also provides various ways to
   545   work with \<^emph>\<open>abbreviations\<close> to produce certain non-ASCII characters. Since
   546   none of these standard input methods work satisfactorily for the
   547   mathematical characters required for Isabelle, various specific
   548   Isabelle/jEdit mechanisms are provided.
   549 
   550   This is a summary for practically relevant input methods for Isabelle
   551   symbols.
   552 
   553   \<^enum> The \<^emph>\<open>Symbols\<close> panel: some GUI buttons allow to insert certain symbols in
   554   the text buffer. There are also tooltips to reveal the official Isabelle
   555   representation with some additional information about \<^emph>\<open>symbol
   556   abbreviations\<close> (see below).
   557 
   558   \<^enum> Copy/paste from decoded source files: text that is rendered as Unicode
   559   already can be re-used to produce further text. This also works between
   560   different applications, e.g.\ Isabelle/jEdit and some web browser or mail
   561   client, as long as the same Unicode interpretation of Isabelle symbols is
   562   used.
   563 
   564   \<^enum> Copy/paste from prover output within Isabelle/jEdit. The same principles
   565   as for text buffers apply, but note that \<^emph>\<open>copy\<close> in secondary Isabelle/jEdit
   566   windows works via the keyboard shortcuts \<^verbatim>\<open>C+c\<close> or \<^verbatim>\<open>C+INSERT\<close>, while jEdit
   567   menu actions always refer to the primary text area!
   568 
   569   \<^enum> Completion provided by the Isabelle plugin (see \secref{sec:completion}).
   570   Isabelle symbols have a canonical name and optional abbreviations. This can
   571   be used with the text completion mechanism of Isabelle/jEdit, to replace a
   572   prefix of the actual symbol like \<^verbatim>\<open>\<lambda>\<close>, or its name preceded by backslash
   573   \<^verbatim>\<open>\lambda\<close>, or its ASCII abbreviation \<^verbatim>\<open>%\<close> by the Unicode rendering.
   574 
   575   The following table is an extract of the information provided by the
   576   standard \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> file:
   577 
   578   \<^medskip>
   579   \begin{tabular}{lll}
   580     \<^bold>\<open>symbol\<close> & \<^bold>\<open>name with backslash\<close> & \<^bold>\<open>abbreviation\<close> \\\hline
   581     \<open>\<lambda>\<close> & \<^verbatim>\<open>\lambda\<close> & \<^verbatim>\<open>%\<close> \\
   582     \<open>\<Rightarrow>\<close> & \<^verbatim>\<open>\Rightarrow\<close> & \<^verbatim>\<open>=>\<close> \\
   583     \<open>\<Longrightarrow>\<close> & \<^verbatim>\<open>\Longrightarrow\<close> & \<^verbatim>\<open>==>\<close> \\[0.5ex]
   584     \<open>\<And>\<close> & \<^verbatim>\<open>\And\<close> & \<^verbatim>\<open>!!\<close> \\
   585     \<open>\<equiv>\<close> & \<^verbatim>\<open>\equiv\<close> & \<^verbatim>\<open>==\<close> \\[0.5ex]
   586     \<open>\<forall>\<close> & \<^verbatim>\<open>\forall\<close> & \<^verbatim>\<open>!\<close> \\
   587     \<open>\<exists>\<close> & \<^verbatim>\<open>\exists\<close> & \<^verbatim>\<open>?\<close> \\
   588     \<open>\<longrightarrow>\<close> & \<^verbatim>\<open>\longrightarrow\<close> & \<^verbatim>\<open>-->\<close> \\
   589     \<open>\<and>\<close> & \<^verbatim>\<open>\and\<close> & \<^verbatim>\<open>&\<close> \\
   590     \<open>\<or>\<close> & \<^verbatim>\<open>\or\<close> & \<^verbatim>\<open>|\<close> \\
   591     \<open>\<not>\<close> & \<^verbatim>\<open>\not\<close> & \<^verbatim>\<open>~\<close> \\
   592     \<open>\<noteq>\<close> & \<^verbatim>\<open>\noteq\<close> & \<^verbatim>\<open>~=\<close> \\
   593     \<open>\<in>\<close> & \<^verbatim>\<open>\in\<close> & \<^verbatim>\<open>:\<close> \\
   594     \<open>\<notin>\<close> & \<^verbatim>\<open>\notin\<close> & \<^verbatim>\<open>~:\<close> \\
   595   \end{tabular}
   596   \<^medskip>
   597 
   598   Note that the above abbreviations refer to the input method. The logical
   599   notation provides ASCII alternatives that often coincide, but sometimes
   600   deviate. This occasionally causes user confusion with old-fashioned Isabelle
   601   source that use ASCII replacement notation like \<^verbatim>\<open>!\<close> or \<^verbatim>\<open>ALL\<close> directly in
   602   the text.
   603 
   604   On the other hand, coincidence of symbol abbreviations with ASCII
   605   replacement syntax syntax helps to update old theory sources via explicit
   606   completion (see also \<^verbatim>\<open>C+b\<close> explained in \secref{sec:completion}).
   607 \<close>
   608 
   609 paragraph \<open>Control symbols.\<close>
   610 text \<open>There are some special control symbols to modify the display style of a
   611   single symbol (without nesting). Control symbols may be applied to a region
   612   of selected text, either using the \<^emph>\<open>Symbols\<close> panel or keyboard shortcuts or
   613   jEdit actions. These editor operations produce a separate control symbol for
   614   each symbol in the text, in order to make the whole text appear in a certain
   615   style.
   616 
   617   \<^medskip>
   618   \begin{tabular}{llll}
   619     \<^bold>\<open>style\<close> & \<^bold>\<open>symbol\<close> & \<^bold>\<open>shortcut\<close> & \<^bold>\<open>action\<close> \\\hline
   620     superscript & \<^verbatim>\<open>\<^sup>\<close> & \<^verbatim>\<open>C+e UP\<close> & @{action_ref "isabelle.control-sup"} \\
   621     subscript & \<^verbatim>\<open>\<^sub>\<close> & \<^verbatim>\<open>C+e DOWN\<close> & @{action_ref "isabelle.control-sub"} \\
   622     bold face & \<^verbatim>\<open>\<^bold>\<close> & \<^verbatim>\<open>C+e RIGHT\<close> & @{action_ref "isabelle.control-bold"} \\
   623     emphasized & \<^verbatim>\<open>\<^emph>\<close> & \<^verbatim>\<open>C+e LEFT\<close> & @{action_ref "isabelle.control-emph"} \\
   624     reset & & \<^verbatim>\<open>C+e BACK_SPACE\<close> & @{action_ref "isabelle.control-reset"} \\
   625   \end{tabular}
   626   \<^medskip>
   627 
   628   To produce a single control symbol, it is also possible to complete on
   629   \<^verbatim>\<open>\sup\<close>, \<^verbatim>\<open>\sub\<close>, \<^verbatim>\<open>\bold\<close>, \<^verbatim>\<open>\emph\<close> as for regular symbols.
   630 
   631   The emphasized style only takes effect in document output (when used with a
   632   cartouche), but not in the editor.
   633 \<close>
   634 
   635 
   636 section \<open>Scala console \label{sec:scala-console}\<close>
   637 
   638 text \<open>
   639   The \<^emph>\<open>Console\<close> plugin manages various shells (command interpreters), e.g.\
   640   \<^emph>\<open>BeanShell\<close>, which is the official jEdit scripting language, and the
   641   cross-platform \<^emph>\<open>System\<close> shell. Thus the console provides similar
   642   functionality than the Emacs buffers \<^verbatim>\<open>*scratch*\<close> and \<^verbatim>\<open>*shell*\<close>.
   643 
   644   Isabelle/jEdit extends the repertoire of the console by \<^emph>\<open>Scala\<close>, which is
   645   the regular Scala toplevel loop running inside the same JVM process as
   646   Isabelle/jEdit itself. This means the Scala command interpreter has access
   647   to the JVM name space and state of the running Prover IDE application. The
   648   default environment imports the full content of packages \<^verbatim>\<open>isabelle\<close> and
   649   \<^verbatim>\<open>isabelle.jedit\<close>.
   650 
   651   For example, \<^verbatim>\<open>PIDE\<close> refers to the Isabelle/jEdit plugin object, and \<^verbatim>\<open>view\<close>
   652   to the current editor view of jEdit. The Scala expression
   653   \<^verbatim>\<open>PIDE.snapshot(view)\<close> makes a PIDE document snapshot of the current buffer
   654   within the current editor view.
   655 
   656   This helps to explore Isabelle/Scala functionality interactively. Some care
   657   is required to avoid interference with the internals of the running
   658   application.
   659 \<close>
   660 
   661 
   662 section \<open>File-system access\<close>
   663 
   664 text \<open>
   665   File specifications in jEdit follow various formats and conventions
   666   according to \<^emph>\<open>Virtual File Systems\<close>, which may be also provided by
   667   additional plugins. This allows to access remote files via the \<^verbatim>\<open>http:\<close>
   668   protocol prefix, for example. Isabelle/jEdit attempts to work with the
   669   file-system model of jEdit as far as possible. In particular, theory sources
   670   are passed directly from the editor to the prover, without indirection via
   671   physical files.
   672 
   673   Despite the flexibility of URLs in jEdit, local files are particularly
   674   important and are accessible without protocol prefix. The file path notation
   675   is that of the Java Virtual Machine on the underlying platform. On Windows
   676   the preferred form uses backslashes, but happens to accept forward slashes
   677   like Unix/POSIX as well. Further differences arise due to Windows drive
   678   letters and network shares.
   679 
   680   The Java notation for files needs to be distinguished from the one of
   681   Isabelle, which uses POSIX notation with forward slashes on \<^emph>\<open>all\<close>
   682   platforms. Isabelle/ML on Windows uses Unix-style path notation, too, and
   683   driver letter representation as in Cygwin (e.g.\ \<^verbatim>\<open>/cygdrive/c\<close>). Moreover,
   684   environment variables from the Isabelle process may be used freely, e.g.\
   685   \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> or \<^file>\<open>$POLYML_HOME/README\<close>. There are special
   686   shortcuts: \<^dir>\<open>~\<close> for \<^dir>\<open>$USER_HOME\<close> and \<^dir>\<open>~~\<close> for \<^dir>\<open>$ISABELLE_HOME\<close>.
   687 
   688   \<^medskip>
   689   Since jEdit happens to support environment variables within file
   690   specifications as well, it is natural to use similar notation within the
   691   editor, e.g.\ in the file-browser. This does not work in full generality,
   692   though, due to the bias of jEdit towards platform-specific notation and of
   693   Isabelle towards POSIX. Moreover, the Isabelle settings environment is not
   694   yet active when starting Isabelle/jEdit via its standard application
   695   wrapper, in contrast to @{tool jedit} run from the command line
   696   (\secref{sec:command-line}).
   697 
   698   Isabelle/jEdit imitates important system settings within the Java process
   699   environment, in order to allow easy access to these important places from
   700   the editor: \<^verbatim>\<open>$ISABELLE_HOME\<close>, \<^verbatim>\<open>$ISABELLE_HOME_USER\<close>, \<^verbatim>\<open>$JEDIT_HOME\<close>,
   701   \<^verbatim>\<open>$JEDIT_SETTINGS\<close>. The file browser of jEdit also includes \<^emph>\<open>Favorites\<close> for
   702   these two important locations.
   703 
   704   \<^medskip>
   705   Path specifications in prover input or output usually include formal markup
   706   that turns it into a hyperlink (see also \secref{sec:tooltips-hyperlinks}).
   707   This allows to open the corresponding file in the text editor, independently
   708   of the path notation. If the path refers to a directory, the jEdit file
   709   browser is opened on it.
   710 
   711   Formally checked paths in prover input are subject to completion
   712   (\secref{sec:completion}): partial specifications are resolved via directory
   713   content and possible completions are offered in a popup.
   714 \<close>
   715 
   716 
   717 section \<open>Indentation\<close>
   718 
   719 text \<open>
   720   Isabelle/jEdit augments the existing indentation facilities of jEdit to take
   721   the structure of theory and proof texts into account. There is also special
   722   support for unstructured proof scripts.
   723 
   724     \<^descr>[Syntactic indentation] follows the outer syntax of Isabelle/Isar.
   725 
   726     Action @{action "indent-lines"} (shortcut \<^verbatim>\<open>C+i\<close>) indents the current line
   727     according to command keywords and some command substructure: this
   728     approximation may need further manual tuning.
   729 
   730     Action @{action "isabelle.newline"} (shortcut \<^verbatim>\<open>ENTER\<close>) indents the old
   731     and the new line according to command keywords only: this leads to precise
   732     alignment of the main Isar language elements. This depends on option
   733     @{system_option_def "jedit_indent_newline"} (enabled by default).
   734 
   735     Regular input (via keyboard or completion) indents the current line
   736     whenever an new keyword is emerging at the start of the line. This depends
   737     on option @{system_option_def "jedit_indent_input"} (enabled by default).
   738 
   739     \<^descr>[Semantic indentation] adds additional white space to unstructured proof
   740     scripts (\<^theory_text>\<open>apply\<close> etc.) via number of subgoals. This requires information
   741     of ongoing document processing and may thus lag behind, when the user is
   742     editing too quickly; see also option @{system_option_def
   743     "jedit_script_indent"} and @{system_option_def
   744     "jedit_script_indent_limit"}.
   745 
   746   The above options are accessible in the menu \<^emph>\<open>Plugins / Plugin Options /
   747   Isabelle / General\<close>. A prerequisite for advanced indentation is \<^emph>\<open>Utilities
   748   / Buffer Options / Automatic indentation\<close>: it needs to be set to \<^verbatim>\<open>full\<close>
   749   (default).
   750 \<close>
   751 
   752 
   753 section \<open>SideKick parsers \label{sec:sidekick}\<close>
   754 
   755 text \<open>
   756   The \<^emph>\<open>SideKick\<close> plugin provides some general services to display buffer
   757   structure in a tree view. Isabelle/jEdit provides SideKick parsers for its
   758   main mode for theory files, ML files, as well as some minor modes for the
   759   \<^verbatim>\<open>NEWS\<close> file (see \figref{fig:sidekick}), session \<^verbatim>\<open>ROOT\<close> files, system
   760   \<^verbatim>\<open>options\<close>, and Bib{\TeX} files (\secref{sec:bibtex}).
   761 
   762   \begin{figure}[!htb]
   763   \begin{center}
   764   \includegraphics[scale=0.333]{sidekick}
   765   \end{center}
   766   \caption{The Isabelle NEWS file with SideKick tree view}
   767   \label{fig:sidekick}
   768   \end{figure}
   769 
   770   The default SideKick parser for theory files is \<^verbatim>\<open>isabelle\<close>: it provides a
   771   tree-view on the formal document structure, with section headings at the top
   772   and formal specification elements at the bottom. The alternative parser
   773   \<^verbatim>\<open>isabelle-context\<close> shows nesting of context blocks according to \<^theory_text>\<open>begin \<dots>
   774   end\<close> structure.
   775 
   776   \<^medskip>
   777   Isabelle/ML files are structured according to semi-formal comments that are
   778   explained in @{cite "isabelle-implementation"}. This outline is turned into
   779   a tree-view by default, by using the \<^verbatim>\<open>isabelle-ml\<close> parser. There is also a
   780   folding mode of the same name, for hierarchic text folds within ML files.
   781 
   782   \<^medskip>
   783   The special SideKick parser \<^verbatim>\<open>isabelle-markup\<close> exposes the uninterpreted
   784   markup tree of the PIDE document model of the current buffer. This is
   785   occasionally useful for informative purposes, but the amount of displayed
   786   information might cause problems for large buffers.
   787 \<close>
   788 
   789 
   790 chapter \<open>Prover IDE functionality \label{sec:document-model}\<close>
   791 
   792 section \<open>Document model \label{sec:document-model}\<close>
   793 
   794 text \<open>
   795   The document model is central to the PIDE architecture: the editor and the
   796   prover have a common notion of structured source text with markup, which is
   797   produced by formal processing. The editor is responsible for edits of
   798   document source, as produced by the user. The prover is responsible for
   799   reports of document markup, as produced by its processing in the background.
   800 
   801   Isabelle/jEdit handles classic editor events of jEdit, in order to connect
   802   the physical world of the GUI (with its singleton state) to the mathematical
   803   world of multiple document versions (with timeless and stateless updates).
   804 \<close>
   805 
   806 
   807 subsection \<open>Editor buffers and document nodes \label{sec:buffer-node}\<close>
   808 
   809 text \<open>
   810   As a regular text editor, jEdit maintains a collection of \<^emph>\<open>buffers\<close> to
   811   store text files; each buffer may be associated with any number of visible
   812   \<^emph>\<open>text areas\<close>. Buffers are subject to an \<^emph>\<open>edit mode\<close> that is determined
   813   from the file name extension. The following modes are treated specifically
   814   in Isabelle/jEdit:
   815 
   816   \<^medskip>
   817   \begin{tabular}{lll}
   818   \<^bold>\<open>mode\<close> & \<^bold>\<open>file name\<close> & \<^bold>\<open>content\<close> \\\hline
   819   \<^verbatim>\<open>isabelle\<close> & \<^verbatim>\<open>*.thy\<close> & theory source \\
   820   \<^verbatim>\<open>isabelle-ml\<close> & \<^verbatim>\<open>*.ML\<close> & Isabelle/ML source \\
   821   \<^verbatim>\<open>sml\<close> & \<^verbatim>\<open>*.sml\<close> or \<^verbatim>\<open>*.sig\<close> & Standard ML source \\
   822   \<^verbatim>\<open>isabelle-root\<close> & \<^verbatim>\<open>ROOT\<close> & session root \\
   823   \<^verbatim>\<open>isabelle-options\<close> & & Isabelle options \\
   824   \<^verbatim>\<open>isabelle-news\<close> & & Isabelle NEWS \\
   825   \end{tabular}
   826   \<^medskip>
   827 
   828   All jEdit buffers are automatically added to the PIDE document-model as
   829   \<^emph>\<open>document nodes\<close>. The overall document structure is defined by the theory
   830   nodes in two dimensions:
   831 
   832     \<^enum> via \<^bold>\<open>theory imports\<close> that are specified in the \<^emph>\<open>theory header\<close> using
   833     concrete syntax of the @{command_ref theory} command @{cite
   834     "isabelle-isar-ref"};
   835 
   836     \<^enum> via \<^bold>\<open>auxiliary files\<close> that are included into a theory by \<^emph>\<open>load
   837     commands\<close>, notably @{command_ref ML_file} and @{command_ref SML_file}
   838     @{cite "isabelle-isar-ref"}.
   839 
   840   In any case, source files are managed by the PIDE infrastructure: the
   841   physical file-system only plays a subordinate role. The relevant version of
   842   source text is passed directly from the editor to the prover, using internal
   843   communication channels.
   844 \<close>
   845 
   846 
   847 subsection \<open>Theories \label{sec:theories}\<close>
   848 
   849 text \<open>
   850   The \<^emph>\<open>Theories\<close> panel (see also \figref{fig:theories}) provides an overview
   851   of the status of continuous checking of theory nodes within the document
   852   model.
   853 
   854   \begin{figure}[!htb]
   855   \begin{center}
   856   \includegraphics[scale=0.333]{theories}
   857   \end{center}
   858   \caption{Theories panel with an overview of the document-model, and jEdit
   859   text areas as editable views on some of the document nodes}
   860   \label{fig:theories}
   861   \end{figure}
   862 
   863   Theory imports are resolved automatically by the PIDE document model: all
   864   required files are loaded and stored internally, without the need to open
   865   corresponding jEdit buffers. Opening or closing editor buffers later on has
   866   no direct impact on the formal document content: it only affects visibility.
   867 
   868   In contrast, auxiliary files (e.g.\ from @{command ML_file} commands) are
   869   \<^emph>\<open>not\<close> resolved within the editor by default, but the prover process takes
   870   care of that. This may be changed by enabling the system option
   871   @{system_option jedit_auto_resolve}: it ensures that all files are uniformly
   872   provided by the editor.
   873 
   874   \<^medskip>
   875   The visible \<^emph>\<open>perspective\<close> of Isabelle/jEdit is defined by the collective
   876   view on theory buffers via open text areas. The perspective is taken as a
   877   hint for document processing: the prover ensures that those parts of a
   878   theory where the user is looking are checked, while other parts that are
   879   presently not required are ignored. The perspective is changed by opening or
   880   closing text area windows, or scrolling within a window.
   881 
   882   The \<^emph>\<open>Theories\<close> panel provides some further options to influence the process
   883   of continuous checking: it may be switched off globally to restrict the
   884   prover to superficial processing of command syntax. It is also possible to
   885   indicate theory nodes as \<^emph>\<open>required\<close> for continuous checking: this means
   886   such nodes and all their imports are always processed independently of the
   887   visibility status (if continuous checking is enabled). Big theory libraries
   888   that are marked as required can have significant impact on performance!
   889 
   890   The \<^emph>\<open>Purge\<close> button restricts the document model to theories that are
   891   required for open editor buffers: inaccessible theories are removed and will
   892   be rechecked when opened or imported later.
   893 
   894   \<^medskip>
   895   Formal markup of checked theory content is turned into GUI rendering, based
   896   on a standard repertoire known from mainstream IDEs for programming
   897   languages: colors, icons, highlighting, squiggly underlines, tooltips,
   898   hyperlinks etc. For outer syntax of Isabelle/Isar there is some traditional
   899   syntax-highlighting via static keywords and tokenization within the editor;
   900   this buffer syntax is determined from theory imports. In contrast, the
   901   painting of inner syntax (term language etc.)\ uses semantic information
   902   that is reported dynamically from the logical context. Thus the prover can
   903   provide additional markup to help the user to understand the meaning of
   904   formal text, and to produce more text with some add-on tools (e.g.\
   905   information messages with \<^emph>\<open>sendback\<close> markup by automated provers or
   906   disprovers in the background). \<close>
   907 
   908 
   909 subsection \<open>Auxiliary files \label{sec:aux-files}\<close>
   910 
   911 text \<open>
   912   Special load commands like @{command_ref ML_file} and @{command_ref
   913   SML_file} @{cite "isabelle-isar-ref"} refer to auxiliary files within some
   914   theory. Conceptually, the file argument of the command extends the theory
   915   source by the content of the file, but its editor buffer may be loaded~/
   916   changed~/ saved separately. The PIDE document model propagates changes of
   917   auxiliary file content to the corresponding load command in the theory, to
   918   update and process it accordingly: changes of auxiliary file content are
   919   treated as changes of the corresponding load command.
   920 
   921   \<^medskip>
   922   As a concession to the massive amount of ML files in Isabelle/HOL itself,
   923   the content of auxiliary files is only added to the PIDE document-model on
   924   demand, the first time when opened explicitly in the editor. There are
   925   further tricks to manage markup of ML files, such that Isabelle/HOL may be
   926   edited conveniently in the Prover IDE on small machines with only 8\,GB of
   927   main memory. Using \<^verbatim>\<open>Pure\<close> as logic session image, the exploration may start
   928   at the top \<^file>\<open>$ISABELLE_HOME/src/HOL/Main.thy\<close> or the bottom
   929   \<^file>\<open>$ISABELLE_HOME/src/HOL/HOL.thy\<close>, for example. It is also possible to
   930   explore the Isabelle/Pure bootstrap process (a virtual copy) by opening
   931   \<^file>\<open>$ISABELLE_HOME/src/Pure/ROOT.ML\<close> like a theory in the Prover IDE.
   932 
   933   Initially, before an auxiliary file is opened in the editor, the prover
   934   reads its content from the physical file-system. After the file is opened
   935   for the first time in the editor, e.g.\ by following the hyperlink
   936   (\secref{sec:tooltips-hyperlinks}) for the argument of its @{command
   937   ML_file} command, the content is taken from the jEdit buffer.
   938 
   939   The change of responsibility from prover to editor counts as an update of
   940   the document content, so subsequent theory sources need to be re-checked.
   941   When the buffer is closed, the responsibility remains to the editor: the
   942   file may be opened again without causing another document update.
   943 
   944   A file that is opened in the editor, but its theory with the load command is
   945   not, is presently inactive in the document model. A file that is loaded via
   946   multiple load commands is associated to an arbitrary one: this situation is
   947   morally unsupported and might lead to confusion.
   948 
   949   \<^medskip>
   950   Output that refers to an auxiliary file is combined with that of the
   951   corresponding load command, and shown whenever the file or the command are
   952   active (see also \secref{sec:output}).
   953 
   954   Warnings, errors, and other useful markup is attached directly to the
   955   positions in the auxiliary file buffer, in the manner of standard IDEs. By
   956   using the load command @{command SML_file} as explained in
   957   \<^file>\<open>$ISABELLE_HOME/src/Tools/SML/Examples.thy\<close>, Isabelle/jEdit may be used as
   958   fully-featured IDE for Standard ML, independently of theory or proof
   959   development: the required theory merely serves as some kind of project file
   960   for a collection of SML source modules.
   961 \<close>
   962 
   963 
   964 section \<open>Output \label{sec:output}\<close>
   965 
   966 text \<open>
   967   Prover output consists of \<^emph>\<open>markup\<close> and \<^emph>\<open>messages\<close>. Both are directly
   968   attached to the corresponding positions in the original source text, and
   969   visualized in the text area, e.g.\ as text colours for free and bound
   970   variables, or as squiggly underlines for warnings, errors etc.\ (see also
   971   \figref{fig:output}). In the latter case, the corresponding messages are
   972   shown by hovering with the mouse over the highlighted text --- although in
   973   many situations the user should already get some clue by looking at the
   974   position of the text highlighting, without seeing the message body itself.
   975 
   976   \begin{figure}[!htb]
   977   \begin{center}
   978   \includegraphics[scale=0.333]{output}
   979   \end{center}
   980   \caption{Multiple views on prover output: gutter with icon, text area with
   981   popup, text overview column, \<^emph>\<open>Theories\<close> panel, \<^emph>\<open>Output\<close> panel}
   982   \label{fig:output}
   983   \end{figure}
   984 
   985   The ``gutter'' on the left-hand-side of the text area uses icons to
   986   provide a summary of the messages within the adjacent text line. Message
   987   priorities are used to prefer errors over warnings, warnings over
   988   information messages; other output is ignored.
   989 
   990   The ``text overview column'' on the right-hand-side of the text area uses
   991   similar information to paint small rectangles for the overall status of the
   992   whole text buffer. The graphics is scaled to fit the logical buffer length
   993   into the given window height. Mouse clicks on the overview area move the
   994   cursor approximately to the corresponding text line in the buffer.
   995 
   996   The \<^emph>\<open>Theories\<close> panel provides another course-grained overview, but without
   997   direct correspondence to text positions. The coloured rectangles represent
   998   the amount of messages of a certain kind (warnings, errors, etc.) and the
   999   execution status of commands. The border of each rectangle indicates the
  1000   overall status of processing: a thick border means it is \<^emph>\<open>finished\<close> or
  1001   \<^emph>\<open>failed\<close> (with color for errors). A double-click on one of the theory
  1002   entries with their status overview opens the corresponding text buffer,
  1003   without moving the cursor to a specific point.
  1004 
  1005   \<^medskip>
  1006   The \<^emph>\<open>Output\<close> panel displays prover messages that correspond to a given
  1007   command, within a separate window. The cursor position in the presently
  1008   active text area determines the prover command whose cumulative message
  1009   output is appended and shown in that window (in canonical order according to
  1010   the internal execution of the command). There are also control elements to
  1011   modify the update policy of the output wrt.\ continued editor movements:
  1012   \<^emph>\<open>Auto update\<close> and \<^emph>\<open>Update\<close>. This is particularly useful for multiple
  1013   instances of the \<^emph>\<open>Output\<close> panel to look at different situations.
  1014   Alternatively, the panel can be turned into a passive \<^emph>\<open>Info\<close> window via the
  1015   \<^emph>\<open>Detach\<close> menu item.
  1016 
  1017   Proof state is handled separately (\secref{sec:state-output}), but it is
  1018   also possible to tick the corresponding checkbox to append it to regular
  1019   output (\figref{fig:output-including-state}). This is a globally persistent
  1020   option: it affects all open panels and future editor sessions.
  1021 
  1022   \begin{figure}[!htb]
  1023   \begin{center}
  1024   \includegraphics[scale=0.333]{output-including-state}
  1025   \end{center}
  1026   \caption{Proof state display within the regular output panel}
  1027   \label{fig:output-including-state}
  1028   \end{figure}
  1029 
  1030   \<^medskip>
  1031   Following the IDE principle, regular messages are attached to the original
  1032   source in the proper place and may be inspected on demand via popups. This
  1033   excludes messages that are somehow internal to the machinery of proof
  1034   checking, notably \<^emph>\<open>proof state\<close> and \<^emph>\<open>tracing\<close>.
  1035 
  1036   In any case, the same display technology is used for small popups and big
  1037   output windows. The formal text contains markup that may be explored
  1038   recursively via further popups and hyperlinks (see
  1039   \secref{sec:tooltips-hyperlinks}), or clicked directly to initiate certain
  1040   actions (see \secref{sec:auto-tools} and \secref{sec:sledgehammer}).
  1041 \<close>
  1042 
  1043 
  1044 section \<open>Proof state \label{sec:state-output}\<close>
  1045 
  1046 text \<open>
  1047   The main purpose of the Prover IDE is to help the user editing proof
  1048   documents, with ongoing formal checking by the prover in the background.
  1049   This can be done to some extent in the main text area alone, especially for
  1050   well-structured Isar proofs.
  1051 
  1052   Nonetheless, internal proof state needs to be inspected in many situations
  1053   of exploration and ``debugging''. The \<^emph>\<open>State\<close> panel shows exclusively such
  1054   proof state messages without further distraction, while all other messages
  1055   are displayed in \<^emph>\<open>Output\<close> (\secref{sec:output}).
  1056   \Figref{fig:output-and-state} shows a typical GUI layout where both panels
  1057   are open.
  1058 
  1059   \begin{figure}[!htb]
  1060   \begin{center}
  1061   \includegraphics[scale=0.333]{output-and-state}
  1062   \end{center}
  1063   \caption{Separate proof state display (right) and other output (bottom).}
  1064   \label{fig:output-and-state}
  1065   \end{figure}
  1066 
  1067   Another typical arrangement has more than one \<^emph>\<open>State\<close> panel open (as
  1068   floating windows), with \<^emph>\<open>Auto update\<close> disabled to look at an old situation
  1069   while the proof text in the vicinity is changed. The \<^emph>\<open>Update\<close> button
  1070   triggers an explicit one-shot update; this operation is also available via
  1071   the action @{action "isabelle.update-state"} (keyboard shortcut \<^verbatim>\<open>S+ENTER\<close>).
  1072 
  1073   On small screens, it is occasionally useful to have all messages
  1074   concatenated in the regular \<^emph>\<open>Output\<close> panel, e.g.\ see
  1075   \figref{fig:output-including-state}.
  1076 
  1077   \<^medskip>
  1078   The mechanics of \<^emph>\<open>Output\<close> versus \<^emph>\<open>State\<close> are slightly different:
  1079 
  1080     \<^item> \<^emph>\<open>Output\<close> shows information that is continuously produced and already
  1081     present when the GUI wants to show it. This is implicitly controlled by
  1082     the visible perspective on the text.
  1083 
  1084     \<^item> \<^emph>\<open>State\<close> initiates a real-time query on demand, with a full round trip
  1085     including a fresh print operation on the prover side. This is controlled
  1086     explicitly when the cursor is moved to the next command (\<^emph>\<open>Auto update\<close>)
  1087     or the \<^emph>\<open>Update\<close> operation is triggered.
  1088 
  1089   This can make a difference in GUI responsibility and resource usage within
  1090   the prover process. Applications with very big proof states that are only
  1091   inspected in isolation work better with the \<^emph>\<open>State\<close> panel.
  1092 \<close>
  1093 
  1094 
  1095 section \<open>Query \label{sec:query}\<close>
  1096 
  1097 text \<open>
  1098   The \<^emph>\<open>Query\<close> panel provides various GUI forms to request extra information
  1099   from the prover, as a replacement of old-style diagnostic commands like
  1100   @{command find_theorems}. There are input fields and buttons for a
  1101   particular query command, with output in a dedicated text area.
  1102 
  1103   The main query modes are presented as separate tabs: \<^emph>\<open>Find Theorems\<close>,
  1104   \<^emph>\<open>Find Constants\<close>, \<^emph>\<open>Print Context\<close>, e.g.\ see \figref{fig:query}. As usual
  1105   in jEdit, multiple \<^emph>\<open>Query\<close> windows may be active at the same time: any
  1106   number of floating instances, but at most one docked instance (which is used
  1107   by default).
  1108 
  1109   \begin{figure}[!htb]
  1110   \begin{center}
  1111   \includegraphics[scale=0.333]{query}
  1112   \end{center}
  1113   \caption{An instance of the Query panel: find theorems}
  1114   \label{fig:query}
  1115   \end{figure}
  1116 
  1117   \<^medskip>
  1118   The following GUI elements are common to all query modes:
  1119 
  1120     \<^item> The spinning wheel provides feedback about the status of a pending query
  1121     wrt.\ the evaluation of its context and its own operation.
  1122 
  1123     \<^item> The \<^emph>\<open>Apply\<close> button attaches a fresh query invocation to the current
  1124     context of the command where the cursor is pointing in the text.
  1125 
  1126     \<^item> The \<^emph>\<open>Search\<close> field allows to highlight query output according to some
  1127     regular expression, in the notation that is commonly used on the Java
  1128     platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/javase/8/docs/api/java/util/regex/Pattern.html\<close>\<close>
  1129     This may serve as an additional visual filter of the result.
  1130 
  1131     \<^item> The \<^emph>\<open>Zoom\<close> box controls the font size of the output area.
  1132 
  1133   All query operations are asynchronous: there is no need to wait for the
  1134   evaluation of the document for the query context, nor for the query
  1135   operation itself. Query output may be detached as independent \<^emph>\<open>Info\<close>
  1136   window, using a menu operation of the dockable window manager. The printed
  1137   result usually provides sufficient clues about the original query, with some
  1138   hyperlink to its context (via markup of its head line).
  1139 \<close>
  1140 
  1141 
  1142 subsection \<open>Find theorems\<close>
  1143 
  1144 text \<open>
  1145   The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Theorems\<close> mode retrieves facts from the theory
  1146   or proof context matching all of given criteria in the \<^emph>\<open>Find\<close> text field. A
  1147   single criterium has the following syntax:
  1148 
  1149   @{rail \<open>
  1150     ('-'?) ('name' ':' @{syntax name} | 'intro' | 'elim' | 'dest' |
  1151       'solves' | 'simp' ':' @{syntax term} | @{syntax term})
  1152   \<close>}
  1153 
  1154   See also the Isar command @{command_ref find_theorems} in @{cite
  1155   "isabelle-isar-ref"}.
  1156 \<close>
  1157 
  1158 
  1159 subsection \<open>Find constants\<close>
  1160 
  1161 text \<open>
  1162   The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Constants\<close> mode prints all constants whose type
  1163   meets all of the given criteria in the \<^emph>\<open>Find\<close> text field. A single
  1164   criterium has the following syntax:
  1165 
  1166   @{rail \<open>
  1167     ('-'?)
  1168       ('name' ':' @{syntax name} | 'strict' ':' @{syntax type} | @{syntax type})
  1169   \<close>}
  1170 
  1171   See also the Isar command @{command_ref find_consts} in @{cite
  1172   "isabelle-isar-ref"}.
  1173 \<close>
  1174 
  1175 
  1176 subsection \<open>Print context\<close>
  1177 
  1178 text \<open>
  1179   The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Print Context\<close> mode prints information from the
  1180   theory or proof context, or proof state. See also the Isar commands
  1181   @{command_ref print_context}, @{command_ref print_cases}, @{command_ref
  1182   print_term_bindings}, @{command_ref print_theorems}, described in @{cite
  1183   "isabelle-isar-ref"}.
  1184 \<close>
  1185 
  1186 
  1187 section \<open>Tooltips and hyperlinks \label{sec:tooltips-hyperlinks}\<close>
  1188 
  1189 text \<open>
  1190   Formally processed text (prover input or output) contains rich markup that
  1191   can be explored by using the \<^verbatim>\<open>CONTROL\<close> modifier key on Linux and Windows,
  1192   or \<^verbatim>\<open>COMMAND\<close> on Mac OS X. Hovering with the mouse while the modifier is
  1193   pressed reveals a \<^emph>\<open>tooltip\<close> (grey box over the text with a yellow popup)
  1194   and/or a \<^emph>\<open>hyperlink\<close> (black rectangle over the text with change of mouse
  1195   pointer); see also \figref{fig:tooltip}.
  1196 
  1197   \begin{figure}[!htb]
  1198   \begin{center}
  1199   \includegraphics[scale=0.5]{popup1}
  1200   \end{center}
  1201   \caption{Tooltip and hyperlink for some formal entity}
  1202   \label{fig:tooltip}
  1203   \end{figure}
  1204 
  1205   Tooltip popups use the same rendering technology as the main text area, and
  1206   further tooltips and/or hyperlinks may be exposed recursively by the same
  1207   mechanism; see \figref{fig:nested-tooltips}.
  1208 
  1209   \begin{figure}[!htb]
  1210   \begin{center}
  1211   \includegraphics[scale=0.5]{popup2}
  1212   \end{center}
  1213   \caption{Nested tooltips over formal entities}
  1214   \label{fig:nested-tooltips}
  1215   \end{figure}
  1216 
  1217   The tooltip popup window provides some controls to \<^emph>\<open>close\<close> or \<^emph>\<open>detach\<close> the
  1218   window, turning it into a separate \<^emph>\<open>Info\<close> window managed by jEdit. The
  1219   \<^verbatim>\<open>ESCAPE\<close> key closes \<^emph>\<open>all\<close> popups, which is particularly relevant when
  1220   nested tooltips are stacking up.
  1221 
  1222   \<^medskip>
  1223   A black rectangle in the text indicates a hyperlink that may be followed by
  1224   a mouse click (while the \<^verbatim>\<open>CONTROL\<close> or \<^verbatim>\<open>COMMAND\<close> modifier key is still
  1225   pressed). Such jumps to other text locations are recorded by the
  1226   \<^emph>\<open>Navigator\<close> plugin, which is bundled with Isabelle/jEdit and enabled by
  1227   default. There are usually navigation arrows in the main jEdit toolbar.
  1228 
  1229   Note that the link target may be a file that is itself not subject to formal
  1230   document processing of the editor session and thus prevents further
  1231   exploration: the chain of hyperlinks may end in some source file of the
  1232   underlying logic image, or within the ML bootstrap sources of Isabelle/Pure.
  1233 \<close>
  1234 
  1235 
  1236 section \<open>Formal scopes and semantic selection\<close>
  1237 
  1238 text \<open>
  1239   Formal entities are semantically annotated in the source text as explained
  1240   in \secref{sec:tooltips-hyperlinks}. A \<^emph>\<open>formal scope\<close> consists of the
  1241   defining position with all its referencing positions. This correspondence is
  1242   highlighted in the text according to the cursor position, see also
  1243   \figref{fig:scope1}. Here the referencing positions are rendered with an
  1244   additional border, in reminiscence to a hyperlink: clicking there moves the
  1245   cursor to the original defining position.
  1246 
  1247   \begin{figure}[!htb]
  1248   \begin{center}
  1249   \includegraphics[scale=0.5]{scope1}
  1250   \end{center}
  1251   \caption{Scope of formal entity: defining vs.\ referencing positions}
  1252   \label{fig:scope1}
  1253   \end{figure}
  1254 
  1255   The action @{action_def "isabelle.select-entity"} (shortcut \<^verbatim>\<open>CS+ENTER\<close>)
  1256   supports semantic selection of all occurrences of the formal entity at the
  1257   caret position. This facilitates systematic renaming, using regular jEdit
  1258   editing of a multi-selection, see also \figref{fig:scope2}.
  1259 
  1260   \begin{figure}[!htb]
  1261   \begin{center}
  1262   \includegraphics[scale=0.5]{scope2}
  1263   \end{center}
  1264   \caption{The result of semantic selection and systematic renaming}
  1265   \label{fig:scope2}
  1266   \end{figure}
  1267 \<close>
  1268 
  1269 
  1270 section \<open>Completion \label{sec:completion}\<close>
  1271 
  1272 text \<open>
  1273   Smart completion of partial input is the IDE functionality \<^emph>\<open>par
  1274   excellance\<close>. Isabelle/jEdit combines several sources of information to
  1275   achieve that. Despite its complexity, it should be possible to get some idea
  1276   how completion works by experimentation, based on the overview of completion
  1277   varieties in \secref{sec:completion-varieties}. The remaining subsections
  1278   explain concepts around completion more systematically.
  1279 
  1280   \<^medskip>
  1281   \<^emph>\<open>Explicit completion\<close> is triggered by the action @{action_ref
  1282   "isabelle.complete"}, which is bound to the keyboard shortcut \<^verbatim>\<open>C+b\<close>, and
  1283   thus overrides the jEdit default for @{action_ref "complete-word"}.
  1284 
  1285   \<^emph>\<open>Implicit completion\<close> hooks into the regular keyboard input stream of the
  1286   editor, with some event filtering and optional delays.
  1287 
  1288   \<^medskip>
  1289   Completion options may be configured in \<^emph>\<open>Plugin Options~/ Isabelle~/
  1290   General~/ Completion\<close>. These are explained in further detail below, whenever
  1291   relevant. There is also a summary of options in
  1292   \secref{sec:completion-options}.
  1293 
  1294   The asynchronous nature of PIDE interaction means that information from the
  1295   prover is delayed --- at least by a full round-trip of the document update
  1296   protocol. The default options already take this into account, with a
  1297   sufficiently long completion delay to speculate on the availability of all
  1298   relevant information from the editor and the prover, before completing text
  1299   immediately or producing a popup. Although there is an inherent danger of
  1300   non-deterministic behaviour due to such real-time parameters, the general
  1301   completion policy aims at determined results as far as possible.
  1302 \<close>
  1303 
  1304 
  1305 subsection \<open>Varieties of completion \label{sec:completion-varieties}\<close>
  1306 
  1307 subsubsection \<open>Built-in templates\<close>
  1308 
  1309 text \<open>
  1310   Isabelle is ultimately a framework of nested sub-languages of different
  1311   kinds and purposes. The completion mechanism supports this by the following
  1312   built-in templates:
  1313 
  1314     \<^descr> \<^verbatim>\<open>`\<close> (single ASCII back-quote) or \<^verbatim>\<open>"\<close> (double ASCII quote) support
  1315     \<^emph>\<open>quotations\<close> via text cartouches. There are three selections, which are
  1316     always presented in the same order and do not depend on any context
  1317     information. The default choice produces a template ``\<open>\<open>\<box>\<close>\<close>'', where the
  1318     box indicates the cursor position after insertion; the other choices help
  1319     to repair the block structure of unbalanced text cartouches.
  1320 
  1321     \<^descr> \<^verbatim>\<open>@{\<close> is completed to the template ``\<open>@{\<box>}\<close>'', where the box indicates
  1322     the cursor position after insertion. Here it is convenient to use the
  1323     wildcard ``\<^verbatim>\<open>__\<close>'' or a more specific name prefix to let semantic
  1324     completion of name-space entries propose antiquotation names.
  1325 
  1326   With some practice, input of quoted sub-languages and antiquotations of
  1327   embedded languages should work fluently. Note that national keyboard layouts
  1328   might cause problems with back-quote as dead key, but double quote can be
  1329   used instead.
  1330 \<close>
  1331 
  1332 
  1333 subsubsection \<open>Syntax keywords\<close>
  1334 
  1335 text \<open>
  1336   Syntax completion tables are determined statically from the keywords of the
  1337   ``outer syntax'' of the underlying edit mode: for theory files this is the
  1338   syntax of Isar commands according to the cumulative theory imports.
  1339 
  1340   Keywords are usually plain words, which means the completion mechanism only
  1341   inserts them directly into the text for explicit completion
  1342   (\secref{sec:completion-input}), but produces a popup
  1343   (\secref{sec:completion-popup}) otherwise.
  1344 
  1345   At the point where outer syntax keywords are defined, it is possible to
  1346   specify an alternative replacement string to be inserted instead of the
  1347   keyword itself. An empty string means to suppress the keyword altogether,
  1348   which is occasionally useful to avoid confusion, e.g.\ the rare keyword
  1349   @{command simproc_setup} vs.\ the frequent name-space entry \<open>simp\<close>.
  1350 \<close>
  1351 
  1352 
  1353 subsubsection \<open>Isabelle symbols\<close>
  1354 
  1355 text \<open>
  1356   The completion tables for Isabelle symbols (\secref{sec:symbols}) are
  1357   determined statically from \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and @{path
  1358   "$ISABELLE_HOME_USER/etc/symbols"} for each symbol specification as follows:
  1359 
  1360   \<^medskip>
  1361   \begin{tabular}{ll}
  1362   \<^bold>\<open>completion entry\<close> & \<^bold>\<open>example\<close> \\\hline
  1363   literal symbol & \<^verbatim>\<open>\<forall>\<close> \\
  1364   symbol name with backslash & \<^verbatim>\<open>\\<close>\<^verbatim>\<open>forall\<close> \\
  1365   symbol abbreviation & \<^verbatim>\<open>ALL\<close> or \<^verbatim>\<open>!\<close> \\
  1366   \end{tabular}
  1367   \<^medskip>
  1368 
  1369   When inserted into the text, the above examples all produce the same Unicode
  1370   rendering \<open>\<forall>\<close> of the underlying symbol \<^verbatim>\<open>\<forall>\<close>.
  1371 
  1372   A symbol abbreviation that is a plain word, like \<^verbatim>\<open>ALL\<close>, is treated like a
  1373   syntax keyword. Non-word abbreviations like \<^verbatim>\<open>-->\<close> are inserted more
  1374   aggressively, except for single-character abbreviations like \<^verbatim>\<open>!\<close> above.
  1375 
  1376   Completion via abbreviations like \<^verbatim>\<open>ALL\<close> or \<^verbatim>\<open>-->\<close> depends on the semantic
  1377   language context (\secref{sec:completion-context}). In contrast, backslash
  1378   sequences like \<^verbatim>\<open>\forall\<close> \<^verbatim>\<open>\<forall>\<close> are always possible, but require
  1379   additional interaction to confirm (via popup).
  1380 
  1381   The latter is important in ambiguous situations, e.g.\ for Isabelle document
  1382   source, which may contain formal symbols or informal {\LaTeX} macros.
  1383   Backslash sequences also help when input is broken, and thus escapes its
  1384   normal semantic context: e.g.\ antiquotations or string literals in ML,
  1385   which do not allow arbitrary backslash sequences.
  1386 \<close>
  1387 
  1388 
  1389 subsubsection \<open>User-defined abbreviations\<close>
  1390 
  1391 text \<open>
  1392   The theory header syntax supports abbreviations via the \<^theory_text>\<open>abbrevs\<close> keyword
  1393   @{cite "isabelle-isar-ref"}. This is a slight generalization of built-in
  1394   templates and abbreviations for Isabelle symbols, as explained above.
  1395   Examples may be found in the Isabelle sources, by searching for
  1396   ``\<^verbatim>\<open>abbrevs\<close>'' in \<^verbatim>\<open>*.thy\<close> files.
  1397 
  1398   The \<^emph>\<open>Symbols\<close> panel shows the abbreviations that are available in the
  1399   current theory buffer (according to its \<^theory_text>\<open>imports\<close>) in the \<^verbatim>\<open>Abbrevs\<close> tab.
  1400 \<close>
  1401 
  1402 
  1403 subsubsection \<open>Name-space entries\<close>
  1404 
  1405 text \<open>
  1406   This is genuine semantic completion, using information from the prover, so
  1407   it requires some delay. A \<^emph>\<open>failed name-space lookup\<close> produces an error
  1408   message that is annotated with a list of alternative names that are legal.
  1409   The list of results is truncated according to the system option
  1410   @{system_option_ref completion_limit}. The completion mechanism takes this
  1411   into account when collecting information on the prover side.
  1412 
  1413   Already recognized names are \<^emph>\<open>not\<close> completed further, but completion may be
  1414   extended by appending a suffix of underscores. This provokes a failed
  1415   lookup, and another completion attempt while ignoring the underscores. For
  1416   example, in a name space where \<^verbatim>\<open>foo\<close> and \<^verbatim>\<open>foobar\<close> are known, the input
  1417   \<^verbatim>\<open>foo\<close> remains unchanged, but \<^verbatim>\<open>foo_\<close> may be completed to \<^verbatim>\<open>foo\<close> or
  1418   \<^verbatim>\<open>foobar\<close>.
  1419 
  1420   The special identifier ``\<^verbatim>\<open>__\<close>'' serves as a wild-card for arbitrary
  1421   completion: it exposes the name-space content to the completion mechanism
  1422   (truncated according to @{system_option completion_limit}). This is
  1423   occasionally useful to explore an unknown name-space, e.g.\ in some
  1424   template.
  1425 \<close>
  1426 
  1427 
  1428 subsubsection \<open>File-system paths\<close>
  1429 
  1430 text \<open>
  1431   Depending on prover markup about file-system paths in the source text, e.g.\
  1432   for the argument of a load command (\secref{sec:aux-files}), the completion
  1433   mechanism explores the directory content and offers the result as completion
  1434   popup. Relative path specifications are understood wrt.\ the \<^emph>\<open>master
  1435   directory\<close> of the document node (\secref{sec:buffer-node}) of the enclosing
  1436   editor buffer; this requires a proper theory, not an auxiliary file.
  1437 
  1438   A suffix of slashes may be used to continue the exploration of an already
  1439   recognized directory name.
  1440 \<close>
  1441 
  1442 
  1443 subsubsection \<open>Spell-checking\<close>
  1444 
  1445 text \<open>
  1446   The spell-checker combines semantic markup from the prover (regions of plain
  1447   words) with static dictionaries (word lists) that are known to the editor.
  1448 
  1449   Unknown words are underlined in the text, using @{system_option_ref
  1450   spell_checker_color} (blue by default). This is not an error, but a hint to
  1451   the user that some action may be taken. The jEdit context menu provides
  1452   various actions, as far as applicable:
  1453 
  1454   \<^medskip>
  1455   \begin{tabular}{l}
  1456   @{action_ref "isabelle.complete-word"} \\
  1457   @{action_ref "isabelle.exclude-word"} \\
  1458   @{action_ref "isabelle.exclude-word-permanently"} \\
  1459   @{action_ref "isabelle.include-word"} \\
  1460   @{action_ref "isabelle.include-word-permanently"} \\
  1461   \end{tabular}
  1462   \<^medskip>
  1463 
  1464   Instead of the specific @{action_ref "isabelle.complete-word"}, it is also
  1465   possible to use the generic @{action_ref "isabelle.complete"} with its
  1466   default keyboard shortcut \<^verbatim>\<open>C+b\<close>.
  1467 
  1468   \<^medskip>
  1469   Dictionary lookup uses some educated guesses about lower-case, upper-case,
  1470   and capitalized words. This is oriented on common use in English, where this
  1471   aspect is not decisive for proper spelling (in contrast to German, for
  1472   example).
  1473 \<close>
  1474 
  1475 
  1476 subsection \<open>Semantic completion context \label{sec:completion-context}\<close>
  1477 
  1478 text \<open>
  1479   Completion depends on a semantic context that is provided by the prover,
  1480   although with some delay, because at least a full PIDE protocol round-trip
  1481   is required. Until that information becomes available in the PIDE
  1482   document-model, the default context is given by the outer syntax of the
  1483   editor mode (see also \secref{sec:buffer-node}).
  1484 
  1485   The semantic \<^emph>\<open>language context\<close> provides information about nested
  1486   sub-languages of Isabelle: keywords are only completed for outer syntax, and
  1487   antiquotations for languages that support them. Symbol abbreviations only
  1488   work for specific sub-languages: e.g.\ ``\<^verbatim>\<open>=>\<close>'' is \<^emph>\<open>not\<close> completed in
  1489   regular ML source, but is completed within ML strings, comments,
  1490   antiquotations. Backslash representations of symbols like ``\<^verbatim>\<open>\foobar\<close>'' or
  1491   ``\<^verbatim>\<open>\<foobar>\<close>'' work in any context --- after additional confirmation.
  1492 
  1493   The prover may produce \<^emph>\<open>no completion\<close> markup in exceptional situations, to
  1494   tell that some language keywords should be excluded from further completion
  1495   attempts. For example, ``\<^verbatim>\<open>:\<close>'' within accepted Isar syntax looses its
  1496   meaning as abbreviation for symbol ``\<open>\<in>\<close>''.
  1497 \<close>
  1498 
  1499 
  1500 subsection \<open>Input events \label{sec:completion-input}\<close>
  1501 
  1502 text \<open>
  1503   Completion is triggered by certain events produced by the user, with
  1504   optional delay after keyboard input according to @{system_option
  1505   jedit_completion_delay}.
  1506 
  1507   \<^descr>[Explicit completion] works via action @{action_ref "isabelle.complete"}
  1508   with keyboard shortcut \<^verbatim>\<open>C+b\<close>. This overrides the shortcut for @{action_ref
  1509   "complete-word"} in jEdit, but it is possible to restore the original jEdit
  1510   keyboard mapping of @{action "complete-word"} via \<^emph>\<open>Global Options~/
  1511   Shortcuts\<close> and invent a different one for @{action "isabelle.complete"}.
  1512 
  1513   \<^descr>[Explicit spell-checker completion] works via @{action_ref
  1514   "isabelle.complete-word"}, which is exposed in the jEdit context menu, if
  1515   the mouse points to a word that the spell-checker can complete.
  1516 
  1517   \<^descr>[Implicit completion] works via regular keyboard input of the editor. It
  1518   depends on further side-conditions:
  1519 
  1520     \<^enum> The system option @{system_option_ref jedit_completion} needs to be
  1521     enabled (default).
  1522 
  1523     \<^enum> Completion of syntax keywords requires at least 3 relevant characters in
  1524     the text.
  1525 
  1526     \<^enum> The system option @{system_option_ref jedit_completion_delay} determines
  1527     an additional delay (0.5 by default), before opening a completion popup.
  1528     The delay gives the prover a chance to provide semantic completion
  1529     information, notably the context (\secref{sec:completion-context}).
  1530 
  1531     \<^enum> The system option @{system_option_ref jedit_completion_immediate}
  1532     (enabled by default) controls whether replacement text should be inserted
  1533     immediately without popup, regardless of @{system_option
  1534     jedit_completion_delay}. This aggressive mode of completion is restricted
  1535     to symbol abbreviations that are not plain words (\secref{sec:symbols}).
  1536 
  1537     \<^enum> Completion of symbol abbreviations with only one relevant character in
  1538     the text always enforces an explicit popup, regardless of
  1539     @{system_option_ref jedit_completion_immediate}.
  1540 \<close>
  1541 
  1542 
  1543 subsection \<open>Completion popup \label{sec:completion-popup}\<close>
  1544 
  1545 text \<open>
  1546   A \<^emph>\<open>completion popup\<close> is a minimally invasive GUI component over the text
  1547   area that offers a selection of completion items to be inserted into the
  1548   text, e.g.\ by mouse clicks. Items are sorted dynamically, according to the
  1549   frequency of selection, with persistent history. The popup may interpret
  1550   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>,
  1551   \<^verbatim>\<open>PAGE_DOWN\<close>, but all other key events are passed to the underlying text
  1552   area. This allows to ignore unwanted completions most of the time and
  1553   continue typing quickly. Thus the popup serves as a mechanism of
  1554   confirmation of proposed items, while the default is to continue without
  1555   completion.
  1556 
  1557   The meaning of special keys is as follows:
  1558 
  1559   \<^medskip>
  1560   \begin{tabular}{ll}
  1561   \<^bold>\<open>key\<close> & \<^bold>\<open>action\<close> \\\hline
  1562   \<^verbatim>\<open>ENTER\<close> & select completion (if @{system_option jedit_completion_select_enter}) \\
  1563   \<^verbatim>\<open>TAB\<close> & select completion (if @{system_option jedit_completion_select_tab}) \\
  1564   \<^verbatim>\<open>ESCAPE\<close> & dismiss popup \\
  1565   \<^verbatim>\<open>UP\<close> & move up one item \\
  1566   \<^verbatim>\<open>DOWN\<close> & move down one item \\
  1567   \<^verbatim>\<open>PAGE_UP\<close> & move up one page of items \\
  1568   \<^verbatim>\<open>PAGE_DOWN\<close> & move down one page of items \\
  1569   \end{tabular}
  1570   \<^medskip>
  1571 
  1572   Movement within the popup is only active for multiple items. Otherwise the
  1573   corresponding key event retains its standard meaning within the underlying
  1574   text area.
  1575 \<close>
  1576 
  1577 
  1578 subsection \<open>Insertion \label{sec:completion-insert}\<close>
  1579 
  1580 text \<open>
  1581   Completion may first propose replacements to be selected (via a popup), or
  1582   replace text immediately in certain situations and depending on certain
  1583   options like @{system_option jedit_completion_immediate}. In any case,
  1584   insertion works uniformly, by imitating normal jEdit text insertion,
  1585   depending on the state of the \<^emph>\<open>text selection\<close>. Isabelle/jEdit tries to
  1586   accommodate the most common forms of advanced selections in jEdit, but not
  1587   all combinations make sense. At least the following important cases are
  1588   well-defined:
  1589 
  1590     \<^descr>[No selection.] The original is removed and the replacement inserted,
  1591     depending on the caret position.
  1592 
  1593     \<^descr>[Rectangular selection of zero width.] This special case is treated by
  1594     jEdit as ``tall caret'' and insertion of completion imitates its normal
  1595     behaviour: separate copies of the replacement are inserted for each line
  1596     of the selection.
  1597 
  1598     \<^descr>[Other rectangular selection or multiple selections.] Here the original
  1599     is removed and the replacement is inserted for each line (or segment) of
  1600     the selection.
  1601 
  1602   Support for multiple selections is particularly useful for \<^emph>\<open>HyperSearch\<close>:
  1603   clicking on one of the items in the \<^emph>\<open>HyperSearch Results\<close> window makes
  1604   jEdit select all its occurrences in the corresponding line of text. Then
  1605   explicit completion can be invoked via \<^verbatim>\<open>C+b\<close>, e.g.\ to replace occurrences
  1606   of \<^verbatim>\<open>-->\<close> by \<open>\<longrightarrow>\<close>.
  1607 
  1608   \<^medskip>
  1609   Insertion works by removing and inserting pieces of text from the buffer.
  1610   This counts as one atomic operation on the jEdit history. Thus unintended
  1611   completions may be reverted by the regular @{action undo} action of jEdit.
  1612   According to normal jEdit policies, the recovered text after @{action undo}
  1613   is selected: \<^verbatim>\<open>ESCAPE\<close> is required to reset the selection and to continue
  1614   typing more text.
  1615 \<close>
  1616 
  1617 
  1618 subsection \<open>Options \label{sec:completion-options}\<close>
  1619 
  1620 text \<open>
  1621   This is a summary of Isabelle/Scala system options that are relevant for
  1622   completion. They may be configured in \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>
  1623   as usual.
  1624 
  1625   \<^item> @{system_option_def completion_limit} specifies the maximum number of
  1626   items for various semantic completion operations (name-space entries etc.)
  1627 
  1628   \<^item> @{system_option_def jedit_completion} guards implicit completion via
  1629   regular jEdit key events (\secref{sec:completion-input}): it allows to
  1630   disable implicit completion altogether.
  1631 
  1632   \<^item> @{system_option_def jedit_completion_select_enter} and @{system_option_def
  1633   jedit_completion_select_tab} enable keys to select a completion item from
  1634   the popup (\secref{sec:completion-popup}). Note that a regular mouse click
  1635   on the list of items is always possible.
  1636 
  1637   \<^item> @{system_option_def jedit_completion_context} specifies whether the
  1638   language context provided by the prover should be used at all. Disabling
  1639   that option makes completion less ``semantic''. Note that incomplete or
  1640   severely broken input may cause some disagreement of the prover and the user
  1641   about the intended language context.
  1642 
  1643   \<^item> @{system_option_def jedit_completion_delay} and @{system_option_def
  1644   jedit_completion_immediate} determine the handling of keyboard events for
  1645   implicit completion (\secref{sec:completion-input}).
  1646 
  1647   A @{system_option jedit_completion_delay}~\<^verbatim>\<open>> 0\<close> postpones the processing of
  1648   key events, until after the user has stopped typing for the given time span,
  1649   but @{system_option jedit_completion_immediate}~\<^verbatim>\<open>= true\<close> means that
  1650   abbreviations of Isabelle symbols are handled nonetheless.
  1651 
  1652   \<^item> @{system_option_def completion_path_ignore} specifies ``glob''
  1653   patterns to ignore in file-system path completion (separated by colons),
  1654   e.g.\ backup files ending with tilde.
  1655 
  1656   \<^item> @{system_option_def spell_checker} is a global guard for all spell-checker
  1657   operations: it allows to disable that mechanism altogether.
  1658 
  1659   \<^item> @{system_option_def spell_checker_dictionary} determines the current
  1660   dictionary, taken from the colon-separated list in the settings variable
  1661   @{setting_def JORTHO_DICTIONARIES}. There are jEdit actions to specify local
  1662   updates to a dictionary, by including or excluding words. The result of
  1663   permanent dictionary updates is stored in the directory @{path
  1664   "$ISABELLE_HOME_USER/dictionaries"}, in a separate file for each dictionary.
  1665 
  1666   \<^item> @{system_option_def spell_checker_elements} specifies a comma-separated
  1667   list of markup elements that delimit words in the source that is subject to
  1668   spell-checking, including various forms of comments.
  1669 \<close>
  1670 
  1671 
  1672 section \<open>Automatically tried tools \label{sec:auto-tools}\<close>
  1673 
  1674 text \<open>
  1675   Continuous document processing works asynchronously in the background.
  1676   Visible document source that has been evaluated may get augmented by
  1677   additional results of \<^emph>\<open>asynchronous print functions\<close>. An example for that
  1678   is proof state output, if that is enabled in the Output panel
  1679   (\secref{sec:output}). More heavy-weight print functions may be applied as
  1680   well, e.g.\ to prove or disprove parts of the formal text by other means.
  1681 
  1682   Isabelle/HOL provides various automatically tried tools that operate on
  1683   outermost goal statements (e.g.\ @{command lemma}, @{command theorem}),
  1684   independently of the state of the current proof attempt. They work
  1685   implicitly without any arguments. Results are output as \<^emph>\<open>information
  1686   messages\<close>, which are indicated in the text area by blue squiggles and a blue
  1687   information sign in the gutter (see \figref{fig:auto-tools}). The message
  1688   content may be shown as for other output (see also \secref{sec:output}).
  1689   Some tools produce output with \<^emph>\<open>sendback\<close> markup, which means that clicking
  1690   on certain parts of the text inserts that into the source in the proper
  1691   place.
  1692 
  1693   \begin{figure}[!htb]
  1694   \begin{center}
  1695   \includegraphics[scale=0.333]{auto-tools}
  1696   \end{center}
  1697   \caption{Result of automatically tried tools}
  1698   \label{fig:auto-tools}
  1699   \end{figure}
  1700 
  1701   \<^medskip>
  1702   The following Isabelle system options control the behavior of automatically
  1703   tried tools (see also the jEdit dialog window \<^emph>\<open>Plugin Options~/ Isabelle~/
  1704   General~/ Automatically tried tools\<close>):
  1705 
  1706   \<^item> @{system_option_ref auto_methods} controls automatic use of a combination
  1707   of standard proof methods (@{method auto}, @{method simp}, @{method blast},
  1708   etc.). This corresponds to the Isar command @{command_ref "try0"} @{cite
  1709   "isabelle-isar-ref"}.
  1710 
  1711   The tool is disabled by default, since unparameterized invocation of
  1712   standard proof methods often consumes substantial CPU resources without
  1713   leading to success.
  1714 
  1715   \<^item> @{system_option_ref auto_nitpick} controls a slightly reduced version of
  1716   @{command_ref nitpick}, which tests for counterexamples using first-order
  1717   relational logic. See also the Nitpick manual @{cite "isabelle-nitpick"}.
  1718 
  1719   This tool is disabled by default, due to the extra overhead of invoking an
  1720   external Java process for each attempt to disprove a subgoal.
  1721 
  1722   \<^item> @{system_option_ref auto_quickcheck} controls automatic use of
  1723   @{command_ref quickcheck}, which tests for counterexamples using a series of
  1724   assignments for free variables of a subgoal.
  1725 
  1726   This tool is \<^emph>\<open>enabled\<close> by default. It requires little overhead, but is a
  1727   bit weaker than @{command nitpick}.
  1728 
  1729   \<^item> @{system_option_ref auto_sledgehammer} controls a significantly reduced
  1730   version of @{command_ref sledgehammer}, which attempts to prove a subgoal
  1731   using external automatic provers. See also the Sledgehammer manual @{cite
  1732   "isabelle-sledgehammer"}.
  1733 
  1734   This tool is disabled by default, due to the relatively heavy nature of
  1735   Sledgehammer.
  1736 
  1737   \<^item> @{system_option_ref auto_solve_direct} controls automatic use of
  1738   @{command_ref solve_direct}, which checks whether the current subgoals can
  1739   be solved directly by an existing theorem. This also helps to detect
  1740   duplicate lemmas.
  1741 
  1742   This tool is \<^emph>\<open>enabled\<close> by default.
  1743 
  1744 
  1745   Invocation of automatically tried tools is subject to some global policies
  1746   of parallel execution, which may be configured as follows:
  1747 
  1748   \<^item> @{system_option_ref auto_time_limit} (default 2.0) determines the timeout
  1749   (in seconds) for each tool execution.
  1750 
  1751   \<^item> @{system_option_ref auto_time_start} (default 1.0) determines the start
  1752   delay (in seconds) for automatically tried tools, after the main command
  1753   evaluation is finished.
  1754 
  1755 
  1756   Each tool is submitted independently to the pool of parallel execution tasks
  1757   in Isabelle/ML, using hardwired priorities according to its relative
  1758   ``heaviness''. The main stages of evaluation and printing of proof states
  1759   take precedence, but an already running tool is not canceled and may thus
  1760   reduce reactivity of proof document processing.
  1761 
  1762   Users should experiment how the available CPU resources (number of cores)
  1763   are best invested to get additional feedback from prover in the background,
  1764   by using a selection of weaker or stronger tools.
  1765 \<close>
  1766 
  1767 
  1768 section \<open>Sledgehammer \label{sec:sledgehammer}\<close>
  1769 
  1770 text \<open>
  1771   The \<^emph>\<open>Sledgehammer\<close> panel (\figref{fig:sledgehammer}) provides a view on
  1772   some independent execution of the Isar command @{command_ref sledgehammer},
  1773   with process indicator (spinning wheel) and GUI elements for important
  1774   Sledgehammer arguments and options. Any number of Sledgehammer panels may be
  1775   active, according to the standard policies of Dockable Window Management in
  1776   jEdit. Closing such windows also cancels the corresponding prover tasks.
  1777 
  1778   \begin{figure}[!htb]
  1779   \begin{center}
  1780   \includegraphics[scale=0.333]{sledgehammer}
  1781   \end{center}
  1782   \caption{An instance of the Sledgehammer panel}
  1783   \label{fig:sledgehammer}
  1784   \end{figure}
  1785 
  1786   The \<^emph>\<open>Apply\<close> button attaches a fresh invocation of @{command sledgehammer}
  1787   to the command where the cursor is pointing in the text --- this should be
  1788   some pending proof problem. Further buttons like \<^emph>\<open>Cancel\<close> and \<^emph>\<open>Locate\<close>
  1789   help to manage the running process.
  1790 
  1791   Results appear incrementally in the output window of the panel. Proposed
  1792   proof snippets are marked-up as \<^emph>\<open>sendback\<close>, which means a single mouse
  1793   click inserts the text into a suitable place of the original source. Some
  1794   manual editing may be required nonetheless, say to remove earlier proof
  1795   attempts.
  1796 \<close>
  1797 
  1798 
  1799 chapter \<open>Isabelle document preparation\<close>
  1800 
  1801 text \<open>
  1802   The ultimate purpose of Isabelle is to produce nicely rendered documents
  1803   with the Isabelle document preparation system, which is based on {\LaTeX};
  1804   see also @{cite "isabelle-system" and "isabelle-isar-ref"}. Isabelle/jEdit
  1805   provides some additional support for document editing.
  1806 \<close>
  1807 
  1808 
  1809 section \<open>Document outline\<close>
  1810 
  1811 text \<open>
  1812   Theory sources may contain document markup commands, such as @{command_ref
  1813   chapter}, @{command_ref section}, @{command subsection}. The Isabelle
  1814   SideKick parser (\secref{sec:sidekick}) represents this document outline as
  1815   structured tree view, with formal statements and proofs nested inside; see
  1816   \figref{fig:sidekick-document}.
  1817 
  1818   \begin{figure}[!htb]
  1819   \begin{center}
  1820   \includegraphics[scale=0.333]{sidekick-document}
  1821   \end{center}
  1822   \caption{Isabelle document outline via SideKick tree view}
  1823   \label{fig:sidekick-document}
  1824   \end{figure}
  1825 
  1826   It is also possible to use text folding according to this structure, by
  1827   adjusting \<^emph>\<open>Utilities / Buffer Options / Folding mode\<close> of jEdit. The default
  1828   mode \<^verbatim>\<open>isabelle\<close> uses the structure of formal definitions, statements, and
  1829   proofs. The alternative mode \<^verbatim>\<open>sidekick\<close> uses the document structure of the
  1830   SideKick parser, as explained above.
  1831 \<close>
  1832 
  1833 
  1834 section \<open>Markdown structure\<close>
  1835 
  1836 text \<open>
  1837   Document text is internally structured in paragraphs and nested lists, using
  1838   notation that is similar to Markdown\<^footnote>\<open>\<^url>\<open>http://commonmark.org\<close>\<close>. There are
  1839   special control symbols for items of different kinds of lists, corresponding
  1840   to \<^verbatim>\<open>itemize\<close>, \<^verbatim>\<open>enumerate\<close>, \<^verbatim>\<open>description\<close> in {\LaTeX}. This is illustrated
  1841   in for \<^verbatim>\<open>itemize\<close> in \figref{fig:markdown-document}.
  1842 
  1843   \begin{figure}[!htb]
  1844   \begin{center}
  1845   \includegraphics[scale=0.333]{markdown-document}
  1846   \end{center}
  1847   \caption{Markdown structure within document text}
  1848   \label{fig:markdown-document}
  1849   \end{figure}
  1850 
  1851   Items take colour according to the depth of nested lists. This helps to
  1852   explore the implicit rules for list structure interactively. There is also
  1853   markup for individual paragraphs in the text: it may be explored via mouse
  1854   hovering with \<^verbatim>\<open>CONTROL\<close> / \<^verbatim>\<open>COMMAND\<close> as usual
  1855   (\secref{sec:tooltips-hyperlinks}).
  1856 \<close>
  1857 
  1858 
  1859 section \<open>Citations and Bib{\TeX} entries \label{sec:bibtex}\<close>
  1860 
  1861 text \<open>
  1862   Citations are managed by {\LaTeX} and Bib{\TeX} in \<^verbatim>\<open>.bib\<close> files. The
  1863   Isabelle session build process and the @{tool latex} tool @{cite
  1864   "isabelle-system"} are smart enough to assemble the result, based on the
  1865   session directory layout.
  1866 
  1867   The document antiquotation \<open>@{cite}\<close> is described in @{cite
  1868   "isabelle-isar-ref"}. Within the Prover IDE it provides semantic markup for
  1869   tooltips, hyperlinks, and completion for Bib{\TeX} database entries.
  1870   Isabelle/jEdit does \<^emph>\<open>not\<close> know about the actual Bib{\TeX} environment used
  1871   in {\LaTeX} batch-mode, but it can take citations from those \<^verbatim>\<open>.bib\<close> files
  1872   that happen to be open in the editor; see \figref{fig:cite-completion}.
  1873 
  1874   \begin{figure}[!htb]
  1875   \begin{center}
  1876   \includegraphics[scale=0.333]{cite-completion}
  1877   \end{center}
  1878   \caption{Semantic completion of citations from open Bib{\TeX} files}
  1879   \label{fig:cite-completion}
  1880   \end{figure}
  1881 
  1882   Isabelle/jEdit also provides some support for editing \<^verbatim>\<open>.bib\<close> files
  1883   themselves. There is syntax highlighting based on entry types (according to
  1884   standard Bib{\TeX} styles), a context-menu to compose entries
  1885   systematically, and a SideKick tree view of the overall content; see
  1886   \figref{fig:bibtex-mode}.
  1887 
  1888   \begin{figure}[!htb]
  1889   \begin{center}
  1890   \includegraphics[scale=0.333]{bibtex-mode}
  1891   \end{center}
  1892   \caption{Bib{\TeX} mode with context menu and SideKick tree view}
  1893   \label{fig:bibtex-mode}
  1894   \end{figure}
  1895 \<close>
  1896 
  1897 
  1898 section \<open>Document preview\<close>
  1899 
  1900 text \<open>
  1901   The action @{action_def isabelle.preview} opens an HTML preview of the
  1902   current theory document in the default web browser. The content is derived
  1903   from the semantic markup produced by the prover, and thus depends on the
  1904   status of formal processing.
  1905 \<close>
  1906 
  1907 
  1908 chapter \<open>ML debugging within the Prover IDE\<close>
  1909 
  1910 text \<open>
  1911   Isabelle/ML is based on Poly/ML\<^footnote>\<open>\<^url>\<open>http://www.polyml.org\<close>\<close> and thus
  1912   benefits from the source-level debugger of that implementation of Standard
  1913   ML. The Prover IDE provides the \<^emph>\<open>Debugger\<close> dockable to connect to running
  1914   ML threads, inspect the stack frame with local ML bindings, and evaluate ML
  1915   expressions in a particular run-time context. A typical debugger session is
  1916   shown in \figref{fig:ml-debugger}.
  1917 
  1918   ML debugging depends on the following pre-requisites.
  1919 
  1920     \<^enum> ML source needs to be compiled with debugging enabled. This may be
  1921     controlled for particular chunks of ML sources using any of the subsequent
  1922     facilities.
  1923 
  1924       \<^enum> The system option @{system_option_ref ML_debugger} as implicit state
  1925       of the Isabelle process. It may be changed in the menu \<^emph>\<open>Plugins /
  1926       Plugin Options / Isabelle / General\<close>. ML modules need to be reloaded and
  1927       recompiled to pick up that option as intended.
  1928 
  1929       \<^enum> The configuration option @{attribute_ref ML_debugger}, with an
  1930       attribute of the same name, to update a global or local context (e.g.\
  1931       with the @{command declare} command).
  1932 
  1933       \<^enum> Commands that modify @{attribute ML_debugger} state for individual
  1934       files: @{command_ref ML_file_debug}, @{command_ref ML_file_no_debug},
  1935       @{command_ref SML_file_debug}, @{command_ref SML_file_no_debug}.
  1936 
  1937     The instrumentation of ML code for debugging causes minor run-time
  1938     overhead. ML modules that implement critical system infrastructure may
  1939     lead to deadlocks or other undefined behaviour, when put under debugger
  1940     control!
  1941 
  1942     \<^enum> The \<^emph>\<open>Debugger\<close> panel needs to be active, otherwise the program ignores
  1943     debugger instrumentation of the compiler and runs unmanaged. It is also
  1944     possible to start debugging with the panel open, and later undock it, to
  1945     let the program continue unhindered.
  1946 
  1947     \<^enum> The ML program needs to be stopped at a suitable breakpoint, which may
  1948     be activated individually or globally as follows.
  1949 
  1950     For ML sources that have been compiled with debugger support, the IDE
  1951     visualizes possible breakpoints in the text. A breakpoint may be toggled
  1952     by pointing accurately with the mouse, with a right-click to activate
  1953     jEdit's context menu and its \<^emph>\<open>Toggle Breakpoint\<close> item. Alternatively, the
  1954     \<^emph>\<open>Break\<close> checkbox in the \<^emph>\<open>Debugger\<close> panel may be enabled to stop ML
  1955     threads always at the next possible breakpoint.
  1956 
  1957   Note that the state of individual breakpoints \<^emph>\<open>gets lost\<close> when the
  1958   coresponding ML source is re-compiled! This may happen unintentionally,
  1959   e.g.\ when following hyperlinks into ML modules that have not been loaded
  1960   into the IDE before.
  1961 
  1962   \begin{figure}[!htb]
  1963   \begin{center}
  1964   \includegraphics[scale=0.333]{ml-debugger}
  1965   \end{center}
  1966   \caption{ML debugger session}
  1967   \label{fig:ml-debugger}
  1968   \end{figure}
  1969 
  1970   The debugger panel (\figref{fig:ml-debugger}) shows a list of all threads
  1971   that are presently stopped. Each thread shows a stack of all function
  1972   invocations that lead to the current breakpoint at the top.
  1973 
  1974   It is possible to jump between stack positions freely, by clicking on this
  1975   list. The current situation is displayed in the big output window, as a
  1976   local ML environment with names and printed values.
  1977 
  1978   ML expressions may be evaluated in the current context by entering snippets
  1979   of source into the text fields labeled \<open>Context\<close> and \<open>ML\<close>, and pushing the
  1980   \<open>Eval\<close> button. By default, the source is interpreted as Isabelle/ML with the
  1981   usual support for antiquotations (like @{command ML}, @{command ML_file}).
  1982   Alternatively, strict Standard ML may be enforced via the \<^emph>\<open>SML\<close> checkbox
  1983   (like @{command SML_file}).
  1984 
  1985   The context for Isabelle/ML is optional, it may evaluate to a value of type
  1986   @{ML_type theory}, @{ML_type Proof.context}, or @{ML_type Context.generic}.
  1987   Thus the given ML expression (with its antiquotations) may be subject to the
  1988   intended dynamic run-time context, instead of the static compile-time
  1989   context.
  1990 
  1991   \<^medskip>
  1992   The buttons labeled \<^emph>\<open>Continue\<close>, \<^emph>\<open>Step\<close>, \<^emph>\<open>Step over\<close>, \<^emph>\<open>Step out\<close>
  1993   recommence execution of the program, with different policies concerning
  1994   nested function invocations. The debugger always moves the cursor within the
  1995   ML source to the next breakpoint position, and offers new stack frames as
  1996   before.
  1997 \<close>
  1998 
  1999 
  2000 chapter \<open>Miscellaneous tools\<close>
  2001 
  2002 section \<open>Timing\<close>
  2003 
  2004 text \<open>
  2005   Managed evaluation of commands within PIDE documents includes timing
  2006   information, which consists of elapsed (wall-clock) time, CPU time, and GC
  2007   (garbage collection) time. Note that in a multithreaded system it is
  2008   difficult to measure execution time precisely: elapsed time is closer to the
  2009   real requirements of runtime resources than CPU or GC time, which are both
  2010   subject to influences from the parallel environment that are outside the
  2011   scope of the current command transaction.
  2012 
  2013   The \<^emph>\<open>Timing\<close> panel provides an overview of cumulative command timings for
  2014   each document node. Commands with elapsed time below the given threshold are
  2015   ignored in the grand total. Nodes are sorted according to their overall
  2016   timing. For the document node that corresponds to the current buffer,
  2017   individual command timings are shown as well. A double-click on a theory
  2018   node or command moves the editor focus to that particular source position.
  2019 
  2020   It is also possible to reveal individual timing information via some tooltip
  2021   for the corresponding command keyword, using the technique of mouse hovering
  2022   with \<^verbatim>\<open>CONTROL\<close>~/ \<^verbatim>\<open>COMMAND\<close> modifier (\secref{sec:tooltips-hyperlinks}).
  2023   Actual display of timing depends on the global option @{system_option_ref
  2024   jedit_timing_threshold}, which can be configured in \<^emph>\<open>Plugin Options~/
  2025   Isabelle~/ General\<close>.
  2026 
  2027   \<^medskip>
  2028   The \<^emph>\<open>Monitor\<close> panel visualizes various data collections about recent
  2029   activity of the Isabelle/ML task farm and the underlying ML runtime system.
  2030   The display is continuously updated according to @{system_option_ref
  2031   editor_chart_delay}. Note that the painting of the chart takes considerable
  2032   runtime itself --- on the Java Virtual Machine that runs Isabelle/Scala, not
  2033   Isabelle/ML. Internally, the Isabelle/Scala module \<^verbatim>\<open>isabelle.ML_Statistics\<close>
  2034   provides further access to statistics of Isabelle/ML.
  2035 \<close>
  2036 
  2037 
  2038 section \<open>Low-level output\<close>
  2039 
  2040 text \<open>
  2041   Prover output is normally shown directly in the main text area or specific
  2042   panels like \<^emph>\<open>Output\<close> (\secref{sec:output}) or \<^emph>\<open>State\<close>
  2043   (\secref{sec:state-output}). Beyond this, it is occasionally useful to
  2044   inspect low-level output channels via some of the following additional
  2045   panels:
  2046 
  2047   \<^item> \<^emph>\<open>Protocol\<close> shows internal messages between the Isabelle/Scala and
  2048   Isabelle/ML side of the PIDE document editing protocol. Recording of
  2049   messages starts with the first activation of the corresponding dockable
  2050   window; earlier messages are lost.
  2051 
  2052   Actual display of protocol messages causes considerable slowdown, so it is
  2053   important to undock all \<^emph>\<open>Protocol\<close> panels for production work.
  2054 
  2055   \<^item> \<^emph>\<open>Raw Output\<close> shows chunks of text from the \<^verbatim>\<open>stdout\<close> and \<^verbatim>\<open>stderr\<close>
  2056   channels of the prover process. Recording of output starts with the first
  2057   activation of the corresponding dockable window; earlier output is lost.
  2058 
  2059   The implicit stateful nature of physical I/O channels makes it difficult to
  2060   relate raw output to the actual command from where it was originating.
  2061   Parallel execution may add to the confusion. Peeking at physical process I/O
  2062   is only the last resort to diagnose problems with tools that are not PIDE
  2063   compliant.
  2064 
  2065   Under normal circumstances, prover output always works via managed message
  2066   channels (corresponding to @{ML writeln}, @{ML warning}, @{ML
  2067   Output.error_message} in Isabelle/ML), which are displayed by regular means
  2068   within the document model (\secref{sec:output}). Unhandled Isabelle/ML
  2069   exceptions are printed by the system via @{ML Output.error_message}.
  2070 
  2071   \<^item> \<^emph>\<open>Syslog\<close> shows system messages that might be relevant to diagnose
  2072   problems with the startup or shutdown phase of the prover process; this also
  2073   includes raw output on \<^verbatim>\<open>stderr\<close>. Isabelle/ML also provides an explicit @{ML
  2074   Output.system_message} operation, which is occasionally useful for
  2075   diagnostic purposes within the system infrastructure itself.
  2076 
  2077   A limited amount of syslog messages are buffered, independently of the
  2078   docking state of the \<^emph>\<open>Syslog\<close> panel. This allows to diagnose serious
  2079   problems with Isabelle/PIDE process management, outside of the actual
  2080   protocol layer.
  2081 
  2082   Under normal situations, such low-level system output can be ignored.
  2083 \<close>
  2084 
  2085 
  2086 chapter \<open>Known problems and workarounds \label{sec:problems}\<close>
  2087 
  2088 text \<open>
  2089   \<^item> \<^bold>\<open>Problem:\<close> Odd behavior of some diagnostic commands with global
  2090   side-effects, like writing a physical file.
  2091 
  2092   \<^bold>\<open>Workaround:\<close> Copy/paste complete command text from elsewhere, or disable
  2093   continuous checking temporarily.
  2094 
  2095   \<^item> \<^bold>\<open>Problem:\<close> Keyboard shortcuts \<^verbatim>\<open>C+PLUS\<close> and \<^verbatim>\<open>C+MINUS\<close> for adjusting the
  2096   editor font size depend on platform details and national keyboards.
  2097 
  2098   \<^bold>\<open>Workaround:\<close> Rebind keys via \<^emph>\<open>Global Options~/ Shortcuts\<close>.
  2099 
  2100   \<^item> \<^bold>\<open>Problem:\<close> The Mac OS X key sequence \<^verbatim>\<open>COMMAND+COMMA\<close> for application
  2101   \<^emph>\<open>Preferences\<close> is in conflict with the jEdit default keyboard shortcut for
  2102   \<^emph>\<open>Incremental Search Bar\<close> (action @{action_ref "quick-search"}).
  2103 
  2104   \<^bold>\<open>Workaround:\<close> Rebind key via \<^emph>\<open>Global Options~/ Shortcuts\<close> according to
  2105   national keyboard, e.g.\ \<^verbatim>\<open>COMMAND+SLASH\<close> on English ones.
  2106 
  2107   \<^item> \<^bold>\<open>Problem:\<close> On Mac OS X with native Apple look-and-feel, some exotic
  2108   national keyboards may cause a conflict of menu accelerator keys with
  2109   regular jEdit key bindings. This leads to duplicate execution of the
  2110   corresponding jEdit action.
  2111 
  2112   \<^bold>\<open>Workaround:\<close> Disable the native Apple menu bar via Java runtime option
  2113   \<^verbatim>\<open>-Dapple.laf.useScreenMenuBar=false\<close>.
  2114 
  2115   \<^item> \<^bold>\<open>Problem:\<close> Mac OS X system fonts sometimes lead to character drop-outs in
  2116   the main text area.
  2117 
  2118   \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>IsabelleText\<close> font.
  2119 
  2120   \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key
  2121   event handling of Java/AWT/Swing.
  2122 
  2123   \<^bold>\<open>Workaround:\<close> Do not use X11 input methods. Note that environment variable
  2124   \<^verbatim>\<open>XMODIFIERS\<close> is reset by default within Isabelle settings.
  2125 
  2126   \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 window managers that are not ``re-parenting''
  2127   cause problems with additional windows opened by Java. This affects either
  2128   historic or neo-minimalistic window managers like \<^verbatim>\<open>awesome\<close> or \<^verbatim>\<open>xmonad\<close>.
  2129 
  2130   \<^bold>\<open>Workaround:\<close> Use a regular re-parenting X11 window manager.
  2131 
  2132   \<^item> \<^bold>\<open>Problem:\<close> Various forks of Linux/X11 window managers and desktop
  2133   environments (like Gnome) disrupt the handling of menu popups and mouse
  2134   positions of Java/AWT/Swing.
  2135 
  2136   \<^bold>\<open>Workaround:\<close> Use suitable version of Linux desktops.
  2137 
  2138   \<^item> \<^bold>\<open>Problem:\<close> Full-screen mode via jEdit action @{action_ref
  2139   "toggle-full-screen"} (default keyboard shortcut \<^verbatim>\<open>F11\<close>) works on Windows,
  2140   but not on Mac OS X or various Linux/X11 window managers.
  2141 
  2142   \<^bold>\<open>Workaround:\<close> Use native full-screen control of the window manager (notably
  2143   on Mac OS X).
  2144 
  2145   \<^item> \<^bold>\<open>Problem:\<close> Heap space of the JVM may fill up and render the Prover IDE
  2146   unresponsive, e.g.\ when editing big Isabelle sessions with many theories.
  2147 
  2148   \<^bold>\<open>Workaround:\<close> On a 64bit platform, ensure that the JVM runs in 64bit mode,
  2149   but the Isabelle/ML process remains in 32bit mode! Do not switch Isabelle/ML
  2150   into 64bit mode in the expectation to be ``more efficient'' --- this
  2151   requires 16--32\,GB to make sense.
  2152 
  2153   For the JVM, always use the 64bit version. That is the default on all
  2154   platforms, except for Windows: the standard download is for win32, but there
  2155   is a separate download for win64. This implicitly provides a larger default
  2156   heap for the JVM.
  2157 
  2158   Moreover, it is possible to increase JVM heap parameters explicitly, by
  2159   editing platform-specific files (for ``properties'' or ``options'') that are
  2160   associated with the main app bundle.
  2161 
  2162   Also note that jEdit provides a heap space monitor in the status line
  2163   (bottom-right). Double-clicking on that causes full garbage-collection,
  2164   which sometimes helps in low-memory situations.
  2165 \<close>
  2166 
  2167 end