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