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