src/Doc/JEdit/JEdit.thy
author wenzelm
Wed Nov 20 23:00:18 2013 +0100 (2013-11-20)
changeset 54639 5adc68deb322
parent 54638 46adb57c89db
child 54643 57aefb80b639
permissions -rw-r--r--
updated to Isabelle2013-2;
wenzelm@53981
     1
(*:wrap=hard:maxLineLen=78:*)
wenzelm@53981
     2
wenzelm@53769
     3
theory JEdit
wenzelm@53769
     4
imports Base
wenzelm@53769
     5
begin
wenzelm@53769
     6
wenzelm@53769
     7
chapter {* Introduction *}
wenzelm@53769
     8
wenzelm@53770
     9
section {* Concepts and terminology *}
wenzelm@53770
    10
wenzelm@54321
    11
text {* Isabelle/jEdit is a Prover IDE that integrates \emph{parallel
wenzelm@54321
    12
  proof checking} \cite{Wenzel:2009,Wenzel:2013:ITP} with
wenzelm@54321
    13
  \emph{asynchronous user interaction}
wenzelm@54321
    14
  \cite{Wenzel:2010,Wenzel:2012:UITP-EPTCS}, based on a
wenzelm@54321
    15
  document-oriented approach to \emph{continuous proof processing}
wenzelm@54321
    16
  \cite{Wenzel:2011:CICM,Wenzel:2012}. Many concepts and system
wenzelm@54321
    17
  components are fit together in order to make this work. The main
wenzelm@54329
    18
  building blocks are as follows.
wenzelm@53769
    19
wenzelm@54321
    20
  \begin{description}
wenzelm@53769
    21
wenzelm@54329
    22
  \item [PIDE] is a general framework for Prover IDEs based on
wenzelm@54329
    23
  Isabelle/Scala. It is built around a concept of parallel and
wenzelm@54329
    24
  asynchronous document processing, which is supported natively by the
wenzelm@54329
    25
  parallel proof engine that is implemented in Isabelle/ML. The prover
wenzelm@54329
    26
  discontinues the traditional TTY-based command loop, and supports
wenzelm@54329
    27
  direct editing of formal source text with rich formal markup for GUI
wenzelm@54329
    28
  rendering.
wenzelm@53770
    29
wenzelm@54321
    30
  \item [Isabelle/ML] is the implementation and extension language of
wenzelm@54321
    31
  Isabelle, see also \cite{isabelle-implementation}. It is integrated
wenzelm@54329
    32
  into the logical context of Isabelle/Isar and allows to manipulate
wenzelm@54329
    33
  logical entities directly. Arbitrary add-on tools may be implemented
wenzelm@54329
    34
  for object-logics such as Isabelle/HOL.
wenzelm@53770
    35
wenzelm@54321
    36
  \item [Isabelle/Scala] is the system programming language of
wenzelm@54321
    37
  Isabelle. It extends the pure logical environment of Isabelle/ML
wenzelm@54321
    38
  towards the ``real world'' of graphical user interfaces, text
wenzelm@54321
    39
  editors, IDE frameworks, web services etc.  Special infrastructure
wenzelm@54372
    40
  allows to transfer algebraic datatypes and formatted text easily
wenzelm@54372
    41
  between ML and Scala, using asynchronous protocol commands.
wenzelm@54321
    42
wenzelm@54329
    43
  \item [jEdit] is a sophisticated text editor implemented in
wenzelm@54329
    44
  Java.\footnote{\url{http://www.jedit.org}} It is easily extensible
wenzelm@54329
    45
  by plugins written in languages that work on the JVM, e.g.\
wenzelm@54329
    46
  Scala\footnote{\url{http://www.scala-lang.org/}}.
wenzelm@53770
    47
wenzelm@54321
    48
  \item [Isabelle/jEdit] is the main example application of the PIDE
wenzelm@54329
    49
  framework and the default user-interface for Isabelle. It targets
wenzelm@54329
    50
  both beginners and experts. Technically, Isabelle/jEdit combines a
wenzelm@54372
    51
  slightly modified version of the jEdit code base with a special
wenzelm@54372
    52
  plugin for Isabelle, integrated as standalone application for the
wenzelm@54372
    53
  main operating system platforms: Linux, Windows, Mac OS X.
wenzelm@53770
    54
wenzelm@54321
    55
  \end{description}
wenzelm@53770
    56
wenzelm@54321
    57
  The subtle differences of Isabelle/ML versus Standard ML,
wenzelm@54330
    58
  Isabelle/Scala versus Scala, Isabelle/jEdit versus jEdit need to be
wenzelm@54330
    59
  taken into account when discussing any of these PIDE building blocks
wenzelm@54330
    60
  in public forums, mailing lists, or even scientific publications.
wenzelm@54330
    61
  *}
wenzelm@53770
    62
wenzelm@53770
    63
wenzelm@53770
    64
section {* The Isabelle/jEdit Prover IDE *}
wenzelm@53770
    65
wenzelm@53770
    66
text {*
wenzelm@54357
    67
  \begin{figure}[htb]
wenzelm@54331
    68
  \begin{center}
wenzelm@53773
    69
  \includegraphics[width=\textwidth]{isabelle-jedit}
wenzelm@54331
    70
  \end{center}
wenzelm@54331
    71
  \caption{The Isabelle/jEdit Prover IDE}
wenzelm@54357
    72
  \label{fig:isabelle-jedit}
wenzelm@54331
    73
  \end{figure}
wenzelm@53773
    74
wenzelm@54357
    75
  Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some
wenzelm@54357
    76
  plugins for the well-known jEdit text editor
wenzelm@54357
    77
  \url{http://www.jedit.org}, according to the following principles.
wenzelm@53770
    78
wenzelm@53770
    79
  \begin{itemize}
wenzelm@53769
    80
wenzelm@54321
    81
  \item The original jEdit look-and-feel is generally preserved,
wenzelm@54348
    82
  although some default properties are changed to accommodate Isabelle
wenzelm@54348
    83
  (e.g.\ the text area font).
wenzelm@53770
    84
wenzelm@54321
    85
  \item Formal Isabelle/Isar text is checked asynchronously while
wenzelm@54321
    86
  editing.  The user is in full command of the editor, and the prover
wenzelm@54321
    87
  refrains from locking portions of the buffer.
wenzelm@53770
    88
wenzelm@53770
    89
  \item Prover feedback works via colors, boxes, squiggly underline,
wenzelm@54348
    90
  hyperlinks, popup windows, icons, clickable output --- all based on
wenzelm@54321
    91
  semantic markup produced by Isabelle in the background.
wenzelm@53770
    92
wenzelm@54321
    93
  \item Using the mouse together with the modifier key @{verbatim
wenzelm@54321
    94
  CONTROL} (Linux, Windows) or @{verbatim COMMAND} (Mac OS X) exposes
wenzelm@54321
    95
  additional formal content via tooltips and/or hyperlinks.
wenzelm@53769
    96
wenzelm@54321
    97
  \item Formal output (in popups etc.) may be explored recursively,
wenzelm@54321
    98
  using the same techniques as in the editor source buffer.
wenzelm@53770
    99
wenzelm@54329
   100
  \item Additional panels (e.g.\ \emph{Output}, \emph{Symbols}) are
wenzelm@54329
   101
  organized by the Dockable Window Manager of jEdit, which also allows
wenzelm@54329
   102
  multiple floating instances of each window class.
wenzelm@54329
   103
wenzelm@54321
   104
  \item The prover process and source files are managed on the editor
wenzelm@54321
   105
  side.  The prover operates on timeless and stateless document
wenzelm@54348
   106
  content as provided via Isabelle/Scala.
wenzelm@53770
   107
wenzelm@54321
   108
  \item Plugin options of jEdit (for the \emph{Isabelle} plugin) give
wenzelm@54348
   109
  access to a selection of Isabelle/Scala options and its persistent
wenzelm@54321
   110
  preferences, usually with immediate effect on the prover back-end or
wenzelm@54321
   111
  editor front-end.
wenzelm@53770
   112
wenzelm@53770
   113
  \item The logic image of the prover session may be specified within
wenzelm@54348
   114
  Isabelle/jEdit.  The new image is provided automatically by the
wenzelm@54348
   115
  Isabelle build tool after restart of the application.
wenzelm@53770
   116
wenzelm@53770
   117
  \end{itemize}
wenzelm@53769
   118
*}
wenzelm@53769
   119
wenzelm@53770
   120
wenzelm@54321
   121
subsection {* Documentation *}
wenzelm@54321
   122
wenzelm@54321
   123
text {* Regular jEdit documentation is accessible via its @{verbatim
wenzelm@54321
   124
  Help} menu or @{verbatim F1} keyboard shortcut. This includes a full
wenzelm@54321
   125
  \emph{User's Guide} and \emph{Frequently Asked Questions} for this
wenzelm@54321
   126
  sophisticated text editor.
wenzelm@54321
   127
wenzelm@54329
   128
  Most of this information about jEdit is relevant for Isabelle/jEdit
wenzelm@54329
   129
  as well, but one needs to keep in mind that defaults sometimes
wenzelm@54329
   130
  differ, and the official jEdit documentation does not know about the
wenzelm@54329
   131
  Isabelle plugin with its special support for theory editing.
wenzelm@54321
   132
*}
wenzelm@54321
   133
wenzelm@54321
   134
wenzelm@54321
   135
subsection {* Plugins *}
wenzelm@54321
   136
wenzelm@54321
   137
text {* The \emph{Plugin Manager} of jEdit allows to augment editor
wenzelm@54321
   138
  functionality by JVM modules (jars) that are provided by the central
wenzelm@54372
   139
  plugin repository, which is accessible via various mirror sites.
wenzelm@54321
   140
wenzelm@54321
   141
  Connecting to the plugin server infrastructure of the jEdit project
wenzelm@54348
   142
  allows to update bundled plugins or to add further functionality.
wenzelm@54348
   143
  This needs to be done with the usual care for such an open bazaar of
wenzelm@54348
   144
  contributions. Arbitrary combinations of add-on features are apt to
wenzelm@54348
   145
  cause problems.  It is advisable to start with the default
wenzelm@54348
   146
  configuration of Isabelle/jEdit and develop some understanding how
wenzelm@54348
   147
  it is supposed to work, before loading additional plugins at a grand
wenzelm@54348
   148
  scale.
wenzelm@54321
   149
wenzelm@54348
   150
  \medskip The main \emph{Isabelle} plugin is an integral part of
wenzelm@54348
   151
  Isabelle/jEdit and needs to remain active at all times! A few
wenzelm@54348
   152
  additional plugins are bundled with Isabelle/jEdit for convenience
wenzelm@54348
   153
  or out of necessity, notably \emph{Console} with its Isabelle/Scala
wenzelm@54348
   154
  sub-plugin and \emph{SideKick} with some Isabelle-specific parsers
wenzelm@54348
   155
  for document tree structure.  The \emph{ErrorList} plugin is
wenzelm@54348
   156
  required by \emph{SideKick}, but not used specifically in
wenzelm@54348
   157
  Isabelle/jEdit. *}
wenzelm@54321
   158
wenzelm@54321
   159
wenzelm@54321
   160
subsection {* Options *}
wenzelm@54321
   161
wenzelm@54329
   162
text {* Both jEdit and Isabelle have distinctive management of
wenzelm@54348
   163
  persistent options.
wenzelm@54321
   164
wenzelm@54372
   165
  Regular jEdit options are accessible via the dialog for
wenzelm@54372
   166
  \emph{Plugins / Plugin Options}, which is also accessible via
wenzelm@54372
   167
  \emph{Utilities / Global Options}.  Changed properties are stored in
wenzelm@54372
   168
  @{file_unchecked "$ISABELLE_HOME_USER/jedit/properties"}.  In
wenzelm@54372
   169
  contrast, Isabelle system options are managed by Isabelle/Scala and
wenzelm@54372
   170
  changed values stored in @{file_unchecked
wenzelm@54372
   171
  "$ISABELLE_HOME_USER/etc/preferences"}, independently of the jEdit
wenzelm@54372
   172
  properties.  See also \cite{isabelle-sys}, especially the coverage
wenzelm@54372
   173
  of sessions and command-line tools like @{tool build} or @{tool
wenzelm@54372
   174
  options}.
wenzelm@54321
   175
wenzelm@54348
   176
  Those Isabelle options that are declared as \textbf{public} are
wenzelm@54348
   177
  configurable in jEdit via \emph{Plugin Options / Isabelle /
wenzelm@54348
   178
  General}.  Moreover, there are various options for rendering of
wenzelm@54348
   179
  document content, which are configurable via \emph{Plugin Options /
wenzelm@54348
   180
  Isabelle / Rendering}.  Thus \emph{Plugin Options / Isabelle} in
wenzelm@54372
   181
  jEdit provides a view on a subset of Isabelle system options.  Note
wenzelm@54372
   182
  that some of these options affect general parameters that are
wenzelm@54372
   183
  relevant outside Isabelle/jEdit as well, e.g.\ @{system_option
wenzelm@54372
   184
  threads} or @{system_option parallel_proofs} for the Isabelle build
wenzelm@54372
   185
  tool \cite{isabelle-sys}.
wenzelm@54329
   186
wenzelm@54348
   187
  \medskip All options are loaded on startup and saved on shutdown of
wenzelm@54372
   188
  Isabelle/jEdit.  Editing the machine-generated @{file_unchecked
wenzelm@54372
   189
  "$ISABELLE_HOME_USER/jedit/properties"} or @{file_unchecked
wenzelm@54329
   190
  "$ISABELLE_HOME_USER/etc/preferences"} manually while the
wenzelm@54348
   191
  application is running is likely to cause surprise due to lost
wenzelm@54348
   192
  update!  *}
wenzelm@54321
   193
wenzelm@54321
   194
wenzelm@54321
   195
subsection {* Keymaps *}
wenzelm@54321
   196
wenzelm@54321
   197
text {* Keyboard shortcuts used to be managed as jEdit properties in
wenzelm@54321
   198
  the past, but recent versions (2013) have a separate concept of
wenzelm@54348
   199
  \emph{keymap} that is configurable via \emph{Global Options /
wenzelm@54348
   200
  Shortcuts}.  The @{verbatim imported} keymap is derived from the
wenzelm@54330
   201
  initial environment of properties that is available at the first
wenzelm@54348
   202
  start of the editor; afterwards the keymap file takes precedence.
wenzelm@54321
   203
wenzelm@54321
   204
  This is relevant for Isabelle/jEdit due to various fine-tuning of
wenzelm@54321
   205
  default properties, and additional keyboard shortcuts for Isabelle
wenzelm@54372
   206
  specific functionality. Users may change their keymap later, but
wenzelm@54372
   207
  need to copy Isabelle-specific key bindings manually (see also
wenzelm@54372
   208
  @{file_unchecked "$ISABELLE_HOME_USER/jedit/keymaps"}).  *}
wenzelm@54321
   209
wenzelm@54321
   210
wenzelm@54322
   211
subsection {* Look-and-feel *}
wenzelm@54321
   212
wenzelm@54330
   213
text {* jEdit is a Java/AWT/Swing application with some ambition to
wenzelm@54329
   214
  support ``native'' look-and-feel on all platforms, within the limits
wenzelm@54330
   215
  of what Oracle as Java provider and major operating system
wenzelm@54330
   216
  distributors allow (see also \secref{sec:problems}).
wenzelm@54321
   217
wenzelm@54329
   218
  Isabelle/jEdit enables platform-specific look-and-feel by default as
wenzelm@54330
   219
  follows:
wenzelm@54321
   220
wenzelm@54321
   221
  \begin{description}
wenzelm@54321
   222
wenzelm@54321
   223
  \item[Linux] The platform-independent \emph{Nimbus} is used by
wenzelm@54372
   224
  default.
wenzelm@54321
   225
wenzelm@54372
   226
  \emph{GTK+} works under the side-condition that the overall GTK
wenzelm@54372
   227
  theme is selected in a Swing-friendly way.\footnote{GTK support in
wenzelm@54372
   228
  Java/Swing was once marketed aggressively by Sun, but never quite
wenzelm@54372
   229
  finished, and is today (2013) lagging a bit behind further
wenzelm@54372
   230
  development of Swing and GTK.}
wenzelm@54321
   231
wenzelm@54381
   232
  \item[Windows] Regular \emph{Windows} is used by default, but
wenzelm@54381
   233
  \emph{Windows Classic} also works.
wenzelm@54372
   234
wenzelm@54372
   235
  \item[Mac OS X] Regular \emph{Mac OS X} is used by default.
wenzelm@54372
   236
wenzelm@54321
   237
  Moreover the bundled \emph{MacOSX} plugin provides various functions
wenzelm@54321
   238
  that are expected from applications on that particular platform:
wenzelm@54321
   239
  quit from menu or dock, preferences menu, drag-and-drop of text
wenzelm@54321
   240
  files on the application, full-screen mode for main editor windows
wenzelm@54321
   241
  etc.
wenzelm@54321
   242
wenzelm@54321
   243
  \end{description}
wenzelm@54321
   244
wenzelm@54321
   245
  Users may experiment with different look-and-feels, but need to keep
wenzelm@54329
   246
  in mind that this extra variance of GUI functionality is unlikely to
wenzelm@54372
   247
  work in arbitrary combinations.  The platform-independent
wenzelm@54372
   248
  \emph{Nimbus} and \emph{Metal} should always work.  The historic
wenzelm@54372
   249
  \emph{CDE/Motif} is better avoided.
wenzelm@54372
   250
wenzelm@54372
   251
  After changing the look-and-feel in \emph{Global Options /
wenzelm@54372
   252
  Appearance}, it is advisable to restart Isabelle/jEdit in order to
wenzelm@54372
   253
  take full effect.  *}
wenzelm@54321
   254
wenzelm@54321
   255
wenzelm@54372
   256
chapter {* Prover IDE functionality *}
wenzelm@54372
   257
wenzelm@54372
   258
section {* File-system access *}
wenzelm@54351
   259
wenzelm@54351
   260
text {* File specifications in jEdit follow various formats and
wenzelm@54351
   261
  conventions according to \emph{Virtual File Systems}, which may be
wenzelm@54351
   262
  also provided by additional plugins.  This allows to access remote
wenzelm@54351
   263
  files via the @{verbatim "http:"} protocol prefix, for example.
wenzelm@54351
   264
  Isabelle/jEdit attempts to work with the file-system access model of
wenzelm@54351
   265
  jEdit as far as possible.  In particular, theory sources are passed
wenzelm@54351
   266
  directly from the editor to the prover, without indirection via
wenzelm@54351
   267
  files.
wenzelm@54351
   268
wenzelm@54351
   269
  Despite the flexibility of URLs in jEdit, local files are
wenzelm@54351
   270
  particularly important and are accessible without protocol prefix.
wenzelm@54351
   271
  Here the path notation is that of the Java Virtual Machine on the
wenzelm@54351
   272
  underlying platform.  On Windows the preferred form uses
wenzelm@54351
   273
  backslashes, but happens to accept Unix/POSIX forward slashes, too.
wenzelm@54351
   274
  Further differences arise due to drive letters and network shares.
wenzelm@54351
   275
wenzelm@54351
   276
  The Java notation for files needs to be distinguished from the one
wenzelm@54351
   277
  of Isabelle, which uses POSIX notation with forward slashes on
wenzelm@54351
   278
  \emph{all} platforms.\footnote{Isabelle on Windows uses Cygwin
wenzelm@54351
   279
  file-system access.}  Moreover, environment variables from the
wenzelm@54351
   280
  Isabelle process may be used freely, e.g.\ @{file
wenzelm@54638
   281
  "$ISABELLE_HOME/etc/symbols"} or @{file "$POLYML_HOME/README"}.
wenzelm@54638
   282
  There are special shortcuts: @{file "~"} for @{file "$USER_HOME"}
wenzelm@54638
   283
  and @{file "~~"} for @{file "$ISABELLE_HOME"}.
wenzelm@54351
   284
wenzelm@54351
   285
  \medskip Since jEdit happens to support environment variables within
wenzelm@54351
   286
  file specifications as well, it is natural to use similar notation
wenzelm@54351
   287
  within the editor, e.g.\ in the file-browser.  This does not work in
wenzelm@54351
   288
  full generality, though, due to the bias of jEdit towards
wenzelm@54351
   289
  platform-specific notation and of Isabelle towards POSIX.  Moreover,
wenzelm@54351
   290
  the Isabelle settings environment is not yet active when starting
wenzelm@54351
   291
  Isabelle/jEdit via its standard application wrapper (in contrast to
wenzelm@54351
   292
  @{verbatim "isabelle jedit"} run from the command line).
wenzelm@54351
   293
wenzelm@54351
   294
  For convenience, Isabelle/jEdit imitates at least @{verbatim
wenzelm@54351
   295
  "$ISABELLE_HOME"} and @{verbatim "$ISABELLE_HOME_USER"} within the
wenzelm@54351
   296
  Java process environment, in order to allow easy access to these
wenzelm@54351
   297
  important places from the editor.
wenzelm@54351
   298
wenzelm@54351
   299
  Moreover note that path specifications in prover input or output
wenzelm@54351
   300
  usually include formal markup that turns it into a hyperlink (see
wenzelm@54352
   301
  also \secref{sec:tooltips-hyperlinks}).  This allows to open the
wenzelm@54351
   302
  corresponding file in the text editor, independently of the path
wenzelm@54351
   303
  notation.  *}
wenzelm@54351
   304
wenzelm@54351
   305
wenzelm@54353
   306
section {* Text buffers and theories \label{sec:buffers-theories} *}
wenzelm@54322
   307
wenzelm@54350
   308
text {* As regular text editor, jEdit maintains a collection of open
wenzelm@54350
   309
  \emph{text buffers} to store source files; each buffer may be
wenzelm@54350
   310
  associated with any number of visible \emph{text areas}.  Buffers
wenzelm@54350
   311
  are subject to an \emph{edit mode} that is determined from the file
wenzelm@54350
   312
  type.  Files with extension \texttt{.thy} are assigned to the mode
wenzelm@54350
   313
  \emph{isabelle} and treated specifically.
wenzelm@54321
   314
wenzelm@54329
   315
  \medskip Isabelle theory files are automatically added to the formal
wenzelm@54329
   316
  document model of Isabelle/Scala, which maintains a family of
wenzelm@54329
   317
  versions of all sources for the prover.  The \emph{Theories} panel
wenzelm@54322
   318
  provides an overview of the status of continuous checking of theory
wenzelm@54329
   319
  sources.  Unlike batch sessions \cite{isabelle-sys}, theory nodes
wenzelm@54329
   320
  are identified by full path names; this allows to work with multiple
wenzelm@54329
   321
  (disjoint) Isabelle sessions simultaneously within the same editor
wenzelm@54329
   322
  session.
wenzelm@54322
   323
wenzelm@54329
   324
  Certain events to open or update buffers with theory files cause
wenzelm@54329
   325
  Isabelle/jEdit to resolve dependencies of \emph{theory imports}.
wenzelm@54350
   326
  The system requests to load additional files into editor buffers, in
wenzelm@54350
   327
  order to be included in the theory document model for further
wenzelm@54350
   328
  checking.  It is also possible to resolve dependencies
wenzelm@54350
   329
  automatically, depending on \emph{Plugin Options / Isabelle /
wenzelm@54372
   330
  General / Auto load}.
wenzelm@54321
   331
wenzelm@54329
   332
  \medskip The open text area views on theory buffers define the
wenzelm@54329
   333
  visible \emph{perspective} of Isabelle/jEdit.  This is taken as a
wenzelm@54329
   334
  hint for document processing: the prover ensures that those parts of
wenzelm@54329
   335
  a theory where the user is looking are checked, while other parts
wenzelm@54350
   336
  that are presently not required are ignored.  The perspective is
wenzelm@54330
   337
  changed by opening or closing text area windows, or scrolling within
wenzelm@54372
   338
  an editor window.
wenzelm@54322
   339
wenzelm@54330
   340
  The \emph{Theories} panel provides some further options to influence
wenzelm@54330
   341
  the process of continuous checking: it may be switched off globally
wenzelm@54350
   342
  to restrict the prover to superficial processing of command syntax.
wenzelm@54350
   343
  It is also possible to indicate theory nodes as \emph{required} for
wenzelm@54330
   344
  continuous checking: this means such nodes and all their imports are
wenzelm@54330
   345
  always processed independently of the visibility status (if
wenzelm@54330
   346
  continuous checking is enabled).  Big theory libraries that are
wenzelm@54330
   347
  marked as required can have significant impact on performance,
wenzelm@54330
   348
  though.
wenzelm@54322
   349
wenzelm@54322
   350
  \medskip Formal markup of checked theory content is turned into GUI
wenzelm@54322
   351
  rendering, based on a standard repertoire known from IDEs for
wenzelm@54322
   352
  programming languages: colors, icons, highlighting, squiggly
wenzelm@54329
   353
  underline, tooltips, hyperlinks etc.  For outer syntax of
wenzelm@54350
   354
  Isabelle/Isar there is some traditional syntax-highlighting via
wenzelm@54350
   355
  static keyword tables and tokenization within the editor.  In
wenzelm@54350
   356
  contrast, the painting of inner syntax (term language etc.)\ uses
wenzelm@54350
   357
  semantic information that is reported dynamically from the logical
wenzelm@54350
   358
  context.  Thus the prover can provide additional markup to help the
wenzelm@54350
   359
  user to understand the meaning of formal text, and to produce more
wenzelm@54350
   360
  text with some add-on tools (e.g.\ information messages by automated
wenzelm@54350
   361
  provers or disprovers running in the background).
wenzelm@54352
   362
*}
wenzelm@54322
   363
wenzelm@54352
   364
wenzelm@54354
   365
section {* Prover output \label{sec:prover-output} *}
wenzelm@54353
   366
wenzelm@54353
   367
text {* Prover output consists of \emph{markup} and \emph{messages}.
wenzelm@54353
   368
  Both are directly attached to the corresponding positions in the
wenzelm@54353
   369
  original source text, and visualized in the text area, e.g.\ as text
wenzelm@54353
   370
  colours for free and bound variables, or as squiggly underline for
wenzelm@54357
   371
  warnings, errors etc.\ (see also \figref{fig:output}).  In the
wenzelm@54357
   372
  latter case, the corresponding messages are shown by hovering with
wenzelm@54357
   373
  the mouse over the highlighted text --- although in many situations
wenzelm@54372
   374
  the user should already get some clue by looking at the position of
wenzelm@54372
   375
  the text highlighting.
wenzelm@54357
   376
wenzelm@54357
   377
  \begin{figure}[htb]
wenzelm@54357
   378
  \begin{center}
wenzelm@54373
   379
  \includegraphics[width=\textwidth]{output}
wenzelm@54357
   380
  \end{center}
wenzelm@54372
   381
  \caption{Multiple views on prover output: gutter area with icon,
wenzelm@54372
   382
    text area with popup, overview area, Theories panel, Output panel}
wenzelm@54357
   383
  \label{fig:output}
wenzelm@54357
   384
  \end{figure}
wenzelm@54353
   385
wenzelm@54353
   386
  The ``gutter area'' on the left-hand-side of the text area uses
wenzelm@54372
   387
  icons to provide a summary of the messages within the adjacent
wenzelm@54353
   388
  line of text.  Message priorities are used to prefer errors over
wenzelm@54353
   389
  warnings, warnings over information messages etc.  Plain output is
wenzelm@54353
   390
  ignored here.
wenzelm@54353
   391
wenzelm@54353
   392
  The ``overview area'' on the right-hand-side of the text area uses
wenzelm@54353
   393
  similar information to paint small rectangles for the overall status
wenzelm@54353
   394
  of the whole text buffer.  The graphics is scaled to fit the logical
wenzelm@54353
   395
  buffer length into the given window height.  Mouse clicks on the
wenzelm@54353
   396
  overview area position the cursor approximately to the corresponding
wenzelm@54372
   397
  line of text in the buffer.  Repainting the overview in real-time
wenzelm@54372
   398
  causes problems with big theories, so it is restricted to part of
wenzelm@54372
   399
  the text according to \emph{Plugin Options / Isabelle / General /
wenzelm@54372
   400
  Text Overview Limit} (in characters).
wenzelm@54353
   401
wenzelm@54353
   402
  Another course-grained overview is provided by the \emph{Theories}
wenzelm@54372
   403
  panel, but without direct correspondence to text positions.  A
wenzelm@54372
   404
  double-click on one of the theory entries with their status overview
wenzelm@54372
   405
  opens the corresponding text buffer, without changing the cursor
wenzelm@54372
   406
  position.
wenzelm@54353
   407
wenzelm@54353
   408
  \medskip In addition, the \emph{Output} panel displays prover
wenzelm@54353
   409
  messages that correspond to a given command, within a separate
wenzelm@54353
   410
  window.
wenzelm@54353
   411
wenzelm@54353
   412
  The cursor position in the presently active text area determines the
wenzelm@54372
   413
  prover commands whose cumulative message output is appended and
wenzelm@54372
   414
  shown in that window (in canonical order according to the processing
wenzelm@54372
   415
  of the command).  There are also control elements to modify the
wenzelm@54372
   416
  update policy of the output wrt.\ continued editor movements.  This
wenzelm@54372
   417
  is particularly useful with several independent instances of the
wenzelm@54353
   418
  \emph{Output} panel, which the Dockable Window Manager of jEdit can
wenzelm@54353
   419
  handle conveniently.
wenzelm@54353
   420
wenzelm@54353
   421
  Former users of the old TTY interaction model (e.g.\ Proof~General)
wenzelm@54353
   422
  might find a separate window for prover messages familiar, but it is
wenzelm@54353
   423
  important to understand that the main Prover IDE feedback happens
wenzelm@54353
   424
  elsewhere.  It is possible to do meaningful proof editing
wenzelm@54372
   425
  efficiently, using secondary output windows only rarely.
wenzelm@54353
   426
wenzelm@54353
   427
  The main purpose of the output window is to ``debug'' unclear
wenzelm@54353
   428
  situations by inspecting internal state of the prover.\footnote{In
wenzelm@54355
   429
  that sense, unstructured tactic scripts depend on continuous
wenzelm@54353
   430
  debugging with internal state inspection.} Consequently, some
wenzelm@54353
   431
  special messages for \emph{tracing} or \emph{proof state} only
wenzelm@54353
   432
  appear here, and are not attached to the original source.
wenzelm@54353
   433
wenzelm@54353
   434
  \medskip In any case, prover messages also contain markup that may
wenzelm@54353
   435
  be explored recursively via tooltips or hyperlinks (see
wenzelm@54353
   436
  \secref{sec:tooltips-hyperlinks}), or clicked directly to initiate
wenzelm@54355
   437
  certain actions (see \secref{sec:auto-tools} and
wenzelm@54355
   438
  \secref{sec:sledgehammer}).  *}
wenzelm@54353
   439
wenzelm@54353
   440
wenzelm@54352
   441
section {* Tooltips and hyperlinks \label{sec:tooltips-hyperlinks} *}
wenzelm@54352
   442
wenzelm@54352
   443
text {* Formally processed text (prover input or output) contains rich
wenzelm@54352
   444
  markup information that can be explored further by using the
wenzelm@54352
   445
  @{verbatim CONTROL} modifier key on Linux and Windows, or @{verbatim
wenzelm@54352
   446
  COMMAND} on Mac OS X.  Hovering with the mouse while the modifier is
wenzelm@54352
   447
  pressed reveals a \emph{tooltip} (grey box over the text with a
wenzelm@54352
   448
  yellow popup) and/or a \emph{hyperlink} (black rectangle over the
wenzelm@54352
   449
  text); see also \figref{fig:tooltip}.
wenzelm@54331
   450
wenzelm@54357
   451
  \begin{figure}[htb]
wenzelm@54331
   452
  \begin{center}
wenzelm@54373
   453
  \includegraphics[scale=0.3]{popup1}
wenzelm@54331
   454
  \end{center}
wenzelm@54356
   455
  \caption{Tooltip and hyperlink for some formal entity}
wenzelm@54350
   456
  \label{fig:tooltip}
wenzelm@54331
   457
  \end{figure}
wenzelm@54331
   458
wenzelm@54350
   459
  Tooltip popups use the same rendering principles as the main text
wenzelm@54350
   460
  area, and further tooltips and/or hyperlinks may be exposed
wenzelm@54357
   461
  recursively by the same mechanism; see \figref{fig:nested-tooltips}.
wenzelm@54323
   462
wenzelm@54357
   463
  \begin{figure}[htb]
wenzelm@54331
   464
  \begin{center}
wenzelm@54373
   465
  \includegraphics[scale=0.3]{popup2}
wenzelm@54331
   466
  \end{center}
wenzelm@54356
   467
  \caption{Nested tooltips over formal entities}
wenzelm@54350
   468
  \label{fig:nested-tooltips}
wenzelm@54331
   469
  \end{figure}
wenzelm@54350
   470
wenzelm@54350
   471
  The tooltip popup window provides some controls to \emph{close} or
wenzelm@54350
   472
  \emph{detach} the window, turning it into a separate \emph{Info}
wenzelm@54372
   473
  window managed by jEdit.  The @{verbatim ESCAPE} key closes
wenzelm@54352
   474
  \emph{all} popups, which is particularly relevant when nested
wenzelm@54352
   475
  tooltips are stacking up.
wenzelm@54352
   476
wenzelm@54352
   477
  \medskip A black rectangle in the text indicates a hyperlink that
wenzelm@54352
   478
  may be followed by a mouse click (while the @{verbatim CONTROL} or
wenzelm@54361
   479
  @{verbatim COMMAND} modifier key is still pressed). Presently
wenzelm@54639
   480
  (Isabelle2013-2) there is no systematic navigation within the
wenzelm@54372
   481
  editor to return to the original location.
wenzelm@54352
   482
wenzelm@54352
   483
  Also note that the link target may be a file that is itself not
wenzelm@54352
   484
  subject to formal document processing of the editor session and thus
wenzelm@54352
   485
  prevents further exploration: the chain of hyperlinks may end in
wenzelm@54372
   486
  some source file of the underlying logic image, or within the
wenzelm@54372
   487
  Isabelle/ML bootstrap sources of Isabelle/Pure. *}
wenzelm@54321
   488
wenzelm@54321
   489
wenzelm@54361
   490
section {* Text completion \label{sec:completion} *}
wenzelm@54361
   491
wenzelm@54362
   492
text {* \paragraph{Completion tables} are determined statically from
wenzelm@54362
   493
  the ``outer syntax'' of the underlying edit mode (for theory files
wenzelm@54372
   494
  this is the syntax of Isar commands), and specifications of Isabelle
wenzelm@54362
   495
  symbols (see also \secref{sec:symbols}).
wenzelm@54362
   496
wenzelm@54362
   497
  Symbols are completed in backslashed forms, e.g.\ @{verbatim
wenzelm@54362
   498
  "\\"}@{verbatim "forall"} or @{verbatim "\<forall>"} that both produce the
wenzelm@54362
   499
  Isabelle symbol @{text "\<forall>"} in its Unicode rendering.\footnote{The
wenzelm@54362
   500
  extra backslash avoids overlap with keywords of the buffer syntax,
wenzelm@54372
   501
  and allows to produce Isabelle symbols robustly in most syntactic
wenzelm@54362
   502
  contexts.}  Alternatively, symbol abbreviations may be used as
wenzelm@54362
   503
  specified in @{file "$ISABELLE_HOME/etc/symbols"}.
wenzelm@54362
   504
wenzelm@54362
   505
  \paragraph{Completion popups} are required in situations of
wenzelm@54362
   506
  ambiguous completion results or where explicit confirmation is
wenzelm@54362
   507
  demanded before inserting completed text into the buffer.
wenzelm@54362
   508
wenzelm@54362
   509
  The popup is some minimally invasive GUI component over the text
wenzelm@54362
   510
  area.  It interprets special keys @{verbatim TAB}, @{verbatim
wenzelm@54362
   511
  ESCAPE}, @{verbatim UP}, @{verbatim DOWN}, @{verbatim PAGE_UP},
wenzelm@54362
   512
  @{verbatim PAGE_DOWN}, but all other key events are passed to the
wenzelm@54362
   513
  underlying text area.  This allows to ignore unwanted completions
wenzelm@54362
   514
  most of the time and continue typing quickly.
wenzelm@54361
   515
wenzelm@54362
   516
  The meaning of special keys is as follows:
wenzelm@54362
   517
wenzelm@54362
   518
  \medskip
wenzelm@54362
   519
  \begin{tabular}{ll}
wenzelm@54372
   520
  \textbf{key} & \textbf{action} \\\hline
wenzelm@54362
   521
  @{verbatim "TAB"} & select completion \\
wenzelm@54362
   522
  @{verbatim "ESCAPE"} & dismiss popup \\
wenzelm@54362
   523
  @{verbatim "UP"} & move up one item \\
wenzelm@54362
   524
  @{verbatim "DOWN"} & move down one item \\
wenzelm@54362
   525
  @{verbatim "PAGE_UP"} & move up one page of items \\
wenzelm@54362
   526
  @{verbatim "PAGE_DOWN"} & move down one page of items \\
wenzelm@54362
   527
  \end{tabular}
wenzelm@54362
   528
  \medskip
wenzelm@54362
   529
wenzelm@54362
   530
  Movement within the popup is only active for multiple items.
wenzelm@54362
   531
  Otherwise the corresponding key event retains its standard meaning
wenzelm@54362
   532
  within the underlying text area.
wenzelm@54362
   533
wenzelm@54372
   534
  \paragraph{Explicit completion} is triggered by the keyboard
wenzelm@54372
   535
  shortcut @{verbatim "C+b"} (action @{verbatim "isabelle.complete"}).
wenzelm@54372
   536
  This overrides the original jEdit binding for action @{verbatim
wenzelm@54372
   537
  "complete-word"}, but the latter is used as fall-back for
wenzelm@54362
   538
  non-Isabelle edit modes.  It is also possible to restore the
wenzelm@54372
   539
  original jEdit keyboard mapping of @{verbatim "complete-word"} via
wenzelm@54372
   540
  \emph{Global Options / Shortcuts}.
wenzelm@54361
   541
wenzelm@54362
   542
  Replacement text is inserted immediately into the buffer, unless
wenzelm@54362
   543
  ambiguous results demand an explicit popup.
wenzelm@54362
   544
wenzelm@54362
   545
  \paragraph{Implicit completion} is triggered by regular keyboard
wenzelm@54362
   546
  input events during of the editing process in the main jEdit text
wenzelm@54372
   547
  area (and a few additional text fields like the search criteria of
wenzelm@54362
   548
  the Find panel, see \secref{sec:find}).  Implicit completion depends
wenzelm@54362
   549
  on on further side-conditions:
wenzelm@54362
   550
wenzelm@54362
   551
  \begin{enumerate}
wenzelm@54362
   552
wenzelm@54362
   553
  \item The system option @{system_option jedit_completion} needs to
wenzelm@54362
   554
  be enabled (default).
wenzelm@54362
   555
wenzelm@54372
   556
  \item Completion of syntax keywords requires at least 3 relevant
wenzelm@54372
   557
  characters in the text.
wenzelm@54362
   558
wenzelm@54372
   559
  \item The system option @{system_option jedit_completion_delay}
wenzelm@54372
   560
  determines an additional delay (0.0 by default), before opening a
wenzelm@54372
   561
  completion popup.
wenzelm@54361
   562
wenzelm@54380
   563
  \item The system option @{system_option
wenzelm@54380
   564
  jedit_completion_dismiss_delay} determines an additional delay (0.0
wenzelm@54380
   565
  by default), before dismissing an earlier completion popup.  A value
wenzelm@54380
   566
  like 0.1 is occasionally useful to reduce the chance of loosing key
wenzelm@54380
   567
  strokes when the speed of typing exceeds that of repainting GUI
wenzelm@54380
   568
  components.
wenzelm@54380
   569
wenzelm@54362
   570
  \item The system option @{system_option jedit_completion_immediate}
wenzelm@54362
   571
  (disabled by default) controls whether replacement text should be
wenzelm@54372
   572
  inserted immediately without popup.  This is restricted to Isabelle
wenzelm@54372
   573
  symbols and their abbreviations (\secref{sec:symbols}) --- plain
wenzelm@54372
   574
  keywords always demand a popup for clarity.
wenzelm@54362
   575
wenzelm@54372
   576
  \item Completion of symbol abbreviations with only one relevant
wenzelm@54372
   577
  character in the text always enforces an explicit popup,
wenzelm@54372
   578
  independently of @{system_option jedit_completion_immediate}.
wenzelm@54362
   579
wenzelm@54362
   580
  \end{enumerate}
wenzelm@54361
   581
wenzelm@54362
   582
  These completion options may be configured in \emph{Plugin Options /
wenzelm@54362
   583
  Isabelle / General / Completion}.  The default is quite moderate in
wenzelm@54362
   584
  showing occasional popups and refraining from immediate insertion.
wenzelm@54372
   585
  An additional completion delay of 0.3 seconds will make it even less
wenzelm@54372
   586
  ambitious.
wenzelm@54361
   587
wenzelm@54372
   588
  In contrast, more aggressive completion works via @{system_option
wenzelm@54362
   589
  jedit_completion_delay}~@{verbatim "= 0.0"} and @{system_option
wenzelm@54362
   590
  jedit_completion_immediate}~@{verbatim "= true"}.  Thus the editing
wenzelm@54372
   591
  process becomes dependent on the system guessing correctly what the
wenzelm@54372
   592
  user had in mind.  It requires some practice (and study of the
wenzelm@54372
   593
  symbol abbreviation tables) to become productive in this advanced
wenzelm@54372
   594
  mode.
wenzelm@54362
   595
wenzelm@54372
   596
  In any case, unintended completions can be reverted by the regular
wenzelm@54372
   597
  @{verbatim undo} operation of jEdit.  When editing embedded
wenzelm@54372
   598
  languages such as ML, it is better to disable either @{system_option
wenzelm@54362
   599
  jedit_completion} or @{system_option jedit_completion_immediate}
wenzelm@54372
   600
  temporarily.  *}
wenzelm@54361
   601
wenzelm@54361
   602
wenzelm@54362
   603
section {* Isabelle symbols \label{sec:symbols} *}
wenzelm@53770
   604
wenzelm@54323
   605
text {* Isabelle sources consist of \emph{symbols} that extend plain
wenzelm@54330
   606
  ASCII to allow infinitely many mathematical symbols within the
wenzelm@54330
   607
  formal sources.  This works without depending on particular
wenzelm@54372
   608
  encodings and varying Unicode standards
wenzelm@54352
   609
  \cite{Wenzel:2011:CICM}.\footnote{Raw Unicode characters within
wenzelm@54352
   610
  formal sources would compromise portability and reliability in the
wenzelm@54372
   611
  face of changing interpretation of special features of Unicode, such
wenzelm@54372
   612
  as Combining Characters or Bi-directional Text.}
wenzelm@54323
   613
wenzelm@54323
   614
  For the prover back-end, formal text consists of ASCII characters
wenzelm@54323
   615
  that are grouped according to some simple rules, e.g.\ as plain
wenzelm@54323
   616
  ``@{verbatim a}'' or symbolic ``@{verbatim "\<alpha>"}''.
wenzelm@54323
   617
wenzelm@54352
   618
  For the editor front-end, a certain subset of symbols is rendered
wenzelm@54352
   619
  physically via Unicode glyphs, in order to show ``@{verbatim "\<alpha>"}''
wenzelm@54352
   620
  as ``@{text "\<alpha>"}'', for example.  This symbol interpretation is
wenzelm@54352
   621
  specified by the Isabelle system distribution in @{file
wenzelm@54352
   622
  "$ISABELLE_HOME/etc/symbols"} and may be augmented by the user in
wenzelm@54372
   623
  @{file_unchecked "$ISABELLE_HOME_USER/etc/symbols"}.
wenzelm@54323
   624
wenzelm@54329
   625
  The appendix of \cite{isabelle-isar-ref} gives an overview of the
wenzelm@54329
   626
  standard interpretation of finitely many symbols from the infinite
wenzelm@54352
   627
  collection.  Uninterpreted symbols are displayed literally, e.g.\
wenzelm@54352
   628
  ``@{verbatim "\<foobar>"}''.  Overlap of Unicode characters used in
wenzelm@54372
   629
  symbol interpretation with informal ones (which might appear e.g.\
wenzelm@54372
   630
  in comments) needs to be avoided!  Raw Unicode characters within
wenzelm@54372
   631
  prover source files should be restricted to informal parts, e.g.\ to
wenzelm@54372
   632
  write text in non-latin alphabets in comments.
wenzelm@54323
   633
wenzelm@54352
   634
  \medskip \paragraph{Encoding.} Technically, the Unicode view on
wenzelm@54352
   635
  Isabelle symbols is an \emph{encoding} in jEdit (not in the
wenzelm@54352
   636
  underlying JVM) that is called @{verbatim "UTF-8-Isabelle"}.  It is
wenzelm@54352
   637
  provided by the Isabelle/jEdit plugin and enabled by default for all
wenzelm@54352
   638
  source files.  Sometimes such defaults are reset accidentally, or
wenzelm@54352
   639
  malformed UTF-8 sequences in the text force jEdit to fall back on a
wenzelm@54352
   640
  different encoding like @{verbatim "ISO-8859-15"}.  In that case,
wenzelm@54352
   641
  verbatim ``@{verbatim "\<alpha>"}'' will be shown in the text buffer
wenzelm@54352
   642
  instead of its Unicode rendering ``@{text "\<alpha>"}''.  The jEdit menu
wenzelm@54352
   643
  operation \emph{File / Reload with Encoding / UTF-8-Isabelle} helps
wenzelm@54352
   644
  to resolve such problems, potentially after repairing malformed
wenzelm@54352
   645
  parts of the text.
wenzelm@53770
   646
wenzelm@54352
   647
  \medskip \paragraph{Font.} Correct rendering via Unicode requires a
wenzelm@54352
   648
  font that contains glyphs for the corresponding codepoints.  Most
wenzelm@54352
   649
  system fonts lack that, so Isabelle/jEdit prefers its own
wenzelm@54352
   650
  application font @{verbatim IsabelleText}, which ensures that
wenzelm@54352
   651
  standard collection of Isabelle symbols are actually seen on the
wenzelm@54352
   652
  screen (or printer).
wenzelm@54329
   653
wenzelm@54330
   654
  Note that a Java/AWT/Swing application can load additional fonts
wenzelm@54372
   655
  only if they are not installed on the operating system already!
wenzelm@54372
   656
  Some old version of @{verbatim IsabelleText} that happens to be
wenzelm@54372
   657
  provided by the operating system would prevents Isabelle/jEdit from
wenzelm@54372
   658
  its bundled version.  This could lead to missing glyphs (black
wenzelm@54372
   659
  rectangles), when the system version of @{verbatim IsabelleText} is
wenzelm@54372
   660
  older than the application version.  This problem can be avoided by
wenzelm@54372
   661
  refraining to ``install'' any version of @{verbatim IsabelleText} in
wenzelm@54372
   662
  the first place (although it might be occasionally tempting to use
wenzelm@54372
   663
  the same font in other applications).
wenzelm@54329
   664
wenzelm@54323
   665
  \medskip \paragraph{Input methods.} In principle, Isabelle/jEdit
wenzelm@54323
   666
  could delegate the problem to produce Isabelle symbols in their
wenzelm@54323
   667
  Unicode rendering to the underlying operating system and its
wenzelm@54329
   668
  \emph{input methods}.  Regular jEdit also provides various ways to
wenzelm@54329
   669
  work with \emph{abbreviations} to produce certain non-ASCII
wenzelm@54329
   670
  characters.  Since none of these standard input methods work
wenzelm@54329
   671
  satisfactorily for the mathematical characters required for
wenzelm@54329
   672
  Isabelle, various specific Isabelle/jEdit mechanisms are provided.
wenzelm@54323
   673
wenzelm@54329
   674
  Here is a summary for practically relevant input methods for
wenzelm@54330
   675
  Isabelle symbols:
wenzelm@54323
   676
wenzelm@53770
   677
  \begin{enumerate}
wenzelm@54323
   678
wenzelm@54330
   679
  \item The \emph{Symbols} panel with some GUI buttons to insert
wenzelm@54323
   680
  certain symbols in the text buffer.  There are also tooltips to
wenzelm@54372
   681
  reveal the official Isabelle representation with some additional
wenzelm@54323
   682
  information about \emph{symbol abbreviations} (see below).
wenzelm@54323
   683
wenzelm@54323
   684
  \item Copy / paste from decoded source files: text that is rendered
wenzelm@54352
   685
  as Unicode already can be re-used to produce further text.  This
wenzelm@54352
   686
  also works between different applications, e.g.\ Isabelle/jEdit and
wenzelm@54352
   687
  some web browser or mail client, as long as the same Unicode view on
wenzelm@54352
   688
  Isabelle symbols is used uniformly.
wenzelm@54323
   689
wenzelm@54329
   690
  \item Copy / paste from prover output within Isabelle/jEdit.  The
wenzelm@54329
   691
  same principles as for text buffers apply, but note that \emph{copy}
wenzelm@54352
   692
  in secondary Isabelle/jEdit windows works via the keyboard shortcut
wenzelm@54372
   693
  @{verbatim "C+c"}, while jEdit menu actions always refer to the
wenzelm@54352
   694
  primary text area!
wenzelm@54323
   695
wenzelm@54323
   696
  \item Completion provided by Isabelle plugin (see
wenzelm@54323
   697
  \secref{sec:completion}).  Isabelle symbols have a canonical name
wenzelm@54323
   698
  and optional abbreviations.  This can be used with the text
wenzelm@54323
   699
  completion mechanism of Isabelle/jEdit, to replace a prefix of the
wenzelm@54329
   700
  actual symbol like @{verbatim "\<lambda>"}, or its backslashed name
wenzelm@54329
   701
  @{verbatim "\\"}@{verbatim "lambda"}, or its ASCII abbreviation
wenzelm@54330
   702
  @{verbatim "%"} by the Unicode rendering.
wenzelm@54323
   703
wenzelm@54323
   704
  The following table is an extract of the information provided by the
wenzelm@54329
   705
  standard @{file "$ISABELLE_HOME/etc/symbols"} file:
wenzelm@53770
   706
wenzelm@53770
   707
  \medskip
wenzelm@53770
   708
  \begin{tabular}{lll}
wenzelm@54372
   709
    \textbf{symbol} & \textbf{backslashed name} & \textbf{abbreviation} \\\hline
wenzelm@54372
   710
    @{text "\<lambda>"} & @{verbatim "\\lambda"} & @{verbatim "%"} \\
wenzelm@54372
   711
    @{text "\<Rightarrow>"} & @{verbatim "\\Rightarrow"} & @{verbatim "=>"} \\
wenzelm@54372
   712
    @{text "\<Longrightarrow>"} & @{verbatim "\\Longrightarrow"} & @{verbatim "==>"} \\[0.5ex]
wenzelm@54372
   713
    @{text "\<And>"} & @{verbatim "\\And"} & @{verbatim "!!"} \\
wenzelm@54372
   714
    @{text "\<equiv>"} & @{verbatim "\\equiv"} & @{verbatim "=="} \\[0.5ex]
wenzelm@54372
   715
    @{text "\<forall>"} & @{verbatim "\\forall"} & @{verbatim "!"} \\
wenzelm@54372
   716
    @{text "\<exists>"} & @{verbatim "\\exists"} & @{verbatim "?"} \\
wenzelm@54372
   717
    @{text "\<longrightarrow>"} & @{verbatim "\\longrightarrow"} & @{verbatim "-->"} \\
wenzelm@54372
   718
    @{text "\<and>"} & @{verbatim "\\and"} & @{verbatim "&"} \\
wenzelm@54372
   719
    @{text "\<or>"} & @{verbatim "\\or"} & @{verbatim "|"} \\
wenzelm@54372
   720
    @{text "\<not>"} & @{verbatim "\\not"} & @{verbatim "~"} \\
wenzelm@54372
   721
    @{text "\<noteq>"} & @{verbatim "\\noteq"} & @{verbatim "~="} \\
wenzelm@54372
   722
    @{text "\<in>"} & @{verbatim "\\in"} & @{verbatim ":"} \\
wenzelm@54372
   723
    @{text "\<notin>"} & @{verbatim "\\notin"} & @{verbatim "~:"} \\
wenzelm@53770
   724
  \end{tabular}
wenzelm@54329
   725
  \medskip
wenzelm@54329
   726
wenzelm@54329
   727
  Note that the above abbreviations refer to the input method. The
wenzelm@54329
   728
  logical notation provides ASCII alternatives that often coincide,
wenzelm@54352
   729
  but deviate occasionally.  This occasionally causes user confusion
wenzelm@54352
   730
  with very old-fashioned Isabelle source that use ASCII replacement
wenzelm@54372
   731
  notation like @{verbatim "!"} or @{verbatim "ALL"} directly in the
wenzelm@54372
   732
  text.
wenzelm@54372
   733
wenzelm@54372
   734
  On the other hand, coincidence of symbol abbreviations with ASCII
wenzelm@54372
   735
  replacement syntax syntax helps to update old theory sources via
wenzelm@54372
   736
  explicit completion (see also @{verbatim "C+b"} explained in
wenzelm@54372
   737
  \secref{sec:completion}).
wenzelm@53770
   738
wenzelm@53770
   739
  \end{enumerate}
wenzelm@53770
   740
wenzelm@54323
   741
  \paragraph{Control symbols.} There are some special control symbols
wenzelm@54372
   742
  to modify the display style of a single symbol (without
wenzelm@54372
   743
  nesting). Control symbols may be applied to a region of selected
wenzelm@54372
   744
  text, either using the \emph{Symbols} panel or keyboard shortcuts or
wenzelm@54372
   745
  jEdit actions.  These editor operations produce a separate control
wenzelm@54372
   746
  symbol for each symbol in the text, in order to make the whole text
wenzelm@54372
   747
  appear in a certain style.
wenzelm@53770
   748
wenzelm@53770
   749
  \medskip
wenzelm@54352
   750
  \begin{tabular}{llll}
wenzelm@54372
   751
    \textbf{style} & \textbf{symbol} & \textbf{shortcut} & \textbf{action} \\\hline
wenzelm@54352
   752
    superscript & @{verbatim "\<^sup>"} & @{verbatim "C+e UP"} & @{verbatim "isabelle.control-sup"} \\
wenzelm@54352
   753
    subscript & @{verbatim "\<^sub>"} & @{verbatim "C+e DOWN"} & @{verbatim "isabelle.control-sub"} \\
wenzelm@54352
   754
    bold face & @{verbatim "\<^bold>"} & @{verbatim "C+e RIGHT"} & @{verbatim "isabelle.control-bold"} \\
wenzelm@54352
   755
    reset & & @{verbatim "C+e LEFT"} & @{verbatim "isabelle.control-reset"} \\
wenzelm@53770
   756
  \end{tabular}
wenzelm@54352
   757
  \medskip
wenzelm@54323
   758
wenzelm@54352
   759
  To produce a single control symbol, it is also possible to complete
wenzelm@54352
   760
  on @{verbatim "\\"}@{verbatim sup}, @{verbatim "\\"}@{verbatim sub},
wenzelm@54352
   761
  @{verbatim "\\"}@{verbatim bold} as for regular symbols.  *}
wenzelm@53770
   762
wenzelm@53770
   763
wenzelm@54355
   764
section {* Automatically tried tools \label{sec:auto-tools} *}
wenzelm@54353
   765
wenzelm@54354
   766
text {* Continuous document processing works asynchronously in the
wenzelm@54354
   767
  background.  Visible document source that has been evaluated already
wenzelm@54354
   768
  may get augmented by additional results of \emph{asynchronous print
wenzelm@54354
   769
  functions}.  The canonical example is proof state output, which is
wenzelm@54354
   770
  always enabled.  More heavy-weight print functions may be applied,
wenzelm@54354
   771
  in order to prove or disprove parts of the formal text by other
wenzelm@54354
   772
  means.
wenzelm@54354
   773
wenzelm@54354
   774
  Isabelle/HOL provides various automatically tried tools that operate
wenzelm@54354
   775
  on outermost goal statements (e.g.\ @{command lemma}, @{command
wenzelm@54354
   776
  theorem}), independently of the state of the current proof attempt.
wenzelm@54354
   777
  They work implicitly without any arguments.  Results are output as
wenzelm@54354
   778
  \emph{information messages}, which are indicated in the text area by
wenzelm@54356
   779
  blue squiggles and a blue information sign in the gutter (see
wenzelm@54356
   780
  \figref{fig:auto-tools}).  The message content may be shown as for
wenzelm@54372
   781
  other output (see also \secref{sec:prover-output}).  Some tools
wenzelm@54356
   782
  produce output with \emph{sendback} markup, which means that
wenzelm@54356
   783
  clicking on certain parts of the output inserts that text into the
wenzelm@54356
   784
  source in the proper place.
wenzelm@54356
   785
wenzelm@54357
   786
  \begin{figure}[htb]
wenzelm@54356
   787
  \begin{center}
wenzelm@54373
   788
  \includegraphics[scale=0.3]{auto-tools}
wenzelm@54356
   789
  \end{center}
wenzelm@54356
   790
  \caption{Results of automatically tried tools}
wenzelm@54356
   791
  \label{fig:auto-tools}
wenzelm@54356
   792
  \end{figure}
wenzelm@54354
   793
wenzelm@54372
   794
  \medskip The following Isabelle system options control the behavior
wenzelm@54354
   795
  of automatically tried tools (see also the jEdit dialog window
wenzelm@54354
   796
  \emph{Plugin Options / Isabelle / General / Automatically tried
wenzelm@54354
   797
  tools}):
wenzelm@54354
   798
wenzelm@54354
   799
  \begin{itemize}
wenzelm@54354
   800
wenzelm@54354
   801
  \item @{system_option auto_methods} controls automatic use of a
wenzelm@54354
   802
  combination of standard proof methods (@{method auto}, @{method
wenzelm@54372
   803
  simp}, @{method blast}, etc.).  This corresponds to the Isar command
wenzelm@54354
   804
  @{command "try0"}.
wenzelm@54354
   805
wenzelm@54354
   806
  The tool is disabled by default, since unparameterized invocation of
wenzelm@54354
   807
  standard proof methods often consumes substantial CPU resources
wenzelm@54354
   808
  without leading to success.
wenzelm@54354
   809
wenzelm@54354
   810
  \item @{system_option auto_nitpick} controls a slightly reduced
wenzelm@54354
   811
  version of @{command nitpick}, which tests for counterexamples using
wenzelm@54354
   812
  first-order relational logic. See also the Nitpick manual
wenzelm@54354
   813
  \cite{isabelle-nitpick}.
wenzelm@54354
   814
wenzelm@54354
   815
  This tool is disabled by default, due to the extra overhead of
wenzelm@54354
   816
  invoking an external Java process for each attempt to disprove a
wenzelm@54354
   817
  subgoal.
wenzelm@54354
   818
wenzelm@54354
   819
  \item @{system_option auto_quickcheck} controls automatic use of
wenzelm@54354
   820
  @{command quickcheck}, which tests for counterexamples using a
wenzelm@54354
   821
  series of assignments for free variables of a subgoal.
wenzelm@54354
   822
wenzelm@54354
   823
  This tool is \emph{enabled} by default.  It requires little
wenzelm@54354
   824
  overhead, but is a bit weaker than @{command nitpick}.
wenzelm@54354
   825
wenzelm@54354
   826
  \item @{system_option auto_sledgehammer} controls a significantly
wenzelm@54354
   827
  reduced version of @{command sledgehammer}, which attempts to prove
wenzelm@54354
   828
  a subgoal using external automatic provers. See also the
wenzelm@54354
   829
  Sledgehammer manual \cite{isabelle-sledgehammer}.
wenzelm@54354
   830
wenzelm@54354
   831
  This tool is disabled by default, due to the relatively heavy nature
wenzelm@54354
   832
  of Sledgehammer.
wenzelm@54354
   833
wenzelm@54354
   834
  \item @{system_option auto_solve_direct} controls automatic use of
wenzelm@54354
   835
  @{command solve_direct}, which checks whether the current subgoals
wenzelm@54354
   836
  can be solved directly by an existing theorem.  This also helps to
wenzelm@54354
   837
  detect duplicate lemmas.
wenzelm@54354
   838
wenzelm@54354
   839
  This tool is \emph{enabled} by default.
wenzelm@54354
   840
wenzelm@54354
   841
  \end{itemize}
wenzelm@54354
   842
wenzelm@54354
   843
  Invocation of automatically tried tools is subject to some global
wenzelm@54354
   844
  policies of parallel execution, which may be configured as follows:
wenzelm@54354
   845
wenzelm@54354
   846
  \begin{itemize}
wenzelm@54354
   847
wenzelm@54354
   848
  \item @{system_option auto_time_limit} (default 2.0) determines the
wenzelm@54372
   849
  timeout (in seconds) for each tool execution.
wenzelm@54354
   850
wenzelm@54354
   851
  \item @{system_option auto_time_start} (default 1.0) determines the
wenzelm@54354
   852
  start delay (in seconds) for automatically tried tools, after the
wenzelm@54354
   853
  main command evaluation is finished.
wenzelm@54354
   854
wenzelm@54354
   855
  \end{itemize}
wenzelm@54354
   856
wenzelm@54354
   857
  Each tool is submitted independently to the pool of parallel
wenzelm@54354
   858
  execution tasks in Isabelle/ML, using hardwired priorities according
wenzelm@54354
   859
  to its relative ``heaviness''.  The main stages of evaluation and
wenzelm@54354
   860
  printing of proof states take precedence, but an already running
wenzelm@54354
   861
  tool is not canceled and may thus reduce reactivity of proof
wenzelm@54354
   862
  document processing.
wenzelm@54354
   863
wenzelm@54354
   864
  Users should experiment how the available CPU resources (number of
wenzelm@54354
   865
  cores) are best invested to get additional feedback from prover in
wenzelm@54372
   866
  the background, by using a selection of weaker or stronger tools.
wenzelm@54372
   867
*}
wenzelm@54353
   868
wenzelm@54353
   869
wenzelm@54353
   870
section {* Sledgehammer \label{sec:sledgehammer} *}
wenzelm@54353
   871
wenzelm@54356
   872
text {* The \emph{Sledgehammer} panel (\figref{fig:sledgehammer})
wenzelm@54372
   873
  provides a view on some independent execution of the Isar command
wenzelm@54372
   874
  @{command sledgehammer}, with process indicator (spinning wheel) and
wenzelm@54372
   875
  GUI elements for important Sledgehammer arguments and options.  Any
wenzelm@54356
   876
  number of Sledgehammer panels may be active, according to the
wenzelm@54372
   877
  standard policies of Dockable Window Management in jEdit.  Closing
wenzelm@54372
   878
  such windows also cancels the corresponding prover tasks.
wenzelm@54356
   879
wenzelm@54357
   880
  \begin{figure}[htb]
wenzelm@54356
   881
  \begin{center}
wenzelm@54356
   882
  \includegraphics[scale=0.3]{sledgehammer}
wenzelm@54356
   883
  \end{center}
wenzelm@54356
   884
  \caption{An instance of the Sledgehammer panel}
wenzelm@54356
   885
  \label{fig:sledgehammer}
wenzelm@54356
   886
  \end{figure}
wenzelm@54355
   887
wenzelm@54355
   888
  The \emph{Apply} button attaches a fresh invocation of @{command
wenzelm@54355
   889
  sledgehammer} to the command where the cursor is pointing in the
wenzelm@54355
   890
  text --- this should be some pending proof problem.  Further buttons
wenzelm@54355
   891
  like \emph{Cancel} and \emph{Locate} help to manage the running
wenzelm@54355
   892
  process.
wenzelm@54355
   893
wenzelm@54355
   894
  Results appear incrementally in the output window of the panel.
wenzelm@54372
   895
  Proposed proof snippets are marked-up as \emph{sendback}, which
wenzelm@54355
   896
  means a single mouse click inserts the text into a suitable place of
wenzelm@54355
   897
  the original source.  Some manual editing may be required
wenzelm@54355
   898
  nonetheless, say to remove earlier proof attempts. *}
wenzelm@54353
   899
wenzelm@54353
   900
wenzelm@54362
   901
section {* Find theorems \label{sec:find} *}
wenzelm@54353
   902
wenzelm@54356
   903
text {* The \emph{Find} panel (\figref{fig:find}) provides an
wenzelm@54372
   904
  independent view for the Isar command @{command find_theorems}.  The
wenzelm@54372
   905
  main text field accepts search criteria according to the syntax
wenzelm@54372
   906
  @{syntax thmcriterium} given in \cite{isabelle-isar-ref}.  Further
wenzelm@54372
   907
  options of @{command find_theorems} are available via GUI elements.
wenzelm@54356
   908
wenzelm@54357
   909
  \begin{figure}[htb]
wenzelm@54356
   910
  \begin{center}
wenzelm@54356
   911
  \includegraphics[scale=0.3]{find}
wenzelm@54356
   912
  \end{center}
wenzelm@54356
   913
  \caption{An instance of the Find panel}
wenzelm@54356
   914
  \label{fig:find}
wenzelm@54356
   915
  \end{figure}
wenzelm@54355
   916
wenzelm@54355
   917
  The \emph{Apply} button attaches a fresh invocation of @{command
wenzelm@54355
   918
  find_theorems} to the current context of the command where the
wenzelm@54355
   919
  cursor is pointing in the text, unless an alternative theory context
wenzelm@54355
   920
  (from the underlying logic image) is specified explicitly. *}
wenzelm@54353
   921
wenzelm@54353
   922
wenzelm@54358
   923
chapter {* Miscellaneous tools *}
wenzelm@54358
   924
wenzelm@54358
   925
section {* SideKick *}
wenzelm@54358
   926
wenzelm@54358
   927
text {* The \emph{SideKick} plugin of jEdit provides some general
wenzelm@54358
   928
  services to display buffer structure in a tree view.
wenzelm@54358
   929
wenzelm@54358
   930
  Isabelle/jEdit provides SideKick parsers for its main mode for
wenzelm@54358
   931
  theory files, as well as some minor modes for the @{verbatim NEWS}
wenzelm@54372
   932
  file, session @{verbatim ROOT} files, and system @{verbatim
wenzelm@54372
   933
  options}.
wenzelm@54358
   934
wenzelm@54358
   935
  Moreover, the special SideKick parser @{verbatim "isabelle-markup"}
wenzelm@54358
   936
  provides access to the full (uninterpreted) markup tree of the PIDE
wenzelm@54358
   937
  document model of the current buffer.  This is occasionally useful
wenzelm@54358
   938
  for informative purposes, but the amount of displayed information
wenzelm@54358
   939
  might cause problems for large buffers, both for the human and the
wenzelm@54358
   940
  machine.
wenzelm@54358
   941
*}
wenzelm@54358
   942
wenzelm@54358
   943
wenzelm@54359
   944
section {* Timing *}
wenzelm@54359
   945
wenzelm@54359
   946
text {* Managed evaluation of commands within PIDE documents includes
wenzelm@54359
   947
  timing information, which consists of elapsed (wall-clock) time, CPU
wenzelm@54359
   948
  time, and GC (garbage collection) time.  Note that in a
wenzelm@54359
   949
  multithreaded system it is difficult to measure execution time
wenzelm@54359
   950
  precisely: elapsed time is closer to the real requirements of
wenzelm@54359
   951
  runtime resources than CPU or GC time, which are both subject to
wenzelm@54359
   952
  influences from the parallel environment that are outside the scope
wenzelm@54359
   953
  of the current command transaction.
wenzelm@54359
   954
wenzelm@54359
   955
  The \emph{Timing} panel provides an overview of cumulative command
wenzelm@54359
   956
  timings for each document node.  Commands with elapsed time below
wenzelm@54359
   957
  the given threshold are ignored in the grand total.  Nodes are
wenzelm@54359
   958
  sorted according to their overall timing.  For the document node
wenzelm@54359
   959
  that corresponds to the current buffer, individual command timings
wenzelm@54359
   960
  are shown as well.  A double-click on a theory node or command moves
wenzelm@54359
   961
  the editor focus to that particular source position.
wenzelm@54359
   962
wenzelm@54359
   963
  It is also possible to reveal individual timing information via some
wenzelm@54359
   964
  tooltip for the corresponding command keyword, using the technique
wenzelm@54359
   965
  of mouse hovering with @{verbatim CONTROL}/@{verbatim COMMAND}
wenzelm@54359
   966
  modifier key as explained in \secref{sec:tooltips-hyperlinks}.
wenzelm@54359
   967
  Actual display of timing depends on the global option
wenzelm@54359
   968
  @{system_option jedit_timing_threshold}, which can be configured in
wenzelm@54360
   969
  "Plugin Options / Isabelle / General".
wenzelm@54360
   970
wenzelm@54360
   971
  \medskip The \emph{Monitor} panel provides a general impression of
wenzelm@54360
   972
  recent activity of the farm of worker threads in Isabelle/ML.  Its
wenzelm@54360
   973
  display is continuously updated according to @{system_option
wenzelm@54360
   974
  editor_chart_delay}.  Note that the painting of the chart takes
wenzelm@54360
   975
  considerable runtime itself --- on the Java Virtual Machine that
wenzelm@54360
   976
  runs Isabelle/Scala, not Isabelle/ML.  Internally, the
wenzelm@54360
   977
  Isabelle/Scala module @{verbatim isabelle.ML_Statistics} provides
wenzelm@54372
   978
  further access to statistics of Isabelle/ML.  *}
wenzelm@54359
   979
wenzelm@54359
   980
wenzelm@54358
   981
section {* Isabelle/Scala console *}
wenzelm@54358
   982
wenzelm@54358
   983
text {* The \emph{Console} plugin of jEdit manages various shells
wenzelm@54358
   984
  (command interpreters), e.g.\ \emph{BeanShell}, which is the
wenzelm@54372
   985
  official jEdit scripting language, and the cross-platform
wenzelm@54372
   986
  \emph{System} shell.  Thus the console provides similar
wenzelm@54372
   987
  functionality than the special buffers @{verbatim "*scratch*"} and
wenzelm@54372
   988
  @{verbatim "*shell*"} in Emacs.
wenzelm@54358
   989
wenzelm@54358
   990
  Isabelle/jEdit extends the repertoire of the console by
wenzelm@54358
   991
  \emph{Scala}, which is the regular Scala toplevel loop running
wenzelm@54358
   992
  inside the \emph{same} JVM process as Isabelle/jEdit itself.  This
wenzelm@54358
   993
  means the Scala command interpreter has access to the JVM name space
wenzelm@54358
   994
  and state of the running Prover IDE application: the main entry
wenzelm@54358
   995
  points are @{verbatim view} (the current editor view of jEdit) and
wenzelm@54358
   996
  @{verbatim PIDE} (the Isabelle/jEdit plugin object).
wenzelm@54358
   997
wenzelm@54358
   998
  For example, the subsequent Scala snippet gets the PIDE document
wenzelm@54358
   999
  model of the current buffer within the current editor view:
wenzelm@54358
  1000
wenzelm@54358
  1001
  \begin{center}
wenzelm@54358
  1002
  @{verbatim "PIDE.document_model(view.getBuffer).get"}
wenzelm@54358
  1003
  \end{center}
wenzelm@54358
  1004
wenzelm@54358
  1005
  This helps to explore Isabelle/Scala functionality interactively.
wenzelm@54358
  1006
  Some care is required to avoid interference with the internals of
wenzelm@54358
  1007
  the running application, especially in production use.  *}
wenzelm@54358
  1008
wenzelm@54358
  1009
wenzelm@54358
  1010
section {* Low-level output *}
wenzelm@54358
  1011
wenzelm@54358
  1012
text {* Prover output is normally shown directly in the main text area
wenzelm@54372
  1013
  or secondary \emph{Output} panels, as explained in
wenzelm@54358
  1014
  \secref{sec:prover-output}.
wenzelm@54358
  1015
wenzelm@54358
  1016
  Beyond this, it is occasionally useful to inspect low-level output
wenzelm@54358
  1017
  channels via some of the following additional panels:
wenzelm@54358
  1018
wenzelm@54358
  1019
  \begin{itemize}
wenzelm@54358
  1020
wenzelm@54358
  1021
  \item \emph{Protocol} shows internal messages between the
wenzelm@54358
  1022
  Isabelle/Scala and Isabelle/ML side of the PIDE editing protocol.
wenzelm@54358
  1023
  Recording of messages starts with the first activation of the
wenzelm@54358
  1024
  corresponding dockable window; earlier messages are lost.
wenzelm@54358
  1025
wenzelm@54358
  1026
  Actual display of protocol messages causes considerable slowdown, so
wenzelm@54372
  1027
  it is important to undock all \emph{Protocol} panels for production
wenzelm@54372
  1028
  work.
wenzelm@54358
  1029
wenzelm@54358
  1030
  \item \emph{Raw Output} shows chunks of text from the @{verbatim
wenzelm@54358
  1031
  stdout} and @{verbatim stderr} channels of the prover process.
wenzelm@54358
  1032
  Recording of output starts with the first activation of the
wenzelm@54358
  1033
  corresponding dockable window; earlier output is lost.
wenzelm@54358
  1034
wenzelm@54358
  1035
  The implicit stateful nature of physical I/O channels makes it
wenzelm@54358
  1036
  difficult to relate raw output to the actual command from where it
wenzelm@54358
  1037
  was originating.  Parallel execution may add to the confusion.
wenzelm@54358
  1038
  Peeking at physical process I/O is only the last resort to diagnose
wenzelm@54358
  1039
  problems with tools that are not fully PIDE compliant.
wenzelm@54358
  1040
wenzelm@54358
  1041
  Under normal circumstances, prover output always works via managed
wenzelm@54358
  1042
  message channels (corresponding to @{ML writeln}, @{ML warning},
wenzelm@54358
  1043
  @{ML error} etc.\ in Isabelle/ML), which are displayed by regular
wenzelm@54358
  1044
  means within the document model (\secref{sec:prover-output}).
wenzelm@54358
  1045
wenzelm@54358
  1046
  \item \emph{Syslog} shows system messages that might be relevant to
wenzelm@54358
  1047
  diagnose problems with the startup or shutdown phase of the prover
wenzelm@54358
  1048
  process; this also includes raw output on @{verbatim stderr}.
wenzelm@54358
  1049
wenzelm@54358
  1050
  A limited amount of syslog messages are buffered, independently of
wenzelm@54358
  1051
  the docking state of the \emph{Syslog} panel.  This allows to
wenzelm@54358
  1052
  diagnose serious problems with Isabelle/PIDE process management,
wenzelm@54358
  1053
  outside of the actual protocol layer.
wenzelm@54358
  1054
wenzelm@54358
  1055
  Under normal situations, such low-level system output can be
wenzelm@54358
  1056
  ignored.
wenzelm@54358
  1057
wenzelm@54358
  1058
  \end{itemize}
wenzelm@54358
  1059
*}
wenzelm@54358
  1060
wenzelm@54358
  1061
wenzelm@54329
  1062
chapter {* Known problems and workarounds \label{sec:problems} *}
wenzelm@53770
  1063
wenzelm@53770
  1064
text {*
wenzelm@53770
  1065
  \begin{itemize}
wenzelm@53770
  1066
wenzelm@53770
  1067
  \item \textbf{Problem:} Lack of dependency management for auxiliary files
wenzelm@53771
  1068
  that contribute to a theory (e.g.\ @{command ML_file}).
wenzelm@53770
  1069
wenzelm@54330
  1070
  \textbf{Workaround:} Re-load files manually within the prover, by
wenzelm@54330
  1071
  editing corresponding command in the text.
wenzelm@53770
  1072
wenzelm@53770
  1073
  \item \textbf{Problem:} Odd behavior of some diagnostic commands with
wenzelm@53770
  1074
  global side-effects, like writing a physical file.
wenzelm@53770
  1075
wenzelm@54372
  1076
  \textbf{Workaround:} Copy / paste complete command text from
wenzelm@54372
  1077
  elsewhere, or discontinue continuous checking temporarily.
wenzelm@53770
  1078
wenzelm@53770
  1079
  \item \textbf{Problem:} No way to delete document nodes from the overall
wenzelm@53770
  1080
  collection of theories.
wenzelm@53770
  1081
wenzelm@54329
  1082
  \textbf{Workaround:} Ignore unused files.  Restart whole
wenzelm@54329
  1083
  Isabelle/jEdit session in worst-case situation.
wenzelm@53770
  1084
wenzelm@54330
  1085
  \item \textbf{Problem:} Keyboard shortcuts @{verbatim "C+PLUS"} and
wenzelm@54330
  1086
  @{verbatim "C+MINUS"} for adjusting the editor font size depend on
wenzelm@54330
  1087
  platform details and national keyboards.
wenzelm@54330
  1088
wenzelm@54372
  1089
  \textbf{Workaround:} Rebind keys via \emph{Global Options /
wenzelm@54372
  1090
  Shortcuts}.
wenzelm@54330
  1091
wenzelm@53886
  1092
  \item \textbf{Problem:} The Mac OS X keyboard shortcut @{verbatim
wenzelm@54349
  1093
  "COMMAND+COMMA"} for application \emph{Preferences} is in conflict
wenzelm@54349
  1094
  with the jEdit default shortcut for \emph{Incremental Search Bar}
wenzelm@54349
  1095
  (action @{verbatim "quick-search"}).
wenzelm@53770
  1096
wenzelm@54372
  1097
  \textbf{Workaround:} Rebind key via \emph{Global Options /
wenzelm@54372
  1098
  Shortcuts} according to national keyboard, e.g.\ @{verbatim
wenzelm@54372
  1099
  "COMMAND+SLASH"} on English ones.
wenzelm@53770
  1100
wenzelm@54349
  1101
  \item \textbf{Problem:} Mac OS X system fonts sometimes lead to
wenzelm@54349
  1102
  character drop-outs in the main text area.
wenzelm@54349
  1103
wenzelm@54349
  1104
  \textbf{Workaround:} Use the default @{verbatim IsabelleText} font.
wenzelm@54349
  1105
  (Do not install that font on the system.)
wenzelm@54349
  1106
wenzelm@54329
  1107
  \item \textbf{Problem:} Some Linux / X11 input methods such as IBus
wenzelm@54330
  1108
  tend to disrupt key event handling of Java/AWT/Swing.
wenzelm@53770
  1109
wenzelm@54329
  1110
  \textbf{Workaround:} Do not use input methods, reset the environment
wenzelm@54329
  1111
  variable @{verbatim XMODIFIERS} within Isabelle settings (default in
wenzelm@54639
  1112
  Isabelle2013-2).
wenzelm@54329
  1113
wenzelm@54329
  1114
  \item \textbf{Problem:} Some Linux / X11 window managers that are
wenzelm@54329
  1115
  not ``re-parenting'' cause problems with additional windows opened
wenzelm@54331
  1116
  by Java. This affects either historic or neo-minimalistic window
wenzelm@54331
  1117
  managers like @{verbatim awesome} or @{verbatim xmonad}.
wenzelm@54329
  1118
wenzelm@54329
  1119
  \textbf{Workaround:} Use regular re-parenting window manager.
wenzelm@54329
  1120
wenzelm@54329
  1121
  \item \textbf{Problem:} Recent forks of Linux / X11 window managers
wenzelm@54329
  1122
  and desktop environments (variants of Gnome) disrupt the handling of
wenzelm@54329
  1123
  menu popups and mouse positions of Java/AWT/Swing.
wenzelm@54329
  1124
wenzelm@54329
  1125
  \textbf{Workaround:} Use mainstream versions of Linux desktops.
wenzelm@53770
  1126
wenzelm@54349
  1127
  \item \textbf{Problem:} Full-screen mode via jEdit action @{verbatim
wenzelm@54349
  1128
  "toggle-full-screen"} (default shortcut @{verbatim F11}) works on
wenzelm@54349
  1129
  Windows, but not on Mac OS X or various Linux / X11 window managers.
wenzelm@54349
  1130
wenzelm@54349
  1131
  \textbf{Workaround:} Use native full-screen control of the window
wenzelm@54372
  1132
  manager (notably on Mac OS X).
wenzelm@54349
  1133
wenzelm@54349
  1134
  \item \textbf{Problem:} Full-screen mode and dockable windows in
wenzelm@54349
  1135
  \emph{floating} state may lead to confusion about window placement
wenzelm@54349
  1136
  (depending on platform characteristics).
wenzelm@54349
  1137
wenzelm@54349
  1138
  \textbf{Workaround:} Avoid this combination.
wenzelm@54349
  1139
wenzelm@53770
  1140
  \end{itemize}
wenzelm@53770
  1141
*}
wenzelm@53770
  1142
wenzelm@53769
  1143
end