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