src/Doc/JEdit/JEdit.thy
 author wenzelm Sat Nov 24 18:56:44 2018 +0100 (5 months ago) changeset 69343 395c4fb15ea2 parent 68737 a8bef9ff7dc0 child 69597 ff784d5a5bfb permissions -rw-r--r--
use "Isabelle DejaVu" fonts uniformly: Text Area, GUI elements, HTML output etc.;
     1 (*:maxLineLen=78:*)

     2

     3 theory JEdit

     4 imports Base

     5 begin

     6

     7 chapter \<open>Introduction\<close>

     8

     9 section \<open>Concepts and terminology\<close>

    10

    11 text \<open>

    12   Isabelle/jEdit is a Prover IDE that integrates \<^emph>\<open>parallel proof checking\<close>

    13   @{cite "Wenzel:2009" and "Wenzel:2013:ITP"} with \<^emph>\<open>asynchronous user

    14   interaction\<close> @{cite "Wenzel:2010" and "Wenzel:2012:UITP-EPTCS" and

    15   "Wenzel:2014:ITP-PIDE" and "Wenzel:2014:UITP"}, based on a document-oriented

    16   approach to \<^emph>\<open>continuous proof processing\<close> @{cite "Wenzel:2011:CICM" and

    17   "Wenzel:2012"}. Many concepts and system components are fit together in

    18   order to make this work. The main building blocks are as follows.

    19

    20     \<^descr>[Isabelle/ML] is the implementation and extension language of Isabelle,

    21     see also @{cite "isabelle-implementation"}. It is integrated into the

    22     logical context of Isabelle/Isar and allows to manipulate logical entities

    23     directly. Arbitrary add-on tools may be implemented for object-logics such

    24     as Isabelle/HOL.

    25

    26     \<^descr>[Isabelle/Scala] is the system programming language of Isabelle. It

    27     extends the pure logical environment of Isabelle/ML towards the outer

    28     world of graphical user interfaces, text editors, IDE frameworks, web

    29     services, SSH servers, SQL databases etc. Special infrastructure allows to

    30     transfer algebraic datatypes and formatted text easily between ML and

    31     Scala, using asynchronous protocol commands.

    32

    33     \<^descr>[PIDE] is a general framework for Prover IDEs based on Isabelle/Scala. It

    34     is built around a concept of parallel and asynchronous document

    35     processing, which is supported natively by the parallel proof engine that

    36     is implemented in Isabelle/ML. The traditional prover command loop is

    37     given up; instead there is direct support for editing of source text, with

    38     rich formal markup for GUI rendering.

    39

    40     \<^descr>[jEdit] is a sophisticated text editor\<^footnote>\<open>\<^url>\<open>http://www.jedit.org\<close>\<close>

    41     implemented in Java\<^footnote>\<open>\<^url>\<open>https://www.java.com\<close>\<close>. It is easily extensible by

    42     plugins written in any language that works on the JVM. In the context of

    43     Isabelle this is always Scala\<^footnote>\<open>\<^url>\<open>https://www.scala-lang.org\<close>\<close>.

    44

    45     \<^descr>[Isabelle/jEdit] is the main application of the PIDE framework and the

    46     default user-interface for Isabelle. It targets both beginners and

    47     experts. Technically, Isabelle/jEdit consists of the original jEdit code

    48     base with minimal patches and a special plugin for Isabelle. This is

    49     integrated as a desktop application for the main operating system

    50     families: Linux, Windows, Mac OS X.

    51

    52   End-users of Isabelle download and run a standalone application that exposes

    53   jEdit as a text editor on the surface. Thus there is occasionally a tendency

    54   to apply the name jEdit'' to any of the Isabelle Prover IDE aspects,

    55   without proper differentiation. When discussing these PIDE building blocks

    56   in public forums, mailing lists, or even scientific publications, it is

    57   particularly important to distinguish Isabelle/ML versus Standard ML,

    58   Isabelle/Scala versus Scala, Isabelle/jEdit versus jEdit.

    59 \<close>

    60

    61

    62 section \<open>The Isabelle/jEdit Prover IDE\<close>

    63

    64 text \<open>

    65   \begin{figure}[!htb]

    66   \begin{center}

    67   \includegraphics[scale=0.333]{isabelle-jedit}

    68   \end{center}

    69   \caption{The Isabelle/jEdit Prover IDE}

    70   \label{fig:isabelle-jedit}

    71   \end{figure}

    72

    73   Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some plugins for

    74   the jEdit text editor, while preserving its general look-and-feel as far as

    75   possible. The main plugin is called Isabelle'' and has its own menu

    76   \<^emph>\<open>Plugins~/ Isabelle\<close> with access to several actions and add-on panels (see

    77   also \secref{sec:dockables}), as well as \<^emph>\<open>Plugins~/ Plugin Options~/

    78   Isabelle\<close> (see also \secref{sec:options}).

    79

    80   The options allow to specify a logic session name, but the same selector is

    81   also accessible in the \<^emph>\<open>Theories\<close> panel (\secref{sec:theories}). After

    82   startup of the Isabelle plugin, the selected logic session image is provided

    83   automatically by the Isabelle build tool @{cite "isabelle-system"}: if it is

    84   absent or outdated wrt.\ its sources, the build process updates it within

    85   the running text editor. Prover IDE functionality is fully activated after

    86   successful termination of the build process. A failure may require changing

    87   some options and restart of the Isabelle plugin or application. Changing the

    88   logic session, or the underlying ML system platform (32\,bit versus 64\,bit)

    89   requires a restart of the whole application to take effect.

    90

    91   \<^medskip>

    92   The main job of the Prover IDE is to manage sources and their changes,

    93   taking the logical structure as a formal document into account (see also

    94   \secref{sec:document-model}). The editor and the prover are connected

    95   asynchronously in a lock-free manner. The prover is free to organize the

    96   checking of the formal text in parallel on multiple cores, and provides

    97   feedback via markup, which is rendered in the editor via colors, boxes,

    98   squiggly underlines, hyperlinks, popup windows, icons, clickable output etc.

    99

   100   Using the mouse together with the modifier key \<^verbatim>\<open>CONTROL\<close> (Linux, Windows)

   101   or \<^verbatim>\<open>COMMAND\<close> (Mac OS X) exposes formal content via tooltips and/or

   102   hyperlinks (see also \secref{sec:tooltips-hyperlinks}). Output (in popups

   103   etc.) may be explored recursively, using the same techniques as in the

   104   editor source buffer.

   105

   106   Thus the Prover IDE gives an impression of direct access to formal content

   107   of the prover within the editor, but in reality only certain aspects are

   108   exposed, according to the possibilities of the prover and its add-on tools.

   109 \<close>

   110

   111

   112 subsection \<open>Documentation\<close>

   113

   114 text \<open>

   115   The \<^emph>\<open>Documentation\<close> panel of Isabelle/jEdit provides access to some example

   116   theory files and the standard Isabelle documentation. PDF files are opened

   117   by regular desktop operations of the underlying platform. The section

   118   Original jEdit Documentation'' contains the original \<^emph>\<open>User's Guide\<close> of

   119   this sophisticated text editor. The same is accessible via the \<^verbatim>\<open>Help\<close> menu

   120   or \<^verbatim>\<open>F1\<close> keyboard shortcut, using the built-in HTML viewer of Java/Swing.

   121   The latter also includes \<^emph>\<open>Frequently Asked Questions\<close> and documentation of

   122   individual plugins.

   123

   124   Most of the information about jEdit is relevant for Isabelle/jEdit as well,

   125   but users need to keep in mind that defaults sometimes differ, and the

   126   official jEdit documentation does not know about the Isabelle plugin with

   127   its support for continuous checking of formal source text: jEdit is a plain

   128   text editor, but Isabelle/jEdit is a Prover IDE.

   129 \<close>

   130

   131

   132 subsection \<open>Plugins\<close>

   133

   134 text \<open>

   135   The \<^emph>\<open>Plugin Manager\<close> of jEdit allows to augment editor functionality by JVM

   136   modules (jars) that are provided by the central plugin repository, which is

   137   accessible via various mirror sites.

   138

   139   Connecting to the plugin server-infrastructure of the jEdit project allows

   140   to update bundled plugins or to add further functionality. This needs to be

   141   done with the usual care for such an open bazaar of contributions. Arbitrary

   142   combinations of add-on features are apt to cause problems. It is advisable

   143   to start with the default configuration of Isabelle/jEdit and develop some

   144   sense how it is meant to work, before loading too many other plugins.

   145

   146   \<^medskip>

   147   The \<^emph>\<open>Isabelle\<close> plugin is responsible for the main Prover IDE functionality

   148   of Isabelle/jEdit: it manages the prover session in the background. A few

   149   additional plugins are bundled with Isabelle/jEdit for convenience or out of

   150   necessity, notably \<^emph>\<open>Console\<close> with its \<^emph>\<open>Scala\<close> sub-plugin

   151   (\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close> with some Isabelle-specific

   152   parsers for document tree structure (\secref{sec:sidekick}). The

   153   \<^emph>\<open>Navigator\<close> plugin is particularly important for hyperlinks within the

   154   formal document-model (\secref{sec:tooltips-hyperlinks}). Further plugins

   155   (e.g.\ \<^emph>\<open>ErrorList\<close>, \<^emph>\<open>Code2HTML\<close>) are included to saturate the dependencies

   156   of bundled plugins, but have no particular use in Isabelle/jEdit.

   157 \<close>

   158

   159

   160 subsection \<open>Options \label{sec:options}\<close>

   161

   162 text \<open>

   163   Both jEdit and Isabelle have distinctive management of persistent options.

   164

   165   Regular jEdit options are accessible via the dialogs \<^emph>\<open>Utilities~/ Global

   166   Options\<close> or \<^emph>\<open>Plugins~/ Plugin Options\<close>, with a second chance to flip the

   167   two within the central options dialog. Changes are stored in @{path

   168   "$JEDIT_SETTINGS/properties"} and @{path "$JEDIT_SETTINGS/keymaps"}.

   169

   170   Isabelle system options are managed by Isabelle/Scala and changes are stored

   171   in @{path "$ISABELLE_HOME_USER/etc/preferences"}, independently of   172 other jEdit properties. See also @{cite "isabelle-system"}, especially the   173 coverage of sessions and command-line tools like @{tool build} or @{tool   174 options}.   175   176 Those Isabelle options that are declared as \<^verbatim>\<open>public\<close> are configurable in   177 Isabelle/jEdit via \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>. Moreover, there   178 are various options for rendering document content, which are configurable   179 via \<^emph>\<open>Plugin Options~/ Isabelle~/ Rendering\<close>. Thus \<^emph>\<open>Plugin Options~/   180 Isabelle\<close> in jEdit provides a view on a subset of Isabelle system options.   181 Note that some of these options affect general parameters that are relevant   182 outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or   183 @{system_option parallel_proofs} for the Isabelle build tool @{cite   184 "isabelle-system"}, but it is possible to use the settings variable   185 @{setting ISABELLE_BUILD_OPTIONS} to change defaults for batch builds   186 without affecting the Prover IDE.   187   188 The jEdit action @{action_def isabelle.options} opens the options dialog for   189 the Isabelle plugin; it can be mapped to editor GUI elements as usual.   190   191 \<^medskip>   192 Options are usually loaded on startup and saved on shutdown of   193 Isabelle/jEdit. Editing the generated @{path "$JEDIT_SETTINGS/properties"}

   194   or @{path "$ISABELLE_HOME_USER/etc/preferences"} manually while the   195 application is running may cause surprise due to lost updates!   196 \<close>   197   198   199 subsection \<open>Keymaps\<close>   200   201 text \<open>   202 Keyboard shortcuts are managed as a separate concept of \<^emph>\<open>keymap\<close> that is   203 configurable via \<^emph>\<open>Global Options~/ Shortcuts\<close>. The \<^verbatim>\<open>imported\<close> keymap is   204 derived from the initial environment of properties that is available at the   205 first start of the editor; afterwards the keymap file takes precedence and   206 is no longer affected by change of default properties.   207   208 Users may change their keymap later, but this may lead to conflicts with   209 \<^verbatim>\<open>shortcut\<close> properties in \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>.

   210

   211   The action @{action_def "isabelle.keymap-merge"} helps to resolve pending

   212   Isabelle keymap changes that are in conflict with the current jEdit keymap;

   213   while non-conflicting changes are applied implicitly. This action is

   214   automatically invoked on Isabelle/jEdit startup.

   215 \<close>

   216

   217

   218 section \<open>Command-line invocation \label{sec:command-line}\<close>

   219

   220 text \<open>

   221   Isabelle/jEdit is normally invoked as a single-instance desktop application,

   222   based on platform-specific executables for Linux, Windows, Mac OS X.

   223

   224   It is also possible to invoke the Prover IDE on the command-line, with some

   225   extra options and environment settings. The command-line usage of @{tool_def

   226   jedit} is as follows:

   227   @{verbatim [display]

   228 \<open>Usage: isabelle jedit [OPTIONS] [FILES ...]

   229

   230   Options are:

   231     -A NAME      ancestor session for options -R and -S (default: parent)

   232     -D NAME=X    set JVM system property

   233     -J OPTION    add JVM runtime option

   234                  (default $JEDIT_JAVA_SYSTEM_OPTIONS$JEDIT_JAVA_OPTIONS)

   235     -R NAME      build image with requirements from other sessions

   236     -S NAME      like option -R, with focus on selected session

   237     -b           build only

   238     -d DIR       include session directory

   239     -f           fresh build

   240     -i NAME      include session in name-space of theories

   241     -j OPTION    add jEdit runtime option

   242                  (default $JEDIT_OPTIONS)   243 -l NAME logic image name   244 -m MODE add print mode for output   245 -n no build of session image on startup   246 -p CMD ML process command prefix (process policy)   247 -s system build mode for session image   248   249 Start jEdit with Isabelle plugin setup and open FILES   250 (default "$USER_HOME/Scratch.thy" or ":" for empty buffer).\<close>}

   251

   252   The \<^verbatim>\<open>-l\<close> option specifies the session name of the logic image to be used

   253   for proof processing. Additional session root directories may be included

   254   via option \<^verbatim>\<open>-d\<close> to augment the session name space (see also @{cite

   255   "isabelle-system"}). By default, the specified image is checked and built on

   256   demand. The \<^verbatim>\<open>-s\<close> option determines where to store the result session image

   257   of @{tool build}. The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for

   258   the selected session image.

   259

   260   The \<^verbatim>\<open>-R\<close> option builds an auxiliary logic image with all theories from

   261   other sessions that are not already present in its parent; it also opens the

   262   session \<^verbatim>\<open>ROOT\<close> entry in the editor to facilitate editing of the main

   263   session. The \<^verbatim>\<open>-S\<close> option is like \<^verbatim>\<open>-R\<close>, with a focus on the selected

   264   session and its descendants: the namespace of accessible theories is

   265   restricted accordingly. This reduces startup time for big projects, notably

   266   the Archive of Formal Proofs''. The \<^verbatim>\<open>-A\<close> option specifies and alternative

   267   ancestor session for options \<^verbatim>\<open>-R\<close> and \<^verbatim>\<open>-S\<close>: this allows to restructure the

   268   hierarchy of session images on the spot.

   269

   270   The \<^verbatim>\<open>-i\<close> option includes additional sessions into the name-space of

   271   theories: multiple occurrences are possible.

   272

   273   The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover process.

   274   Note that the system option @{system_option_ref jedit_print_mode} allows to

   275   do the same persistently (e.g.\ via the \<^emph>\<open>Plugin Options\<close> dialog of

   276   Isabelle/jEdit), without requiring command-line invocation.

   277

   278   The \<^verbatim>\<open>-J\<close> and \<^verbatim>\<open>-j\<close> options pass additional low-level options to the JVM or

   279   jEdit, respectively. The defaults are provided by the Isabelle settings

   280   environment @{cite "isabelle-system"}, but note that these only work for the

   281   command-line tool described here, and not the regular application.

   282

   283   The \<^verbatim>\<open>-D\<close> option allows to define JVM system properties; this is passed

   284   directly to the underlying \<^verbatim>\<open>java\<close> process.

   285

   286   The \<^verbatim>\<open>-b\<close> and \<^verbatim>\<open>-f\<close> options control the self-build mechanism of

   287   Isabelle/jEdit. This is only relevant for building from sources, which also

   288   requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component from

   289   \<^url>\<open>https://isabelle.in.tum.de/components\<close>. The official Isabelle release

   290   already includes a pre-built version of Isabelle/jEdit.

   291

   292   \<^bigskip>

   293   It is also possible to connect to an already running Isabelle/jEdit process

   294   via @{tool_def jedit_client}:

   295   @{verbatim [display]

   296 \<open>Usage: isabelle jedit_client [OPTIONS] [FILES ...]

   297

   298   Options are:

   299     -c           only check presence of server

   300     -n           only report server name

   301     -s NAME      server name (default Isabelle)

   302

   303   Connect to already running Isabelle/jEdit instance and open FILES\<close>}

   304

   305   The \<^verbatim>\<open>-c\<close> option merely checks the presence of the server, producing a

   306   process return code accordingly.

   307

   308   The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a

   309   different server name. The default server name is the official distribution

   310   name (e.g.\ \<^verbatim>\<open>Isabelle2018\<close>). Thus @{tool jedit_client} can connect to the

   311   Isabelle desktop application without further options.

   312

   313   The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system

   314   option @{system_option_ref ML_process_policy} for ML processes started by

   315   the Prover IDE, e.g. to control CPU affinity on multiprocessor systems.

   316

   317   The JVM system property \<^verbatim>\<open>isabelle.jedit_server\<close> provides a different server

   318   name, e.g.\ use \<^verbatim>\<open>isabelle jedit -Disabelle.jedit_server=\<close>\<open>name\<close> and

   319   \<^verbatim>\<open>isabelle jedit_client -s\<close>~\<open>name\<close> to connect later on.

   320 \<close>

   321

   322

   323 section \<open>GUI rendering\<close>

   324

   325 subsection \<open>Look-and-feel \label{sec:look-and-feel}\<close>

   326

   327 text \<open>

   328   jEdit is a Java/AWT/Swing application with the ambition to support

   329   native'' look-and-feel on all platforms, within the limits of what Oracle

   330   as Java provider and major operating system distributors allow (see also

   331   \secref{sec:problems}).

   332

   333   Isabelle/jEdit enables platform-specific look-and-feel by default as

   334   follows.

   335

   336     \<^descr>[Linux:] The platform-independent \<^emph>\<open>Metal\<close> is used by default.

   337

   338     The Linux-specific \<^emph>\<open>GTK+\<close> often works as well, but the overall GTK theme

   339     and options need to be selected to suite Java/AWT/Swing. Note that Java

   340     Virtual Machine has no direct influence of GTK rendering.

   341

   342     \<^descr>[Windows:] Regular \<^emph>\<open>Windows\<close> is used by default.

   343

   344     \<^descr>[Mac OS X:] Regular \<^emph>\<open>Mac OS X\<close> is used by default.

   345

   346     The bundled \<^emph>\<open>MacOSX\<close> plugin provides various functions that are expected

   347     from applications on that particular platform: quit from menu or dock,

   348     preferences menu, drag-and-drop of text files on the application,

   349     full-screen mode for main editor windows. It is advisable to have the

   350     \<^emph>\<open>MacOSX\<close> plugin enabled all the time on that platform.

   351

   352   Users may experiment with different Swing look-and-feels, but need to keep

   353   in mind that this extra variance of GUI functionality often causes problems.

   354   The platform-independent \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close> should always work on all

   355   platforms, although they are technically and stylistically outdated. The

   356   historic \<^emph>\<open>CDE/Motif\<close> should be ignored.

   357

   358   Changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close> may update the

   359   GUI only partially: proper restart of Isabelle/jEdit is usually required.

   360 \<close>

   361

   362

   363 subsection \<open>Displays with very high resolution \label{sec:hdpi}\<close>

   364

   365 text \<open>

   366   In distant past, displays with $1024 \times 768$ or $1280 \times 1024$

   367   pixels were considered high resolution'' and bitmap fonts with 12 or 14

   368   pixels as adequate for text rendering. After 2016, we have routinely seen

   369   much higher resolutions, e.g. Full HD'' at $1920 \times 1080$ pixels or

   370   Ultra HD'' / 4K'' at $3840 \times 2160$.

   371

   372   GUI frameworks are usually lagging behind, with hard-wired icon sizes and

   373   tiny fonts. Java and jEdit do provide reasonable support for very high

   374   resolution, but this requires manual adjustments as described below.

   375

   376   \<^medskip>

   377   The \<^bold>\<open>operating-system\<close> usually provides some configuration for global

   378   scaling of text fonts, e.g.\ $120\%$--$250\%$ on Windows. This impacts

   379   regular GUI elements, when used with native look-and-feel: Linux \<^emph>\<open>GTK+\<close>,

   380   \<^emph>\<open>Windows\<close>, \<^emph>\<open>Mac OS X\<close>, respectively. Alternatively, it is possible to use

   381   the platform-independent \<^emph>\<open>Metal\<close> look-and-feel and readjust its main font

   382   sizes via jEdit options explained below. The Isabelle/jEdit \<^bold>\<open>application\<close>

   383   provides further options to adjust font sizes in particular GUI elements.

   384   Here is a summary of all relevant font properties:

   385

   386     \<^item> \<^emph>\<open>Global Options / Text Area / Text font\<close>: the main text area font,

   387     which is also used as reference point for various derived font sizes,

   388     e.g.\ the \<^emph>\<open>Output\<close> (\secref{sec:output}) and \<^emph>\<open>State\<close>

   389     (\secref{sec:state-output}) panels.

   390

   391     \<^item> \<^emph>\<open>Global Options / Gutter / Gutter font\<close>: the font for the gutter area

   392     left of the main text area, e.g.\ relevant for display of line numbers

   393     (disabled by default).

   394

   395     \<^item> \<^emph>\<open>Global Options / Appearance / Button, menu and label font\<close> as well as

   396     \<^emph>\<open>List and text field font\<close>: this specifies the primary and secondary font

   397     for the \<^emph>\<open>Metal\<close> look-and-feel (\secref{sec:look-and-feel}).

   398

   399     \<^item> \<^emph>\<open>Plugin Options / Isabelle / General / Reset Font Size\<close>: the main text

   400     area font size for action @{action_ref "isabelle.reset-font-size"}, e.g.\

   401     relevant for quick scaling like in common web browsers.

   402

   403     \<^item> \<^emph>\<open>Plugin Options / Console / General / Font\<close>: the console window font,

   404     e.g.\ relevant for Isabelle/Scala command-line.

   405

   406   In \figref{fig:isabelle-jedit-hdpi} the \<^emph>\<open>Metal\<close> look-and-feel is configured

   407   with custom fonts at 30 pixels, and the main text area and console at 36

   408   pixels. This leads to decent rendering quality, despite the old-fashioned

   409   appearance of \<^emph>\<open>Metal\<close>.

   410

   411   \begin{figure}[!htb]

   412   \begin{center}

   413   \includegraphics[width=\textwidth]{isabelle-jedit-hdpi}

   414   \end{center}

   415   \caption{Metal look-and-feel with custom fonts for very high resolution}

   416   \label{fig:isabelle-jedit-hdpi}

   417   \end{figure}

   418 \<close>

   419

   420

   421 chapter \<open>Augmented jEdit functionality\<close>

   422

   423 section \<open>Dockable windows \label{sec:dockables}\<close>

   424

   425 text \<open>

   426   In jEdit terminology, a \<^emph>\<open>view\<close> is an editor window with one or more \<^emph>\<open>text

   427   areas\<close> that show the content of one or more \<^emph>\<open>buffers\<close>. A regular view may

   428   be surrounded by \<^emph>\<open>dockable windows\<close> that show additional information in

   429   arbitrary format, not just text; a \<^emph>\<open>plain view\<close> does not allow dockables.

   430   The \<^emph>\<open>dockable window manager\<close> of jEdit organizes these dockable windows,

   431   either as \<^emph>\<open>floating\<close> windows, or \<^emph>\<open>docked\<close> panels within one of the four

   432   margins of the view. There may be any number of floating instances of some

   433   dockable window, but at most one docked instance; jEdit actions that address

   434   \<^emph>\<open>the\<close> dockable window of a particular kind refer to the unique docked

   435   instance.

   436

   437   Dockables are used routinely in jEdit for important functionality like

   438   \<^emph>\<open>HyperSearch Results\<close> or the \<^emph>\<open>File System Browser\<close>. Plugins often provide

   439   a central dockable to access their main functionality, which may be opened

   440   by the user on demand. The Isabelle/jEdit plugin takes this approach to the

   441   extreme: its plugin menu provides the entry-points to many panels that are

   442   managed as dockable windows. Some important panels are docked by default,

   443   e.g.\ \<^emph>\<open>Documentation\<close>, \<^emph>\<open>State\<close>, \<^emph>\<open>Theories\<close> \<^emph>\<open>Output\<close>, \<^emph>\<open>Query\<close>. The user

   444   can change this arrangement easily and persistently.

   445

   446   Compared to plain jEdit, dockable window management in Isabelle/jEdit is

   447   slightly augmented according to the the following principles:

   448

   449   \<^item> Floating windows are dependent on the main window as \<^emph>\<open>dialog\<close> in

   450   the sense of Java/AWT/Swing. Dialog windows always stay on top of the view,

   451   which is particularly important in full-screen mode. The desktop environment

   452   of the underlying platform may impose further policies on such dependent

   453   dialogs, in contrast to fully independent windows, e.g.\ some window

   454   management functions may be missing.

   455

   456   \<^item> Keyboard focus of the main view vs.\ a dockable window is carefully

   457   managed according to the intended semantics, as a panel mainly for output or

   458   input. For example, activating the \<^emph>\<open>Output\<close> (\secref{sec:output}) or State

   459   (\secref{sec:state-output}) panel via the dockable window manager returns

   460   keyboard focus to the main text area, but for \<^emph>\<open>Query\<close> (\secref{sec:query})

   461   or \<^emph>\<open>Sledgehammer\<close> \secref{sec:sledgehammer} the focus is given to the main

   462   input field of that panel.

   463

   464   \<^item> Panels that provide their own text area for output have an additional

   465   dockable menu item \<^emph>\<open>Detach\<close>. This produces an independent copy of the

   466   current output as a floating \<^emph>\<open>Info\<close> window, which displays that content

   467   independently of ongoing changes of the PIDE document-model. Note that

   468   Isabelle/jEdit popup windows (\secref{sec:tooltips-hyperlinks}) provide a

   469   similar \<^emph>\<open>Detach\<close> operation as an icon.

   470 \<close>

   471

   472

   473 section \<open>Isabelle symbols \label{sec:symbols}\<close>

   474

   475 text \<open>

   476   Isabelle sources consist of \<^emph>\<open>symbols\<close> that extend plain ASCII to allow

   477   infinitely many mathematical symbols within the formal sources. This works

   478   without depending on particular encodings and varying Unicode

   479   standards.\<^footnote>\<open>Raw Unicode characters within formal sources would compromise

   480   portability and reliability in the face of changing interpretation of

   481   special features of Unicode, such as Combining Characters or Bi-directional

   482   Text.\<close> See @{cite "Wenzel:2011:CICM"}.

   483

   484   For the prover back-end, formal text consists of ASCII characters that are

   485   grouped according to some simple rules, e.g.\ as plain \<^verbatim>\<open>a\<close>'' or symbolic

   486   \<^verbatim>\<open>\<alpha>\<close>''. For the editor front-end, a certain subset of symbols is rendered

   487   physically via Unicode glyphs, in order to show \<^verbatim>\<open>\<alpha>\<close>'' as \<open>\<alpha>\<close>'', for

   488   example. This symbol interpretation is specified by the Isabelle system

   489   distribution in \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and may be augmented by the   490 user in @{path "$ISABELLE_HOME_USER/etc/symbols"}.

   491

   492   The appendix of @{cite "isabelle-isar-ref"} gives an overview of the

   493   standard interpretation of finitely many symbols from the infinite

   494   collection. Uninterpreted symbols are displayed literally, e.g.\

   495   \<^verbatim>\<open>\<foobar>\<close>''. Overlap of Unicode characters used in symbol

   496   interpretation with informal ones (which might appear e.g.\ in comments)

   497   needs to be avoided. Raw Unicode characters within prover source files

   498   should be restricted to informal parts, e.g.\ to write text in non-latin

   499   alphabets in comments.

   500 \<close>

   501

   502 paragraph \<open>Encoding.\<close>

   503

   504 text \<open>Technically, the Unicode interpretation of Isabelle symbols is an

   505   \<^emph>\<open>encoding\<close> called \<^verbatim>\<open>UTF-8-Isabelle\<close> in jEdit (\<^emph>\<open>not\<close> in the underlying

   506   JVM). It is provided by the Isabelle Base plugin and enabled by default for

   507   all source files in Isabelle/jEdit.

   508

   509   Sometimes such defaults are reset accidentally, or malformed UTF-8 sequences

   510   in the text force jEdit to fall back on a different encoding like

   511   \<^verbatim>\<open>ISO-8859-15\<close>. In that case, verbatim \<^verbatim>\<open>\<alpha>\<close>'' will be shown in the text

   512   buffer instead of its Unicode rendering \<open>\<alpha>\<close>''. The jEdit menu operation

   513   \<^emph>\<open>File~/ Reload with Encoding~/ UTF-8-Isabelle\<close> helps to resolve such

   514   problems (after repairing malformed parts of the text).

   515

   516   If the loaded text already contains Unicode sequences that are in conflict

   517   with the Isabelle symbol encoding, the fallback-encoding UTF-8 is used and

   518   Isabelle symbols remain in literal \<^verbatim>\<open>\<symbol>\<close> form. The jEdit menu

   519   operation \<^emph>\<open>Utilities~/ Buffer Options~/ Character encoding\<close> allows to

   520   enforce the UTF-8-Isabelle, but this will also change original Unicode

   521   text into Isabelle symbols when saving the file!

   522 \<close>

   523

   524 paragraph \<open>Font.\<close>

   525 text \<open>Correct rendering via Unicode requires a font that contains glyphs for

   526   the corresponding codepoints. There are also various unusual symbols with

   527   particular purpose in Isabelle, e.g.\ control symbols and very long arrows.

   528   Isabelle/jEdit prefers its own font collection \<^verbatim>\<open>Isabelle DejaVu\<close>, which

   529   ensures that all standard Isabelle symbols are shown on the screen (or

   530   printer) as expected.

   531

   532   Note that a Java/AWT/Swing application can load additional fonts only if

   533   they are not installed on the operating system already! Outdated versions of

   534   Isabelle fonts that happen to be provided by the operating system prevent

   535   Isabelle/jEdit to use its bundled version. This could lead to missing glyphs

   536   (black rectangles), when the system version of a font is older than the

   537   application version. This problem can be avoided by refraining to

   538   install'' any version of \<^verbatim>\<open>IsabelleText\<close> in the first place, although it

   539   might be tempting to use the same font in other applications.

   540

   541   HTML pages generated by Isabelle refer to the same Isabelle fonts as a

   542   server-side resource. Thus a web-browser can use that without requiring a

   543   locally installed copy.

   544 \<close>

   545

   546 paragraph \<open>Input methods.\<close>

   547 text \<open>In principle, Isabelle/jEdit could delegate the problem to produce

   548   Isabelle symbols in their Unicode rendering to the underlying operating

   549   system and its \<^emph>\<open>input methods\<close>. Regular jEdit also provides various ways to

   550   work with \<^emph>\<open>abbreviations\<close> to produce certain non-ASCII characters. Since

   551   none of these standard input methods work satisfactorily for the

   552   mathematical characters required for Isabelle, various specific

   553   Isabelle/jEdit mechanisms are provided.

   554

   555   This is a summary for practically relevant input methods for Isabelle

   556   symbols.

   557

   558   \<^enum> The \<^emph>\<open>Symbols\<close> panel: some GUI buttons allow to insert certain symbols in

   559   the text buffer. There are also tooltips to reveal the official Isabelle

   560   representation with some additional information about \<^emph>\<open>symbol

   561   abbreviations\<close> (see below).

   562

   563   \<^enum> Copy/paste from decoded source files: text that is rendered as Unicode

   564   already can be re-used to produce further text. This also works between

   565   different applications, e.g.\ Isabelle/jEdit and some web browser or mail

   566   client, as long as the same Unicode interpretation of Isabelle symbols is

   567   used.

   568

   569   \<^enum> Copy/paste from prover output within Isabelle/jEdit. The same principles

   570   as for text buffers apply, but note that \<^emph>\<open>copy\<close> in secondary Isabelle/jEdit

   571   windows works via the keyboard shortcuts \<^verbatim>\<open>C+c\<close> or \<^verbatim>\<open>C+INSERT\<close>, while jEdit

   572   menu actions always refer to the primary text area!

   573

   574   \<^enum> Completion provided by the Isabelle plugin (see \secref{sec:completion}).

   575   Isabelle symbols have a canonical name and optional abbreviations. This can

   576   be used with the text completion mechanism of Isabelle/jEdit, to replace a

   577   prefix of the actual symbol like \<^verbatim>\<open>\<lambda>\<close>, or its name preceded by backslash

   578   \<^verbatim>\<open>\lambda\<close>, or its ASCII abbreviation \<^verbatim>\<open>%\<close> by the Unicode rendering.

   579

   580   The following table is an extract of the information provided by the

   581   standard \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> file:   582   583 \<^medskip>   584 \begin{tabular}{lll}   585 \<^bold>\<open>symbol\<close> & \<^bold>\<open>name with backslash\<close> & \<^bold>\<open>abbreviation\<close> \\\hline   586 \<open>\<lambda>\<close> & \<^verbatim>\<open>\lambda\<close> & \<^verbatim>\<open>%\<close> \\   587 \<open>\<Rightarrow>\<close> & \<^verbatim>\<open>\Rightarrow\<close> & \<^verbatim>\<open>=>\<close> \\   588 \<open>\<Longrightarrow>\<close> & \<^verbatim>\<open>\Longrightarrow\<close> & \<^verbatim>\<open>==>\<close> \\[0.5ex]   589 \<open>\<And>\<close> & \<^verbatim>\<open>\And\<close> & \<^verbatim>\<open>!!\<close> \\   590 \<open>\<equiv>\<close> & \<^verbatim>\<open>\equiv\<close> & \<^verbatim>\<open>==\<close> \\[0.5ex]   591 \<open>\<forall>\<close> & \<^verbatim>\<open>\forall\<close> & \<^verbatim>\<open>!\<close> \\   592 \<open>\<exists>\<close> & \<^verbatim>\<open>\exists\<close> & \<^verbatim>\<open>?\<close> \\   593 \<open>\<longrightarrow>\<close> & \<^verbatim>\<open>\longrightarrow\<close> & \<^verbatim>\<open>-->\<close> \\   594 \<open>\<and>\<close> & \<^verbatim>\<open>\and\<close> & \<^verbatim>\<open>&\<close> \\   595 \<open>\<or>\<close> & \<^verbatim>\<open>\or\<close> & \<^verbatim>\<open>|\<close> \\   596 \<open>\<not>\<close> & \<^verbatim>\<open>\not\<close> & \<^verbatim>\<open>~\<close> \\   597 \<open>\<noteq>\<close> & \<^verbatim>\<open>\noteq\<close> & \<^verbatim>\<open>~=\<close> \\   598 \<open>\<in>\<close> & \<^verbatim>\<open>\in\<close> & \<^verbatim>\<open>:\<close> \\   599 \<open>\<notin>\<close> & \<^verbatim>\<open>\notin\<close> & \<^verbatim>\<open>~:\<close> \\   600 \end{tabular}   601 \<^medskip>   602   603 Note that the above abbreviations refer to the input method. The logical   604 notation provides ASCII alternatives that often coincide, but sometimes   605 deviate. This occasionally causes user confusion with old-fashioned Isabelle   606 source that use ASCII replacement notation like \<^verbatim>\<open>!\<close> or \<^verbatim>\<open>ALL\<close> directly in   607 the text.   608   609 On the other hand, coincidence of symbol abbreviations with ASCII   610 replacement syntax syntax helps to update old theory sources via explicit   611 completion (see also \<^verbatim>\<open>C+b\<close> explained in \secref{sec:completion}).   612 \<close>   613   614 paragraph \<open>Control symbols.\<close>   615 text \<open>There are some special control symbols to modify the display style of a   616 single symbol (without nesting). Control symbols may be applied to a region   617 of selected text, either using the \<^emph>\<open>Symbols\<close> panel or keyboard shortcuts or   618 jEdit actions. These editor operations produce a separate control symbol for   619 each symbol in the text, in order to make the whole text appear in a certain   620 style.   621   622 \<^medskip>   623 \begin{tabular}{llll}   624 \<^bold>\<open>style\<close> & \<^bold>\<open>symbol\<close> & \<^bold>\<open>shortcut\<close> & \<^bold>\<open>action\<close> \\\hline   625 superscript & \<^verbatim>\<open>\<^sup>\<close> & \<^verbatim>\<open>C+e UP\<close> & @{action_ref "isabelle.control-sup"} \\   626 subscript & \<^verbatim>\<open>\<^sub>\<close> & \<^verbatim>\<open>C+e DOWN\<close> & @{action_ref "isabelle.control-sub"} \\   627 bold face & \<^verbatim>\<open>\<^bold>\<close> & \<^verbatim>\<open>C+e RIGHT\<close> & @{action_ref "isabelle.control-bold"} \\   628 emphasized & \<^verbatim>\<open>\<^emph>\<close> & \<^verbatim>\<open>C+e LEFT\<close> & @{action_ref "isabelle.control-emph"} \\   629 reset & & \<^verbatim>\<open>C+e BACK_SPACE\<close> & @{action_ref "isabelle.control-reset"} \\   630 \end{tabular}   631 \<^medskip>   632   633 To produce a single control symbol, it is also possible to complete on   634 \<^verbatim>\<open>\sup\<close>, \<^verbatim>\<open>\sub\<close>, \<^verbatim>\<open>\bold\<close>, \<^verbatim>\<open>\emph\<close> as for regular symbols.   635   636 The emphasized style only takes effect in document output (when used with a   637 cartouche), but not in the editor.   638 \<close>   639   640   641 section \<open>Scala console \label{sec:scala-console}\<close>   642   643 text \<open>   644 The \<^emph>\<open>Console\<close> plugin manages various shells (command interpreters), e.g.\   645 \<^emph>\<open>BeanShell\<close>, which is the official jEdit scripting language, and the   646 cross-platform \<^emph>\<open>System\<close> shell. Thus the console provides similar   647 functionality than the Emacs buffers \<^verbatim>\<open>*scratch*\<close> and \<^verbatim>\<open>*shell*\<close>.   648   649 Isabelle/jEdit extends the repertoire of the console by \<^emph>\<open>Scala\<close>, which is   650 the regular Scala toplevel loop running inside the same JVM process as   651 Isabelle/jEdit itself. This means the Scala command interpreter has access   652 to the JVM name space and state of the running Prover IDE application. The   653 default environment imports the full content of packages \<^verbatim>\<open>isabelle\<close> and   654 \<^verbatim>\<open>isabelle.jedit\<close>.   655   656 For example, \<^verbatim>\<open>PIDE\<close> refers to the Isabelle/jEdit plugin object, and \<^verbatim>\<open>view\<close>   657 to the current editor view of jEdit. The Scala expression   658 \<^verbatim>\<open>PIDE.snapshot(view)\<close> makes a PIDE document snapshot of the current buffer   659 within the current editor view.   660   661 This helps to explore Isabelle/Scala functionality interactively. Some care   662 is required to avoid interference with the internals of the running   663 application.   664 \<close>   665   666   667 section \<open>File-system access\<close>   668   669 text \<open>   670 File specifications in jEdit follow various formats and conventions   671 according to \<^emph>\<open>Virtual File Systems\<close>, which may be also provided by   672 additional plugins. This allows to access remote files via the \<^verbatim>\<open>http:\<close>   673 protocol prefix, for example. Isabelle/jEdit attempts to work with the   674 file-system model of jEdit as far as possible. In particular, theory sources   675 are passed directly from the editor to the prover, without indirection via   676 physical files.   677   678 Despite the flexibility of URLs in jEdit, local files are particularly   679 important and are accessible without protocol prefix. The file path notation   680 is that of the Java Virtual Machine on the underlying platform. On Windows   681 the preferred form uses backslashes, but happens to accept forward slashes   682 like Unix/POSIX as well. Further differences arise due to Windows drive   683 letters and network shares.   684   685 The Java notation for files needs to be distinguished from the one of   686 Isabelle, which uses POSIX notation with forward slashes on \<^emph>\<open>all\<close>   687 platforms. Isabelle/ML on Windows uses Unix-style path notation, too, and   688 driver letter representation as in Cygwin (e.g.\ \<^verbatim>\<open>/cygdrive/c\<close>). Moreover,   689 environment variables from the Isabelle process may be used freely, e.g.\   690 \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> or \<^file>\<open>$POLYML_HOME/README\<close>. There are special   691 shortcuts: \<^dir>\<open>~\<close> for \<^dir>\<open>$USER_HOME\<close> and \<^dir>\<open>~~\<close> for \<^dir>\<open>$ISABELLE_HOME\<close>.   692   693 \<^medskip>   694 Since jEdit happens to support environment variables within file   695 specifications as well, it is natural to use similar notation within the   696 editor, e.g.\ in the file-browser. This does not work in full generality,   697 though, due to the bias of jEdit towards platform-specific notation and of   698 Isabelle towards POSIX. Moreover, the Isabelle settings environment is not   699 yet active when starting Isabelle/jEdit via its standard application   700 wrapper, in contrast to @{tool jedit} run from the command line   701 (\secref{sec:command-line}).   702   703 Isabelle/jEdit imitates important system settings within the Java process   704 environment, in order to allow easy access to these important places from   705 the editor: \<^verbatim>\<open>$ISABELLE_HOME\<close>, \<^verbatim>\<open>$ISABELLE_HOME_USER\<close>, \<^verbatim>\<open>$JEDIT_HOME\<close>,

   706   \<^verbatim>\<open>JEDIT_SETTINGS\<close>. The file browser of jEdit also includes \<^emph>\<open>Favorites\<close> for   707 these two important locations.   708   709 \<^medskip>   710 Path specifications in prover input or output usually include formal markup   711 that turns it into a hyperlink (see also \secref{sec:tooltips-hyperlinks}).   712 This allows to open the corresponding file in the text editor, independently   713 of the path notation. If the path refers to a directory, the jEdit file   714 browser is opened on it.   715   716 Formally checked paths in prover input are subject to completion   717 (\secref{sec:completion}): partial specifications are resolved via directory   718 content and possible completions are offered in a popup.   719 \<close>   720   721   722 section \<open>Indentation\<close>   723   724 text \<open>   725 Isabelle/jEdit augments the existing indentation facilities of jEdit to take   726 the structure of theory and proof texts into account. There is also special   727 support for unstructured proof scripts.   728   729 \<^descr>[Syntactic indentation] follows the outer syntax of Isabelle/Isar.   730   731 Action @{action "indent-lines"} (shortcut \<^verbatim>\<open>C+i\<close>) indents the current line   732 according to command keywords and some command substructure: this   733 approximation may need further manual tuning.   734   735 Action @{action "isabelle.newline"} (shortcut \<^verbatim>\<open>ENTER\<close>) indents the old   736 and the new line according to command keywords only: this leads to precise   737 alignment of the main Isar language elements. This depends on option   738 @{system_option_def "jedit_indent_newline"} (enabled by default).   739   740 Regular input (via keyboard or completion) indents the current line   741 whenever an new keyword is emerging at the start of the line. This depends   742 on option @{system_option_def "jedit_indent_input"} (enabled by default).   743   744 \<^descr>[Semantic indentation] adds additional white space to unstructured proof   745 scripts (\<^theory_text>\<open>apply\<close> etc.) via number of subgoals. This requires information   746 of ongoing document processing and may thus lag behind, when the user is   747 editing too quickly; see also option @{system_option_def   748 "jedit_script_indent"} and @{system_option_def   749 "jedit_script_indent_limit"}.   750   751 The above options are accessible in the menu \<^emph>\<open>Plugins / Plugin Options /   752 Isabelle / General\<close>. A prerequisite for advanced indentation is \<^emph>\<open>Utilities   753 / Buffer Options / Automatic indentation\<close>: it needs to be set to \<^verbatim>\<open>full\<close>   754 (default).   755 \<close>   756   757   758 section \<open>SideKick parsers \label{sec:sidekick}\<close>   759   760 text \<open>   761 The \<^emph>\<open>SideKick\<close> plugin provides some general services to display buffer   762 structure in a tree view. Isabelle/jEdit provides SideKick parsers for its   763 main mode for theory files, ML files, as well as some minor modes for the   764 \<^verbatim>\<open>NEWS\<close> file (see \figref{fig:sidekick}), session \<^verbatim>\<open>ROOT\<close> files, system   765 \<^verbatim>\<open>options\<close>, and Bib{\TeX} files (\secref{sec:bibtex}).   766   767 \begin{figure}[!htb]   768 \begin{center}   769 \includegraphics[scale=0.333]{sidekick}   770 \end{center}   771 \caption{The Isabelle NEWS file with SideKick tree view}   772 \label{fig:sidekick}   773 \end{figure}   774   775 The default SideKick parser for theory files is \<^verbatim>\<open>isabelle\<close>: it provides a   776 tree-view on the formal document structure, with section headings at the top   777 and formal specification elements at the bottom. The alternative parser   778 \<^verbatim>\<open>isabelle-context\<close> shows nesting of context blocks according to \<^theory_text>\<open>begin \<dots>   779 end\<close> structure.   780   781 \<^medskip>   782 Isabelle/ML files are structured according to semi-formal comments that are   783 explained in @{cite "isabelle-implementation"}. This outline is turned into   784 a tree-view by default, by using the \<^verbatim>\<open>isabelle-ml\<close> parser. There is also a   785 folding mode of the same name, for hierarchic text folds within ML files.   786   787 \<^medskip>   788 The special SideKick parser \<^verbatim>\<open>isabelle-markup\<close> exposes the uninterpreted   789 markup tree of the PIDE document model of the current buffer. This is   790 occasionally useful for informative purposes, but the amount of displayed   791 information might cause problems for large buffers.   792 \<close>   793   794   795 chapter \<open>Prover IDE functionality \label{sec:document-model}\<close>   796   797 section \<open>Document model \label{sec:document-model}\<close>   798   799 text \<open>   800 The document model is central to the PIDE architecture: the editor and the   801 prover have a common notion of structured source text with markup, which is   802 produced by formal processing. The editor is responsible for edits of   803 document source, as produced by the user. The prover is responsible for   804 reports of document markup, as produced by its processing in the background.   805   806 Isabelle/jEdit handles classic editor events of jEdit, in order to connect   807 the physical world of the GUI (with its singleton state) to the mathematical   808 world of multiple document versions (with timeless and stateless updates).   809 \<close>   810   811   812 subsection \<open>Editor buffers and document nodes \label{sec:buffer-node}\<close>   813   814 text \<open>   815 As a regular text editor, jEdit maintains a collection of \<^emph>\<open>buffers\<close> to   816 store text files; each buffer may be associated with any number of visible   817 \<^emph>\<open>text areas\<close>. Buffers are subject to an \<^emph>\<open>edit mode\<close> that is determined   818 from the file name extension. The following modes are treated specifically   819 in Isabelle/jEdit:   820   821 \<^medskip>   822 \begin{tabular}{lll}   823 \<^bold>\<open>mode\<close> & \<^bold>\<open>file name\<close> & \<^bold>\<open>content\<close> \\\hline   824 \<^verbatim>\<open>isabelle\<close> & \<^verbatim>\<open>*.thy\<close> & theory source \\   825 \<^verbatim>\<open>isabelle-ml\<close> & \<^verbatim>\<open>*.ML\<close> & Isabelle/ML source \\   826 \<^verbatim>\<open>sml\<close> & \<^verbatim>\<open>*.sml\<close> or \<^verbatim>\<open>*.sig\<close> & Standard ML source \\   827 \<^verbatim>\<open>isabelle-root\<close> & \<^verbatim>\<open>ROOT\<close> & session root \\   828 \<^verbatim>\<open>isabelle-options\<close> & & Isabelle options \\   829 \<^verbatim>\<open>isabelle-news\<close> & & Isabelle NEWS \\   830 \end{tabular}   831 \<^medskip>   832   833 All jEdit buffers are automatically added to the PIDE document-model as   834 \<^emph>\<open>document nodes\<close>. The overall document structure is defined by the theory   835 nodes in two dimensions:   836   837 \<^enum> via \<^bold>\<open>theory imports\<close> that are specified in the \<^emph>\<open>theory header\<close> using   838 concrete syntax of the @{command_ref theory} command @{cite   839 "isabelle-isar-ref"};   840   841 \<^enum> via \<^bold>\<open>auxiliary files\<close> that are included into a theory by \<^emph>\<open>load   842 commands\<close>, notably @{command_ref ML_file} and @{command_ref SML_file}   843 @{cite "isabelle-isar-ref"}.   844   845 In any case, source files are managed by the PIDE infrastructure: the   846 physical file-system only plays a subordinate role. The relevant version of   847 source text is passed directly from the editor to the prover, using internal   848 communication channels.   849 \<close>   850   851   852 subsection \<open>Theories \label{sec:theories}\<close>   853   854 text \<open>   855 The \<^emph>\<open>Theories\<close> panel (see also \figref{fig:theories}) provides an overview   856 of the status of continuous checking of theory nodes within the document   857 model.   858   859 \begin{figure}[!htb]   860 \begin{center}   861 \includegraphics[scale=0.333]{theories}   862 \end{center}   863 \caption{Theories panel with an overview of the document-model, and jEdit   864 text areas as editable views on some of the document nodes}   865 \label{fig:theories}   866 \end{figure}   867   868 Theory imports are resolved automatically by the PIDE document model: all   869 required files are loaded and stored internally, without the need to open   870 corresponding jEdit buffers. Opening or closing editor buffers later on has   871 no direct impact on the formal document content: it only affects visibility.   872   873 In contrast, auxiliary files (e.g.\ from @{command ML_file} commands) are   874 \<^emph>\<open>not\<close> resolved within the editor by default, but the prover process takes   875 care of that. This may be changed by enabling the system option   876 @{system_option jedit_auto_resolve}: it ensures that all files are uniformly   877 provided by the editor.   878   879 \<^medskip>   880 The visible \<^emph>\<open>perspective\<close> of Isabelle/jEdit is defined by the collective   881 view on theory buffers via open text areas. The perspective is taken as a   882 hint for document processing: the prover ensures that those parts of a   883 theory where the user is looking are checked, while other parts that are   884 presently not required are ignored. The perspective is changed by opening or   885 closing text area windows, or scrolling within a window.   886   887 The \<^emph>\<open>Theories\<close> panel provides some further options to influence the process   888 of continuous checking: it may be switched off globally to restrict the   889 prover to superficial processing of command syntax. It is also possible to   890 indicate theory nodes as \<^emph>\<open>required\<close> for continuous checking: this means   891 such nodes and all their imports are always processed independently of the   892 visibility status (if continuous checking is enabled). Big theory libraries   893 that are marked as required can have significant impact on performance!   894   895 The \<^emph>\<open>Purge\<close> button restricts the document model to theories that are   896 required for open editor buffers: inaccessible theories are removed and will   897 be rechecked when opened or imported later.   898   899 \<^medskip>   900 Formal markup of checked theory content is turned into GUI rendering, based   901 on a standard repertoire known from mainstream IDEs for programming   902 languages: colors, icons, highlighting, squiggly underlines, tooltips,   903 hyperlinks etc. For outer syntax of Isabelle/Isar there is some traditional   904 syntax-highlighting via static keywords and tokenization within the editor;   905 this buffer syntax is determined from theory imports. In contrast, the   906 painting of inner syntax (term language etc.)\ uses semantic information   907 that is reported dynamically from the logical context. Thus the prover can   908 provide additional markup to help the user to understand the meaning of   909 formal text, and to produce more text with some add-on tools (e.g.\   910 information messages with \<^emph>\<open>sendback\<close> markup by automated provers or   911 disprovers in the background). \<close>   912   913   914 subsection \<open>Auxiliary files \label{sec:aux-files}\<close>   915   916 text \<open>   917 Special load commands like @{command_ref ML_file} and @{command_ref   918 SML_file} @{cite "isabelle-isar-ref"} refer to auxiliary files within some   919 theory. Conceptually, the file argument of the command extends the theory   920 source by the content of the file, but its editor buffer may be loaded~/   921 changed~/ saved separately. The PIDE document model propagates changes of   922 auxiliary file content to the corresponding load command in the theory, to   923 update and process it accordingly: changes of auxiliary file content are   924 treated as changes of the corresponding load command.   925   926 \<^medskip>   927 As a concession to the massive amount of ML files in Isabelle/HOL itself,   928 the content of auxiliary files is only added to the PIDE document-model on   929 demand, the first time when opened explicitly in the editor. There are   930 further tricks to manage markup of ML files, such that Isabelle/HOL may be   931 edited conveniently in the Prover IDE on small machines with only 8\,GB of   932 main memory. Using \<^verbatim>\<open>Pure\<close> as logic session image, the exploration may start   933 at the top \<^file>\<open>ISABELLE_HOME/src/HOL/Main.thy\<close> or the bottom

   934   \<^file>\<open>$ISABELLE_HOME/src/HOL/HOL.thy\<close>, for example. It is also possible to   935 explore the Isabelle/Pure bootstrap process (a virtual copy) by opening   936 \<^file>\<open>$ISABELLE_HOME/src/Pure/ROOT.ML\<close> like a theory in the Prover IDE.

   937

   938   Initially, before an auxiliary file is opened in the editor, the prover

   939   reads its content from the physical file-system. After the file is opened

   940   for the first time in the editor, e.g.\ by following the hyperlink

   941   (\secref{sec:tooltips-hyperlinks}) for the argument of its @{command

   942   ML_file} command, the content is taken from the jEdit buffer.

   943

   944   The change of responsibility from prover to editor counts as an update of

   945   the document content, so subsequent theory sources need to be re-checked.

   946   When the buffer is closed, the responsibility remains to the editor: the

   947   file may be opened again without causing another document update.

   948

   949   A file that is opened in the editor, but its theory with the load command is

   950   not, is presently inactive in the document model. A file that is loaded via

   951   multiple load commands is associated to an arbitrary one: this situation is

   952   morally unsupported and might lead to confusion.

   953

   954   \<^medskip>

   955   Output that refers to an auxiliary file is combined with that of the

   956   corresponding load command, and shown whenever the file or the command are

   957   active (see also \secref{sec:output}).

   958

   959   Warnings, errors, and other useful markup is attached directly to the

   960   positions in the auxiliary file buffer, in the manner of standard IDEs. By

   961   using the load command @{command SML_file} as explained in

   962   \<^file>\<open>$ISABELLE_HOME/src/Tools/SML/Examples.thy\<close>, Isabelle/jEdit may be used as   963 fully-featured IDE for Standard ML, independently of theory or proof   964 development: the required theory merely serves as some kind of project file   965 for a collection of SML source modules.   966 \<close>   967   968   969 section \<open>Output \label{sec:output}\<close>   970   971 text \<open>   972 Prover output consists of \<^emph>\<open>markup\<close> and \<^emph>\<open>messages\<close>. Both are directly   973 attached to the corresponding positions in the original source text, and   974 visualized in the text area, e.g.\ as text colours for free and bound   975 variables, or as squiggly underlines for warnings, errors etc.\ (see also   976 \figref{fig:output}). In the latter case, the corresponding messages are   977 shown by hovering with the mouse over the highlighted text --- although in   978 many situations the user should already get some clue by looking at the   979 position of the text highlighting, without seeing the message body itself.   980   981 \begin{figure}[!htb]   982 \begin{center}   983 \includegraphics[scale=0.333]{output}   984 \end{center}   985 \caption{Multiple views on prover output: gutter with icon, text area with   986 popup, text overview column, \<^emph>\<open>Theories\<close> panel, \<^emph>\<open>Output\<close> panel}   987 \label{fig:output}   988 \end{figure}   989   990 The gutter'' on the left-hand-side of the text area uses icons to   991 provide a summary of the messages within the adjacent text line. Message   992 priorities are used to prefer errors over warnings, warnings over   993 information messages; other output is ignored.   994   995 The text overview column'' on the right-hand-side of the text area uses   996 similar information to paint small rectangles for the overall status of the   997 whole text buffer. The graphics is scaled to fit the logical buffer length   998 into the given window height. Mouse clicks on the overview area move the   999 cursor approximately to the corresponding text line in the buffer.   1000   1001 The \<^emph>\<open>Theories\<close> panel provides another course-grained overview, but without   1002 direct correspondence to text positions. The coloured rectangles represent   1003 the amount of messages of a certain kind (warnings, errors, etc.) and the   1004 execution status of commands. The border of each rectangle indicates the   1005 overall status of processing: a thick border means it is \<^emph>\<open>finished\<close> or   1006 \<^emph>\<open>failed\<close> (with color for errors). A double-click on one of the theory   1007 entries with their status overview opens the corresponding text buffer,   1008 without moving the cursor to a specific point.   1009   1010 \<^medskip>   1011 The \<^emph>\<open>Output\<close> panel displays prover messages that correspond to a given   1012 command, within a separate window. The cursor position in the presently   1013 active text area determines the prover command whose cumulative message   1014 output is appended and shown in that window (in canonical order according to   1015 the internal execution of the command). There are also control elements to   1016 modify the update policy of the output wrt.\ continued editor movements:   1017 \<^emph>\<open>Auto update\<close> and \<^emph>\<open>Update\<close>. This is particularly useful for multiple   1018 instances of the \<^emph>\<open>Output\<close> panel to look at different situations.   1019 Alternatively, the panel can be turned into a passive \<^emph>\<open>Info\<close> window via the   1020 \<^emph>\<open>Detach\<close> menu item.   1021   1022 Proof state is handled separately (\secref{sec:state-output}), but it is   1023 also possible to tick the corresponding checkbox to append it to regular   1024 output (\figref{fig:output-including-state}). This is a globally persistent   1025 option: it affects all open panels and future editor sessions.   1026   1027 \begin{figure}[!htb]   1028 \begin{center}   1029 \includegraphics[scale=0.333]{output-including-state}   1030 \end{center}   1031 \caption{Proof state display within the regular output panel}   1032 \label{fig:output-including-state}   1033 \end{figure}   1034   1035 \<^medskip>   1036 Following the IDE principle, regular messages are attached to the original   1037 source in the proper place and may be inspected on demand via popups. This   1038 excludes messages that are somehow internal to the machinery of proof   1039 checking, notably \<^emph>\<open>proof state\<close> and \<^emph>\<open>tracing\<close>.   1040   1041 In any case, the same display technology is used for small popups and big   1042 output windows. The formal text contains markup that may be explored   1043 recursively via further popups and hyperlinks (see   1044 \secref{sec:tooltips-hyperlinks}), or clicked directly to initiate certain   1045 actions (see \secref{sec:auto-tools} and \secref{sec:sledgehammer}).   1046 \<close>   1047   1048   1049 section \<open>Proof state \label{sec:state-output}\<close>   1050   1051 text \<open>   1052 The main purpose of the Prover IDE is to help the user editing proof   1053 documents, with ongoing formal checking by the prover in the background.   1054 This can be done to some extent in the main text area alone, especially for   1055 well-structured Isar proofs.   1056   1057 Nonetheless, internal proof state needs to be inspected in many situations   1058 of exploration and debugging''. The \<^emph>\<open>State\<close> panel shows exclusively such   1059 proof state messages without further distraction, while all other messages   1060 are displayed in \<^emph>\<open>Output\<close> (\secref{sec:output}).   1061 \Figref{fig:output-and-state} shows a typical GUI layout where both panels   1062 are open.   1063   1064 \begin{figure}[!htb]   1065 \begin{center}   1066 \includegraphics[scale=0.333]{output-and-state}   1067 \end{center}   1068 \caption{Separate proof state display (right) and other output (bottom).}   1069 \label{fig:output-and-state}   1070 \end{figure}   1071   1072 Another typical arrangement has more than one \<^emph>\<open>State\<close> panel open (as   1073 floating windows), with \<^emph>\<open>Auto update\<close> disabled to look at an old situation   1074 while the proof text in the vicinity is changed. The \<^emph>\<open>Update\<close> button   1075 triggers an explicit one-shot update; this operation is also available via   1076 the action @{action "isabelle.update-state"} (keyboard shortcut \<^verbatim>\<open>S+ENTER\<close>).   1077   1078 On small screens, it is occasionally useful to have all messages   1079 concatenated in the regular \<^emph>\<open>Output\<close> panel, e.g.\ see   1080 \figref{fig:output-including-state}.   1081   1082 \<^medskip>   1083 The mechanics of \<^emph>\<open>Output\<close> versus \<^emph>\<open>State\<close> are slightly different:   1084   1085 \<^item> \<^emph>\<open>Output\<close> shows information that is continuously produced and already   1086 present when the GUI wants to show it. This is implicitly controlled by   1087 the visible perspective on the text.   1088   1089 \<^item> \<^emph>\<open>State\<close> initiates a real-time query on demand, with a full round trip   1090 including a fresh print operation on the prover side. This is controlled   1091 explicitly when the cursor is moved to the next command (\<^emph>\<open>Auto update\<close>)   1092 or the \<^emph>\<open>Update\<close> operation is triggered.   1093   1094 This can make a difference in GUI responsibility and resource usage within   1095 the prover process. Applications with very big proof states that are only   1096 inspected in isolation work better with the \<^emph>\<open>State\<close> panel.   1097 \<close>   1098   1099   1100 section \<open>Query \label{sec:query}\<close>   1101   1102 text \<open>   1103 The \<^emph>\<open>Query\<close> panel provides various GUI forms to request extra information   1104 from the prover, as a replacement of old-style diagnostic commands like   1105 @{command find_theorems}. There are input fields and buttons for a   1106 particular query command, with output in a dedicated text area.   1107   1108 The main query modes are presented as separate tabs: \<^emph>\<open>Find Theorems\<close>,   1109 \<^emph>\<open>Find Constants\<close>, \<^emph>\<open>Print Context\<close>, e.g.\ see \figref{fig:query}. As usual   1110 in jEdit, multiple \<^emph>\<open>Query\<close> windows may be active at the same time: any   1111 number of floating instances, but at most one docked instance (which is used   1112 by default).   1113   1114 \begin{figure}[!htb]   1115 \begin{center}   1116 \includegraphics[scale=0.333]{query}   1117 \end{center}   1118 \caption{An instance of the Query panel: find theorems}   1119 \label{fig:query}   1120 \end{figure}   1121   1122 \<^medskip>   1123 The following GUI elements are common to all query modes:   1124   1125 \<^item> The spinning wheel provides feedback about the status of a pending query   1126 wrt.\ the evaluation of its context and its own operation.   1127   1128 \<^item> The \<^emph>\<open>Apply\<close> button attaches a fresh query invocation to the current   1129 context of the command where the cursor is pointing in the text.   1130   1131 \<^item> The \<^emph>\<open>Search\<close> field allows to highlight query output according to some   1132 regular expression, in the notation that is commonly used on the Java   1133 platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/javase/8/docs/api/java/util/regex/Pattern.html\<close>\<close>   1134 This may serve as an additional visual filter of the result.   1135   1136 \<^item> The \<^emph>\<open>Zoom\<close> box controls the font size of the output area.   1137   1138 All query operations are asynchronous: there is no need to wait for the   1139 evaluation of the document for the query context, nor for the query   1140 operation itself. Query output may be detached as independent \<^emph>\<open>Info\<close>   1141 window, using a menu operation of the dockable window manager. The printed   1142 result usually provides sufficient clues about the original query, with some   1143 hyperlink to its context (via markup of its head line).   1144 \<close>   1145   1146   1147 subsection \<open>Find theorems\<close>   1148   1149 text \<open>   1150 The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Theorems\<close> mode retrieves facts from the theory   1151 or proof context matching all of given criteria in the \<^emph>\<open>Find\<close> text field. A   1152 single criterion has the following syntax:   1153   1154 @{rail \<open>   1155 ('-'?) ('name' ':' @{syntax name} | 'intro' | 'elim' | 'dest' |   1156 'solves' | 'simp' ':' @{syntax term} | @{syntax term})   1157 \<close>}   1158   1159 See also the Isar command @{command_ref find_theorems} in @{cite   1160 "isabelle-isar-ref"}.   1161 \<close>   1162   1163   1164 subsection \<open>Find constants\<close>   1165   1166 text \<open>   1167 The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Constants\<close> mode prints all constants whose type   1168 meets all of the given criteria in the \<^emph>\<open>Find\<close> text field. A single   1169 criterion has the following syntax:   1170   1171 @{rail \<open>   1172 ('-'?)   1173 ('name' ':' @{syntax name} | 'strict' ':' @{syntax type} | @{syntax type})   1174 \<close>}   1175   1176 See also the Isar command @{command_ref find_consts} in @{cite   1177 "isabelle-isar-ref"}.   1178 \<close>   1179   1180   1181 subsection \<open>Print context\<close>   1182   1183 text \<open>   1184 The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Print Context\<close> mode prints information from the   1185 theory or proof context, or proof state. See also the Isar commands   1186 @{command_ref print_context}, @{command_ref print_cases}, @{command_ref   1187 print_term_bindings}, @{command_ref print_theorems}, described in @{cite   1188 "isabelle-isar-ref"}.   1189 \<close>   1190   1191   1192 section \<open>Tooltips and hyperlinks \label{sec:tooltips-hyperlinks}\<close>   1193   1194 text \<open>   1195 Formally processed text (prover input or output) contains rich markup that   1196 can be explored by using the \<^verbatim>\<open>CONTROL\<close> modifier key on Linux and Windows,   1197 or \<^verbatim>\<open>COMMAND\<close> on Mac OS X. Hovering with the mouse while the modifier is   1198 pressed reveals a \<^emph>\<open>tooltip\<close> (grey box over the text with a yellow popup)   1199 and/or a \<^emph>\<open>hyperlink\<close> (black rectangle over the text with change of mouse   1200 pointer); see also \figref{fig:tooltip}.   1201   1202 \begin{figure}[!htb]   1203 \begin{center}   1204 \includegraphics[scale=0.5]{popup1}   1205 \end{center}   1206 \caption{Tooltip and hyperlink for some formal entity}   1207 \label{fig:tooltip}   1208 \end{figure}   1209   1210 Tooltip popups use the same rendering technology as the main text area, and   1211 further tooltips and/or hyperlinks may be exposed recursively by the same   1212 mechanism; see \figref{fig:nested-tooltips}.   1213   1214 \begin{figure}[!htb]   1215 \begin{center}   1216 \includegraphics[scale=0.5]{popup2}   1217 \end{center}   1218 \caption{Nested tooltips over formal entities}   1219 \label{fig:nested-tooltips}   1220 \end{figure}   1221   1222 The tooltip popup window provides some controls to \<^emph>\<open>close\<close> or \<^emph>\<open>detach\<close> the   1223 window, turning it into a separate \<^emph>\<open>Info\<close> window managed by jEdit. The   1224 \<^verbatim>\<open>ESCAPE\<close> key closes \<^emph>\<open>all\<close> popups, which is particularly relevant when   1225 nested tooltips are stacking up.   1226   1227 \<^medskip>   1228 A black rectangle in the text indicates a hyperlink that may be followed by   1229 a mouse click (while the \<^verbatim>\<open>CONTROL\<close> or \<^verbatim>\<open>COMMAND\<close> modifier key is still   1230 pressed). Such jumps to other text locations are recorded by the   1231 \<^emph>\<open>Navigator\<close> plugin, which is bundled with Isabelle/jEdit and enabled by   1232 default. There are usually navigation arrows in the main jEdit toolbar.   1233   1234 Note that the link target may be a file that is itself not subject to formal   1235 document processing of the editor session and thus prevents further   1236 exploration: the chain of hyperlinks may end in some source file of the   1237 underlying logic image, or within the ML bootstrap sources of Isabelle/Pure.   1238 \<close>   1239   1240   1241 section \<open>Formal scopes and semantic selection\<close>   1242   1243 text \<open>   1244 Formal entities are semantically annotated in the source text as explained   1245 in \secref{sec:tooltips-hyperlinks}. A \<^emph>\<open>formal scope\<close> consists of the   1246 defining position with all its referencing positions. This correspondence is   1247 highlighted in the text according to the cursor position, see also   1248 \figref{fig:scope1}. Here the referencing positions are rendered with an   1249 additional border, in reminiscence to a hyperlink: clicking there moves the   1250 cursor to the original defining position.   1251   1252 \begin{figure}[!htb]   1253 \begin{center}   1254 \includegraphics[scale=0.5]{scope1}   1255 \end{center}   1256 \caption{Scope of formal entity: defining vs.\ referencing positions}   1257 \label{fig:scope1}   1258 \end{figure}   1259   1260 The action @{action_def "isabelle.select-entity"} (shortcut \<^verbatim>\<open>CS+ENTER\<close>)   1261 supports semantic selection of all occurrences of the formal entity at the   1262 caret position. This facilitates systematic renaming, using regular jEdit   1263 editing of a multi-selection, see also \figref{fig:scope2}.   1264   1265 \begin{figure}[!htb]   1266 \begin{center}   1267 \includegraphics[scale=0.5]{scope2}   1268 \end{center}   1269 \caption{The result of semantic selection and systematic renaming}   1270 \label{fig:scope2}   1271 \end{figure}   1272 \<close>   1273   1274   1275 section \<open>Completion \label{sec:completion}\<close>   1276   1277 text \<open>   1278 Smart completion of partial input is the IDE functionality \<^emph>\<open>par   1279 excellance\<close>. Isabelle/jEdit combines several sources of information to   1280 achieve that. Despite its complexity, it should be possible to get some idea   1281 how completion works by experimentation, based on the overview of completion   1282 varieties in \secref{sec:completion-varieties}. The remaining subsections   1283 explain concepts around completion more systematically.   1284   1285 \<^medskip>   1286 \<^emph>\<open>Explicit completion\<close> is triggered by the action @{action_ref   1287 "isabelle.complete"}, which is bound to the keyboard shortcut \<^verbatim>\<open>C+b\<close>, and   1288 thus overrides the jEdit default for @{action_ref "complete-word"}.   1289   1290 \<^emph>\<open>Implicit completion\<close> hooks into the regular keyboard input stream of the   1291 editor, with some event filtering and optional delays.   1292   1293 \<^medskip>   1294 Completion options may be configured in \<^emph>\<open>Plugin Options~/ Isabelle~/   1295 General~/ Completion\<close>. These are explained in further detail below, whenever   1296 relevant. There is also a summary of options in   1297 \secref{sec:completion-options}.   1298   1299 The asynchronous nature of PIDE interaction means that information from the   1300 prover is delayed --- at least by a full round-trip of the document update   1301 protocol. The default options already take this into account, with a   1302 sufficiently long completion delay to speculate on the availability of all   1303 relevant information from the editor and the prover, before completing text   1304 immediately or producing a popup. Although there is an inherent danger of   1305 non-deterministic behaviour due to such real-time parameters, the general   1306 completion policy aims at determined results as far as possible.   1307 \<close>   1308   1309   1310 subsection \<open>Varieties of completion \label{sec:completion-varieties}\<close>   1311   1312 subsubsection \<open>Built-in templates\<close>   1313   1314 text \<open>   1315 Isabelle is ultimately a framework of nested sub-languages of different   1316 kinds and purposes. The completion mechanism supports this by the following   1317 built-in templates:   1318   1319 \<^descr> \<^verbatim>\<open>\<close> (single ASCII back-quote) or \<^verbatim>\<open>"\<close> (double ASCII quote) support   1320 \<^emph>\<open>quotations\<close> via text cartouches. There are three selections, which are   1321 always presented in the same order and do not depend on any context   1322 information. The default choice produces a template \<open>\<open>\<box>\<close>\<close>'', where the   1323 box indicates the cursor position after insertion; the other choices help   1324 to repair the block structure of unbalanced text cartouches.   1325   1326 \<^descr> \<^verbatim>\<open>@{\<close> is completed to the template \<open>@{\<box>}\<close>'', where the box indicates   1327 the cursor position after insertion. Here it is convenient to use the   1328 wildcard \<^verbatim>\<open>__\<close>'' or a more specific name prefix to let semantic   1329 completion of name-space entries propose antiquotation names.   1330   1331 With some practice, input of quoted sub-languages and antiquotations of   1332 embedded languages should work fluently. Note that national keyboard layouts   1333 might cause problems with back-quote as dead key, but double quote can be   1334 used instead.   1335 \<close>   1336   1337   1338 subsubsection \<open>Syntax keywords\<close>   1339   1340 text \<open>   1341 Syntax completion tables are determined statically from the keywords of the   1342 outer syntax'' of the underlying edit mode: for theory files this is the   1343 syntax of Isar commands according to the cumulative theory imports.   1344   1345 Keywords are usually plain words, which means the completion mechanism only   1346 inserts them directly into the text for explicit completion   1347 (\secref{sec:completion-input}), but produces a popup   1348 (\secref{sec:completion-popup}) otherwise.   1349   1350 At the point where outer syntax keywords are defined, it is possible to   1351 specify an alternative replacement string to be inserted instead of the   1352 keyword itself. An empty string means to suppress the keyword altogether,   1353 which is occasionally useful to avoid confusion, e.g.\ the rare keyword   1354 @{command simproc_setup} vs.\ the frequent name-space entry \<open>simp\<close>.   1355 \<close>   1356   1357   1358 subsubsection \<open>Isabelle symbols\<close>   1359   1360 text \<open>   1361 The completion tables for Isabelle symbols (\secref{sec:symbols}) are   1362 determined statically from \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and @{path

  1363   "$ISABELLE_HOME_USER/etc/symbols"} for each symbol specification as follows:   1364   1365 \<^medskip>   1366 \begin{tabular}{ll}   1367 \<^bold>\<open>completion entry\<close> & \<^bold>\<open>example\<close> \\\hline   1368 literal symbol & \<^verbatim>\<open>\<forall>\<close> \\   1369 symbol name with backslash & \<^verbatim>\<open>\\<close>\<^verbatim>\<open>forall\<close> \\   1370 symbol abbreviation & \<^verbatim>\<open>ALL\<close> or \<^verbatim>\<open>!\<close> \\   1371 \end{tabular}   1372 \<^medskip>   1373   1374 When inserted into the text, the above examples all produce the same Unicode   1375 rendering \<open>\<forall>\<close> of the underlying symbol \<^verbatim>\<open>\<forall>\<close>.   1376   1377 A symbol abbreviation that is a plain word, like \<^verbatim>\<open>ALL\<close>, is treated like a   1378 syntax keyword. Non-word abbreviations like \<^verbatim>\<open>-->\<close> are inserted more   1379 aggressively, except for single-character abbreviations like \<^verbatim>\<open>!\<close> above.   1380   1381 Completion via abbreviations like \<^verbatim>\<open>ALL\<close> or \<^verbatim>\<open>-->\<close> depends on the semantic   1382 language context (\secref{sec:completion-context}). In contrast, backslash   1383 sequences like \<^verbatim>\<open>\forall\<close> \<^verbatim>\<open>\<forall>\<close> are always possible, but require additional   1384 interaction to confirm (via popup). This is important in ambiguous   1385 situations, e.g.\ for Isabelle document source, which may contain formal   1386 symbols or informal {\LaTeX} macros. Backslash sequences also help when   1387 input is broken, and thus escapes its normal semantic context: e.g.\   1388 antiquotations or string literals in ML, which do not allow arbitrary   1389 backslash sequences.   1390   1391 Special symbols like \<^verbatim>\<open>\<comment>\<close> or control symbols like \<^verbatim>\<open>\<^cancel>\<close>,   1392 \<^verbatim>\<open>\<^latex>\<close>, \<^verbatim>\<open>\<^binding>\<close> can have an argument: completing on a name   1393 prefix offers a template with an empty cartouche. Thus completion of \<^verbatim>\<open>\co\<close>   1394 or \<^verbatim>\<open>\ca\<close> allows to compose formal document comments quickly.\<^footnote>\<open>It is   1395 customary to put a space between \<^verbatim>\<open>\<comment>\<close> and its argument, while   1396 control symbols do \<^emph>\<open>not\<close> allow extra space here.\<close>   1397 \<close>   1398   1399   1400 subsubsection \<open>User-defined abbreviations\<close>   1401   1402 text \<open>   1403 The theory header syntax supports abbreviations via the \<^theory_text>\<open>abbrevs\<close> keyword   1404 @{cite "isabelle-isar-ref"}. This is a slight generalization of built-in   1405 templates and abbreviations for Isabelle symbols, as explained above.   1406 Examples may be found in the Isabelle sources, by searching for   1407 \<^verbatim>\<open>abbrevs\<close>'' in \<^verbatim>\<open>*.thy\<close> files.   1408   1409 The \<^emph>\<open>Symbols\<close> panel shows the abbreviations that are available in the   1410 current theory buffer (according to its \<^theory_text>\<open>imports\<close>) in the \<^verbatim>\<open>Abbrevs\<close> tab.   1411 \<close>   1412   1413   1414 subsubsection \<open>Name-space entries\<close>   1415   1416 text \<open>   1417 This is genuine semantic completion, using information from the prover, so   1418 it requires some delay. A \<^emph>\<open>failed name-space lookup\<close> produces an error   1419 message that is annotated with a list of alternative names that are legal.   1420 The list of results is truncated according to the system option   1421 @{system_option_ref completion_limit}. The completion mechanism takes this   1422 into account when collecting information on the prover side.   1423   1424 Already recognized names are \<^emph>\<open>not\<close> completed further, but completion may be   1425 extended by appending a suffix of underscores. This provokes a failed   1426 lookup, and another completion attempt while ignoring the underscores. For   1427 example, in a name space where \<^verbatim>\<open>foo\<close> and \<^verbatim>\<open>foobar\<close> are known, the input   1428 \<^verbatim>\<open>foo\<close> remains unchanged, but \<^verbatim>\<open>foo_\<close> may be completed to \<^verbatim>\<open>foo\<close> or   1429 \<^verbatim>\<open>foobar\<close>.   1430   1431 The special identifier \<^verbatim>\<open>__\<close>'' serves as a wild-card for arbitrary   1432 completion: it exposes the name-space content to the completion mechanism   1433 (truncated according to @{system_option completion_limit}). This is   1434 occasionally useful to explore an unknown name-space, e.g.\ in some   1435 template.   1436 \<close>   1437   1438   1439 subsubsection \<open>File-system paths\<close>   1440   1441 text \<open>   1442 Depending on prover markup about file-system paths in the source text, e.g.\   1443 for the argument of a load command (\secref{sec:aux-files}), the completion   1444 mechanism explores the directory content and offers the result as completion   1445 popup. Relative path specifications are understood wrt.\ the \<^emph>\<open>master   1446 directory\<close> of the document node (\secref{sec:buffer-node}) of the enclosing   1447 editor buffer; this requires a proper theory, not an auxiliary file.   1448   1449 A suffix of slashes may be used to continue the exploration of an already   1450 recognized directory name.   1451 \<close>   1452   1453   1454 subsubsection \<open>Spell-checking\<close>   1455   1456 text \<open>   1457 The spell-checker combines semantic markup from the prover (regions of plain   1458 words) with static dictionaries (word lists) that are known to the editor.   1459   1460 Unknown words are underlined in the text, using @{system_option_ref   1461 spell_checker_color} (blue by default). This is not an error, but a hint to   1462 the user that some action may be taken. The jEdit context menu provides   1463 various actions, as far as applicable:   1464   1465 \<^medskip>   1466 \begin{tabular}{l}   1467 @{action_ref "isabelle.complete-word"} \\   1468 @{action_ref "isabelle.exclude-word"} \\   1469 @{action_ref "isabelle.exclude-word-permanently"} \\   1470 @{action_ref "isabelle.include-word"} \\   1471 @{action_ref "isabelle.include-word-permanently"} \\   1472 \end{tabular}   1473 \<^medskip>   1474   1475 Instead of the specific @{action_ref "isabelle.complete-word"}, it is also   1476 possible to use the generic @{action_ref "isabelle.complete"} with its   1477 default keyboard shortcut \<^verbatim>\<open>C+b\<close>.   1478   1479 \<^medskip>   1480 Dictionary lookup uses some educated guesses about lower-case, upper-case,   1481 and capitalized words. This is oriented on common use in English, where this   1482 aspect is not decisive for proper spelling (in contrast to German, for   1483 example).   1484 \<close>   1485   1486   1487 subsection \<open>Semantic completion context \label{sec:completion-context}\<close>   1488   1489 text \<open>   1490 Completion depends on a semantic context that is provided by the prover,   1491 although with some delay, because at least a full PIDE protocol round-trip   1492 is required. Until that information becomes available in the PIDE   1493 document-model, the default context is given by the outer syntax of the   1494 editor mode (see also \secref{sec:buffer-node}).   1495   1496 The semantic \<^emph>\<open>language context\<close> provides information about nested   1497 sub-languages of Isabelle: keywords are only completed for outer syntax, and   1498 antiquotations for languages that support them. Symbol abbreviations only   1499 work for specific sub-languages: e.g.\ \<^verbatim>\<open>=>\<close>'' is \<^emph>\<open>not\<close> completed in   1500 regular ML source, but is completed within ML strings, comments,   1501 antiquotations. Backslash representations of symbols like \<^verbatim>\<open>\foobar\<close>'' or   1502 \<^verbatim>\<open>\<foobar>\<close>'' work in any context --- after additional confirmation.   1503   1504 The prover may produce \<^emph>\<open>no completion\<close> markup in exceptional situations, to   1505 tell that some language keywords should be excluded from further completion   1506 attempts. For example, \<^verbatim>\<open>:\<close>'' within accepted Isar syntax looses its   1507 meaning as abbreviation for symbol \<open>\<in>\<close>''.   1508 \<close>   1509   1510   1511 subsection \<open>Input events \label{sec:completion-input}\<close>   1512   1513 text \<open>   1514 Completion is triggered by certain events produced by the user, with   1515 optional delay after keyboard input according to @{system_option   1516 jedit_completion_delay}.   1517   1518 \<^descr>[Explicit completion] works via action @{action_ref "isabelle.complete"}   1519 with keyboard shortcut \<^verbatim>\<open>C+b\<close>. This overrides the shortcut for @{action_ref   1520 "complete-word"} in jEdit, but it is possible to restore the original jEdit   1521 keyboard mapping of @{action "complete-word"} via \<^emph>\<open>Global Options~/   1522 Shortcuts\<close> and invent a different one for @{action "isabelle.complete"}.   1523   1524 \<^descr>[Explicit spell-checker completion] works via @{action_ref   1525 "isabelle.complete-word"}, which is exposed in the jEdit context menu, if   1526 the mouse points to a word that the spell-checker can complete.   1527   1528 \<^descr>[Implicit completion] works via regular keyboard input of the editor. It   1529 depends on further side-conditions:   1530   1531 \<^enum> The system option @{system_option_ref jedit_completion} needs to be   1532 enabled (default).   1533   1534 \<^enum> Completion of syntax keywords requires at least 3 relevant characters in   1535 the text.   1536   1537 \<^enum> The system option @{system_option_ref jedit_completion_delay} determines   1538 an additional delay (0.5 by default), before opening a completion popup.   1539 The delay gives the prover a chance to provide semantic completion   1540 information, notably the context (\secref{sec:completion-context}).   1541   1542 \<^enum> The system option @{system_option_ref jedit_completion_immediate}   1543 (enabled by default) controls whether replacement text should be inserted   1544 immediately without popup, regardless of @{system_option   1545 jedit_completion_delay}. This aggressive mode of completion is restricted   1546 to symbol abbreviations that are not plain words (\secref{sec:symbols}).   1547   1548 \<^enum> Completion of symbol abbreviations with only one relevant character in   1549 the text always enforces an explicit popup, regardless of   1550 @{system_option_ref jedit_completion_immediate}.   1551 \<close>   1552   1553   1554 subsection \<open>Completion popup \label{sec:completion-popup}\<close>   1555   1556 text \<open>   1557 A \<^emph>\<open>completion popup\<close> is a minimally invasive GUI component over the text   1558 area that offers a selection of completion items to be inserted into the   1559 text, e.g.\ by mouse clicks. Items are sorted dynamically, according to the   1560 frequency of selection, with persistent history. The popup may interpret   1561 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>,   1562 \<^verbatim>\<open>PAGE_DOWN\<close>, but all other key events are passed to the underlying text   1563 area. This allows to ignore unwanted completions most of the time and   1564 continue typing quickly. Thus the popup serves as a mechanism of   1565 confirmation of proposed items, while the default is to continue without   1566 completion.   1567   1568 The meaning of special keys is as follows:   1569   1570 \<^medskip>   1571 \begin{tabular}{ll}   1572 \<^bold>\<open>key\<close> & \<^bold>\<open>action\<close> \\\hline   1573 \<^verbatim>\<open>ENTER\<close> & select completion (if @{system_option jedit_completion_select_enter}) \\   1574 \<^verbatim>\<open>TAB\<close> & select completion (if @{system_option jedit_completion_select_tab}) \\   1575 \<^verbatim>\<open>ESCAPE\<close> & dismiss popup \\   1576 \<^verbatim>\<open>UP\<close> & move up one item \\   1577 \<^verbatim>\<open>DOWN\<close> & move down one item \\   1578 \<^verbatim>\<open>PAGE_UP\<close> & move up one page of items \\   1579 \<^verbatim>\<open>PAGE_DOWN\<close> & move down one page of items \\   1580 \end{tabular}   1581 \<^medskip>   1582   1583 Movement within the popup is only active for multiple items. Otherwise the   1584 corresponding key event retains its standard meaning within the underlying   1585 text area.   1586 \<close>   1587   1588   1589 subsection \<open>Insertion \label{sec:completion-insert}\<close>   1590   1591 text \<open>   1592 Completion may first propose replacements to be selected (via a popup), or   1593 replace text immediately in certain situations and depending on certain   1594 options like @{system_option jedit_completion_immediate}. In any case,   1595 insertion works uniformly, by imitating normal jEdit text insertion,   1596 depending on the state of the \<^emph>\<open>text selection\<close>. Isabelle/jEdit tries to   1597 accommodate the most common forms of advanced selections in jEdit, but not   1598 all combinations make sense. At least the following important cases are   1599 well-defined:   1600   1601 \<^descr>[No selection.] The original is removed and the replacement inserted,   1602 depending on the caret position.   1603   1604 \<^descr>[Rectangular selection of zero width.] This special case is treated by   1605 jEdit as tall caret'' and insertion of completion imitates its normal   1606 behaviour: separate copies of the replacement are inserted for each line   1607 of the selection.   1608   1609 \<^descr>[Other rectangular selection or multiple selections.] Here the original   1610 is removed and the replacement is inserted for each line (or segment) of   1611 the selection.   1612   1613 Support for multiple selections is particularly useful for \<^emph>\<open>HyperSearch\<close>:   1614 clicking on one of the items in the \<^emph>\<open>HyperSearch Results\<close> window makes   1615 jEdit select all its occurrences in the corresponding line of text. Then   1616 explicit completion can be invoked via \<^verbatim>\<open>C+b\<close>, e.g.\ to replace occurrences   1617 of \<^verbatim>\<open>-->\<close> by \<open>\<longrightarrow>\<close>.   1618   1619 \<^medskip>   1620 Insertion works by removing and inserting pieces of text from the buffer.   1621 This counts as one atomic operation on the jEdit history. Thus unintended   1622 completions may be reverted by the regular @{action undo} action of jEdit.   1623 According to normal jEdit policies, the recovered text after @{action undo}   1624 is selected: \<^verbatim>\<open>ESCAPE\<close> is required to reset the selection and to continue   1625 typing more text.   1626 \<close>   1627   1628   1629 subsection \<open>Options \label{sec:completion-options}\<close>   1630   1631 text \<open>   1632 This is a summary of Isabelle/Scala system options that are relevant for   1633 completion. They may be configured in \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>   1634 as usual.   1635   1636 \<^item> @{system_option_def completion_limit} specifies the maximum number of   1637 items for various semantic completion operations (name-space entries etc.)   1638   1639 \<^item> @{system_option_def jedit_completion} guards implicit completion via   1640 regular jEdit key events (\secref{sec:completion-input}): it allows to   1641 disable implicit completion altogether.   1642   1643 \<^item> @{system_option_def jedit_completion_select_enter} and @{system_option_def   1644 jedit_completion_select_tab} enable keys to select a completion item from   1645 the popup (\secref{sec:completion-popup}). Note that a regular mouse click   1646 on the list of items is always possible.   1647   1648 \<^item> @{system_option_def jedit_completion_context} specifies whether the   1649 language context provided by the prover should be used at all. Disabling   1650 that option makes completion less semantic''. Note that incomplete or   1651 severely broken input may cause some disagreement of the prover and the user   1652 about the intended language context.   1653   1654 \<^item> @{system_option_def jedit_completion_delay} and @{system_option_def   1655 jedit_completion_immediate} determine the handling of keyboard events for   1656 implicit completion (\secref{sec:completion-input}).   1657   1658 A @{system_option jedit_completion_delay}~\<^verbatim>\<open>> 0\<close> postpones the processing of   1659 key events, until after the user has stopped typing for the given time span,   1660 but @{system_option jedit_completion_immediate}~\<^verbatim>\<open>= true\<close> means that   1661 abbreviations of Isabelle symbols are handled nonetheless.   1662   1663 \<^item> @{system_option_def completion_path_ignore} specifies glob''   1664 patterns to ignore in file-system path completion (separated by colons),   1665 e.g.\ backup files ending with tilde.   1666   1667 \<^item> @{system_option_def spell_checker} is a global guard for all spell-checker   1668 operations: it allows to disable that mechanism altogether.   1669   1670 \<^item> @{system_option_def spell_checker_dictionary} determines the current   1671 dictionary, taken from the colon-separated list in the settings variable   1672 @{setting_def JORTHO_DICTIONARIES}. There are jEdit actions to specify local   1673 updates to a dictionary, by including or excluding words. The result of   1674 permanent dictionary updates is stored in the directory @{path   1675 "$ISABELLE_HOME_USER/dictionaries"}, in a separate file for each dictionary.

  1676

  1677   \<^item> @{system_option_def spell_checker_include} specifies a comma-separated

  1678   list of markup elements that delimit words in the source that is subject to

  1679   spell-checking, including various forms of comments.

  1680

  1681   \<^item> @{system_option_def spell_checker_exclude} specifies a comma-separated

  1682   list of markup elements that disable spell-checking (e.g.\ in nested

  1683   antiquotations).

  1684 \<close>

  1685

  1686

  1687 section \<open>Automatically tried tools \label{sec:auto-tools}\<close>

  1688

  1689 text \<open>

  1690   Continuous document processing works asynchronously in the background.

  1691   Visible document source that has been evaluated may get augmented by

  1692   additional results of \<^emph>\<open>asynchronous print functions\<close>. An example for that

  1693   is proof state output, if that is enabled in the Output panel

  1694   (\secref{sec:output}). More heavy-weight print functions may be applied as

  1695   well, e.g.\ to prove or disprove parts of the formal text by other means.

  1696

  1697   Isabelle/HOL provides various automatically tried tools that operate on

  1698   outermost goal statements (e.g.\ @{command lemma}, @{command theorem}),

  1699   independently of the state of the current proof attempt. They work

  1700   implicitly without any arguments. Results are output as \<^emph>\<open>information

  1701   messages\<close>, which are indicated in the text area by blue squiggles and a blue

  1702   information sign in the gutter (see \figref{fig:auto-tools}). The message

  1703   content may be shown as for other output (see also \secref{sec:output}).

  1704   Some tools produce output with \<^emph>\<open>sendback\<close> markup, which means that clicking

  1705   on certain parts of the text inserts that into the source in the proper

  1706   place.

  1707

  1708   \begin{figure}[!htb]

  1709   \begin{center}

  1710   \includegraphics[scale=0.333]{auto-tools}

  1711   \end{center}

  1712   \caption{Result of automatically tried tools}

  1713   \label{fig:auto-tools}

  1714   \end{figure}

  1715

  1716   \<^medskip>

  1717   The following Isabelle system options control the behavior of automatically

  1718   tried tools (see also the jEdit dialog window \<^emph>\<open>Plugin Options~/ Isabelle~/

  1719   General~/ Automatically tried tools\<close>):

  1720

  1721   \<^item> @{system_option_ref auto_methods} controls automatic use of a combination

  1722   of standard proof methods (@{method auto}, @{method simp}, @{method blast},

  1723   etc.). This corresponds to the Isar command @{command_ref "try0"} @{cite

  1724   "isabelle-isar-ref"}.

  1725

  1726   The tool is disabled by default, since unparameterized invocation of

  1727   standard proof methods often consumes substantial CPU resources without

  1728   leading to success.

  1729

  1730   \<^item> @{system_option_ref auto_nitpick} controls a slightly reduced version of

  1731   @{command_ref nitpick}, which tests for counterexamples using first-order

  1732   relational logic. See also the Nitpick manual @{cite "isabelle-nitpick"}.

  1733

  1734   This tool is disabled by default, due to the extra overhead of invoking an

  1735   external Java process for each attempt to disprove a subgoal.

  1736

  1737   \<^item> @{system_option_ref auto_quickcheck} controls automatic use of

  1738   @{command_ref quickcheck}, which tests for counterexamples using a series of

  1739   assignments for free variables of a subgoal.

  1740

  1741   This tool is \<^emph>\<open>enabled\<close> by default. It requires little overhead, but is a

  1742   bit weaker than @{command nitpick}.

  1743

  1744   \<^item> @{system_option_ref auto_sledgehammer} controls a significantly reduced

  1745   version of @{command_ref sledgehammer}, which attempts to prove a subgoal

  1746   using external automatic provers. See also the Sledgehammer manual @{cite

  1747   "isabelle-sledgehammer"}.

  1748

  1749   This tool is disabled by default, due to the relatively heavy nature of

  1750   Sledgehammer.

  1751

  1752   \<^item> @{system_option_ref auto_solve_direct} controls automatic use of

  1753   @{command_ref solve_direct}, which checks whether the current subgoals can

  1754   be solved directly by an existing theorem. This also helps to detect

  1755   duplicate lemmas.

  1756

  1757   This tool is \<^emph>\<open>enabled\<close> by default.

  1758

  1759

  1760   Invocation of automatically tried tools is subject to some global policies

  1761   of parallel execution, which may be configured as follows:

  1762

  1763   \<^item> @{system_option_ref auto_time_limit} (default 2.0) determines the timeout

  1764   (in seconds) for each tool execution.

  1765

  1766   \<^item> @{system_option_ref auto_time_start} (default 1.0) determines the start

  1767   delay (in seconds) for automatically tried tools, after the main command

  1768   evaluation is finished.

  1769

  1770

  1771   Each tool is submitted independently to the pool of parallel execution tasks

  1772   in Isabelle/ML, using hardwired priorities according to its relative

  1773   heaviness''. The main stages of evaluation and printing of proof states

  1774   take precedence, but an already running tool is not canceled and may thus

  1775   reduce reactivity of proof document processing.

  1776

  1777   Users should experiment how the available CPU resources (number of cores)

  1778   are best invested to get additional feedback from prover in the background,

  1779   by using a selection of weaker or stronger tools.

  1780 \<close>

  1781

  1782

  1783 section \<open>Sledgehammer \label{sec:sledgehammer}\<close>

  1784

  1785 text \<open>

  1786   The \<^emph>\<open>Sledgehammer\<close> panel (\figref{fig:sledgehammer}) provides a view on

  1787   some independent execution of the Isar command @{command_ref sledgehammer},

  1788   with process indicator (spinning wheel) and GUI elements for important

  1789   Sledgehammer arguments and options. Any number of Sledgehammer panels may be

  1790   active, according to the standard policies of Dockable Window Management in

  1791   jEdit. Closing such windows also cancels the corresponding prover tasks.

  1792

  1793   \begin{figure}[!htb]

  1794   \begin{center}

  1795   \includegraphics[scale=0.333]{sledgehammer}

  1796   \end{center}

  1797   \caption{An instance of the Sledgehammer panel}

  1798   \label{fig:sledgehammer}

  1799   \end{figure}

  1800

  1801   The \<^emph>\<open>Apply\<close> button attaches a fresh invocation of @{command sledgehammer}

  1802   to the command where the cursor is pointing in the text --- this should be

  1803   some pending proof problem. Further buttons like \<^emph>\<open>Cancel\<close> and \<^emph>\<open>Locate\<close>

  1804   help to manage the running process.

  1805

  1806   Results appear incrementally in the output window of the panel. Proposed

  1807   proof snippets are marked-up as \<^emph>\<open>sendback\<close>, which means a single mouse

  1808   click inserts the text into a suitable place of the original source. Some

  1809   manual editing may be required nonetheless, say to remove earlier proof

  1810   attempts.

  1811 \<close>

  1812

  1813

  1814 chapter \<open>Isabelle document preparation\<close>

  1815

  1816 text \<open>

  1817   The ultimate purpose of Isabelle is to produce nicely rendered documents

  1818   with the Isabelle document preparation system, which is based on {\LaTeX};

  1819   see also @{cite "isabelle-system" and "isabelle-isar-ref"}. Isabelle/jEdit

  1820   provides some additional support for document editing.

  1821 \<close>

  1822

  1823

  1824 section \<open>Document outline\<close>

  1825

  1826 text \<open>

  1827   Theory sources may contain document markup commands, such as @{command_ref

  1828   chapter}, @{command_ref section}, @{command subsection}. The Isabelle

  1829   SideKick parser (\secref{sec:sidekick}) represents this document outline as

  1830   structured tree view, with formal statements and proofs nested inside; see

  1831   \figref{fig:sidekick-document}.

  1832

  1833   \begin{figure}[!htb]

  1834   \begin{center}

  1835   \includegraphics[scale=0.333]{sidekick-document}

  1836   \end{center}

  1837   \caption{Isabelle document outline via SideKick tree view}

  1838   \label{fig:sidekick-document}

  1839   \end{figure}

  1840

  1841   It is also possible to use text folding according to this structure, by

  1842   adjusting \<^emph>\<open>Utilities / Buffer Options / Folding mode\<close> of jEdit. The default

  1843   mode \<^verbatim>\<open>isabelle\<close> uses the structure of formal definitions, statements, and

  1844   proofs. The alternative mode \<^verbatim>\<open>sidekick\<close> uses the document structure of the

  1845   SideKick parser, as explained above.

  1846 \<close>

  1847

  1848

  1849 section \<open>Markdown structure\<close>

  1850

  1851 text \<open>

  1852   Document text is internally structured in paragraphs and nested lists, using

  1853   notation that is similar to Markdown\<^footnote>\<open>\<^url>\<open>http://commonmark.org\<close>\<close>. There are

  1854   special control symbols for items of different kinds of lists, corresponding

  1855   to \<^verbatim>\<open>itemize\<close>, \<^verbatim>\<open>enumerate\<close>, \<^verbatim>\<open>description\<close> in {\LaTeX}. This is illustrated

  1856   in for \<^verbatim>\<open>itemize\<close> in \figref{fig:markdown-document}.

  1857

  1858   \begin{figure}[!htb]

  1859   \begin{center}

  1860   \includegraphics[scale=0.333]{markdown-document}

  1861   \end{center}

  1862   \caption{Markdown structure within document text}

  1863   \label{fig:markdown-document}

  1864   \end{figure}

  1865

  1866   Items take colour according to the depth of nested lists. This helps to

  1867   explore the implicit rules for list structure interactively. There is also

  1868   markup for individual paragraphs in the text: it may be explored via mouse

  1869   hovering with \<^verbatim>\<open>CONTROL\<close> / \<^verbatim>\<open>COMMAND\<close> as usual

  1870   (\secref{sec:tooltips-hyperlinks}).

  1871 \<close>

  1872

  1873

  1874 section \<open>Citations and Bib{\TeX} entries \label{sec:bibtex}\<close>

  1875

  1876 text \<open>

  1877   Citations are managed by {\LaTeX} and Bib{\TeX} in \<^verbatim>\<open>.bib\<close> files. The

  1878   Isabelle session build process and the @{tool latex} tool @{cite

  1879   "isabelle-system"} are smart enough to assemble the result, based on the

  1880   session directory layout.

  1881

  1882   The document antiquotation \<open>@{cite}\<close> is described in @{cite

  1883   "isabelle-isar-ref"}. Within the Prover IDE it provides semantic markup for

  1884   tooltips, hyperlinks, and completion for Bib{\TeX} database entries.

  1885   Isabelle/jEdit does \<^emph>\<open>not\<close> know about the actual Bib{\TeX} environment used

  1886   in {\LaTeX} batch-mode, but it can take citations from those \<^verbatim>\<open>.bib\<close> files

  1887   that happen to be open in the editor; see \figref{fig:cite-completion}.

  1888

  1889   \begin{figure}[!htb]

  1890   \begin{center}

  1891   \includegraphics[scale=0.333]{cite-completion}

  1892   \end{center}

  1893   \caption{Semantic completion of citations from open Bib{\TeX} files}

  1894   \label{fig:cite-completion}

  1895   \end{figure}

  1896

  1897   Isabelle/jEdit also provides IDE support for editing \<^verbatim>\<open>.bib\<close> files

  1898   themselves. There is syntax highlighting based on entry types (according to

  1899   standard Bib{\TeX} styles), a context-menu to compose entries

  1900   systematically, and a SideKick tree view of the overall content; see

  1901   \figref{fig:bibtex-mode}. Semantic checking with errors and warnings is

  1902   performed by the original \<^verbatim>\<open>bibtex\<close> tool using style \<^verbatim>\<open>plain\<close>: different

  1903   Bib{\TeX} styles may produce slightly different results.

  1904

  1905   \begin{figure}[!htb]

  1906   \begin{center}

  1907   \includegraphics[scale=0.333]{bibtex-mode}

  1908   \end{center}

  1909   \caption{Bib{\TeX} mode with context menu, SideKick tree view, and

  1910     semantic output from the \<^verbatim>\<open>bibtex\<close> tool}

  1911   \label{fig:bibtex-mode}

  1912   \end{figure}

  1913

  1914   Regular document preview (\secref{sec:document-preview}) of \<^verbatim>\<open>.bib\<close> files

  1915   approximates the usual {\LaTeX} bibliography output in HTML (using style

  1916   \<^verbatim>\<open>unsort\<close>).

  1917 \<close>

  1918

  1919

  1920 section \<open>Document preview \label{sec:document-preview}\<close>

  1921

  1922 text \<open>

  1923   The action @{action_def isabelle.preview} opens an HTML preview of the

  1924   current document node in the default web browser. The content is derived

  1925   from the semantic markup produced by the prover, and thus depends on the

  1926   status of formal processing.

  1927

  1928   Action @{action_def isabelle.draft} is similar to @{action

  1929   isabelle.preview}, but shows a plain-text document draft.

  1930 \<close>

  1931

  1932

  1933 chapter \<open>ML debugging within the Prover IDE\<close>

  1934

  1935 text \<open>

  1936   Isabelle/ML is based on Poly/ML\<^footnote>\<open>\<^url>\<open>https://www.polyml.org\<close>\<close> and thus

  1937   benefits from the source-level debugger of that implementation of Standard

  1938   ML. The Prover IDE provides the \<^emph>\<open>Debugger\<close> dockable to connect to running

  1939   ML threads, inspect the stack frame with local ML bindings, and evaluate ML

  1940   expressions in a particular run-time context. A typical debugger session is

  1941   shown in \figref{fig:ml-debugger}.

  1942

  1943   ML debugging depends on the following pre-requisites.

  1944

  1945     \<^enum> ML source needs to be compiled with debugging enabled. This may be

  1946     controlled for particular chunks of ML sources using any of the subsequent

  1947     facilities.

  1948

  1949       \<^enum> The system option @{system_option_ref ML_debugger} as implicit state

  1950       of the Isabelle process. It may be changed in the menu \<^emph>\<open>Plugins /

  1951       Plugin Options / Isabelle / General\<close>. ML modules need to be reloaded and

  1952       recompiled to pick up that option as intended.

  1953

  1954       \<^enum> The configuration option @{attribute_ref ML_debugger}, with an

  1955       attribute of the same name, to update a global or local context (e.g.\

  1956       with the @{command declare} command).

  1957

  1958       \<^enum> Commands that modify @{attribute ML_debugger} state for individual

  1959       files: @{command_ref ML_file_debug}, @{command_ref ML_file_no_debug},

  1960       @{command_ref SML_file_debug}, @{command_ref SML_file_no_debug}.

  1961

  1962     The instrumentation of ML code for debugging causes minor run-time

  1963     overhead. ML modules that implement critical system infrastructure may

  1964     lead to deadlocks or other undefined behaviour, when put under debugger

  1965     control!

  1966

  1967     \<^enum> The \<^emph>\<open>Debugger\<close> panel needs to be active, otherwise the program ignores

  1968     debugger instrumentation of the compiler and runs unmanaged. It is also

  1969     possible to start debugging with the panel open, and later undock it, to

  1970     let the program continue unhindered.

  1971

  1972     \<^enum> The ML program needs to be stopped at a suitable breakpoint, which may

  1973     be activated individually or globally as follows.

  1974

  1975     For ML sources that have been compiled with debugger support, the IDE

  1976     visualizes possible breakpoints in the text. A breakpoint may be toggled

  1977     by pointing accurately with the mouse, with a right-click to activate

  1978     jEdit's context menu and its \<^emph>\<open>Toggle Breakpoint\<close> item. Alternatively, the

  1979     \<^emph>\<open>Break\<close> checkbox in the \<^emph>\<open>Debugger\<close> panel may be enabled to stop ML

  1980     threads always at the next possible breakpoint.

  1981

  1982   Note that the state of individual breakpoints \<^emph>\<open>gets lost\<close> when the

  1983   coresponding ML source is re-compiled! This may happen unintentionally,

  1984   e.g.\ when following hyperlinks into ML modules that have not been loaded

  1985   into the IDE before.

  1986

  1987   \begin{figure}[!htb]

  1988   \begin{center}

  1989   \includegraphics[scale=0.333]{ml-debugger}

  1990   \end{center}

  1991   \caption{ML debugger session}

  1992   \label{fig:ml-debugger}

  1993   \end{figure}

  1994

  1995   The debugger panel (\figref{fig:ml-debugger}) shows a list of all threads

  1996   that are presently stopped. Each thread shows a stack of all function

  1997   invocations that lead to the current breakpoint at the top.

  1998

  1999   It is possible to jump between stack positions freely, by clicking on this

  2000   list. The current situation is displayed in the big output window, as a

  2001   local ML environment with names and printed values.

  2002

  2003   ML expressions may be evaluated in the current context by entering snippets

  2004   of source into the text fields labeled \<open>Context\<close> and \<open>ML\<close>, and pushing the

  2005   \<open>Eval\<close> button. By default, the source is interpreted as Isabelle/ML with the

  2006   usual support for antiquotations (like @{command ML}, @{command ML_file}).

  2007   Alternatively, strict Standard ML may be enforced via the \<^emph>\<open>SML\<close> checkbox

  2008   (like @{command SML_file}).

  2009

  2010   The context for Isabelle/ML is optional, it may evaluate to a value of type

  2011   @{ML_type theory}, @{ML_type Proof.context}, or @{ML_type Context.generic}.

  2012   Thus the given ML expression (with its antiquotations) may be subject to the

  2013   intended dynamic run-time context, instead of the static compile-time

  2014   context.

  2015

  2016   \<^medskip>

  2017   The buttons labeled \<^emph>\<open>Continue\<close>, \<^emph>\<open>Step\<close>, \<^emph>\<open>Step over\<close>, \<^emph>\<open>Step out\<close>

  2018   recommence execution of the program, with different policies concerning

  2019   nested function invocations. The debugger always moves the cursor within the

  2020   ML source to the next breakpoint position, and offers new stack frames as

  2021   before.

  2022 \<close>

  2023

  2024

  2025 chapter \<open>Miscellaneous tools\<close>

  2026

  2027 section \<open>Timing\<close>

  2028

  2029 text \<open>

  2030   Managed evaluation of commands within PIDE documents includes timing

  2031   information, which consists of elapsed (wall-clock) time, CPU time, and GC

  2032   (garbage collection) time. Note that in a multithreaded system it is

  2033   difficult to measure execution time precisely: elapsed time is closer to the

  2034   real requirements of runtime resources than CPU or GC time, which are both

  2035   subject to influences from the parallel environment that are outside the

  2036   scope of the current command transaction.

  2037

  2038   The \<^emph>\<open>Timing\<close> panel provides an overview of cumulative command timings for

  2039   each document node. Commands with elapsed time below the given threshold are

  2040   ignored in the grand total. Nodes are sorted according to their overall

  2041   timing. For the document node that corresponds to the current buffer,

  2042   individual command timings are shown as well. A double-click on a theory

  2043   node or command moves the editor focus to that particular source position.

  2044

  2045   It is also possible to reveal individual timing information via some tooltip

  2046   for the corresponding command keyword, using the technique of mouse hovering

  2047   with \<^verbatim>\<open>CONTROL\<close>~/ \<^verbatim>\<open>COMMAND\<close> modifier (\secref{sec:tooltips-hyperlinks}).

  2048   Actual display of timing depends on the global option @{system_option_ref

  2049   jedit_timing_threshold}, which can be configured in \<^emph>\<open>Plugin Options~/

  2050   Isabelle~/ General\<close>.

  2051

  2052   \<^medskip>

  2053   The \<^emph>\<open>Monitor\<close> panel visualizes various data collections about recent

  2054   activity of the Isabelle/ML task farm and the underlying ML runtime system.

  2055   The display is continuously updated according to @{system_option_ref

  2056   editor_chart_delay}. Note that the painting of the chart takes considerable

  2057   runtime itself --- on the Java Virtual Machine that runs Isabelle/Scala, not

  2058   Isabelle/ML. Internally, the Isabelle/Scala module \<^verbatim>\<open>isabelle.ML_Statistics\<close>

  2059   provides further access to statistics of Isabelle/ML.

  2060 \<close>

  2061

  2062

  2063 section \<open>Low-level output\<close>

  2064

  2065 text \<open>

  2066   Prover output is normally shown directly in the main text area or specific

  2067   panels like \<^emph>\<open>Output\<close> (\secref{sec:output}) or \<^emph>\<open>State\<close>

  2068   (\secref{sec:state-output}). Beyond this, it is occasionally useful to

  2069   inspect low-level output channels via some of the following additional

  2070   panels:

  2071

  2072   \<^item> \<^emph>\<open>Protocol\<close> shows internal messages between the Isabelle/Scala and

  2073   Isabelle/ML side of the PIDE document editing protocol. Recording of

  2074   messages starts with the first activation of the corresponding dockable

  2075   window; earlier messages are lost.

  2076

  2077   Actual display of protocol messages causes considerable slowdown, so it is

  2078   important to undock all \<^emph>\<open>Protocol\<close> panels for production work.

  2079

  2080   \<^item> \<^emph>\<open>Raw Output\<close> shows chunks of text from the \<^verbatim>\<open>stdout\<close> and \<^verbatim>\<open>stderr\<close>

  2081   channels of the prover process. Recording of output starts with the first

  2082   activation of the corresponding dockable window; earlier output is lost.

  2083

  2084   The implicit stateful nature of physical I/O channels makes it difficult to

  2085   relate raw output to the actual command from where it was originating.

  2086   Parallel execution may add to the confusion. Peeking at physical process I/O

  2087   is only the last resort to diagnose problems with tools that are not PIDE

  2088   compliant.

  2089

  2090   Under normal circumstances, prover output always works via managed message

  2091   channels (corresponding to @{ML writeln}, @{ML warning}, @{ML

  2092   Output.error_message} in Isabelle/ML), which are displayed by regular means

  2093   within the document model (\secref{sec:output}). Unhandled Isabelle/ML

  2094   exceptions are printed by the system via @{ML Output.error_message}.

  2095

  2096   \<^item> \<^emph>\<open>Syslog\<close> shows system messages that might be relevant to diagnose

  2097   problems with the startup or shutdown phase of the prover process; this also

  2098   includes raw output on \<^verbatim>\<open>stderr\<close>. Isabelle/ML also provides an explicit @{ML

  2099   Output.system_message} operation, which is occasionally useful for

  2100   diagnostic purposes within the system infrastructure itself.

  2101

  2102   A limited amount of syslog messages are buffered, independently of the

  2103   docking state of the \<^emph>\<open>Syslog\<close> panel. This allows to diagnose serious

  2104   problems with Isabelle/PIDE process management, outside of the actual

  2105   protocol layer.

  2106

  2107   Under normal situations, such low-level system output can be ignored.

  2108 \<close>

  2109

  2110

  2111 chapter \<open>Known problems and workarounds \label{sec:problems}\<close>

  2112

  2113 text \<open>

  2114   \<^item> \<^bold>\<open>Problem:\<close> Odd behavior of some diagnostic commands with global

  2115   side-effects, like writing a physical file.

  2116

  2117   \<^bold>\<open>Workaround:\<close> Copy/paste complete command text from elsewhere, or disable

  2118   continuous checking temporarily.

  2119

  2120   \<^item> \<^bold>\<open>Problem:\<close> Keyboard shortcuts \<^verbatim>\<open>C+PLUS\<close> and \<^verbatim>\<open>C+MINUS\<close> for adjusting the

  2121   editor font size depend on platform details and national keyboards.

  2122

  2123   \<^bold>\<open>Workaround:\<close> Rebind keys via \<^emph>\<open>Global Options~/ Shortcuts\<close>.

  2124

  2125   \<^item> \<^bold>\<open>Problem:\<close> The Mac OS X key sequence \<^verbatim>\<open>COMMAND+COMMA\<close> for application

  2126   \<^emph>\<open>Preferences\<close> is in conflict with the jEdit default keyboard shortcut for

  2127   \<^emph>\<open>Incremental Search Bar\<close> (action @{action_ref "quick-search"}).

  2128

  2129   \<^bold>\<open>Workaround:\<close> Rebind key via \<^emph>\<open>Global Options~/ Shortcuts\<close> according to

  2130   national keyboard, e.g.\ \<^verbatim>\<open>COMMAND+SLASH\<close> on English ones.

  2131

  2132   \<^item> \<^bold>\<open>Problem:\<close> On Mac OS X with native Apple look-and-feel, some exotic

  2133   national keyboards may cause a conflict of menu accelerator keys with

  2134   regular jEdit key bindings. This leads to duplicate execution of the

  2135   corresponding jEdit action.

  2136

  2137   \<^bold>\<open>Workaround:\<close> Disable the native Apple menu bar via Java runtime option

  2138   \<^verbatim>\<open>-Dapple.laf.useScreenMenuBar=false\<close>.

  2139

  2140   \<^item> \<^bold>\<open>Problem:\<close> Mac OS X system fonts sometimes lead to character drop-outs in

  2141   the main text area.

  2142

  2143   \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>Isabelle DejaVu\<close> fonts.

  2144

  2145   \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 input methods such as IBus tend to disrupt key

  2146   event handling of Java/AWT/Swing.

  2147

  2148   \<^bold>\<open>Workaround:\<close> Do not use X11 input methods. Note that environment variable

  2149   \<^verbatim>\<open>XMODIFIERS\<close> is reset by default within Isabelle settings.

  2150

  2151   \<^item> \<^bold>\<open>Problem:\<close> Some Linux/X11 window managers that are not re-parenting''

  2152   cause problems with additional windows opened by Java. This affects either

  2153   historic or neo-minimalistic window managers like \<^verbatim>\<open>awesome\<close> or \<^verbatim>\<open>xmonad\<close>.

  2154

  2155   \<^bold>\<open>Workaround:\<close> Use a regular re-parenting X11 window manager.

  2156

  2157   \<^item> \<^bold>\<open>Problem:\<close> Various forks of Linux/X11 window managers and desktop

  2158   environments (like Gnome) disrupt the handling of menu popups and mouse

  2159   positions of Java/AWT/Swing.

  2160

  2161   \<^bold>\<open>Workaround:\<close> Use suitable version of Linux desktops.

  2162

  2163   \<^item> \<^bold>\<open>Problem:\<close> Full-screen mode via jEdit action @{action_ref

  2164   "toggle-full-screen"} (default keyboard shortcut \<^verbatim>\<open>F11\<close>) works on Windows,

  2165   but not on Mac OS X or various Linux/X11 window managers.

  2166

  2167   \<^bold>\<open>Workaround:\<close> Use native full-screen control of the window manager (notably

  2168   on Mac OS X).

  2169

  2170   \<^item> \<^bold>\<open>Problem:\<close> Heap space of the JVM may fill up and render the Prover IDE

  2171   unresponsive, e.g.\ when editing big Isabelle sessions with many theories.

  2172

  2173   \<^bold>\<open>Workaround:\<close> Increase JVM heap parameters by editing platform-specific

  2174   files (for properties'' or options'') that are associated with the main

  2175   app bundle.

  2176

  2177   Also note that jEdit provides a heap space monitor in the status line

  2178   (bottom-right). Double-clicking on that causes full garbage-collection,

  2179   which sometimes helps in low-memory situations.

  2180 \<close>

  2181

  2182 end
`