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