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