src/Doc/JEdit/JEdit.thy
 author wenzelm Sun Nov 20 20:12:42 2016 +0100 (2016-11-20) changeset 64514 27914a4f8c70 parent 64513 56972c755027 child 64515 29f0b8d2f952 permissions -rw-r--r--
more on "Formal scopes and semantic selection";
     1 (*:maxLineLen=78:*)

     2

     3 theory JEdit

     4 imports Base

     5 begin

     6

     7 chapter \<open>Introduction\<close>

     8

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

    10

    11 text \<open>

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

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

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

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

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

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

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

    19

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

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

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

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

    24     as Isabelle/HOL.

    25

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

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

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

    29     services etc. Special infrastructure allows to transfer algebraic

    30     datatypes and formatted text easily between ML and Scala, using

    31     asynchronous protocol commands.

    32

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

    34     is built around a concept of parallel and asynchronous document

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

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

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

    38     rich formal markup for GUI rendering.

    39

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

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

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

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

    44

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

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

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

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

    49     integrated as a desktop application for the main operating system

    50     families: Linux, Windows, Mac OS X.

    51

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

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

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

    55   without proper differentiation. When discussing these PIDE building blocks

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

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

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

    59 \<close>

    60

    61

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

    63

    64 text \<open>

    65   \begin{figure}[!htb]

    66   \begin{center}

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

    68   \end{center}

    69   \caption{The Isabelle/jEdit Prover IDE}

    70   \label{fig:isabelle-jedit}

    71   \end{figure}

    72

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

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

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

    76   \<^emph>\<open>Plugins~/ Isabelle\<close> with access to several panels (see also

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

    78   (see also \secref{sec:options}).

    79

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

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

    82   application startup, the selected logic session image is provided

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

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

    85   text editor is running. Prover IDE functionality is only activated after

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

    87   some options and restart the application. Changing the logic session, or the

    88   underlying ML system platform (32\,bit versus 64\,bit) requires a restart of

    89   the application to take effect.

    90

    91   \<^medskip>

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

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

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

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

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

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

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

    99

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

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

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

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

   104   editor source buffer.

   105

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

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

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

   109 \<close>

   110

   111

   112 subsection \<open>Documentation\<close>

   113

   114 text \<open>

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

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

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

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

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

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

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

   122   individual plugins.

   123

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

   125   but one needs to keep in mind that defaults sometimes differ, and the

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

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

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

   129 \<close>

   130

   131

   132 subsection \<open>Plugins\<close>

   133

   134 text \<open>

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

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

   137   accessible via various mirror sites.

   138

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

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

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

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

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

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

   145

   146   \<^medskip>

   147   The main \<^emph>\<open>Isabelle\<close> plugin is an integral part of Isabelle/jEdit and needs

   148   to remain active at all times! A few additional plugins are bundled with

   149   Isabelle/jEdit for convenience or out of necessity, notably \<^emph>\<open>Console\<close> with

   150   its Isabelle/Scala sub-plugin (\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close>

   151   with some Isabelle-specific parsers for document tree structure

   152   (\secref{sec:sidekick}). The \<^emph>\<open>Navigator\<close> plugin is particularly important

   153   for hyperlinks within the formal document-model

   154   (\secref{sec:tooltips-hyperlinks}). Further plugins (e.g.\ \<^emph>\<open>ErrorList\<close>,

   155   \<^emph>\<open>Code2HTML\<close>) are included to saturate the dependencies of bundled plugins,

   156   but have no particular use in Isabelle/jEdit.

   157 \<close>

   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 of document content, which are   179 configurable via \<^emph>\<open>Plugin Options~/ Isabelle~/ Rendering\<close>. Thus \<^emph>\<open>Plugin   180 Options~/ Isabelle\<close> in jEdit provides a view on a subset of Isabelle system   181 options. Note that some of these options affect general parameters that are   182 relevant outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or   183 @{system_option parallel_proofs} for the Isabelle build tool @{cite   184 "isabelle-system"}, but it is possible to use the settings variable   185 @{setting ISABELLE_BUILD_OPTIONS} to change defaults for batch builds   186 without affecting the Prover IDE.   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 machine-generated @{path   194 "$JEDIT_SETTINGS/properties"} or @{path

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

   211   \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>.   212   213 \<^medskip>   214 The action @{action_def "isabelle.keymap-merge"} helps to resolve pending   215 Isabelle keymap changes that are in conflict with the current jEdit keymap;   216 non-conflicting changes are always applied implicitly. This action is   217 automatically invoked on Isabelle/jEdit startup.   218 \<close>   219   220   221 section \<open>Command-line invocation \label{sec:command-line}\<close>   222   223 text \<open>   224 Isabelle/jEdit is normally invoked as a single-instance desktop application,   225 based on platform-specific executables for Linux, Windows, Mac OS X.   226   227 It is also possible to invoke the Prover IDE on the command-line, with some   228 extra options and environment settings. The command-line usage of @{tool_def   229 jedit} is as follows:   230 @{verbatim [display]   231 \<open>Usage: isabelle jedit [OPTIONS] [FILES ...]   232   233 Options are:   234 -D NAME=X set JVM system property   235 -J OPTION add JVM runtime option   236 -b build only   237 -d DIR include session directory   238 -f fresh build   239 -j OPTION add jEdit runtime option   240 -l NAME logic image name   241 -m MODE add print mode for output   242 -n no build of session image on startup   243 -p CMD ML process command prefix (process policy)   244 -s system build mode for session image   245   246 Start jEdit with Isabelle plugin setup and open FILES   247 (default "$USER_HOME/Scratch.thy" or ":" for empty buffer).\<close>}

   248

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

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

   251   via option \<^verbatim>\<open>-d\<close> to augment that name space of @{tool build} @{cite

   252   "isabelle-system"}.

   253

   254   By default, the specified image is checked and built on demand. The \<^verbatim>\<open>-s\<close>

   255   option determines where to store the result session image of @{tool build}.

   256   The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected

   257   session image.

   258

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

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

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

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

   263

   264   The \<^verbatim>\<open>-J\<close> and \<^verbatim>\<open>-j\<close> options allow to pass additional low-level options to

   265   the JVM or jEdit, respectively. The defaults are provided by the Isabelle

   266   settings environment @{cite "isabelle-system"}, but note that these only

   267   work for the command-line tool described here, and not the regular

   268   application.

   269

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

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

   272

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

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

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

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

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

   278

   279   \<^bigskip>

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

   281   via @{tool_def jedit_client}:

   282   @{verbatim [display]

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

   284

   285   Options are:

   286     -c           only check presence of server

   287     -n           only report server name

   288     -s NAME      server name (default Isabelle)

   289

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

   291

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

   293   process return code accordingly.

   294

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

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

   297   name (e.g.\ \<^verbatim>\<open>Isabelle2016-1\<close>). Thus @{tool jedit_client} can connect to the

   298   Isabelle desktop application without further options.

   299

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

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

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

   303

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

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

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

   307 \<close>

   308

   309

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

   311

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

   313

   314 text \<open>

   315   jEdit is a Java/AWT/Swing application with some ambition to support

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

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

   318   \secref{sec:problems}).

   319

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

   321   follows.

   322

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

   324

   325     The Linux-specific \<^emph>\<open>GTK+\<close> also works under the side-condition that the

   326     overall GTK theme and options are selected in a way that works with Java

   327     AWT/Swing. The JVM has no direct influence of GTK rendering.

   328

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

   330

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

   332

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

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

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

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

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

   338

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

   340   in mind that this extra variance of GUI functionality is unlikely to work in

   341   arbitrary combinations. The platform-independent \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close>

   342   should always work on all platforms, although they are technically and

   343   stylistically outdated. The historic \<^emph>\<open>CDE/Motif\<close> should be ignored.

   344

   345   After changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close>,

   346   Isabelle/jEdit should be restarted to take full effect.

   347 \<close>

   348

   349

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

   351

   352 text \<open>

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

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

   355   pixels as adequate for text rendering. In 2016, we routinely see much higher

   356   resolutions, e.g. Full HD'' at $1920 \times 1080$ pixels or Ultra HD'' /

   357   4K'' at $3840 \times 2160$.

   358

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

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

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

   362

   363   \<^medskip>

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

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

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

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

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

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

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

   371   Here is a summary of all relevant font properties:

   372

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

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

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

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

   377

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

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

   380     (disabled by default).

   381

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

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

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

   385

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

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

   388     relevant for quick scaling like in common web browsers.

   389

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

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

   392

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

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

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

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

   397

   398   \begin{figure}[!htb]

   399   \begin{center}

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

   401   \end{center}

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

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

   404   \end{figure}

   405 \<close>

   406

   407

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

   409

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

   411

   412 text \<open>

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

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

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

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

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

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

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

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

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

   422   instance.

   423

   424   Dockables are used routinely in jEdit for important functionality like

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

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

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

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

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

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

   431   can change this arrangement easily and persistently.

   432

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

   434   slightly augmented according to the the following principles:

   435

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

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

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

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

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

   441   management functions may be missing.

   442

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

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

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

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

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

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

   449   input field of that panel.

   450

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

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

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

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

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

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

   457 \<close>

   458

   459

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

   461

   462 text \<open>

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

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

   465   without depending on particular encodings and varying Unicode

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

   467   portability and reliability in the face of changing interpretation of

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

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

   470

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

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

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

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

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

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

   478

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

   480   standard interpretation of finitely many symbols from the infinite

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

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

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

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

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

   486   alphabets in comments.

   487 \<close>

   488

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

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

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

   492   JVM). It is provided by the Isabelle/jEdit plugin and enabled by default for

   493   all source files. Sometimes such defaults are reset accidentally, or

   494   malformed UTF-8 sequences in the text force jEdit to fall back on a

   495   different encoding like \<^verbatim>\<open>ISO-8859-15\<close>. In that case, verbatim \<^verbatim>\<open>\<alpha>\<close>'' will

   496   be shown in the text buffer instead of its Unicode rendering \<open>\<alpha>\<close>''. The

   497   jEdit menu operation \<^emph>\<open>File~/ Reload with Encoding~/ UTF-8-Isabelle\<close> helps

   498   to resolve such problems (after repairing malformed parts of the text). \<close>

   499

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

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

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

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

   504   Isabelle/jEdit prefers its own application fonts \<^verbatim>\<open>IsabelleText\<close>, which

   505   ensures that standard collection of Isabelle symbols is actually shown on

   506   the screen (or printer) as expected.

   507

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

   509   they are not installed on the operating system already! Some outdated

   510   version of \<^verbatim>\<open>IsabelleText\<close> that happens to be provided by the operating

   511   system would prevent Isabelle/jEdit to use its bundled version. This could

   512   lead to missing glyphs (black rectangles), when the system version of

   513   \<^verbatim>\<open>IsabelleText\<close> is older than the application version. This problem can be

   514   avoided by refraining to install'' any version of \<^verbatim>\<open>IsabelleText\<close> in the

   515   first place, although it might be tempting to use the same font in other

   516   applications.

   517

   518   HTML pages generated by Isabelle refer to the same \<^verbatim>\<open>IsabelleText\<close> font as a

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

   520   locally installed copy.

   521 \<close>

   522

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

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

   525   Isabelle symbols in their Unicode rendering to the underlying operating

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

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

   528   none of these standard input methods work satisfactorily for the

   529   mathematical characters required for Isabelle, various specific

   530   Isabelle/jEdit mechanisms are provided.

   531

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

   533   symbols.

   534

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

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

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

   538   abbreviations\<close> (see below).

   539

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

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

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

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

   544   used.

   545

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

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

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

   549   menu actions always refer to the primary text area!

   550

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

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

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

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

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

   556

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

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

   683   \<^verbatim>\<open>$JEDIT_SETTINGS\<close>. The file browser of jEdit also includes \<^emph>\<open>Favorites\<close> for   684 these two important locations.   685   686 \<^medskip>   687 Path specifications in prover input or output usually include formal markup   688 that turns it into a hyperlink (see also \secref{sec:tooltips-hyperlinks}).   689 This allows to open the corresponding file in the text editor, independently   690 of the path notation. If the path refers to a directory, the jEdit file   691 browser is opened on it.   692   693 Formally checked paths in prover input are subject to completion   694 (\secref{sec:completion}): partial specifications are resolved via directory   695 content and possible completions are offered in a popup.   696 \<close>   697   698   699 section \<open>SideKick parsers \label{sec:sidekick}\<close>   700   701 text \<open>   702 The \<^emph>\<open>SideKick\<close> plugin provides some general services to display buffer   703 structure in a tree view. Isabelle/jEdit provides SideKick parsers for its   704 main mode for theory files, ML files, as well as some minor modes for the   705 \<^verbatim>\<open>NEWS\<close> file (see \figref{fig:sidekick}), session \<^verbatim>\<open>ROOT\<close> files, system   706 \<^verbatim>\<open>options\<close>, and Bib{\TeX} files (\secref{sec:bibtex}).   707   708 \begin{figure}[!htb]   709 \begin{center}   710 \includegraphics[scale=0.333]{sidekick}   711 \end{center}   712 \caption{The Isabelle NEWS file with SideKick tree view}   713 \label{fig:sidekick}   714 \end{figure}   715   716 The default SideKick parser for theory files is \<^verbatim>\<open>isabelle\<close>: it provides a   717 tree-view on the formal document structure, with section headings at the top   718 and formal specification elements at the bottom. The alternative parser   719 \<^verbatim>\<open>isabelle-context\<close> shows nesting of context blocks according to \<^theory_text>\<open>begin \<dots>   720 end\<close> structure.   721   722 \<^medskip>   723 Isabelle/ML files are structured according to semi-formal comments that are   724 explained in @{cite "isabelle-implementation"}. This outline is turned into   725 a tree-view by default, by using the \<^verbatim>\<open>isabelle-ml\<close> parser. There is also a   726 folding mode of the same name, for hierarchic text folds within ML files.   727   728 \<^medskip>   729 The special SideKick parser \<^verbatim>\<open>isabelle-markup\<close> exposes the uninterpreted   730 markup tree of the PIDE document model of the current buffer. This is   731 occasionally useful for informative purposes, but the amount of displayed   732 information might cause problems for large buffers.   733 \<close>   734   735   736 chapter \<open>Prover IDE functionality \label{sec:document-model}\<close>   737   738 section \<open>Document model \label{sec:document-model}\<close>   739   740 text \<open>   741 The document model is central to the PIDE architecture: the editor and the   742 prover have a common notion of structured source text with markup, which is   743 produced by formal processing. The editor is responsible for edits of   744 document source, as produced by the user. The prover is responsible for   745 reports of document markup, as produced by its processing in the background.   746   747 Isabelle/jEdit handles classic editor events of jEdit, in order to connect   748 the physical world of the GUI (with its singleton state) to the mathematical   749 world of multiple document versions (with timeless and stateless updates).   750 \<close>   751   752   753 subsection \<open>Editor buffers and document nodes \label{sec:buffer-node}\<close>   754   755 text \<open>   756 As a regular text editor, jEdit maintains a collection of \<^emph>\<open>buffers\<close> to   757 store text files; each buffer may be associated with any number of visible   758 \<^emph>\<open>text areas\<close>. Buffers are subject to an \<^emph>\<open>edit mode\<close> that is determined   759 from the file name extension. The following modes are treated specifically   760 in Isabelle/jEdit:   761   762 \<^medskip>   763 \begin{tabular}{lll}   764 \<^bold>\<open>mode\<close> & \<^bold>\<open>file name\<close> & \<^bold>\<open>content\<close> \\\hline   765 \<^verbatim>\<open>isabelle\<close> & \<^verbatim>\<open>*.thy\<close> & theory source \\   766 \<^verbatim>\<open>isabelle-ml\<close> & \<^verbatim>\<open>*.ML\<close> & Isabelle/ML source \\   767 \<^verbatim>\<open>sml\<close> & \<^verbatim>\<open>*.sml\<close> or \<^verbatim>\<open>*.sig\<close> & Standard ML source \\   768 \<^verbatim>\<open>isabelle-root\<close> & \<^verbatim>\<open>ROOT\<close> & session root \\   769 \<^verbatim>\<open>isabelle-options\<close> & & Isabelle options \\   770 \<^verbatim>\<open>isabelle-news\<close> & & Isabelle NEWS \\   771 \end{tabular}   772 \<^medskip>   773   774 All jEdit buffers are automatically added to the PIDE document-model as   775 \<^emph>\<open>document nodes\<close>. The overall document structure is defined by the theory   776 nodes in two dimensions:   777   778 \<^enum> via \<^bold>\<open>theory imports\<close> that are specified in the \<^emph>\<open>theory header\<close> using   779 concrete syntax of the @{command_ref theory} command @{cite   780 "isabelle-isar-ref"};   781   782 \<^enum> via \<^bold>\<open>auxiliary files\<close> that are loaded into a theory by special \<^emph>\<open>load   783 commands\<close>, notably @{command_ref ML_file} and @{command_ref SML_file}   784 @{cite "isabelle-isar-ref"}.   785   786 In any case, source files are managed by the PIDE infrastructure: the   787 physical file-system only plays a subordinate role. The relevant version of   788 source text is passed directly from the editor to the prover, using internal   789 communication channels.   790 \<close>   791   792   793 subsection \<open>Theories \label{sec:theories}\<close>   794   795 text \<open>   796 The \<^emph>\<open>Theories\<close> panel (see also \figref{fig:theories}) provides an overview   797 of the status of continuous checking of theory nodes within the document   798 model. Unlike batch sessions of @{tool build} @{cite "isabelle-system"},   799 theory nodes are identified by full path names; this allows to work with   800 multiple (disjoint) Isabelle sessions simultaneously within the same editor   801 session.   802   803 \begin{figure}[!htb]   804 \begin{center}   805 \includegraphics[scale=0.333]{theories}   806 \end{center}   807 \caption{Theories panel with an overview of the document-model, and jEdit   808 text areas as editable views on some of the document nodes}   809 \label{fig:theories}   810 \end{figure}   811   812 Certain events to open or update editor buffers cause Isabelle/jEdit to   813 resolve dependencies of theory imports. The system requests to load   814 additional files into editor buffers, in order to be included in the   815 document model for further checking. It is also possible to let the system   816 resolve dependencies automatically, according to the system option   817 @{system_option jedit_auto_load}.   818   819 \<^medskip>   820 The visible \<^emph>\<open>perspective\<close> of Isabelle/jEdit is defined by the collective   821 view on theory buffers via open text areas. The perspective is taken as a   822 hint for document processing: the prover ensures that those parts of a   823 theory where the user is looking are checked, while other parts that are   824 presently not required are ignored. The perspective is changed by opening or   825 closing text area windows, or scrolling within a window.   826   827 The \<^emph>\<open>Theories\<close> panel provides some further options to influence the process   828 of continuous checking: it may be switched off globally to restrict the   829 prover to superficial processing of command syntax. It is also possible to   830 indicate theory nodes as \<^emph>\<open>required\<close> for continuous checking: this means   831 such nodes and all their imports are always processed independently of the   832 visibility status (if continuous checking is enabled). Big theory libraries   833 that are marked as required can have significant impact on performance!   834   835 \<^medskip>   836 Formal markup of checked theory content is turned into GUI rendering, based   837 on a standard repertoire known from mainstream IDEs for programming   838 languages: colors, icons, highlighting, squiggly underlines, tooltips,   839 hyperlinks etc. For outer syntax of Isabelle/Isar there is some traditional   840 syntax-highlighting via static keywords and tokenization within the editor;   841 this buffer syntax is determined from theory imports. In contrast, the   842 painting of inner syntax (term language etc.)\ uses semantic information   843 that is reported dynamically from the logical context. Thus the prover can   844 provide additional markup to help the user to understand the meaning of   845 formal text, and to produce more text with some add-on tools (e.g.\   846 information messages with \<^emph>\<open>sendback\<close> markup by automated provers or   847 disprovers in the background). \<close>   848   849   850 subsection \<open>Auxiliary files \label{sec:aux-files}\<close>   851   852 text \<open>   853 Special load commands like @{command_ref ML_file} and @{command_ref   854 SML_file} @{cite "isabelle-isar-ref"} refer to auxiliary files within some   855 theory. Conceptually, the file argument of the command extends the theory   856 source by the content of the file, but its editor buffer may be loaded~/   857 changed~/ saved separately. The PIDE document model propagates changes of   858 auxiliary file content to the corresponding load command in the theory, to   859 update and process it accordingly: changes of auxiliary file content are   860 treated as changes of the corresponding load command.   861   862 \<^medskip>   863 As a concession to the massive amount of ML files in Isabelle/HOL itself,   864 the content of auxiliary files is only added to the PIDE document-model on   865 demand, the first time when opened explicitly in the editor. There are   866 further tricks to manage markup of ML files, such that Isabelle/HOL may be   867 edited conveniently in the Prover IDE on small machines with only 8\,GB of   868 main memory. Using \<^verbatim>\<open>Pure\<close> as logic session image, the exploration may start   869 at the top \<^file>\<open>$ISABELLE_HOME/src/HOL/Main.thy\<close> or the bottom

   870   \<^file>\<open>$ISABELLE_HOME/src/HOL/HOL.thy\<close>, for example.   871   872 Initially, before an auxiliary file is opened in the editor, the prover   873 reads its content from the physical file-system. After the file is opened   874 for the first time in the editor, e.g.\ by following the hyperlink   875 (\secref{sec:tooltips-hyperlinks}) for the argument of its @{command   876 ML_file} command, the content is taken from the jEdit buffer.   877   878 The change of responsibility from prover to editor counts as an update of   879 the document content, so subsequent theory sources need to be re-checked.   880 When the buffer is closed, the responsibility remains to the editor: the   881 file may be opened again without causing another document update.   882   883 A file that is opened in the editor, but its theory with the load command is   884 not, is presently inactive in the document model. A file that is loaded via   885 multiple load commands is associated to an arbitrary one: this situation is   886 morally unsupported and might lead to confusion.   887   888 \<^medskip>   889 Output that refers to an auxiliary file is combined with that of the   890 corresponding load command, and shown whenever the file or the command are   891 active (see also \secref{sec:output}).   892   893 Warnings, errors, and other useful markup is attached directly to the   894 positions in the auxiliary file buffer, in the manner of standard IDEs. By   895 using the load command @{command SML_file} as explained in   896 \<^file>\<open>$ISABELLE_HOME/src/Tools/SML/Examples.thy\<close>, Isabelle/jEdit may be used as

   897   fully-featured IDE for Standard ML, independently of theory or proof

   898   development: the required theory merely serves as some kind of project file

   899   for a collection of SML source modules.

   900 \<close>

   901

   902

   903 section \<open>Output \label{sec:output}\<close>

   904

   905 text \<open>

   906   Prover output consists of \<^emph>\<open>markup\<close> and \<^emph>\<open>messages\<close>. Both are directly

   907   attached to the corresponding positions in the original source text, and

   908   visualized in the text area, e.g.\ as text colours for free and bound

   909   variables, or as squiggly underlines for warnings, errors etc.\ (see also

   910   \figref{fig:output}). In the latter case, the corresponding messages are

   911   shown by hovering with the mouse over the highlighted text --- although in

   912   many situations the user should already get some clue by looking at the

   913   position of the text highlighting, without seeing the message body itself.

   914

   915   \begin{figure}[!htb]

   916   \begin{center}

   917   \includegraphics[scale=0.333]{output}

   918   \end{center}

   919   \caption{Multiple views on prover output: gutter with icon, text area with

   920   popup, text overview column, \<^emph>\<open>Theories\<close> panel, \<^emph>\<open>Output\<close> panel}

   921   \label{fig:output}

   922   \end{figure}

   923

   924   The gutter'' on the left-hand-side of the text area uses icons to

   925   provide a summary of the messages within the adjacent text line. Message

   926   priorities are used to prefer errors over warnings, warnings over

   927   information messages; other output is ignored.

   928

   929   The text overview column'' on the right-hand-side of the text area uses

   930   similar information to paint small rectangles for the overall status of the

   931   whole text buffer. The graphics is scaled to fit the logical buffer length

   932   into the given window height. Mouse clicks on the overview area move the

   933   cursor approximately to the corresponding text line in the buffer.

   934

   935   The \<^emph>\<open>Theories\<close> panel provides another course-grained overview, but without

   936   direct correspondence to text positions. The coloured rectangles represent

   937   the amount of messages of a certain kind (warnings, errors, etc.) and the

   938   execution status of commands. A double-click on one of the theory entries

   939   with their status overview opens the corresponding text buffer, without

   940   moving the cursor to a specific point.

   941

   942   \<^medskip>

   943   The \<^emph>\<open>Output\<close> panel displays prover messages that correspond to a given

   944   command, within a separate window. The cursor position in the presently

   945   active text area determines the prover command whose cumulative message

   946   output is appended and shown in that window (in canonical order according to

   947   the internal execution of the command). There are also control elements to

   948   modify the update policy of the output wrt.\ continued editor movements:

   949   \<^emph>\<open>Auto update\<close> and \<^emph>\<open>Update\<close>. This is particularly useful for multiple

   950   instances of the \<^emph>\<open>Output\<close> panel to look at different situations.

   951   Alternatively, the panel can be turned into a passive \<^emph>\<open>Info\<close> window via the

   952   \<^emph>\<open>Detach\<close> menu item.

   953

   954   Proof state is handled separately (\secref{sec:state-output}), but it is

   955   also possible to tick the corresponding checkbox to append it to regular

   956   output (\figref{fig:output-including-state}). This is a globally persistent

   957   option: it affects all open panels and future editor sessions.

   958

   959   \begin{figure}[!htb]

   960   \begin{center}

   961   \includegraphics[scale=0.333]{output-including-state}

   962   \end{center}

   963   \caption{Proof state display within the regular output panel}

   964   \label{fig:output-including-state}

   965   \end{figure}

   966

   967   \<^medskip>

   968   Following the IDE principle, regular messages are attached to the original

   969   source in the proper place and may be inspected on demand via popups. This

   970   excludes messages that are somehow internal to the machinery of proof

   971   checking, notably \<^emph>\<open>proof state\<close> and \<^emph>\<open>tracing\<close>.

   972

   973   In any case, the same display technology is used for small popups and big

   974   output windows. The formal text contains markup that may be explored

   975   recursively via further popups and hyperlinks (see

   976   \secref{sec:tooltips-hyperlinks}), or clicked directly to initiate certain

   977   actions (see \secref{sec:auto-tools} and \secref{sec:sledgehammer}).

   978 \<close>

   979

   980

   981 section \<open>Proof state \label{sec:state-output}\<close>

   982

   983 text \<open>

   984   The main purpose of the Prover IDE is to help the user editing proof

   985   documents, with ongoing formal checking by the prover in the background.

   986   This can be done to some extent in the main text area alone, especially for

   987   well-structured Isar proofs.

   988

   989   Nonetheless, internal proof state needs to be inspected in many situations

   990   of exploration and debugging''. The \<^emph>\<open>State\<close> panel shows exclusively such

   991   proof state messages without further distraction, while all other messages

   992   are displayed in \<^emph>\<open>Output\<close> (\secref{sec:output}).

   993   \Figref{fig:output-and-state} shows a typical GUI layout where both panels

   994   are open.

   995

   996   \begin{figure}[!htb]

   997   \begin{center}

   998   \includegraphics[scale=0.333]{output-and-state}

   999   \end{center}

  1000   \caption{Separate proof state display (right) and other output (bottom).}

  1001   \label{fig:output-and-state}

  1002   \end{figure}

  1003

  1004   Another typical arrangement has more than one \<^emph>\<open>State\<close> panel open (as

  1005   floating windows), with \<^emph>\<open>Auto update\<close> disabled to look at an old situation

  1006   while the proof text in the vicinity is changed. The \<^emph>\<open>Update\<close> button

  1007   triggers an explicit one-shot update; this operation is also available via

  1008   the action @{action "isabelle.update-state"} (keyboard shortcut \<^verbatim>\<open>S+ENTER\<close>).

  1009

  1010   On small screens, it is occasionally useful to have all messages

  1011   concatenated in the regular \<^emph>\<open>Output\<close> panel, e.g.\ see

  1012   \figref{fig:output-including-state}.

  1013

  1014   \<^medskip>

  1015   The mechanics of \<^emph>\<open>Output\<close> versus \<^emph>\<open>State\<close> are slightly different:

  1016

  1017     \<^item> \<^emph>\<open>Output\<close> shows information that is continuously produced and already

  1018     present when the GUI wants to show it. This is implicitly controlled by

  1019     the visible perspective on the text.

  1020

  1021     \<^item> \<^emph>\<open>State\<close> initiates a real-time query on demand, with a full round trip

  1022     including a fresh print operation on the prover side. This is controlled

  1023     explicitly when the cursor is moved to the next command (\<^emph>\<open>Auto update\<close>)

  1024     or the \<^emph>\<open>Update\<close> operation is triggered.

  1025

  1026   This can make a difference in GUI responsibility and resource usage within

  1027   the prover process. Applications with very big proof states that are only

  1028   inspected in isolation work better with the \<^emph>\<open>State\<close> panel.

  1029 \<close>

  1030

  1031

  1032 section \<open>Query \label{sec:query}\<close>

  1033

  1034 text \<open>

  1035   The \<^emph>\<open>Query\<close> panel provides various GUI forms to request extra information

  1036   from the prover, as a replacement of old-style diagnostic commands like

  1037   @{command find_theorems}. There are input fields and buttons for a

  1038   particular query command, with output in a dedicated text area.

  1039

  1040   The main query modes are presented as separate tabs: \<^emph>\<open>Find Theorems\<close>,

  1041   \<^emph>\<open>Find Constants\<close>, \<^emph>\<open>Print Context\<close>, e.g.\ see \figref{fig:query}. As usual

  1042   in jEdit, multiple \<^emph>\<open>Query\<close> windows may be active at the same time: any

  1043   number of floating instances, but at most one docked instance (which is used

  1044   by default).

  1045

  1046   \begin{figure}[!htb]

  1047   \begin{center}

  1048   \includegraphics[scale=0.333]{query}

  1049   \end{center}

  1050   \caption{An instance of the Query panel: find theorems}

  1051   \label{fig:query}

  1052   \end{figure}

  1053

  1054   \<^medskip>

  1055   The following GUI elements are common to all query modes:

  1056

  1057     \<^item> The spinning wheel provides feedback about the status of a pending query

  1058     wrt.\ the evaluation of its context and its own operation.

  1059

  1060     \<^item> The \<^emph>\<open>Apply\<close> button attaches a fresh query invocation to the current

  1061     context of the command where the cursor is pointing in the text.

  1062

  1063     \<^item> The \<^emph>\<open>Search\<close> field allows to highlight query output according to some

  1064     regular expression, in the notation that is commonly used on the Java

  1065     platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/javase/8/docs/api/java/util/regex/Pattern.html\<close>\<close>

  1066     This may serve as an additional visual filter of the result.

  1067

  1068     \<^item> The \<^emph>\<open>Zoom\<close> box controls the font size of the output area.

  1069

  1070   All query operations are asynchronous: there is no need to wait for the

  1071   evaluation of the document for the query context, nor for the query

  1072   operation itself. Query output may be detached as independent \<^emph>\<open>Info\<close>

  1073   window, using a menu operation of the dockable window manager. The printed

  1074   result usually provides sufficient clues about the original query, with some

  1075   hyperlink to its context (via markup of its head line).

  1076 \<close>

  1077

  1078

  1079 subsection \<open>Find theorems\<close>

  1080

  1081 text \<open>

  1082   The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Theorems\<close> mode retrieves facts from the theory

  1083   or proof context matching all of given criteria in the \<^emph>\<open>Find\<close> text field. A

  1084   single criterium has the following syntax:

  1085

  1086   @{rail \<open>

  1087     ('-'?) ('name' ':' @{syntax name} | 'intro' | 'elim' | 'dest' |

  1088       'solves' | 'simp' ':' @{syntax term} | @{syntax term})

  1089   \<close>}

  1090

  1091   See also the Isar command @{command_ref find_theorems} in @{cite

  1092   "isabelle-isar-ref"}.

  1093 \<close>

  1094

  1095

  1096 subsection \<open>Find constants\<close>

  1097

  1098 text \<open>

  1099   The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Constants\<close> mode prints all constants whose type

  1100   meets all of the given criteria in the \<^emph>\<open>Find\<close> text field. A single

  1101   criterium has the following syntax:

  1102

  1103   @{rail \<open>

  1104     ('-'?)

  1105       ('name' ':' @{syntax name} | 'strict' ':' @{syntax type} | @{syntax type})

  1106   \<close>}

  1107

  1108   See also the Isar command @{command_ref find_consts} in @{cite

  1109   "isabelle-isar-ref"}.

  1110 \<close>

  1111

  1112

  1113 subsection \<open>Print context\<close>

  1114

  1115 text \<open>

  1116   The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Print Context\<close> mode prints information from the

  1117   theory or proof context, or proof state. See also the Isar commands

  1118   @{command_ref print_context}, @{command_ref print_cases}, @{command_ref

  1119   print_term_bindings}, @{command_ref print_theorems}, described in @{cite

  1120   "isabelle-isar-ref"}.

  1121 \<close>

  1122

  1123

  1124 section \<open>Tooltips and hyperlinks \label{sec:tooltips-hyperlinks}\<close>

  1125

  1126 text \<open>

  1127   Formally processed text (prover input or output) contains rich markup that

  1128   can be explored by using the \<^verbatim>\<open>CONTROL\<close> modifier key on Linux and Windows,

  1129   or \<^verbatim>\<open>COMMAND\<close> on Mac OS X. Hovering with the mouse while the modifier is

  1130   pressed reveals a \<^emph>\<open>tooltip\<close> (grey box over the text with a yellow popup)

  1131   and/or a \<^emph>\<open>hyperlink\<close> (black rectangle over the text with change of mouse

  1132   pointer); see also \figref{fig:tooltip}.

  1133

  1134   \begin{figure}[!htb]

  1135   \begin{center}

  1136   \includegraphics[scale=0.5]{popup1}

  1137   \end{center}

  1138   \caption{Tooltip and hyperlink for some formal entity}

  1139   \label{fig:tooltip}

  1140   \end{figure}

  1141

  1142   Tooltip popups use the same rendering technology as the main text area, and

  1143   further tooltips and/or hyperlinks may be exposed recursively by the same

  1144   mechanism; see \figref{fig:nested-tooltips}.

  1145

  1146   \begin{figure}[!htb]

  1147   \begin{center}

  1148   \includegraphics[scale=0.5]{popup2}

  1149   \end{center}

  1150   \caption{Nested tooltips over formal entities}

  1151   \label{fig:nested-tooltips}

  1152   \end{figure}

  1153

  1154   The tooltip popup window provides some controls to \<^emph>\<open>close\<close> or \<^emph>\<open>detach\<close> the

  1155   window, turning it into a separate \<^emph>\<open>Info\<close> window managed by jEdit. The

  1156   \<^verbatim>\<open>ESCAPE\<close> key closes \<^emph>\<open>all\<close> popups, which is particularly relevant when

  1157   nested tooltips are stacking up.

  1158

  1159   \<^medskip>

  1160   A black rectangle in the text indicates a hyperlink that may be followed by

  1161   a mouse click (while the \<^verbatim>\<open>CONTROL\<close> or \<^verbatim>\<open>COMMAND\<close> modifier key is still

  1162   pressed). Such jumps to other text locations are recorded by the

  1163   \<^emph>\<open>Navigator\<close> plugin, which is bundled with Isabelle/jEdit and enabled by

  1164   default. There are usually navigation arrows in the main jEdit toolbar.

  1165

  1166   Note that the link target may be a file that is itself not subject to formal

  1167   document processing of the editor session and thus prevents further

  1168   exploration: the chain of hyperlinks may end in some source file of the

  1169   underlying logic image, or within the ML bootstrap sources of Isabelle/Pure.

  1170 \<close>

  1171

  1172

  1173 section \<open>Formal scopes and semantic selection\<close>

  1174

  1175 text \<open>

  1176   Formal entities are semantically annotated in the source text as explained

  1177   in \secref{sec:tooltips-hyperlinks}. A \<^emph>\<open>formal scope\<close> consists of the

  1178   defining position with all its referencing positions. This correspondence is

  1179   highlighted in the text according to the cursor position, see also

  1180   \figref{fig:scope1}. Here the referencing positions are rendered with an

  1181   additional border, in reminiscence to a hyperlink: clicking there moves the

  1182   cursor to the original defining position.

  1183

  1184   \begin{figure}[!htb]

  1185   \begin{center}

  1186   \includegraphics[scale=0.5]{scope1}

  1187   \end{center}

  1188   \caption{Scope of formal entity: defining vs.\ referencing positions}

  1189   \label{fig:scope1}

  1190   \end{figure}

  1191

  1192   The action @{action_def "isabelle.select-entity"} (shortcut \<^verbatim>\<open>CS+ENTER\<close>)

  1193   supports semantic selection of all occurrences of the formal entity at the

  1194   caret position. This facilitates systematic renaming, using regular jEdit

  1195   editing of a multi-selection, see also \figref{fig:scope2}.

  1196

  1197   \begin{figure}[!htb]

  1198   \begin{center}

  1199   \includegraphics[scale=0.5]{scope2}

  1200   \end{center}

  1201   \caption{The result of semantic selection and systematic renaming}

  1202   \label{fig:scope2}

  1203   \end{figure}

  1204 \<close>

  1205

  1206

  1207 section \<open>Completion \label{sec:completion}\<close>

  1208

  1209 text \<open>

  1210   Smart completion of partial input is the IDE functionality \<^emph>\<open>par

  1211   excellance\<close>. Isabelle/jEdit combines several sources of information to

  1212   achieve that. Despite its complexity, it should be possible to get some idea

  1213   how completion works by experimentation, based on the overview of completion

  1214   varieties in \secref{sec:completion-varieties}. The remaining subsections

  1215   explain concepts around completion more systematically.

  1216

  1217   \<^medskip>

  1218   \<^emph>\<open>Explicit completion\<close> is triggered by the action @{action_ref

  1219   "isabelle.complete"}, which is bound to the keyboard shortcut \<^verbatim>\<open>C+b\<close>, and

  1220   thus overrides the jEdit default for @{action_ref "complete-word"}.

  1221

  1222   \<^emph>\<open>Implicit completion\<close> hooks into the regular keyboard input stream of the

  1223   editor, with some event filtering and optional delays.

  1224

  1225   \<^medskip>

  1226   Completion options may be configured in \<^emph>\<open>Plugin Options~/ Isabelle~/

  1227   General~/ Completion\<close>. These are explained in further detail below, whenever

  1228   relevant. There is also a summary of options in

  1229   \secref{sec:completion-options}.

  1230

  1231   The asynchronous nature of PIDE interaction means that information from the

  1232   prover is delayed --- at least by a full round-trip of the document update

  1233   protocol. The default options already take this into account, with a

  1234   sufficiently long completion delay to speculate on the availability of all

  1235   relevant information from the editor and the prover, before completing text

  1236   immediately or producing a popup. Although there is an inherent danger of

  1237   non-deterministic behaviour due to such real-time parameters, the general

  1238   completion policy aims at determined results as far as possible.

  1239 \<close>

  1240

  1241

  1242 subsection \<open>Varieties of completion \label{sec:completion-varieties}\<close>

  1243

  1244 subsubsection \<open>Built-in templates\<close>

  1245

  1246 text \<open>

  1247   Isabelle is ultimately a framework of nested sub-languages of different

  1248   kinds and purposes. The completion mechanism supports this by the following

  1249   built-in templates:

  1250

  1251     \<^descr> \<^verbatim>\<open>\<close> (single ASCII back-quote) or \<^verbatim>\<open>"\<close> (double ASCII quote) support

  1252     \<^emph>\<open>quotations\<close> via text cartouches. There are three selections, which are

  1253     always presented in the same order and do not depend on any context

  1254     information. The default choice produces a template \<open>\<open>\<box>\<close>\<close>'', where the

  1255     box indicates the cursor position after insertion; the other choices help

  1256     to repair the block structure of unbalanced text cartouches.

  1257

  1258     \<^descr> \<^verbatim>\<open>@{\<close> is completed to the template \<open>@{\<box>}\<close>'', where the box indicates

  1259     the cursor position after insertion. Here it is convenient to use the

  1260     wildcard \<^verbatim>\<open>__\<close>'' or a more specific name prefix to let semantic

  1261     completion of name-space entries propose antiquotation names.

  1262

  1263   With some practice, input of quoted sub-languages and antiquotations of

  1264   embedded languages should work fluently. Note that national keyboard layouts

  1265   might cause problems with back-quote as dead key, but double quote can be

  1266   used instead.

  1267 \<close>

  1268

  1269

  1270 subsubsection \<open>Syntax keywords\<close>

  1271

  1272 text \<open>

  1273   Syntax completion tables are determined statically from the keywords of the

  1274   outer syntax'' of the underlying edit mode: for theory files this is the

  1275   syntax of Isar commands according to the cumulative theory imports.

  1276

  1277   Keywords are usually plain words, which means the completion mechanism only

  1278   inserts them directly into the text for explicit completion

  1279   (\secref{sec:completion-input}), but produces a popup

  1280   (\secref{sec:completion-popup}) otherwise.

  1281

  1282   At the point where outer syntax keywords are defined, it is possible to

  1283   specify an alternative replacement string to be inserted instead of the

  1284   keyword itself. An empty string means to suppress the keyword altogether,

  1285   which is occasionally useful to avoid confusion, e.g.\ the rare keyword

  1286   @{command simproc_setup} vs.\ the frequent name-space entry \<open>simp\<close>.

  1287 \<close>

  1288

  1289

  1290 subsubsection \<open>Isabelle symbols\<close>

  1291

  1292 text \<open>

  1293   The completion tables for Isabelle symbols (\secref{sec:symbols}) are

  1294   determined statically from \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and @{path   1295 "$ISABELLE_HOME_USER/etc/symbols"} for each symbol specification as follows:

  1296

  1297   \<^medskip>

  1298   \begin{tabular}{ll}

  1299   \<^bold>\<open>completion entry\<close> & \<^bold>\<open>example\<close> \\\hline

  1300   literal symbol & \<^verbatim>\<open>\<forall>\<close> \\

  1301   symbol name with backslash & \<^verbatim>\<open>\\<close>\<^verbatim>\<open>forall\<close> \\

  1302   symbol abbreviation & \<^verbatim>\<open>ALL\<close> or \<^verbatim>\<open>!\<close> \\

  1303   \end{tabular}

  1304   \<^medskip>

  1305

  1306   When inserted into the text, the above examples all produce the same Unicode

  1307   rendering \<open>\<forall>\<close> of the underlying symbol \<^verbatim>\<open>\<forall>\<close>.

  1308

  1309   A symbol abbreviation that is a plain word, like \<^verbatim>\<open>ALL\<close>, is treated like a

  1310   syntax keyword. Non-word abbreviations like \<^verbatim>\<open>-->\<close> are inserted more

  1311   aggressively, except for single-character abbreviations like \<^verbatim>\<open>!\<close> above.

  1312

  1313   Completion via abbreviations like \<^verbatim>\<open>ALL\<close> or \<^verbatim>\<open>-->\<close> depends on the semantic

  1314   language context (\secref{sec:completion-context}). In contrast, backslash

  1315   sequences like \<^verbatim>\<open>\forall\<close> \<^verbatim>\<open>\<forall>\<close> are always possible, but require

  1316   additional interaction to confirm (via popup).

  1317

  1318   The latter is important in ambiguous situations, e.g.\ for Isabelle document

  1319   source, which may contain formal symbols or informal {\LaTeX} macros.

  1320   Backslash sequences also help when input is broken, and thus escapes its

  1321   normal semantic context: e.g.\ antiquotations or string literals in ML,

  1322   which do not allow arbitrary backslash sequences.

  1323 \<close>

  1324

  1325

  1326 subsubsection \<open>User-defined abbreviations\<close>

  1327

  1328 text \<open>

  1329   The theory header syntax supports abbreviations via the \<^theory_text>\<open>abbrevs\<close> keyword

  1330   @{cite "isabelle-isar-ref"}. This is a slight generalization of built-in

  1331   templates and abbreviations for Isabelle symbols, as explained above.

  1332   Examples may be found in the Isabelle sources, by searching for

  1333   \<^verbatim>\<open>abbrevs\<close>'' in \<^verbatim>\<open>*.thy\<close> files.

  1334

  1335   The \<^emph>\<open>Symbols\<close> panel shows the abbreviations that are available in the

  1336   current theory buffer (according to its \<^theory_text>\<open>imports\<close>) in the \<^verbatim>\<open>Abbrevs\<close> tab.

  1337 \<close>

  1338

  1339

  1340 subsubsection \<open>Name-space entries\<close>

  1341

  1342 text \<open>

  1343   This is genuine semantic completion, using information from the prover, so

  1344   it requires some delay. A \<^emph>\<open>failed name-space lookup\<close> produces an error

  1345   message that is annotated with a list of alternative names that are legal.

  1346   The list of results is truncated according to the system option

  1347   @{system_option_ref completion_limit}. The completion mechanism takes this

  1348   into account when collecting information on the prover side.

  1349

  1350   Already recognized names are \<^emph>\<open>not\<close> completed further, but completion may be

  1351   extended by appending a suffix of underscores. This provokes a failed

  1352   lookup, and another completion attempt while ignoring the underscores. For

  1353   example, in a name space where \<^verbatim>\<open>foo\<close> and \<^verbatim>\<open>foobar\<close> are known, the input

  1354   \<^verbatim>\<open>foo\<close> remains unchanged, but \<^verbatim>\<open>foo_\<close> may be completed to \<^verbatim>\<open>foo\<close> or

  1355   \<^verbatim>\<open>foobar\<close>.

  1356

  1357   The special identifier \<^verbatim>\<open>__\<close>'' serves as a wild-card for arbitrary

  1358   completion: it exposes the name-space content to the completion mechanism

  1359   (truncated according to @{system_option completion_limit}). This is

  1360   occasionally useful to explore an unknown name-space, e.g.\ in some

  1361   template.

  1362 \<close>

  1363

  1364

  1365 subsubsection \<open>File-system paths\<close>

  1366

  1367 text \<open>

  1368   Depending on prover markup about file-system paths in the source text, e.g.\

  1369   for the argument of a load command (\secref{sec:aux-files}), the completion

  1370   mechanism explores the directory content and offers the result as completion

  1371   popup. Relative path specifications are understood wrt.\ the \<^emph>\<open>master

  1372   directory\<close> of the document node (\secref{sec:buffer-node}) of the enclosing

  1373   editor buffer; this requires a proper theory, not an auxiliary file.

  1374

  1375   A suffix of slashes may be used to continue the exploration of an already

  1376   recognized directory name.

  1377 \<close>

  1378

  1379

  1380 subsubsection \<open>Spell-checking\<close>

  1381

  1382 text \<open>

  1383   The spell-checker combines semantic markup from the prover (regions of plain

  1384   words) with static dictionaries (word lists) that are known to the editor.

  1385

  1386   Unknown words are underlined in the text, using @{system_option_ref

  1387   spell_checker_color} (blue by default). This is not an error, but a hint to

  1388   the user that some action may be taken. The jEdit context menu provides

  1389   various actions, as far as applicable:

  1390

  1391   \<^medskip>

  1392   \begin{tabular}{l}

  1393   @{action_ref "isabelle.complete-word"} \\

  1394   @{action_ref "isabelle.exclude-word"} \\

  1395   @{action_ref "isabelle.exclude-word-permanently"} \\

  1396   @{action_ref "isabelle.include-word"} \\

  1397   @{action_ref "isabelle.include-word-permanently"} \\

  1398   \end{tabular}

  1399   \<^medskip>

  1400

  1401   Instead of the specific @{action_ref "isabelle.complete-word"}, it is also

  1402   possible to use the generic @{action_ref "isabelle.complete"} with its

  1403   default keyboard shortcut \<^verbatim>\<open>C+b\<close>.

  1404

  1405   \<^medskip>

  1406   Dictionary lookup uses some educated guesses about lower-case, upper-case,

  1407   and capitalized words. This is oriented on common use in English, where this

  1408   aspect is not decisive for proper spelling (in contrast to German, for

  1409   example).

  1410 \<close>

  1411

  1412

  1413 subsection \<open>Semantic completion context \label{sec:completion-context}\<close>

  1414

  1415 text \<open>

  1416   Completion depends on a semantic context that is provided by the prover,

  1417   although with some delay, because at least a full PIDE protocol round-trip

  1418   is required. Until that information becomes available in the PIDE

  1419   document-model, the default context is given by the outer syntax of the

  1420   editor mode (see also \secref{sec:buffer-node}).

  1421

  1422   The semantic \<^emph>\<open>language context\<close> provides information about nested

  1423   sub-languages of Isabelle: keywords are only completed for outer syntax, and

  1424   antiquotations for languages that support them. Symbol abbreviations only

  1425   work for specific sub-languages: e.g.\ \<^verbatim>\<open>=>\<close>'' is \<^emph>\<open>not\<close> completed in

  1426   regular ML source, but is completed within ML strings, comments,

  1427   antiquotations. Backslash representations of symbols like \<^verbatim>\<open>\foobar\<close>'' or

  1428   \<^verbatim>\<open>\<foobar>\<close>'' work in any context --- after additional confirmation.

  1429

  1430   The prover may produce \<^emph>\<open>no completion\<close> markup in exceptional situations, to

  1431   tell that some language keywords should be excluded from further completion

  1432   attempts. For example, \<^verbatim>\<open>:\<close>'' within accepted Isar syntax looses its

  1433   meaning as abbreviation for symbol \<open>\<in>\<close>''.

  1434 \<close>

  1435

  1436

  1437 subsection \<open>Input events \label{sec:completion-input}\<close>

  1438

  1439 text \<open>

  1440   Completion is triggered by certain events produced by the user, with

  1441   optional delay after keyboard input according to @{system_option

  1442   jedit_completion_delay}.

  1443

  1444   \<^descr>[Explicit completion] works via action @{action_ref "isabelle.complete"}

  1445   with keyboard shortcut \<^verbatim>\<open>C+b\<close>. This overrides the shortcut for @{action_ref

  1446   "complete-word"} in jEdit, but it is possible to restore the original jEdit

  1447   keyboard mapping of @{action "complete-word"} via \<^emph>\<open>Global Options~/

  1448   Shortcuts\<close> and invent a different one for @{action "isabelle.complete"}.

  1449

  1450   \<^descr>[Explicit spell-checker completion] works via @{action_ref

  1451   "isabelle.complete-word"}, which is exposed in the jEdit context menu, if

  1452   the mouse points to a word that the spell-checker can complete.

  1453

  1454   \<^descr>[Implicit completion] works via regular keyboard input of the editor. It

  1455   depends on further side-conditions:

  1456

  1457     \<^enum> The system option @{system_option_ref jedit_completion} needs to be

  1458     enabled (default).

  1459

  1460     \<^enum> Completion of syntax keywords requires at least 3 relevant characters in

  1461     the text.

  1462

  1463     \<^enum> The system option @{system_option_ref jedit_completion_delay} determines

  1464     an additional delay (0.5 by default), before opening a completion popup.

  1465     The delay gives the prover a chance to provide semantic completion

  1466     information, notably the context (\secref{sec:completion-context}).

  1467

  1468     \<^enum> The system option @{system_option_ref jedit_completion_immediate}

  1469     (enabled by default) controls whether replacement text should be inserted

  1470     immediately without popup, regardless of @{system_option

  1471     jedit_completion_delay}. This aggressive mode of completion is restricted

  1472     to symbol abbreviations that are not plain words (\secref{sec:symbols}).

  1473

  1474     \<^enum> Completion of symbol abbreviations with only one relevant character in

  1475     the text always enforces an explicit popup, regardless of

  1476     @{system_option_ref jedit_completion_immediate}.

  1477 \<close>

  1478

  1479

  1480 subsection \<open>Completion popup \label{sec:completion-popup}\<close>

  1481

  1482 text \<open>

  1483   A \<^emph>\<open>completion popup\<close> is a minimally invasive GUI component over the text

  1484   area that offers a selection of completion items to be inserted into the

  1485   text, e.g.\ by mouse clicks. Items are sorted dynamically, according to the

  1486   frequency of selection, with persistent history. The popup may interpret

  1487   special keys \<^verbatim>\<open>ENTER\<close>, \<^verbatim>\<open>TAB\<close>, \<^verbatim>\<open>ESCAPE\<close>, \<^verbatim>\<open>UP\<close>, \<^verbatim>\<open>DOWN\<close>, \<^verbatim>\<open>PAGE_UP\<close>,

  1488   \<^verbatim>\<open>PAGE_DOWN\<close>, but all other key events are passed to the underlying text

  1489   area. This allows to ignore unwanted completions most of the time and

  1490   continue typing quickly. Thus the popup serves as a mechanism of

  1491   confirmation of proposed items, while the default is to continue without

  1492   completion.

  1493

  1494   The meaning of special keys is as follows:

  1495

  1496   \<^medskip>

  1497   \begin{tabular}{ll}

  1498   \<^bold>\<open>key\<close> & \<^bold>\<open>action\<close> \\\hline

  1499   \<^verbatim>\<open>ENTER\<close> & select completion (if @{system_option jedit_completion_select_enter}) \\

  1500   \<^verbatim>\<open>TAB\<close> & select completion (if @{system_option jedit_completion_select_tab}) \\

  1501   \<^verbatim>\<open>ESCAPE\<close> & dismiss popup \\

  1502   \<^verbatim>\<open>UP\<close> & move up one item \\

  1503   \<^verbatim>\<open>DOWN\<close> & move down one item \\

  1504   \<^verbatim>\<open>PAGE_UP\<close> & move up one page of items \\

  1505   \<^verbatim>\<open>PAGE_DOWN\<close> & move down one page of items \\

  1506   \end{tabular}

  1507   \<^medskip>

  1508

  1509   Movement within the popup is only active for multiple items. Otherwise the

  1510   corresponding key event retains its standard meaning within the underlying

  1511   text area.

  1512 \<close>

  1513

  1514

  1515 subsection \<open>Insertion \label{sec:completion-insert}\<close>

  1516

  1517 text \<open>

  1518   Completion may first propose replacements to be selected (via a popup), or

  1519   replace text immediately in certain situations and depending on certain

  1520   options like @{system_option jedit_completion_immediate}. In any case,

  1521   insertion works uniformly, by imitating normal jEdit text insertion,

  1522   depending on the state of the \<^emph>\<open>text selection\<close>. Isabelle/jEdit tries to

  1523   accommodate the most common forms of advanced selections in jEdit, but not

  1524   all combinations make sense. At least the following important cases are

  1525   well-defined:

  1526

  1527     \<^descr>[No selection.] The original is removed and the replacement inserted,

  1528     depending on the caret position.

  1529

  1530     \<^descr>[Rectangular selection of zero width.] This special case is treated by

  1531     jEdit as tall caret'' and insertion of completion imitates its normal

  1532     behaviour: separate copies of the replacement are inserted for each line

  1533     of the selection.

  1534

  1535     \<^descr>[Other rectangular selection or multiple selections.] Here the original

  1536     is removed and the replacement is inserted for each line (or segment) of

  1537     the selection.

  1538

  1539   Support for multiple selections is particularly useful for \<^emph>\<open>HyperSearch\<close>:

  1540   clicking on one of the items in the \<^emph>\<open>HyperSearch Results\<close> window makes

  1541   jEdit select all its occurrences in the corresponding line of text. Then

  1542   explicit completion can be invoked via \<^verbatim>\<open>C+b\<close>, e.g.\ to replace occurrences

  1543   of \<^verbatim>\<open>-->\<close> by \<open>\<longrightarrow>\<close>.

  1544

  1545   \<^medskip>

  1546   Insertion works by removing and inserting pieces of text from the buffer.

  1547   This counts as one atomic operation on the jEdit history. Thus unintended

  1548   completions may be reverted by the regular @{action undo} action of jEdit.

  1549   According to normal jEdit policies, the recovered text after @{action undo}

  1550   is selected: \<^verbatim>\<open>ESCAPE\<close> is required to reset the selection and to continue

  1551   typing more text.

  1552 \<close>

  1553

  1554

  1555 subsection \<open>Options \label{sec:completion-options}\<close>

  1556

  1557 text \<open>

  1558   This is a summary of Isabelle/Scala system options that are relevant for

  1559   completion. They may be configured in \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>

  1560   as usual.

  1561

  1562   \<^item> @{system_option_def completion_limit} specifies the maximum number of

  1563   items for various semantic completion operations (name-space entries etc.)

  1564

  1565   \<^item> @{system_option_def jedit_completion} guards implicit completion via

  1566   regular jEdit key events (\secref{sec:completion-input}): it allows to

  1567   disable implicit completion altogether.

  1568

  1569   \<^item> @{system_option_def jedit_completion_select_enter} and @{system_option_def

  1570   jedit_completion_select_tab} enable keys to select a completion item from

  1571   the popup (\secref{sec:completion-popup}). Note that a regular mouse click

  1572   on the list of items is always possible.

  1573

  1574   \<^item> @{system_option_def jedit_completion_context} specifies whether the

  1575   language context provided by the prover should be used at all. Disabling

  1576   that option makes completion less semantic''. Note that incomplete or

  1577   severely broken input may cause some disagreement of the prover and the user

  1578   about the intended language context.

  1579

  1580   \<^item> @{system_option_def jedit_completion_delay} and @{system_option_def

  1581   jedit_completion_immediate} determine the handling of keyboard events for

  1582   implicit completion (\secref{sec:completion-input}).

  1583

  1584   A @{system_option jedit_completion_delay}~\<^verbatim>\<open>> 0\<close> postpones the processing of

  1585   key events, until after the user has stopped typing for the given time span,

  1586   but @{system_option jedit_completion_immediate}~\<^verbatim>\<open>= true\<close> means that

  1587   abbreviations of Isabelle symbols are handled nonetheless.

  1588

  1589   \<^item> @{system_option_def jedit_completion_path_ignore} specifies glob''

  1590   patterns to ignore in file-system path completion (separated by colons),

  1591   e.g.\ backup files ending with tilde.

  1592

  1593   \<^item> @{system_option_def spell_checker} is a global guard for all spell-checker

  1594   operations: it allows to disable that mechanism altogether.

  1595

  1596   \<^item> @{system_option_def spell_checker_dictionary} determines the current

  1597   dictionary, taken from the colon-separated list in the settings variable

  1598   @{setting_def JORTHO_DICTIONARIES}. There are jEdit actions to specify local

  1599   updates to a dictionary, by including or excluding words. The result of

  1600   permanent dictionary updates is stored in the directory @{path

  1601   "$ISABELLE_HOME_USER/dictionaries"}, in a separate file for each dictionary.   1602   1603 \<^item> @{system_option_def spell_checker_elements} specifies a comma-separated   1604 list of markup elements that delimit words in the source that is subject to   1605 spell-checking, including various forms of comments.   1606 \<close>   1607   1608   1609 section \<open>Automatically tried tools \label{sec:auto-tools}\<close>   1610   1611 text \<open>   1612 Continuous document processing works asynchronously in the background.   1613 Visible document source that has been evaluated may get augmented by   1614 additional results of \<^emph>\<open>asynchronous print functions\<close>. An example for that   1615 is proof state output, if that is enabled in the Output panel   1616 (\secref{sec:output}). More heavy-weight print functions may be applied as   1617 well, e.g.\ to prove or disprove parts of the formal text by other means.   1618   1619 Isabelle/HOL provides various automatically tried tools that operate on   1620 outermost goal statements (e.g.\ @{command lemma}, @{command theorem}),   1621 independently of the state of the current proof attempt. They work   1622 implicitly without any arguments. Results are output as \<^emph>\<open>information   1623 messages\<close>, which are indicated in the text area by blue squiggles and a blue   1624 information sign in the gutter (see \figref{fig:auto-tools}). The message   1625 content may be shown as for other output (see also \secref{sec:output}).   1626 Some tools produce output with \<^emph>\<open>sendback\<close> markup, which means that clicking   1627 on certain parts of the text inserts that into the source in the proper   1628 place.   1629   1630 \begin{figure}[!htb]   1631 \begin{center}   1632 \includegraphics[scale=0.333]{auto-tools}   1633 \end{center}   1634 \caption{Result of automatically tried tools}   1635 \label{fig:auto-tools}   1636 \end{figure}   1637   1638 \<^medskip>   1639 The following Isabelle system options control the behavior of automatically   1640 tried tools (see also the jEdit dialog window \<^emph>\<open>Plugin Options~/ Isabelle~/   1641 General~/ Automatically tried tools\<close>):   1642   1643 \<^item> @{system_option_ref auto_methods} controls automatic use of a combination   1644 of standard proof methods (@{method auto}, @{method simp}, @{method blast},   1645 etc.). This corresponds to the Isar command @{command_ref "try0"} @{cite   1646 "isabelle-isar-ref"}.   1647   1648 The tool is disabled by default, since unparameterized invocation of   1649 standard proof methods often consumes substantial CPU resources without   1650 leading to success.   1651   1652 \<^item> @{system_option_ref auto_nitpick} controls a slightly reduced version of   1653 @{command_ref nitpick}, which tests for counterexamples using first-order   1654 relational logic. See also the Nitpick manual @{cite "isabelle-nitpick"}.   1655   1656 This tool is disabled by default, due to the extra overhead of invoking an   1657 external Java process for each attempt to disprove a subgoal.   1658   1659 \<^item> @{system_option_ref auto_quickcheck} controls automatic use of   1660 @{command_ref quickcheck}, which tests for counterexamples using a series of   1661 assignments for free variables of a subgoal.   1662   1663 This tool is \<^emph>\<open>enabled\<close> by default. It requires little overhead, but is a   1664 bit weaker than @{command nitpick}.   1665   1666 \<^item> @{system_option_ref auto_sledgehammer} controls a significantly reduced   1667 version of @{command_ref sledgehammer}, which attempts to prove a subgoal   1668 using external automatic provers. See also the Sledgehammer manual @{cite   1669 "isabelle-sledgehammer"}.   1670   1671 This tool is disabled by default, due to the relatively heavy nature of   1672 Sledgehammer.   1673   1674 \<^item> @{system_option_ref auto_solve_direct} controls automatic use of   1675 @{command_ref solve_direct}, which checks whether the current subgoals can   1676 be solved directly by an existing theorem. This also helps to detect   1677 duplicate lemmas.   1678   1679 This tool is \<^emph>\<open>enabled\<close> by default.   1680   1681   1682 Invocation of automatically tried tools is subject to some global policies   1683 of parallel execution, which may be configured as follows:   1684   1685 \<^item> @{system_option_ref auto_time_limit} (default 2.0) determines the timeout   1686 (in seconds) for each tool execution.   1687   1688 \<^item> @{system_option_ref auto_time_start} (default 1.0) determines the start   1689 delay (in seconds) for automatically tried tools, after the main command   1690 evaluation is finished.   1691   1692   1693 Each tool is submitted independently to the pool of parallel execution tasks   1694 in Isabelle/ML, using hardwired priorities according to its relative   1695 heaviness''. The main stages of evaluation and printing of proof states   1696 take precedence, but an already running tool is not canceled and may thus   1697 reduce reactivity of proof document processing.   1698   1699 Users should experiment how the available CPU resources (number of cores)   1700 are best invested to get additional feedback from prover in the background,   1701 by using a selection of weaker or stronger tools.   1702 \<close>   1703   1704   1705 section \<open>Sledgehammer \label{sec:sledgehammer}\<close>   1706   1707 text \<open>   1708 The \<^emph>\<open>Sledgehammer\<close> panel (\figref{fig:sledgehammer}) provides a view on   1709 some independent execution of the Isar command @{command_ref sledgehammer},   1710 with process indicator (spinning wheel) and GUI elements for important   1711 Sledgehammer arguments and options. Any number of Sledgehammer panels may be   1712 active, according to the standard policies of Dockable Window Management in   1713 jEdit. Closing such windows also cancels the corresponding prover tasks.   1714   1715 \begin{figure}[!htb]   1716 \begin{center}   1717 \includegraphics[scale=0.333]{sledgehammer}   1718 \end{center}   1719 \caption{An instance of the Sledgehammer panel}   1720 \label{fig:sledgehammer}   1721 \end{figure}   1722   1723 The \<^emph>\<open>Apply\<close> button attaches a fresh invocation of @{command sledgehammer}   1724 to the command where the cursor is pointing in the text --- this should be   1725 some pending proof problem. Further buttons like \<^emph>\<open>Cancel\<close> and \<^emph>\<open>Locate\<close>   1726 help to manage the running process.   1727   1728 Results appear incrementally in the output window of the panel. Proposed   1729 proof snippets are marked-up as \<^emph>\<open>sendback\<close>, which means a single mouse   1730 click inserts the text into a suitable place of the original source. Some   1731 manual editing may be required nonetheless, say to remove earlier proof   1732 attempts.   1733 \<close>   1734   1735   1736 chapter \<open>Isabelle document preparation\<close>   1737   1738 text \<open>   1739 The ultimate purpose of Isabelle is to produce nicely rendered documents   1740 with the Isabelle document preparation system, which is based on {\LaTeX};   1741 see also @{cite "isabelle-system" and "isabelle-isar-ref"}. Isabelle/jEdit   1742 provides some additional support for document editing.   1743 \<close>   1744   1745   1746 section \<open>Document outline\<close>   1747   1748 text \<open>   1749 Theory sources may contain document markup commands, such as @{command_ref   1750 chapter}, @{command_ref section}, @{command subsection}. The Isabelle   1751 SideKick parser (\secref{sec:sidekick}) represents this document outline as   1752 structured tree view, with formal statements and proofs nested inside; see   1753 \figref{fig:sidekick-document}.   1754   1755 \begin{figure}[!htb]   1756 \begin{center}   1757 \includegraphics[scale=0.333]{sidekick-document}   1758 \end{center}   1759 \caption{Isabelle document outline via SideKick tree view}   1760 \label{fig:sidekick-document}   1761 \end{figure}   1762   1763 It is also possible to use text folding according to this structure, by   1764 adjusting \<^emph>\<open>Utilities / Buffer Options / Folding mode\<close> of jEdit. The default   1765 mode \<^verbatim>\<open>isabelle\<close> uses the structure of formal definitions, statements, and   1766 proofs. The alternative mode \<^verbatim>\<open>sidekick\<close> uses the document structure of the   1767 SideKick parser, as explained above.   1768 \<close>   1769   1770   1771 section \<open>Markdown structure\<close>   1772   1773 text \<open>   1774 Document text is internally structured in paragraphs and nested lists, using   1775 notation that is similar to Markdown\<^footnote>\<open>\<^url>\<open>http://commonmark.org\<close>\<close>. There are   1776 special control symbols for items of different kinds of lists, corresponding   1777 to \<^verbatim>\<open>itemize\<close>, \<^verbatim>\<open>enumerate\<close>, \<^verbatim>\<open>description\<close> in {\LaTeX}. This is illustrated   1778 in for \<^verbatim>\<open>itemize\<close> in \figref{fig:markdown-document}.   1779   1780 \begin{figure}[!htb]   1781 \begin{center}   1782 \includegraphics[scale=0.333]{markdown-document}   1783 \end{center}   1784 \caption{Markdown structure within document text}   1785 \label{fig:markdown-document}   1786 \end{figure}   1787   1788 Items take colour according to the depth of nested lists. This helps to   1789 explore the implicit rules for list structure interactively. There is also   1790 markup for individual paragraphs in the text: it may be explored via mouse   1791 hovering with \<^verbatim>\<open>CONTROL\<close> / \<^verbatim>\<open>COMMAND\<close> as usual   1792 (\secref{sec:tooltips-hyperlinks}).   1793 \<close>   1794   1795   1796 section \<open>Citations and Bib{\TeX} entries \label{sec:bibtex}\<close>   1797   1798 text \<open>   1799 Citations are managed by {\LaTeX} and Bib{\TeX} in \<^verbatim>\<open>.bib\<close> files. The   1800 Isabelle session build process and the @{tool latex} tool @{cite   1801 "isabelle-system"} are smart enough to assemble the result, based on the   1802 session directory layout.   1803   1804 The document antiquotation \<open>@{cite}\<close> is described in @{cite   1805 "isabelle-isar-ref"}. Within the Prover IDE it provides semantic markup for   1806 tooltips, hyperlinks, and completion for Bib{\TeX} database entries.   1807 Isabelle/jEdit does \<^emph>\<open>not\<close> know about the actual Bib{\TeX} environment used   1808 in {\LaTeX} batch-mode, but it can take citations from those \<^verbatim>\<open>.bib\<close> files   1809 that happen to be open in the editor; see \figref{fig:cite-completion}.   1810   1811 \begin{figure}[!htb]   1812 \begin{center}   1813 \includegraphics[scale=0.333]{cite-completion}   1814 \end{center}   1815 \caption{Semantic completion of citations from open Bib{\TeX} files}   1816 \label{fig:cite-completion}   1817 \end{figure}   1818   1819 Isabelle/jEdit also provides some support for editing \<^verbatim>\<open>.bib\<close> files   1820 themselves. There is syntax highlighting based on entry types (according to   1821 standard Bib{\TeX} styles), a context-menu to compose entries   1822 systematically, and a SideKick tree view of the overall content; see   1823 \figref{fig:bibtex-mode}.   1824   1825 \begin{figure}[!htb]   1826 \begin{center}   1827 \includegraphics[scale=0.333]{bibtex-mode}   1828 \end{center}   1829 \caption{Bib{\TeX} mode with context menu and SideKick tree view}   1830 \label{fig:bibtex-mode}   1831 \end{figure}   1832 \<close>   1833   1834   1835 chapter \<open>ML debugging within the Prover IDE\<close>   1836   1837 text \<open>   1838 Isabelle/ML is based on Poly/ML\<^footnote>\<open>\<^url>\<open>http://www.polyml.org\<close>\<close> and thus   1839 benefits from the source-level debugger of that implementation of Standard   1840 ML. The Prover IDE provides the \<^emph>\<open>Debugger\<close> dockable to connect to running   1841 ML threads, inspect the stack frame with local ML bindings, and evaluate ML   1842 expressions in a particular run-time context. A typical debugger session is   1843 shown in \figref{fig:ml-debugger}.   1844   1845 ML debugging depends on the following pre-requisites.   1846   1847 \<^enum> ML source needs to be compiled with debugging enabled. This may be   1848 controlled for particular chunks of ML sources using any of the subsequent   1849 facilities.   1850   1851 \<^enum> The system option @{system_option_ref ML_debugger} as implicit state   1852 of the Isabelle process. It may be changed in the menu \<^emph>\<open>Plugins /   1853 Plugin Options / Isabelle / General\<close>. ML modules need to be reloaded and   1854 recompiled to pick up that option as intended.   1855   1856 \<^enum> The configuration option @{attribute_ref ML_debugger}, with an   1857 attribute of the same name, to update a global or local context (e.g.\   1858 with the @{command declare} command).   1859   1860 \<^enum> Commands that modify @{attribute ML_debugger} state for individual   1861 files: @{command_ref ML_file_debug}, @{command_ref ML_file_no_debug},   1862 @{command_ref SML_file_debug}, @{command_ref SML_file_no_debug}.   1863   1864 The instrumentation of ML code for debugging causes minor run-time   1865 overhead. ML modules that implement critical system infrastructure may   1866 lead to deadlocks or other undefined behaviour, when put under debugger   1867 control!   1868   1869 \<^enum> The \<^emph>\<open>Debugger\<close> panel needs to be active, otherwise the program ignores   1870 debugger instrumentation of the compiler and runs unmanaged. It is also   1871 possible to start debugging with the panel open, and later undock it, to   1872 let the program continue unhindered.   1873   1874 \<^enum> The ML program needs to be stopped at a suitable breakpoint, which may   1875 be activated individually or globally as follows.   1876   1877 For ML sources that have been compiled with debugger support, the IDE   1878 visualizes possible breakpoints in the text. A breakpoint may be toggled   1879 by pointing accurately with the mouse, with a right-click to activate   1880 jEdit's context menu and its \<^emph>\<open>Toggle Breakpoint\<close> item. Alternatively, the   1881 \<^emph>\<open>Break\<close> checkbox in the \<^emph>\<open>Debugger\<close> panel may be enabled to stop ML   1882 threads always at the next possible breakpoint.   1883   1884 Note that the state of individual breakpoints \<^emph>\<open>gets lost\<close> when the   1885 coresponding ML source is re-compiled! This may happen unintentionally,   1886 e.g.\ when following hyperlinks into ML modules that have not been loaded   1887 into the IDE before.   1888   1889 \begin{figure}[!htb]   1890 \begin{center}   1891 \includegraphics[scale=0.333]{ml-debugger}   1892 \end{center}   1893 \caption{ML debugger session}   1894 \label{fig:ml-debugger}   1895 \end{figure}   1896   1897 The debugger panel (\figref{fig:ml-debugger}) shows a list of all threads   1898 that are presently stopped. Each thread shows a stack of all function   1899 invocations that lead to the current breakpoint at the top.   1900   1901 It is possible to jump between stack positions freely, by clicking on this   1902 list. The current situation is displayed in the big output window, as a   1903 local ML environment with names and printed values.   1904   1905 ML expressions may be evaluated in the current context by entering snippets   1906 of source into the text fields labeled \<open>Context\<close> and \<open>ML\<close>, and pushing the   1907 \<open>Eval\<close> button. By default, the source is interpreted as Isabelle/ML with the   1908 usual support for antiquotations (like @{command ML}, @{command ML_file}).   1909 Alternatively, strict Standard ML may be enforced via the \<^emph>\<open>SML\<close> checkbox   1910 (like @{command SML_file}).   1911   1912 The context for Isabelle/ML is optional, it may evaluate to a value of type   1913 @{ML_type theory}, @{ML_type Proof.context}, or @{ML_type Context.generic}.   1914 Thus the given ML expression (with its antiquotations) may be subject to the   1915 intended dynamic run-time context, instead of the static compile-time   1916 context.   1917   1918 \<^medskip>   1919 The buttons labeled \<^emph>\<open>Continue\<close>, \<^emph>\<open>Step\<close>, \<^emph>\<open>Step over\<close>, \<^emph>\<open>Step out\<close>   1920 recommence execution of the program, with different policies concerning   1921 nested function invocations. The debugger always moves the cursor within the   1922 ML source to the next breakpoint position, and offers new stack frames as   1923 before.   1924 \<close>   1925   1926   1927 chapter \<open>Miscellaneous tools\<close>   1928   1929 section \<open>Timing\<close>   1930   1931 text \<open>   1932 Managed evaluation of commands within PIDE documents includes timing   1933 information, which consists of elapsed (wall-clock) time, CPU time, and GC   1934 (garbage collection) time. Note that in a multithreaded system it is   1935 difficult to measure execution time precisely: elapsed time is closer to the   1936 real requirements of runtime resources than CPU or GC time, which are both   1937 subject to influences from the parallel environment that are outside the   1938 scope of the current command transaction.   1939   1940 The \<^emph>\<open>Timing\<close> panel provides an overview of cumulative command timings for   1941 each document node. Commands with elapsed time below the given threshold are   1942 ignored in the grand total. Nodes are sorted according to their overall   1943 timing. For the document node that corresponds to the current buffer,   1944 individual command timings are shown as well. A double-click on a theory   1945 node or command moves the editor focus to that particular source position.   1946   1947 It is also possible to reveal individual timing information via some tooltip   1948 for the corresponding command keyword, using the technique of mouse hovering   1949 with \<^verbatim>\<open>CONTROL\<close>~/ \<^verbatim>\<open>COMMAND\<close> modifier (\secref{sec:tooltips-hyperlinks}).   1950 Actual display of timing depends on the global option @{system_option_ref   1951 jedit_timing_threshold}, which can be configured in \<^emph>\<open>Plugin Options~/   1952 Isabelle~/ General\<close>.   1953   1954 \<^medskip>   1955 The \<^emph>\<open>Monitor\<close> panel visualizes various data collections about recent   1956 activity of the Isabelle/ML task farm and the underlying ML runtime system.   1957 The display is continuously updated according to @{system_option_ref   1958 editor_chart_delay}. Note that the painting of the chart takes considerable   1959 runtime itself --- on the Java Virtual Machine that runs Isabelle/Scala, not   1960 Isabelle/ML. Internally, the Isabelle/Scala module \<^verbatim>\<open>isabelle.ML_Statistics\<close>   1961 provides further access to statistics of Isabelle/ML.   1962 \<close>   1963   1964   1965 section \<open>Low-level output\<close>   1966   1967 text \<open>   1968 Prover output is normally shown directly in the main text area or specific   1969 panels like \<^emph>\<open>Output\<close> (\secref{sec:output}) or \<^emph>\<open>State\<close>   1970 (\secref{sec:state-output}). Beyond this, it is occasionally useful to   1971 inspect low-level output channels via some of the following additional   1972 panels:   1973   1974 \<^item> \<^emph>\<open>Protocol\<close> shows internal messages between the Isabelle/Scala and   1975 Isabelle/ML side of the PIDE document editing protocol. Recording of   1976 messages starts with the first activation of the corresponding dockable   1977 window; earlier messages are lost.   1978   1979 Actual display of protocol messages causes considerable slowdown, so it is   1980 important to undock all \<^emph>\<open>Protocol\<close> panels for production work.   1981   1982 \<^item> \<^emph>\<open>Raw Output\<close> shows chunks of text from the \<^verbatim>\<open>stdout\<close> and \<^verbatim>\<open>stderr\<close>   1983 channels of the prover process. Recording of output starts with the first   1984 activation of the corresponding dockable window; earlier output is lost.   1985   1986 The implicit stateful nature of physical I/O channels makes it difficult to   1987 relate raw output to the actual command from where it was originating.   1988 Parallel execution may add to the confusion. Peeking at physical process I/O   1989 is only the last resort to diagnose problems with tools that are not PIDE   1990 compliant.   1991   1992 Under normal circumstances, prover output always works via managed message   1993 channels (corresponding to @{ML writeln}, @{ML warning}, @{ML   1994 Output.error_message} in Isabelle/ML), which are displayed by regular means   1995 within the document model (\secref{sec:output}). Unhandled Isabelle/ML   1996 exceptions are printed by the system via @{ML Output.error_message}.   1997   1998 \<^item> \<^emph>\<open>Syslog\<close> shows system messages that might be relevant to diagnose   1999 problems with the startup or shutdown phase of the prover process; this also   2000 includes raw output on \<^verbatim>\<open>stderr\<close>. Isabelle/ML also provides an explicit @{ML   2001 Output.system_message} operation, which is occasionally useful for   2002 diagnostic purposes within the system infrastructure itself.   2003   2004 A limited amount of syslog messages are buffered, independently of the   2005 docking state of the \<^emph>\<open>Syslog\<close> panel. This allows to diagnose serious   2006 problems with Isabelle/PIDE process management, outside of the actual   2007 protocol layer.   2008   2009 Under normal situations, such low-level system output can be ignored.   2010 \<close>   2011   2012   2013 chapter \<open>Known problems and workarounds \label{sec:problems}\<close>   2014   2015 text \<open>   2016 \<^item> \<^bold>\<open>Problem:\<close> Odd behavior of some diagnostic commands with global   2017 side-effects, like writing a physical file.   2018   2019 \<^bold>\<open>Workaround:\<close> Copy/paste complete command text from elsewhere, or disable   2020 continuous checking temporarily.   2021   2022 \<^item> \<^bold>\<open>Problem:\<close> No direct support to remove document nodes from the collection   2023 of theories.   2024   2025 \<^bold>\<open>Workaround:\<close> Clear the buffer content of unused files and close \<^emph>\<open>without\<close>   2026 saving changes.   2027   2028 \<^item> \<^bold>\<open>Problem:\<close> Keyboard shortcuts \<^verbatim>\<open>C+PLUS\<close> and \<^verbatim>\<open>C+MINUS\<close> for adjusting the   2029 editor font size depend on platform details and national keyboards.   2030   2031 \<^bold>\<open>Workaround:\<close> Rebind keys via \<^emph>\<open>Global Options~/ Shortcuts\<close>.   2032   2033 \<^item> \<^bold>\<open>Problem:\<close> The Mac OS X key sequence \<^verbatim>\<open>COMMAND+COMMA\<close> for application   2034 \<^emph>\<open>Preferences\<close> is in conflict with the jEdit default keyboard shortcut for   2035 \<^emph>\<open>Incremental Search Bar\<close> (action @{action_ref "quick-search"}).   2036   2037 \<^bold>\<open>Workaround:\<close> Rebind key via \<^emph>\<open>Global Options~/ Shortcuts\<close> according to   2038 national keyboard, e.g.\ \<^verbatim>\<open>COMMAND+SLASH\<close> on English ones.   2039   2040 \<^item> \<^bold>\<open>Problem:\<close> On Mac OS X with native Apple look-and-feel, some exotic   2041 national keyboards may cause a conflict of menu accelerator keys with   2042 regular jEdit key bindings. This leads to duplicate execution of the   2043 corresponding jEdit action.   2044   2045 \<^bold>\<open>Workaround:\<close> Disable the native Apple menu bar via Java runtime option   2046 \<^verbatim>\<open>-Dapple.laf.useScreenMenuBar=false\<close>.   2047   2048 \<^item> \<^bold>\<open>Problem:\<close> Mac OS X system fonts sometimes lead to character drop-outs in   2049 the main text area.   2050   2051 \<^bold>\<open>Workaround:\<close> Use the default \<^verbatim>\<open>IsabelleText\<close> font.   2052   2053 \<^item> \<^bold>\<open>Problem:\<close> Mac OS X with Retina display has problems to determine the   2054 font metrics of \<^verbatim>\<open>IsabelleText\<close> accurately, notably in plain Swing text   2055 fields (e.g.\ in the \<^emph>\<open>Search and Replace\<close> dialog).   2056   2057 \<^bold>\<open>Workaround:\<close> Install \<^verbatim>\<open>IsabelleText\<close> and \<^verbatim>\<open>IsabelleTextBold\<close> on the system   2058 with \<^emph>\<open>Font Book\<close>, despite the warnings in \secref{sec:symbols} against   2059 that! The \<^verbatim>\<open>.ttf\<close> font files reside in some directory @{path   2060 "$ISABELLE_HOME/contrib/isabelle_fonts-XYZ"}.

  2061

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

  2063   event handling of Java/AWT/Swing.

  2064

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

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

  2067

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

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

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

  2071

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

  2073

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

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

  2076   positions of Java/AWT/Swing.

  2077

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

  2079

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

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

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

  2083

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

  2085   on Mac OS X).

  2086

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

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

  2089

  2090   \<^bold>\<open>Workaround:\<close> On a 64bit platform, ensure that the JVM runs in 64bit mode,

  2091   but the Isabelle/ML process remains in 32bit mode! Do not switch Isabelle/ML

  2092   into 64bit mode in the expectation to be more efficient'' --- this

  2093   requires approx.\ 32\,GB to make sense.

  2094

  2095   For the JVM, always use the 64bit version. That is the default on all

  2096   platforms, except for Windows: the standard download is for win32, but there

  2097   is a separate download for win64. This implicitly provides a larger default

  2098   heap for the JVM.

  2099

  2100   Moreover, it is possible to increase JVM heap parameters explicitly, by

  2101   editing platform-specific files (for properties'' or options'') that are

  2102   associated with the main app bundle.

  2103

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

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

  2106   which sometimes helps in low-memory situations.

  2107 \<close>

  2108

  2109 end`