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