src/Doc/JEdit/JEdit.thy
author wenzelm
Tue, 31 Mar 2015 22:31:05 +0200
changeset 59886 e0dc738eb08c
parent 58618 782f0b662cae
child 60255 0466bd194d74
permissions -rw-r--r--
support for explicit scope of private entries;
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
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
     7
chapter \<open>Introduction\<close>
53769
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
     8
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
     9
section \<open>Concepts and terminology\<close>
53770
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    10
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
    11
text \<open>
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
    12
  Isabelle/jEdit is a Prover IDE that integrates \emph{parallel proof
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
    13
  checking} @{cite "Wenzel:2009" and "Wenzel:2013:ITP"} with
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
    14
  \emph{asynchronous user interaction} @{cite "Wenzel:2010" and
58556
71a63f8a5b84 more refs;
wenzelm
parents: 58554
diff changeset
    15
  "Wenzel:2012:UITP-EPTCS" and "Wenzel:2014:ITP-PIDE" and "Wenzel:2014:UITP"},
71a63f8a5b84 more refs;
wenzelm
parents: 58554
diff changeset
    16
  based on a document-oriented approach to \emph{continuous proof processing}
71a63f8a5b84 more refs;
wenzelm
parents: 58554
diff changeset
    17
  @{cite "Wenzel:2011:CICM" and "Wenzel:2012"}. Many concepts and system
71a63f8a5b84 more refs;
wenzelm
parents: 58554
diff changeset
    18
  components are fit together in order to make this work. The main building
71a63f8a5b84 more refs;
wenzelm
parents: 58554
diff changeset
    19
  blocks are as follows.
53769
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    20
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
    21
  \begin{description}
53769
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    22
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
    23
  \item [PIDE] is a general framework for Prover IDEs based on Isabelle/Scala.
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
    24
  It is built around a concept of parallel and asynchronous document
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
    25
  processing, which is supported natively by the parallel proof engine that is
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
    26
  implemented in Isabelle/ML. The traditional prover command loop is given up;
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
    27
  instead there is direct support for editing of source text, with rich formal
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
    28
  markup for GUI 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
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
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.\
57337
8b46b57008ea misc tuning;
wenzelm
parents: 57336
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.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
    61
\<close>
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
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
    64
section \<open>The Isabelle/jEdit Prover IDE\<close>
53770
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    65
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
    66
text \<open>
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}
57312
afbc20986435 updated screenshots;
wenzelm
parents: 57311
diff changeset
    69
  \includegraphics[scale=0.333]{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
57337
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    75
  Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some plugins for
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    76
  the jEdit text editor, while preserving its general look-and-feel as far as
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    77
  possible. The main plugin is called ``Isabelle'' and has its own menu
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
    78
  \emph{Plugins~/ Isabelle} with access to several panels (see also
57337
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    79
  \secref{sec:dockables}), as well as \emph{Plugins~/ Plugin Options~/
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    80
  Isabelle} (see also \secref{sec:options}).
53770
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    81
57337
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    82
  The options allow to specify a logic session name --- the same selector is
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    83
  accessible in the \emph{Theories} panel (\secref{sec:theories}). On
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    84
  application startup, the selected logic session image is provided
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
    85
  automatically by the Isabelle build tool @{cite "isabelle-sys"}: if it is
57337
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    86
  absent or outdated wrt.\ its sources, the build process updates it before
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    87
  entering the Prover IDE.  Changing the logic session within Isabelle/jEdit
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
    88
  requires a restart of the whole application.
53769
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    89
57337
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    90
  \medskip The main job of the Prover IDE is to manage sources and their
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    91
  changes, taking the logical structure as a formal document into account (see
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    92
  also \secref{sec:document-model}). The editor and the prover are connected
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    93
  asynchronously in a lock-free manner. The prover is free to organize the
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    94
  checking of the formal text in parallel on multiple cores, and provides
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    95
  feedback via markup, which is rendered in the editor via colors, boxes,
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
    96
  squiggly underlines, hyperlinks, popup windows, icons, clickable output etc.
53770
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    97
57337
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    98
  Using the mouse together with the modifier key @{verbatim CONTROL} (Linux,
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    99
  Windows) or @{verbatim COMMAND} (Mac OS X) exposes additional formal content
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
   100
  via tooltips and/or hyperlinks (see also \secref{sec:tooltips-hyperlinks}).
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   101
  Output (in popups etc.) may be explored recursively, using the same
57337
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
   102
  techniques as in the editor source buffer.
53770
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
   103
57337
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
   104
  Thus the Prover IDE gives an impression of direct access to formal content
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
   105
  of the prover within the editor, but in reality only certain aspects are
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   106
  exposed, according to the possibilities of the prover and its many tools.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   107
\<close>
53769
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
   108
53770
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
   109
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   110
subsection \<open>Documentation\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   111
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   112
text \<open>
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   113
  The \emph{Documentation} panel of Isabelle/jEdit provides access to the
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   114
  standard Isabelle documentation: PDF files are opened by regular desktop
57338
wenzelm
parents: 57337
diff changeset
   115
  operations of the underlying platform. The section ``Original jEdit
wenzelm
parents: 57337
diff changeset
   116
  Documentation'' contains the original \emph{User's Guide} of this
wenzelm
parents: 57337
diff changeset
   117
  sophisticated text editor. The same is accessible via the @{verbatim Help}
wenzelm
parents: 57337
diff changeset
   118
  menu or @{verbatim F1} keyboard shortcut, using the built-in HTML viewer of
wenzelm
parents: 57337
diff changeset
   119
  Java/Swing. The latter also includes \emph{Frequently Asked Questions} and
wenzelm
parents: 57337
diff changeset
   120
  documentation of individual plugins.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   121
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   122
  Most of the information about generic jEdit is relevant for Isabelle/jEdit
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   123
  as well, but one needs to keep in mind that defaults sometimes differ, and
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   124
  the official jEdit documentation does not know about the Isabelle plugin
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   125
  with its support for continuous checking of formal source text: jEdit is a
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   126
  plain text editor, but Isabelle/jEdit is a Prover IDE.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   127
\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   128
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   129
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   130
subsection \<open>Plugins\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   131
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   132
text \<open>
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   133
  The \emph{Plugin Manager} of jEdit allows to augment editor functionality by
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   134
  JVM modules (jars) that are provided by the central plugin repository, which
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   135
  is accessible via various mirror sites.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   136
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   137
  Connecting to the plugin server-infrastructure of the jEdit project allows
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   138
  to update bundled plugins or to add further functionality. This needs to be
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   139
  done with the usual care for such an open bazaar of contributions. Arbitrary
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   140
  combinations of add-on features are apt to cause problems. It is advisable
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   141
  to start with the default configuration of Isabelle/jEdit and develop some
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   142
  understanding how it is supposed to work, before loading additional plugins
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   143
  at a grand scale.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   144
54348
wenzelm
parents: 54331
diff changeset
   145
  \medskip The main \emph{Isabelle} plugin is an integral part of
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   146
  Isabelle/jEdit and needs to remain active at all times! A few additional
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   147
  plugins are bundled with Isabelle/jEdit for convenience or out of necessity,
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   148
  notably \emph{Console} with its Isabelle/Scala sub-plugin
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   149
  (\secref{sec:scala-console}) and \emph{SideKick} with some Isabelle-specific
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   150
  parsers for document tree structure (\secref{sec:sidekick}). The
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   151
  \emph{Navigator} plugin is particularly important for hyperlinks within the
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   152
  formal document-model (\secref{sec:tooltips-hyperlinks}). Further plugins
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   153
  (e.g.\ \emph{ErrorList}, \emph{Code2HTML}) are included to saturate the
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   154
  dependencies of bundled plugins, but have no particular use in
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   155
  Isabelle/jEdit.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   156
\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   157
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   158
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   159
subsection \<open>Options \label{sec:options}\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   160
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   161
text \<open>Both jEdit and Isabelle have distinctive management of
54348
wenzelm
parents: 54331
diff changeset
   162
  persistent options.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   163
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
   164
  Regular jEdit options are accessible via the dialogs \emph{Utilities~/
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
   165
  Global Options} or \emph{Plugins~/ Plugin Options}, with a second chance to
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   166
  flip the two within the central options dialog. Changes are stored in
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   167
  @{file_unchecked "$ISABELLE_HOME_USER/jedit/properties"} and
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   168
  @{file_unchecked "$ISABELLE_HOME_USER/jedit/keymaps"}.
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   169
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   170
  Isabelle system options are managed by Isabelle/Scala and changes are stored
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   171
  in @{file_unchecked "$ISABELLE_HOME_USER/etc/preferences"}, independently of
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   172
  other jEdit properties. See also @{cite "isabelle-sys"}, especially the
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   173
  coverage of sessions and command-line tools like @{tool build} or @{tool
54372
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
   174
  options}.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   175
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   176
  Those Isabelle options that are declared as \textbf{public} are configurable
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
   177
  in Isabelle/jEdit via \emph{Plugin Options~/ Isabelle~/ General}. Moreover,
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   178
  there are various options for rendering of document content, which are
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
   179
  configurable via \emph{Plugin Options~/ Isabelle~/ Rendering}. Thus
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
   180
  \emph{Plugin Options~/ Isabelle} in jEdit provides a view on a subset of
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   181
  Isabelle system options. Note that some of these options affect general
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   182
  parameters that are relevant outside Isabelle/jEdit as well, e.g.\
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   183
  @{system_option threads} or @{system_option parallel_proofs} for the
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   184
  Isabelle build tool @{cite "isabelle-sys"}, but it is possible to use the
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   185
  settings variable @{setting ISABELLE_BUILD_OPTIONS} to change defaults for
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   186
  batch builds without affecting Isabelle/jEdit.
54329
e0fa4bd16c80 misc tuning;
wenzelm
parents: 54323
diff changeset
   187
57627
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57603
diff changeset
   188
  The jEdit action @{action_def isabelle.options} opens the options dialog for
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57603
diff changeset
   189
  the Isabelle plugin; it can be mapped to editor GUI elements as usual.
65fc7ae1bf66 added action "isabelle.options" (despite problems with initial window size);
wenzelm
parents: 57603
diff changeset
   190
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   191
  \medskip Options are usually loaded on startup and saved on shutdown of
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   192
  Isabelle/jEdit. Editing the machine-generated @{file_unchecked
54372
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
   193
  "$ISABELLE_HOME_USER/jedit/properties"} or @{file_unchecked
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   194
  "$ISABELLE_HOME_USER/etc/preferences"} manually while the application is
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   195
  running is likely to cause surprise due to lost update!\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   196
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   197
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   198
subsection \<open>Keymaps\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   199
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   200
text \<open>Keyboard shortcuts used to be managed as jEdit properties in
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   201
  the past, but recent versions (2013) have a separate concept of
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
   202
  \emph{keymap} that is configurable via \emph{Global Options~/
54348
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
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   207
  This is relevant for Isabelle/jEdit due to various fine-tuning of default
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   208
  properties, and additional keyboard shortcuts for Isabelle-specific
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   209
  functionality. Users may change their keymap later, but need to copy some
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
   210
  keyboard shortcuts manually (see also @{file_unchecked
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   211
  "$ISABELLE_HOME_USER/jedit/keymaps"} versus @{verbatim shortcut} properties
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   212
  in @{file "$ISABELLE_HOME/src/Tools/jEdit/src/jEdit.props"}).
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   213
\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   214
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   215
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   216
section \<open>Command-line invocation \label{sec:command-line}\<close>
57320
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   217
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   218
text \<open>
57320
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   219
  Isabelle/jEdit is normally invoked as standalone application, with
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   220
  platform-specific executable wrappers for Linux, Windows, Mac OS X.
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   221
  Nonetheless it is occasionally useful to invoke the Prover IDE on the
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   222
  command-line, with some extra options and environment settings as explained
57329
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   223
  below. The command-line usage of @{tool_def jedit} is as follows:
57320
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   224
\begin{ttbox}
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   225
  Usage: isabelle jedit [OPTIONS] [FILES ...]
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   226
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   227
  Options are:
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   228
    -J OPTION    add JVM runtime option (default JEDIT_JAVA_OPTIONS)
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   229
    -b           build only
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   230
    -d DIR       include session directory
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   231
    -f           fresh build
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   232
    -j OPTION    add jEdit runtime option (default JEDIT_OPTIONS)
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   233
    -l NAME      logic image name (default ISABELLE_LOGIC)
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   234
    -m MODE      add print mode for output
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   235
    -n           no build of session image on startup
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   236
    -s           system build mode for session image
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   237
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   238
  Start jEdit with Isabelle plugin setup and open theory FILES
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   239
  (default "\$USER_HOME/Scratch.thy").
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   240
\end{ttbox}
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   241
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   242
  The @{verbatim "-l"} option specifies the session name of the logic
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   243
  image to be used for proof processing.  Additional session root
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   244
  directories may be included via option @{verbatim "-d"} to augment
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   245
  that name space of @{tool build} @{cite "isabelle-sys"}.
57320
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   246
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   247
  By default, the specified image is checked and built on demand. The
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   248
  @{verbatim "-s"} option determines where to store the result session image
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   249
  of @{tool build}. The @{verbatim "-n"} option bypasses the implicit build
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   250
  process for the selected session image.
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   251
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   252
  The @{verbatim "-m"} option specifies additional print modes for the prover
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   253
  process. Note that the system option @{system_option_ref jedit_print_mode}
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   254
  allows to do the same persistently (e.g.\ via the \emph{Plugin Options}
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   255
  dialog of Isabelle/jEdit), without requiring command-line invocation.
57320
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   256
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   257
  The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass additional
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   258
  low-level options to the JVM or jEdit, respectively. The defaults are
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   259
  provided by the Isabelle settings environment @{cite "isabelle-sys"}, but
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   260
  note that these only work for the command-line tool described here, and not
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   261
  the regular application.
57320
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   262
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   263
  The @{verbatim "-b"} and @{verbatim "-f"} options control the self-build
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   264
  mechanism of Isabelle/jEdit. This is only relevant for building from
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   265
  sources, which also requires an auxiliary @{verbatim jedit_build} component
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   266
  from @{url "http://isabelle.in.tum.de/components"}. The official
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   267
  Isabelle release already includes a pre-built version of Isabelle/jEdit.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   268
\<close>
57320
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   269
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   270
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   271
chapter \<open>Augmented jEdit functionality\<close>
57318
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   272
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   273
section \<open>Look-and-feel\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   274
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   275
text \<open>jEdit is a Java/AWT/Swing application with some ambition to
54329
e0fa4bd16c80 misc tuning;
wenzelm
parents: 54323
diff changeset
   276
  support ``native'' look-and-feel on all platforms, within the limits
54330
wenzelm
parents: 54329
diff changeset
   277
  of what Oracle as Java provider and major operating system
wenzelm
parents: 54329
diff changeset
   278
  distributors allow (see also \secref{sec:problems}).
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   279
54329
e0fa4bd16c80 misc tuning;
wenzelm
parents: 54323
diff changeset
   280
  Isabelle/jEdit enables platform-specific look-and-feel by default as
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   281
  follows.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   282
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   283
  \begin{description}
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   284
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   285
  \item[Linux:] The platform-independent \emph{Nimbus} is used by
54372
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
   286
  default.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   287
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   288
  \emph{GTK+} works under the side-condition that the overall GTK theme is
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   289
  selected in a Swing-friendly way.\footnote{GTK support in Java/Swing was
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   290
  once marketed aggressively by Sun, but never quite finished. Today (2013) it
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   291
  is lagging behind further development of Swing and GTK. The graphics
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   292
  rendering performance can be worse than for other Swing look-and-feels.}
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   293
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   294
  \item[Windows:] Regular \emph{Windows} is used by default, but
54381
wenzelm
parents: 54380
diff changeset
   295
  \emph{Windows Classic} also works.
54372
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
   296
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   297
  \item[Mac OS X:] Regular \emph{Mac OS X} is used by default.
54372
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
   298
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   299
  The bundled \emph{MacOSX} plugin provides various functions that are
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   300
  expected from applications on that particular platform: quit from menu or
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   301
  dock, preferences menu, drag-and-drop of text files on the application,
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   302
  full-screen mode for main editor windows. It is advisable to have the
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   303
  \emph{MacOSX} plugin enabled all the time on that platform.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   304
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   305
  \end{description}
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   306
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   307
  Users may experiment with different look-and-feels, but need to keep
54329
e0fa4bd16c80 misc tuning;
wenzelm
parents: 54323
diff changeset
   308
  in mind that this extra variance of GUI functionality is unlikely to
54372
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
   309
  work in arbitrary combinations.  The platform-independent
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
   310
  \emph{Nimbus} and \emph{Metal} should always work.  The historic
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
   311
  \emph{CDE/Motif} is better avoided.
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
   312
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
   313
  After changing the look-and-feel in \emph{Global Options~/
54372
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
   314
  Appearance}, it is advisable to restart Isabelle/jEdit in order to
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   315
  take full effect.\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   316
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   317
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   318
section \<open>Dockable windows \label{sec:dockables}\<close>
57316
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   319
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   320
text \<open>
57316
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   321
  In jEdit terminology, a \emph{view} is an editor window with one or more
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   322
  \emph{text areas} that show the content of one or more \emph{buffers}. A
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   323
  regular view may be surrounded by \emph{dockable windows} that show
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   324
  additional information in arbitrary format, not just text; a \emph{plain
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   325
  view} does not allow dockables. The \emph{dockable window manager} of jEdit
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   326
  organizes these dockable windows, either as \emph{floating} windows, or
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   327
  \emph{docked} panels within one of the four margins of the view. There may
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   328
  be any number of floating instances of some dockable window, but at most one
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   329
  docked instance; jEdit actions that address \emph{the} dockable window of a
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   330
  particular kind refer to the unique docked instance.
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   331
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   332
  Dockables are used routinely in jEdit for important functionality like
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   333
  \emph{HyperSearch Results} or the \emph{File System Browser}. Plugins often
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   334
  provide a central dockable to access their key functionality, which may be
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   335
  opened by the user on demand. The Isabelle/jEdit plugin takes this approach
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   336
  to the extreme: its plugin menu merely provides entry-points to panels that
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   337
  are managed as dockable windows. Some important panels are docked by
57316
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   338
  default, e.g.\ \emph{Documentation}, \emph{Output}, \emph{Query}, but the
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   339
  user can change this arrangement easily.
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   340
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   341
  Compared to plain jEdit, dockable window management in Isabelle/jEdit is
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   342
  slightly augmented according to the the following principles:
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   343
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   344
  \begin{itemize}
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   345
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   346
  \item Floating windows are dependent on the main window as \emph{dialog} in
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   347
  the sense of Java/AWT/Swing. Dialog windows always stay on top of the view,
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   348
  which is particularly important in full-screen mode. The desktop environment
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   349
  of the underlying platform may impose further policies on such dependent
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   350
  dialogs, in contrast to fully independent windows, e.g.\ some window
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   351
  management functions may be missing.
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   352
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   353
  \item Keyboard focus of the main view vs.\ a dockable window is carefully
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   354
  managed according to the intended semantics, as a panel mainly for output or
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   355
  input. For example, activating the \emph{Output} (\secref{sec:output}) panel
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   356
  via the dockable window manager returns keyboard focus to the main text
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   357
  area, but for \emph{Query} (\secref{sec:query}) the focus is given to the
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   358
  main input field of that panel.
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   359
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   360
  \item Panels that provide their own text area for output have an additional
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   361
  dockable menu item \emph{Detach}. This produces an independent copy of the
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   362
  current output as a floating \emph{Info} window, which displays that content
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   363
  independently of ongoing changes of the PIDE document-model. Note that
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   364
  Isabelle/jEdit popup windows (\secref{sec:tooltips-hyperlinks}) provide a
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   365
  similar \emph{Detach} operation as an icon.
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   366
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   367
  \end{itemize}
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   368
\<close>
57316
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   369
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   370
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   371
section \<open>Isabelle symbols \label{sec:symbols}\<close>
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   372
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   373
text \<open>
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   374
  Isabelle sources consist of \emph{symbols} that extend plain ASCII to allow
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   375
  infinitely many mathematical symbols within the formal sources. This works
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   376
  without depending on particular encodings and varying Unicode
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   377
  standards.\footnote{Raw Unicode characters within formal sources would
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   378
  compromise portability and reliability in the face of changing
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   379
  interpretation of special features of Unicode, such as Combining Characters
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   380
  or Bi-directional Text.} See also @{cite "Wenzel:2011:CICM"}.
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   381
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   382
  For the prover back-end, formal text consists of ASCII characters that are
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   383
  grouped according to some simple rules, e.g.\ as plain ``@{verbatim a}'' or
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   384
  symbolic ``@{verbatim "\<alpha>"}''. For the editor front-end, a certain subset of
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   385
  symbols is rendered physically via Unicode glyphs, in order to show
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   386
  ``@{verbatim "\<alpha>"}'' as ``@{text "\<alpha>"}'', for example. This symbol
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   387
  interpretation is specified by the Isabelle system distribution in @{file
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   388
  "$ISABELLE_HOME/etc/symbols"} and may be augmented by the user in
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   389
  @{file_unchecked "$ISABELLE_HOME_USER/etc/symbols"}.
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   390
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   391
  The appendix of @{cite "isabelle-isar-ref"} gives an overview of the
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   392
  standard interpretation of finitely many symbols from the infinite
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   393
  collection. Uninterpreted symbols are displayed literally, e.g.\
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   394
  ``@{verbatim "\<foobar>"}''. Overlap of Unicode characters used in symbol
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   395
  interpretation with informal ones (which might appear e.g.\ in comments)
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   396
  needs to be avoided. Raw Unicode characters within prover source files
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   397
  should be restricted to informal parts, e.g.\ to write text in non-latin
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   398
  alphabets in comments.
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   399
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   400
  \medskip \paragraph{Encoding.} Technically, the Unicode view on Isabelle
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   401
  symbols is an \emph{encoding} in jEdit (not in the underlying JVM) that is
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   402
  called @{verbatim "UTF-8-Isabelle"}. It is provided by the Isabelle/jEdit
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   403
  plugin and enabled by default for all source files. Sometimes such defaults
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   404
  are reset accidentally, or malformed UTF-8 sequences in the text force jEdit
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   405
  to fall back on a different encoding like @{verbatim "ISO-8859-15"}. In that
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   406
  case, verbatim ``@{verbatim "\<alpha>"}'' will be shown in the text buffer instead
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   407
  of its Unicode rendering ``@{text "\<alpha>"}''. The jEdit menu operation
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   408
  \emph{File~/ Reload with Encoding~/ UTF-8-Isabelle} helps to resolve such
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   409
  problems (after repairing malformed parts of the text).
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   410
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   411
  \medskip \paragraph{Font.} Correct rendering via Unicode requires a
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   412
  font that contains glyphs for the corresponding codepoints.  Most
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   413
  system fonts lack that, so Isabelle/jEdit prefers its own
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   414
  application font @{verbatim IsabelleText}, which ensures that
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   415
  standard collection of Isabelle symbols are actually seen on the
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   416
  screen (or printer).
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   417
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   418
  Note that a Java/AWT/Swing application can load additional fonts only if
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   419
  they are not installed on the operating system already! Some outdated
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   420
  version of @{verbatim IsabelleText} that happens to be provided by the
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   421
  operating system would prevent Isabelle/jEdit to use its bundled version.
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   422
  This could lead to missing glyphs (black rectangles), when the system
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   423
  version of @{verbatim IsabelleText} is older than the application version.
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   424
  This problem can be avoided by refraining to ``install'' any version of
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   425
  @{verbatim IsabelleText} in the first place, although it is occasionally
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   426
  tempting to use the same font in other applications.
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   427
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   428
  \medskip \paragraph{Input methods.} In principle, Isabelle/jEdit
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   429
  could delegate the problem to produce Isabelle symbols in their
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   430
  Unicode rendering to the underlying operating system and its
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   431
  \emph{input methods}.  Regular jEdit also provides various ways to
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   432
  work with \emph{abbreviations} to produce certain non-ASCII
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   433
  characters.  Since none of these standard input methods work
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   434
  satisfactorily for the mathematical characters required for
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   435
  Isabelle, various specific Isabelle/jEdit mechanisms are provided.
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   436
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   437
  This is a summary for practically relevant input methods for Isabelle
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   438
  symbols.
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   439
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   440
  \begin{enumerate}
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   441
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   442
  \item The \emph{Symbols} panel: some GUI buttons allow to insert
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   443
  certain symbols in the text buffer.  There are also tooltips to
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   444
  reveal the official Isabelle representation with some additional
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   445
  information about \emph{symbol abbreviations} (see below).
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   446
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
   447
  \item Copy/paste from decoded source files: text that is rendered
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   448
  as Unicode already can be re-used to produce further text.  This
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   449
  also works between different applications, e.g.\ Isabelle/jEdit and
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   450
  some web browser or mail client, as long as the same Unicode view on
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   451
  Isabelle symbols is used.
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   452
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
   453
  \item Copy/paste from prover output within Isabelle/jEdit.  The
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   454
  same principles as for text buffers apply, but note that \emph{copy}
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   455
  in secondary Isabelle/jEdit windows works via the keyboard shortcut
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   456
  @{verbatim "C+c"}, while jEdit menu actions always refer to the
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   457
  primary text area!
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   458
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   459
  \item Completion provided by Isabelle plugin (see
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   460
  \secref{sec:completion}).  Isabelle symbols have a canonical name
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   461
  and optional abbreviations.  This can be used with the text
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   462
  completion mechanism of Isabelle/jEdit, to replace a prefix of the
57328
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
   463
  actual symbol like @{verbatim "\<lambda>"}, or its name preceded by backslash
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   464
  @{verbatim "\\"}@{verbatim "lambda"}, or its ASCII abbreviation
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   465
  @{verbatim "%"} by the Unicode rendering.
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   466
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   467
  The following table is an extract of the information provided by the
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   468
  standard @{file "$ISABELLE_HOME/etc/symbols"} file:
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   469
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   470
  \medskip
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   471
  \begin{tabular}{lll}
57328
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
   472
    \textbf{symbol} & \textbf{name with backslash} & \textbf{abbreviation} \\\hline
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   473
    @{text "\<lambda>"} & @{verbatim "\\lambda"} & @{verbatim "%"} \\
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   474
    @{text "\<Rightarrow>"} & @{verbatim "\\Rightarrow"} & @{verbatim "=>"} \\
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   475
    @{text "\<Longrightarrow>"} & @{verbatim "\\Longrightarrow"} & @{verbatim "==>"} \\[0.5ex]
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   476
    @{text "\<And>"} & @{verbatim "\\And"} & @{verbatim "!!"} \\
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   477
    @{text "\<equiv>"} & @{verbatim "\\equiv"} & @{verbatim "=="} \\[0.5ex]
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   478
    @{text "\<forall>"} & @{verbatim "\\forall"} & @{verbatim "!"} \\
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   479
    @{text "\<exists>"} & @{verbatim "\\exists"} & @{verbatim "?"} \\
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   480
    @{text "\<longrightarrow>"} & @{verbatim "\\longrightarrow"} & @{verbatim "-->"} \\
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   481
    @{text "\<and>"} & @{verbatim "\\and"} & @{verbatim "&"} \\
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   482
    @{text "\<or>"} & @{verbatim "\\or"} & @{verbatim "|"} \\
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   483
    @{text "\<not>"} & @{verbatim "\\not"} & @{verbatim "~"} \\
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   484
    @{text "\<noteq>"} & @{verbatim "\\noteq"} & @{verbatim "~="} \\
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   485
    @{text "\<in>"} & @{verbatim "\\in"} & @{verbatim ":"} \\
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   486
    @{text "\<notin>"} & @{verbatim "\\notin"} & @{verbatim "~:"} \\
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   487
  \end{tabular}
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   488
  \medskip
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   489
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   490
  Note that the above abbreviations refer to the input method. The logical
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   491
  notation provides ASCII alternatives that often coincide, but sometimes
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   492
  deviate. This occasionally causes user confusion with very old-fashioned
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   493
  Isabelle source that use ASCII replacement notation like @{verbatim "!"} or
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   494
  @{verbatim "ALL"} directly in the text.
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   495
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   496
  On the other hand, coincidence of symbol abbreviations with ASCII
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   497
  replacement syntax syntax helps to update old theory sources via
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   498
  explicit completion (see also @{verbatim "C+b"} explained in
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   499
  \secref{sec:completion}).
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   500
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   501
  \end{enumerate}
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   502
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   503
  \paragraph{Control symbols.} There are some special control symbols
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   504
  to modify the display style of a single symbol (without
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   505
  nesting). Control symbols may be applied to a region of selected
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   506
  text, either using the \emph{Symbols} panel or keyboard shortcuts or
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   507
  jEdit actions.  These editor operations produce a separate control
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   508
  symbol for each symbol in the text, in order to make the whole text
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   509
  appear in a certain style.
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   510
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   511
  \medskip
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   512
  \begin{tabular}{llll}
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   513
    \textbf{style} & \textbf{symbol} & \textbf{shortcut} & \textbf{action} \\\hline
57329
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   514
    superscript & @{verbatim "\<^sup>"} & @{verbatim "C+e UP"} & @{action_ref "isabelle.control-sup"} \\
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   515
    subscript & @{verbatim "\<^sub>"} & @{verbatim "C+e DOWN"} & @{action_ref "isabelle.control-sub"} \\
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   516
    bold face & @{verbatim "\<^bold>"} & @{verbatim "C+e RIGHT"} & @{action_ref "isabelle.control-bold"} \\
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   517
    reset & & @{verbatim "C+e LEFT"} & @{action_ref "isabelle.control-reset"} \\
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   518
  \end{tabular}
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   519
  \medskip
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   520
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   521
  To produce a single control symbol, it is also possible to complete
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   522
  on @{verbatim "\\"}@{verbatim sup}, @{verbatim "\\"}@{verbatim sub},
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   523
  @{verbatim "\\"}@{verbatim bold} as for regular symbols.\<close>
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   524
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   525
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   526
section \<open>SideKick parsers \label{sec:sidekick}\<close>
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   527
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   528
text \<open>
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   529
  The \emph{SideKick} plugin provides some general services to display buffer
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   530
  structure in a tree view.
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   531
57336
e13c5dd9c7de added screenshot;
wenzelm
parents: 57335
diff changeset
   532
  Isabelle/jEdit provides SideKick parsers for its main mode for theory files,
e13c5dd9c7de added screenshot;
wenzelm
parents: 57335
diff changeset
   533
  as well as some minor modes for the @{verbatim NEWS} file (see
e13c5dd9c7de added screenshot;
wenzelm
parents: 57335
diff changeset
   534
  \figref{fig:sidekick}), session @{verbatim ROOT} files, and system
e13c5dd9c7de added screenshot;
wenzelm
parents: 57335
diff changeset
   535
  @{verbatim options}.
e13c5dd9c7de added screenshot;
wenzelm
parents: 57335
diff changeset
   536
e13c5dd9c7de added screenshot;
wenzelm
parents: 57335
diff changeset
   537
  \begin{figure}[htb]
e13c5dd9c7de added screenshot;
wenzelm
parents: 57335
diff changeset
   538
  \begin{center}
e13c5dd9c7de added screenshot;
wenzelm
parents: 57335
diff changeset
   539
  \includegraphics[scale=0.333]{sidekick}
e13c5dd9c7de added screenshot;
wenzelm
parents: 57335
diff changeset
   540
  \end{center}
e13c5dd9c7de added screenshot;
wenzelm
parents: 57335
diff changeset
   541
  \caption{The Isabelle NEWS file with SideKick tree view}
e13c5dd9c7de added screenshot;
wenzelm
parents: 57335
diff changeset
   542
  \label{fig:sidekick}
e13c5dd9c7de added screenshot;
wenzelm
parents: 57335
diff changeset
   543
  \end{figure}
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   544
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   545
  Moreover, the special SideKick parser @{verbatim "isabelle-markup"}
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   546
  provides access to the full (uninterpreted) markup tree of the PIDE
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   547
  document model of the current buffer.  This is occasionally useful
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   548
  for informative purposes, but the amount of displayed information
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   549
  might cause problems for large buffers, both for the human and the
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   550
  machine.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   551
\<close>
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   552
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   553
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   554
section \<open>Scala console \label{sec:scala-console}\<close>
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   555
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   556
text \<open>
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   557
  The \emph{Console} plugin manages various shells (command interpreters),
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   558
  e.g.\ \emph{BeanShell}, which is the official jEdit scripting language, and
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   559
  the cross-platform \emph{System} shell. Thus the console provides similar
57603
0f58af858813 more default imports;
wenzelm
parents: 57589
diff changeset
   560
  functionality than the Emacs buffers @{verbatim "*scratch*"} and
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   561
  @{verbatim "*shell*"}.
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   562
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   563
  Isabelle/jEdit extends the repertoire of the console by \emph{Scala}, which
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   564
  is the regular Scala toplevel loop running inside the same JVM process as
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   565
  Isabelle/jEdit itself. This means the Scala command interpreter has access
57603
0f58af858813 more default imports;
wenzelm
parents: 57589
diff changeset
   566
  to the JVM name space and state of the running Prover IDE application. The
0f58af858813 more default imports;
wenzelm
parents: 57589
diff changeset
   567
  default environment imports the full content of packages @{verbatim
0f58af858813 more default imports;
wenzelm
parents: 57589
diff changeset
   568
  "isabelle"} and @{verbatim "isabelle.jedit"}.
0f58af858813 more default imports;
wenzelm
parents: 57589
diff changeset
   569
0f58af858813 more default imports;
wenzelm
parents: 57589
diff changeset
   570
  For example, @{verbatim PIDE} refers to the Isabelle/jEdit plugin object,
0f58af858813 more default imports;
wenzelm
parents: 57589
diff changeset
   571
  and @{verbatim view} to the current editor view of jEdit. The Scala
0f58af858813 more default imports;
wenzelm
parents: 57589
diff changeset
   572
  expression @{verbatim "PIDE.snapshot(view)"} makes a PIDE document snapshot
0f58af858813 more default imports;
wenzelm
parents: 57589
diff changeset
   573
  of the current buffer within the current editor view.
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   574
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   575
  This helps to explore Isabelle/Scala functionality interactively. Some care
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   576
  is required to avoid interference with the internals of the running
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   577
  application, especially in production use.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   578
\<close>
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   579
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   580
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   581
section \<open>File-system access\<close>
57318
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   582
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   583
text \<open>
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   584
  File specifications in jEdit follow various formats and conventions
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   585
  according to \emph{Virtual File Systems}, which may be also provided by
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   586
  additional plugins. This allows to access remote files via the @{verbatim
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   587
  "http:"} protocol prefix, for example. Isabelle/jEdit attempts to work with
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   588
  the file-system model of jEdit as far as possible. In particular, theory
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   589
  sources are passed directly from the editor to the prover, without
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   590
  indirection via physical files.
57318
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   591
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   592
  Despite the flexibility of URLs in jEdit, local files are particularly
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   593
  important and are accessible without protocol prefix. Here the path notation
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   594
  is that of the Java Virtual Machine on the underlying platform. On Windows
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   595
  the preferred form uses backslashes, but happens to accept forward slashes
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   596
  like Unix/POSIX. Further differences arise due to Windows drive letters and
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   597
  network shares.
57318
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   598
57331
wenzelm
parents: 57329
diff changeset
   599
  The Java notation for files needs to be distinguished from the one of
wenzelm
parents: 57329
diff changeset
   600
  Isabelle, which uses POSIX notation with forward slashes on \emph{all}
wenzelm
parents: 57329
diff changeset
   601
  platforms.\footnote{Isabelle/ML on Windows uses Cygwin file-system access
wenzelm
parents: 57329
diff changeset
   602
  and Unix-style path notation.} Moreover, environment variables from the
57318
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   603
  Isabelle process may be used freely, e.g.\ @{file
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   604
  "$ISABELLE_HOME/etc/symbols"} or @{file_unchecked "$POLYML_HOME/README"}.
57331
wenzelm
parents: 57329
diff changeset
   605
  There are special shortcuts: @{file "~"} for @{file "$USER_HOME"} and @{file
wenzelm
parents: 57329
diff changeset
   606
  "~~"} for @{file "$ISABELLE_HOME"}.
57318
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   607
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   608
  \medskip Since jEdit happens to support environment variables within file
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   609
  specifications as well, it is natural to use similar notation within the
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   610
  editor, e.g.\ in the file-browser. This does not work in full generality,
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   611
  though, due to the bias of jEdit towards platform-specific notation and of
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   612
  Isabelle towards POSIX. Moreover, the Isabelle settings environment is not
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   613
  yet active when starting Isabelle/jEdit via its standard application
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   614
  wrapper, in contrast to @{verbatim "isabelle jedit"} run from the command
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   615
  line (\secref{sec:command-line}).
57318
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   616
57331
wenzelm
parents: 57329
diff changeset
   617
  Isabelle/jEdit imitates @{verbatim "$ISABELLE_HOME"} and @{verbatim
wenzelm
parents: 57329
diff changeset
   618
  "$ISABELLE_HOME_USER"} within the Java process environment, in order to
wenzelm
parents: 57329
diff changeset
   619
  allow easy access to these important places from the editor. The file
wenzelm
parents: 57329
diff changeset
   620
  browser of jEdit also includes \emph{Favorites} for these two important
57326
wenzelm
parents: 57325
diff changeset
   621
  locations.
57318
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   622
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   623
  \medskip Path specifications in prover input or output usually include
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   624
  formal markup that turns it into a hyperlink (see also
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   625
  \secref{sec:tooltips-hyperlinks}). This allows to open the corresponding
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   626
  file in the text editor, independently of the path notation.
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   627
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   628
  Formally checked paths in prover input are subject to completion
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   629
  (\secref{sec:completion}): partial specifications are resolved via
57318
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   630
  directory content and possible completions are offered in a popup.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   631
\<close>
57318
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   632
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   633
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   634
chapter \<open>Prover IDE functionality \label{sec:document-model}\<close>
57315
d0f34f328ffa clarified section structure;
wenzelm
parents: 57314
diff changeset
   635
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   636
section \<open>Document model \label{sec:document-model}\<close>
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   637
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   638
text \<open>
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   639
  The document model is central to the PIDE architecture: the editor and the
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   640
  prover have a common notion of structured source text with markup, which is
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   641
  produced by formal processing. The editor is responsible for edits of
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   642
  document source, as produced by the user. The prover is responsible for
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   643
  reports of document markup, as produced by its processing in the background.
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   644
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   645
  Isabelle/jEdit handles classic editor events of jEdit, in order to connect
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   646
  the physical world of the GUI (with its singleton state) to the mathematical
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   647
  world of multiple document versions (with timeless and stateless updates).
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   648
\<close>
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   649
54322
9d156ded3c2a more documentation;
wenzelm
parents: 54321
diff changeset
   650
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   651
subsection \<open>Editor buffers and document nodes \label{sec:buffer-node}\<close>
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   652
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   653
text \<open>
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   654
  As a regular text editor, jEdit maintains a collection of \emph{buffers} to
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   655
  store text files; each buffer may be associated with any number of visible
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   656
  \emph{text areas}. Buffers are subject to an \emph{edit mode} that is
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   657
  determined from the file name extension. The following modes are treated
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   658
  specifically in Isabelle/jEdit:
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   659
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   660
  \medskip
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   661
  \begin{tabular}{lll}
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   662
  \textbf{mode} & \textbf{file extension} & \textbf{content} \\\hline
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   663
  @{verbatim "isabelle"} & @{verbatim ".thy"} & theory source \\
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   664
  @{verbatim "isabelle-ml"} & @{verbatim ".ML"} & Isabelle/ML source \\
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   665
  @{verbatim "sml"} & @{verbatim ".sml"} or @{verbatim ".sig"} & Standard ML source \\
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   666
  \end{tabular}
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   667
  \medskip
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   668
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   669
  All jEdit buffers are automatically added to the PIDE document-model as
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   670
  \emph{document nodes}. The overall document structure is defined by the
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   671
  theory nodes in two dimensions:
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   672
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   673
  \begin{enumerate}
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   674
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   675
  \item via \textbf{theory imports} that are specified in the \emph{theory
57329
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   676
  header} using concrete syntax of the @{command_ref theory} command
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   677
  @{cite "isabelle-isar-ref"};
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   678
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   679
  \item via \textbf{auxiliary files} that are loaded into a theory by special
57329
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   680
  \emph{load commands}, notably @{command_ref ML_file} and @{command_ref
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   681
  SML_file} @{cite "isabelle-isar-ref"}.
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   682
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   683
  \end{enumerate}
54322
9d156ded3c2a more documentation;
wenzelm
parents: 54321
diff changeset
   684
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   685
  In any case, source files are managed by the PIDE infrastructure: the
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   686
  physical file-system only plays a subordinate role. The relevant version of
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   687
  source text is passed directly from the editor to the prover, via internal
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   688
  communication channels.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   689
\<close>
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   690
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   691
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   692
subsection \<open>Theories \label{sec:theories}\<close>
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   693
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   694
text \<open>
57339
3bb94256e0ed added screenshot;
wenzelm
parents: 57338
diff changeset
   695
  The \emph{Theories} panel (see also \figref{fig:theories}) provides an
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   696
  overview of the status of continuous checking of theory nodes within the
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   697
  document model. Unlike batch sessions of @{tool build} @{cite
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   698
  "isabelle-sys"}, theory nodes are identified by full path names; this allows
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   699
  to work with multiple (disjoint) Isabelle sessions simultaneously within the
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   700
  same editor session.
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   701
57339
3bb94256e0ed added screenshot;
wenzelm
parents: 57338
diff changeset
   702
  \begin{figure}[htb]
3bb94256e0ed added screenshot;
wenzelm
parents: 57338
diff changeset
   703
  \begin{center}
3bb94256e0ed added screenshot;
wenzelm
parents: 57338
diff changeset
   704
  \includegraphics[scale=0.333]{theories}
3bb94256e0ed added screenshot;
wenzelm
parents: 57338
diff changeset
   705
  \end{center}
3bb94256e0ed added screenshot;
wenzelm
parents: 57338
diff changeset
   706
  \caption{Theories panel with an overview of the document-model, and some
3bb94256e0ed added screenshot;
wenzelm
parents: 57338
diff changeset
   707
  jEdit text areas as editable view on some of the document nodes}
3bb94256e0ed added screenshot;
wenzelm
parents: 57338
diff changeset
   708
  \label{fig:theories}
3bb94256e0ed added screenshot;
wenzelm
parents: 57338
diff changeset
   709
  \end{figure}
3bb94256e0ed added screenshot;
wenzelm
parents: 57338
diff changeset
   710
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   711
  Certain events to open or update editor buffers cause Isabelle/jEdit to
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   712
  resolve dependencies of theory imports. The system requests to load
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   713
  additional files into editor buffers, in order to be included in the
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   714
  document model for further checking. It is also possible to let the system
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   715
  resolve dependencies automatically, according to the system option
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   716
  @{system_option jedit_auto_load}.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   717
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   718
  \medskip The visible \emph{perspective} of Isabelle/jEdit is defined by the
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   719
  collective view on theory buffers via open text areas. The perspective is
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   720
  taken as a hint for document processing: the prover ensures that those parts
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   721
  of a theory where the user is looking are checked, while other parts that
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   722
  are presently not required are ignored. The perspective is changed by
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   723
  opening or closing text area windows, or scrolling within a window.
54322
9d156ded3c2a more documentation;
wenzelm
parents: 54321
diff changeset
   724
54330
wenzelm
parents: 54329
diff changeset
   725
  The \emph{Theories} panel provides some further options to influence
wenzelm
parents: 54329
diff changeset
   726
  the process of continuous checking: it may be switched off globally
54350
wenzelm
parents: 54349
diff changeset
   727
  to restrict the prover to superficial processing of command syntax.
wenzelm
parents: 54349
diff changeset
   728
  It is also possible to indicate theory nodes as \emph{required} for
54330
wenzelm
parents: 54329
diff changeset
   729
  continuous checking: this means such nodes and all their imports are
wenzelm
parents: 54329
diff changeset
   730
  always processed independently of the visibility status (if
wenzelm
parents: 54329
diff changeset
   731
  continuous checking is enabled).  Big theory libraries that are
wenzelm
parents: 54329
diff changeset
   732
  marked as required can have significant impact on performance,
wenzelm
parents: 54329
diff changeset
   733
  though.
54322
9d156ded3c2a more documentation;
wenzelm
parents: 54321
diff changeset
   734
9d156ded3c2a more documentation;
wenzelm
parents: 54321
diff changeset
   735
  \medskip Formal markup of checked theory content is turned into GUI
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   736
  rendering, based on a standard repertoire known from IDEs for programming
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   737
  languages: colors, icons, highlighting, squiggly underlines, tooltips,
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   738
  hyperlinks etc. For outer syntax of Isabelle/Isar there is some traditional
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   739
  syntax-highlighting via static keyword tables and tokenization within the
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   740
  editor. In contrast, the painting of inner syntax (term language etc.)\ uses
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   741
  semantic information that is reported dynamically from the logical context.
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   742
  Thus the prover can provide additional markup to help the user to understand
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   743
  the meaning of formal text, and to produce more text with some add-on tools
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   744
  (e.g.\ information messages with \emph{sendback} markup by automated provers
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   745
  or disprovers in the background).
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   746
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   747
\<close>
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   748
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   749
subsection \<open>Auxiliary files \label{sec:aux-files}\<close>
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   750
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   751
text \<open>
57329
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   752
  Special load commands like @{command_ref ML_file} and @{command_ref
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   753
  SML_file} @{cite "isabelle-isar-ref"} refer to auxiliary files within some
57329
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   754
  theory. Conceptually, the file argument of the command extends the theory
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   755
  source by the content of the file, but its editor buffer may be loaded~/
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   756
  changed~/ saved separately. The PIDE document model propagates changes of
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   757
  auxiliary file content to the corresponding load command in the theory, to
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   758
  update and process it accordingly: changes of auxiliary file content are
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   759
  treated as changes of the corresponding load command.
57323
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   760
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   761
  \medskip As a concession to the massive amount of ML files in Isabelle/HOL
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   762
  itself, the content of auxiliary files is only added to the PIDE
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   763
  document-model on demand, the first time when opened explicitly in the
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   764
  editor. There are further tricks to manage markup of ML files, such that
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   765
  Isabelle/HOL may be edited conveniently in the Prover IDE on small machines
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   766
  with only 4--8\,GB of main memory. Using @{verbatim Pure} as logic session
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   767
  image, the exploration may start at the top @{file
57323
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   768
  "$ISABELLE_HOME/src/HOL/Main.thy"} or the bottom @{file
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   769
  "$ISABELLE_HOME/src/HOL/HOL.thy"}, for example.
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   770
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   771
  Initially, before an auxiliary file is opened in the editor, the prover
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   772
  reads its content from the physical file-system. After the file is opened
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   773
  for the first time in the editor, e.g.\ by following the hyperlink
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   774
  (\secref{sec:tooltips-hyperlinks}) for the argument of its @{command
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   775
  ML_file} command, the content is taken from the jEdit buffer.
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   776
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   777
  The change of responsibility from prover to editor counts as an update of
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   778
  the document content, so subsequent theory sources need to be re-checked.
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   779
  When the buffer is closed, the responsibility remains to the editor: the
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   780
  file may be opened again without causing another document update.
57323
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   781
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   782
  A file that is opened in the editor, but its theory with the load command is
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   783
  not, is presently inactive in the document model. A file that is loaded via
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   784
  multiple load commands is associated to an arbitrary one: this situation is
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   785
  morally unsupported and might lead to confusion.
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   786
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   787
  \medskip Output that refers to an auxiliary file is combined with that of
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   788
  the corresponding load command, and shown whenever the file or the command
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   789
  are active (see also \secref{sec:output}).
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   790
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   791
  Warnings, errors, and other useful markup is attached directly to the
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   792
  positions in the auxiliary file buffer, in the manner of other well-known
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   793
  IDEs. By using the load command @{command SML_file} as explained in @{file
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   794
  "$ISABELLE_HOME/src/Tools/SML/Examples.thy"}, Isabelle/jEdit may be used as
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   795
  fully-featured IDE for Standard ML, independently of theory or proof
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   796
  development: the required theory merely serves as some kind of project
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   797
  file for a collection of SML source modules.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   798
\<close>
54322
9d156ded3c2a more documentation;
wenzelm
parents: 54321
diff changeset
   799
54352
7557f9f1d4aa misc tuning and clarification;
wenzelm
parents: 54351
diff changeset
   800
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   801
section \<open>Output \label{sec:output}\<close>
54353
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   802
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   803
text \<open>
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   804
  Prover output consists of \emph{markup} and \emph{messages}. Both are
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   805
  directly attached to the corresponding positions in the original source
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   806
  text, and visualized in the text area, e.g.\ as text colours for free and
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   807
  bound variables, or as squiggly underlines for warnings, errors etc.\ (see
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   808
  also \figref{fig:output}). In the latter case, the corresponding messages
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   809
  are shown by hovering with the mouse over the highlighted text --- although
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   810
  in many situations the user should already get some clue by looking at the
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   811
  position of the text highlighting, without the text itself.
54357
157b6eee6a76 more screenshots;
wenzelm
parents: 54356
diff changeset
   812
157b6eee6a76 more screenshots;
wenzelm
parents: 54356
diff changeset
   813
  \begin{figure}[htb]
157b6eee6a76 more screenshots;
wenzelm
parents: 54356
diff changeset
   814
  \begin{center}
57312
afbc20986435 updated screenshots;
wenzelm
parents: 57311
diff changeset
   815
  \includegraphics[scale=0.333]{output}
54357
157b6eee6a76 more screenshots;
wenzelm
parents: 54356
diff changeset
   816
  \end{center}
54372
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
   817
  \caption{Multiple views on prover output: gutter area with icon,
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
   818
    text area with popup, overview area, Theories panel, Output panel}
54357
157b6eee6a76 more screenshots;
wenzelm
parents: 54356
diff changeset
   819
  \label{fig:output}
157b6eee6a76 more screenshots;
wenzelm
parents: 54356
diff changeset
   820
  \end{figure}
54353
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   821
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   822
  The ``gutter area'' on the left-hand-side of the text area uses
54372
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
   823
  icons to provide a summary of the messages within the adjacent
54353
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   824
  line of text.  Message priorities are used to prefer errors over
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   825
  warnings, warnings over information messages, but plain output is
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   826
  ignored.
54353
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   827
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   828
  The ``overview area'' on the right-hand-side of the text area uses similar
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   829
  information to paint small rectangles for the overall status of the whole
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   830
  text buffer. The graphics is scaled to fit the logical buffer length into
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   831
  the given window height. Mouse clicks on the overview area position the
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   832
  cursor approximately to the corresponding line of text in the buffer.
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   833
  Repainting the overview in real-time causes problems with big theories, so
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   834
  it is restricted according to the system option @{system_option
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   835
  jedit_text_overview_limit} (in characters).
54353
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   836
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   837
  Another course-grained overview is provided by the \emph{Theories}
54372
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
   838
  panel, but without direct correspondence to text positions.  A
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
   839
  double-click on one of the theory entries with their status overview
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
   840
  opens the corresponding text buffer, without changing the cursor
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
   841
  position.
54353
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   842
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   843
  \medskip In addition, the \emph{Output} panel displays prover
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   844
  messages that correspond to a given command, within a separate
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   845
  window.
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   846
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   847
  The cursor position in the presently active text area determines the prover
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   848
  command whose cumulative message output is appended and shown in that window
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   849
  (in canonical order according to the internal execution of the command).
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   850
  There are also control elements to modify the update policy of the output
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   851
  wrt.\ continued editor movements. This is particularly useful with several
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   852
  independent instances of the \emph{Output} panel, which the Dockable Window
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   853
  Manager of jEdit can handle conveniently.
54353
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   854
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   855
  Former users of the old TTY interaction model (e.g.\ Proof~General) might
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   856
  find a separate window for prover messages familiar, but it is important to
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   857
  understand that the main Prover IDE feedback happens elsewhere. It is
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   858
  possible to do meaningful proof editing within the primary text area and its
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   859
  markup, while using secondary output windows only rarely.
54353
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   860
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   861
  The main purpose of the output window is to ``debug'' unclear
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   862
  situations by inspecting internal state of the prover.\footnote{In
54355
08cbb9461b48 more on Sledgehammer;
wenzelm
parents: 54354
diff changeset
   863
  that sense, unstructured tactic scripts depend on continuous
54353
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   864
  debugging with internal state inspection.} Consequently, some
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   865
  special messages for \emph{tracing} or \emph{proof state} only
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   866
  appear here, and are not attached to the original source.
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   867
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   868
  \medskip In any case, prover messages also contain markup that may
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   869
  be explored recursively via tooltips or hyperlinks (see
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   870
  \secref{sec:tooltips-hyperlinks}), or clicked directly to initiate
54355
08cbb9461b48 more on Sledgehammer;
wenzelm
parents: 54354
diff changeset
   871
  certain actions (see \secref{sec:auto-tools} and
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   872
  \secref{sec:sledgehammer}).\<close>
54353
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   873
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   874
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   875
section \<open>Query \label{sec:query}\<close>
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   876
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   877
text \<open>
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   878
  The \emph{Query} panel provides various GUI forms to request extra
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   879
  information from the prover. In old times the user would have issued some
57314
wenzelm
parents: 57313
diff changeset
   880
  diagnostic command like @{command find_theorems} and inspected its output,
wenzelm
parents: 57313
diff changeset
   881
  but this is now integrated into the Prover IDE.
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   882
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   883
  A \emph{Query} window provides some input fields and buttons for a
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   884
  particular query command, with output in a dedicated text area. There are
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   885
  various query modes: \emph{Find Theorems}, \emph{Find Constants},
57314
wenzelm
parents: 57313
diff changeset
   886
  \emph{Print Context}, e.g.\ see \figref{fig:query}. As usual in jEdit,
wenzelm
parents: 57313
diff changeset
   887
  multiple \emph{Query} windows may be active at the same time: any number of
57313
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   888
  floating instances, but at most one docked instance (which is used by
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   889
  default).
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   890
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   891
  \begin{figure}[htb]
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   892
  \begin{center}
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   893
  \includegraphics[scale=0.333]{query}
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   894
  \end{center}
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   895
  \caption{An instance of the Query panel}
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   896
  \label{fig:query}
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   897
  \end{figure}
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   898
57314
wenzelm
parents: 57313
diff changeset
   899
  \medskip The following GUI elements are common to all query modes:
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   900
  \begin{itemize}
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   901
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   902
  \item The spinning wheel provides feedback about the status of a pending
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   903
  query wrt.\ the evaluation of its context and its own operation.
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   904
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   905
  \item The \emph{Apply} button attaches a fresh query invocation to the
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   906
  current context of the command where the cursor is pointing in the text.
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   907
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   908
  \item The \emph{Search} field allows to highlight query output according to
57313
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   909
  some regular expression, in the notation that is commonly used on the Java
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   910
  platform.\footnote{@{url
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   911
  "http://docs.oracle.com/javase/7/docs/api/java/util/regex/Pattern.html"}}
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   912
  This may serve as an additional visual filter of the result.
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   913
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   914
  \item The \emph{Zoom} box controls the font size of the output area.
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   915
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   916
  \end{itemize}
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   917
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   918
  All query operations are asynchronous: there is no need to wait for the
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   919
  evaluation of the document for the query context, nor for the query
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   920
  operation itself. Query output may be detached as independent \emph{Info}
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   921
  window, using a menu operation of the dockable window manager. The printed
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   922
  result usually provides sufficient clues about the original query, with some
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   923
  hyperlink to its context (via markup of its head line).
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   924
\<close>
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   925
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   926
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   927
subsection \<open>Find theorems\<close>
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   928
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   929
text \<open>
57313
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   930
  The \emph{Query} panel in \emph{Find Theorems} mode retrieves facts from the
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   931
  theory or proof context matching all of given criteria in the \emph{Find}
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   932
  text field. A single criterium has the following syntax:
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   933
57313
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   934
  @{rail \<open>
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   935
    ('-'?) ('name' ':' @{syntax nameref} | 'intro' | 'elim' | 'dest' |
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   936
      'solves' | 'simp' ':' @{syntax term} | @{syntax term})
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   937
  \<close>}
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   938
57329
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   939
  See also the Isar command @{command_ref find_theorems} in
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   940
  @{cite "isabelle-isar-ref"}.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   941
\<close>
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   942
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   943
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   944
subsection \<open>Find constants\<close>
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   945
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   946
text \<open>
57313
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   947
  The \emph{Query} panel in \emph{Find Constants} mode prints all constants
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   948
  whose type meets all of the given criteria in the \emph{Find} text field.
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   949
  A single criterium has the following syntax:
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   950
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   951
  @{rail \<open>
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   952
    ('-'?)
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   953
      ('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type})
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   954
  \<close>}
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   955
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   956
  See also the Isar command @{command_ref find_consts} in @{cite
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   957
  "isabelle-isar-ref"}.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   958
\<close>
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   959
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   960
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   961
subsection \<open>Print context\<close>
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   962
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   963
text \<open>
57313
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   964
  The \emph{Query} panel in \emph{Print Context} mode prints information from
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
   965
  the theory or proof context, or proof state. See also the Isar commands
57329
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   966
  @{command_ref print_context}, @{command_ref print_cases}, @{command_ref
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   967
  print_term_bindings}, @{command_ref print_theorems}, @{command_ref
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   968
  print_state} described in @{cite "isabelle-isar-ref"}.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   969
\<close>
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   970
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
   971
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   972
section \<open>Tooltips and hyperlinks \label{sec:tooltips-hyperlinks}\<close>
54352
7557f9f1d4aa misc tuning and clarification;
wenzelm
parents: 54351
diff changeset
   973
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   974
text \<open>
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   975
  Formally processed text (prover input or output) contains rich markup
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   976
  information that can be explored further by using the @{verbatim CONTROL}
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   977
  modifier key on Linux and Windows, or @{verbatim COMMAND} on Mac OS X.
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   978
  Hovering with the mouse while the modifier is pressed reveals a
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   979
  \emph{tooltip} (grey box over the text with a yellow popup) and/or a
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   980
  \emph{hyperlink} (black rectangle over the text with change of mouse
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   981
  pointer); see also \figref{fig:tooltip}.
54331
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
   982
54357
157b6eee6a76 more screenshots;
wenzelm
parents: 54356
diff changeset
   983
  \begin{figure}[htb]
54331
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
   984
  \begin{center}
57312
afbc20986435 updated screenshots;
wenzelm
parents: 57311
diff changeset
   985
  \includegraphics[scale=0.5]{popup1}
54331
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
   986
  \end{center}
54356
9538f51da542 more screenshots;
wenzelm
parents: 54355
diff changeset
   987
  \caption{Tooltip and hyperlink for some formal entity}
54350
wenzelm
parents: 54349
diff changeset
   988
  \label{fig:tooltip}
54331
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
   989
  \end{figure}
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
   990
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   991
  Tooltip popups use the same rendering mechanisms as the main text
54350
wenzelm
parents: 54349
diff changeset
   992
  area, and further tooltips and/or hyperlinks may be exposed
54357
157b6eee6a76 more screenshots;
wenzelm
parents: 54356
diff changeset
   993
  recursively by the same mechanism; see \figref{fig:nested-tooltips}.
54323
d521407f8d0f more documentation;
wenzelm
parents: 54322
diff changeset
   994
54357
157b6eee6a76 more screenshots;
wenzelm
parents: 54356
diff changeset
   995
  \begin{figure}[htb]
54331
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
   996
  \begin{center}
57312
afbc20986435 updated screenshots;
wenzelm
parents: 57311
diff changeset
   997
  \includegraphics[scale=0.5]{popup2}
54331
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
   998
  \end{center}
54356
9538f51da542 more screenshots;
wenzelm
parents: 54355
diff changeset
   999
  \caption{Nested tooltips over formal entities}
54350
wenzelm
parents: 54349
diff changeset
  1000
  \label{fig:nested-tooltips}
54331
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
  1001
  \end{figure}
54350
wenzelm
parents: 54349
diff changeset
  1002
wenzelm
parents: 54349
diff changeset
  1003
  The tooltip popup window provides some controls to \emph{close} or
wenzelm
parents: 54349
diff changeset
  1004
  \emph{detach} the window, turning it into a separate \emph{Info}
54372
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
  1005
  window managed by jEdit.  The @{verbatim ESCAPE} key closes
54352
7557f9f1d4aa misc tuning and clarification;
wenzelm
parents: 54351
diff changeset
  1006
  \emph{all} popups, which is particularly relevant when nested
7557f9f1d4aa misc tuning and clarification;
wenzelm
parents: 54351
diff changeset
  1007
  tooltips are stacking up.
7557f9f1d4aa misc tuning and clarification;
wenzelm
parents: 54351
diff changeset
  1008
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
  1009
  \medskip A black rectangle in the text indicates a hyperlink that may be
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
  1010
  followed by a mouse click (while the @{verbatim CONTROL} or @{verbatim
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
  1011
  COMMAND} modifier key is still pressed). Such jumps to other text locations
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
  1012
  are recorded by the \emph{Navigator} plugin, which is bundled with
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
  1013
  Isabelle/jEdit and enabled by default, including navigation arrows in the
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
  1014
  main jEdit toolbar.
54352
7557f9f1d4aa misc tuning and clarification;
wenzelm
parents: 54351
diff changeset
  1015
7557f9f1d4aa misc tuning and clarification;
wenzelm
parents: 54351
diff changeset
  1016
  Also note that the link target may be a file that is itself not
7557f9f1d4aa misc tuning and clarification;
wenzelm
parents: 54351
diff changeset
  1017
  subject to formal document processing of the editor session and thus
7557f9f1d4aa misc tuning and clarification;
wenzelm
parents: 54351
diff changeset
  1018
  prevents further exploration: the chain of hyperlinks may end in
54372
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
  1019
  some source file of the underlying logic image, or within the
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1020
  Isabelle/ML bootstrap sources of Isabelle/Pure.\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
  1021
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
  1022
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1023
section \<open>Completion \label{sec:completion}\<close>
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1024
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1025
text \<open>
57328
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1026
  Smart completion of partial input is the IDE functionality \emph{par
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1027
  excellance}. Isabelle/jEdit combines several sources of information to
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1028
  achieve that. Despite its complexity, it should be possible to get some idea
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1029
  how completion works by experimentation, based on the overview of completion
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1030
  varieties in \secref{sec:completion-varieties}. The remaining subsections
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1031
  explain concepts around completion more systematically.
57325
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1032
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1033
  \medskip \emph{Explicit completion} is triggered by the action @{action_ref
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1034
  "isabelle.complete"}, which is bound to the keyboard shortcut @{verbatim
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1035
  "C+b"}, and thus overrides the jEdit default for @{action_ref
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1036
  "complete-word"}.
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1037
57328
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1038
  \emph{Implicit completion} hooks into the regular keyboard input stream of
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1039
  the editor, with some event filtering and optional delays.
54361
wenzelm
parents: 54360
diff changeset
  1040
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1041
  \medskip Completion options may be configured in \emph{Plugin Options~/
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1042
  Isabelle~/ General~/ Completion}. These are explained in further detail
57328
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1043
  below, whenever relevant. There is also a summary of options in
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1044
  \secref{sec:completion-options}.
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1045
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1046
  The asynchronous nature of PIDE interaction means that information from the
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1047
  prover is delayed --- at least by a full round-trip of the document update
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1048
  protocol. The default options already take this into account, with a
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1049
  sufficiently long completion delay to speculate on the availability of all
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1050
  relevant information from the editor and the prover, before completing text
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1051
  immediately or producing a popup. Although there is an inherent danger of
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1052
  non-deterministic behaviour due to such real-time parameters, the general
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1053
  completion policy aims at determined results as far as possible.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1054
\<close>
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1055
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1056
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1057
subsection \<open>Varieties of completion \label{sec:completion-varieties}\<close>
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1058
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1059
subsubsection \<open>Built-in templates\<close>
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1060
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1061
text \<open>
57327
20a575f99cda more on "Completion";
wenzelm
parents: 57326
diff changeset
  1062
  Isabelle is ultimately a framework of nested sub-languages of different
57328
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1063
  kinds and purposes. The completion mechanism supports this by the following
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1064
  built-in templates:
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1065
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1066
  \begin{description}
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1067
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1068
  \item[] @{verbatim "`"} (single ASCII back-quote) supports \emph{quotations}
57327
20a575f99cda more on "Completion";
wenzelm
parents: 57326
diff changeset
  1069
  via text cartouches. There are three selections, which are always presented
57328
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1070
  in the same order and do not depend on any context information. The default
57327
20a575f99cda more on "Completion";
wenzelm
parents: 57326
diff changeset
  1071
  choice produces a template ``@{text "\<open>\<box>\<close>"}'', where the box indicates the
20a575f99cda more on "Completion";
wenzelm
parents: 57326
diff changeset
  1072
  cursor position after insertion; the other choices help to repair the block
20a575f99cda more on "Completion";
wenzelm
parents: 57326
diff changeset
  1073
  structure of unbalanced text cartouches.
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1074
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1075
  \item[] @{verbatim "@{"} is completed to the template ``@{text "@{\<box>}"}'',
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1076
  where the box indicates the cursor position after insertion. Here it is
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1077
  convenient to use the wildcard ``@{verbatim __}'' or a more specific name
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1078
  prefix to let semantic completion of name-space entries propose
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1079
  antiquotation names.
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1080
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1081
  \end{description}
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1082
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1083
  With some practice, input of quoted sub-languages and antiquotations of
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1084
  embedded languages should work fluently. Note that national keyboard layouts
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1085
  might cause problems with back-quote as dead key: if possible, dead keys
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1086
  should be disabled.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1087
\<close>
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1088
57327
20a575f99cda more on "Completion";
wenzelm
parents: 57326
diff changeset
  1089
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1090
subsubsection \<open>Syntax keywords\<close>
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1091
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1092
text \<open>
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1093
  Syntax completion tables are determined statically from the keywords of the
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1094
  ``outer syntax'' of the underlying edit mode: for theory files this is the
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1095
  syntax of Isar commands.
57327
20a575f99cda more on "Completion";
wenzelm
parents: 57326
diff changeset
  1096
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1097
  Keywords are usually plain words, which means the completion mechanism only
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1098
  inserts them directly into the text for explicit completion
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1099
  (\secref{sec:completion-input}), but produces a popup
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1100
  (\secref{sec:completion-popup}) otherwise.
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1101
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1102
  At the point where outer syntax keywords are defined, it is possible to
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1103
  specify an alternative replacement string to be inserted instead of the
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1104
  keyword itself. An empty string means to suppress the keyword altogether,
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1105
  which is occasionally useful to avoid confusion, e.g.\ the rare keyword
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1106
  @{command simproc_setup} vs.\ the frequent name-space entry @{text simp}.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1107
\<close>
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1108
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1109
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1110
subsubsection \<open>Isabelle symbols\<close>
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1111
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1112
text \<open>
57325
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1113
  The completion tables for Isabelle symbols (\secref{sec:symbols}) are
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1114
  determined statically from @{file "$ISABELLE_HOME/etc/symbols"} and
57328
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1115
  @{file_unchecked "$ISABELLE_HOME_USER/etc/symbols"} for each symbol
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1116
  specification as follows:
57325
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1117
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1118
  \medskip
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1119
  \begin{tabular}{ll}
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1120
  \textbf{completion entry} & \textbf{example} \\\hline
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1121
  literal symbol & @{verbatim "\<forall>"} \\
57328
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1122
  symbol name with backslash & @{verbatim "\\"}@{verbatim forall} \\
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1123
  symbol abbreviation & @{verbatim "ALL"} or @{verbatim "!"} \\
57325
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1124
  \end{tabular}
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1125
  \medskip
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1126
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1127
  When inserted into the text, the above examples all produce the same Unicode
57325
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1128
  rendering @{text "\<forall>"} of the underlying symbol @{verbatim "\<forall>"}.
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1129
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1130
  A symbol abbreviation that is a plain word, like @{verbatim "ALL"}, is
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1131
  treated like a syntax keyword. Non-word abbreviations like @{verbatim "-->"}
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1132
  are inserted more aggressively, except for single-character abbreviations
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1133
  like @{verbatim "!"} above.
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1134
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1135
  \medskip Symbol completion depends on the semantic language context
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1136
  (\secref{sec:completion-context}), to enable or disable that aspect for a
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1137
  particular sub-language of Isabelle. For example, symbol completion is
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1138
  suppressed within document source to avoid confusion with {\LaTeX} macros
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1139
  that use similar notation.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1140
\<close>
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1141
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1142
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1143
subsubsection \<open>Name-space entries\<close>
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1144
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1145
text \<open>
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1146
  This is genuine semantic completion, using information from the prover, so
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1147
  it requires some delay. A \emph{failed name-space lookup} produces an error
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1148
  message that is annotated with a list of alternative names that are legal.
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1149
  The list of results is truncated according to the system option
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1150
  @{system_option_ref completion_limit}. The completion mechanism takes this
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1151
  into account when collecting information on the prover side.
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1152
57328
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1153
  Already recognized names are \emph{not} completed further, but completion
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1154
  may be extended by appending a suffix of underscores. This provokes a failed
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1155
  lookup, and another completion attempt while ignoring the underscores. For
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1156
  example, in a name space where @{verbatim "foo"} and @{verbatim "foobar"}
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1157
  are known, the input @{verbatim "foo"} remains unchanged, but @{verbatim
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1158
  "foo_"} may be completed to @{verbatim "foo"} or @{verbatim "foobar"}.
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1159
57326
wenzelm
parents: 57325
diff changeset
  1160
  The special identifier ``@{verbatim "__"}'' serves as a wild-card for
wenzelm
parents: 57325
diff changeset
  1161
  arbitrary completion: it exposes the name-space content to the completion
wenzelm
parents: 57325
diff changeset
  1162
  mechanism (truncated according to @{system_option completion_limit}). This
wenzelm
parents: 57325
diff changeset
  1163
  is occasionally useful to explore an unknown name-space, e.g.\ in some
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1164
  template.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1165
\<close>
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1166
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1167
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1168
subsubsection \<open>File-system paths\<close>
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1169
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1170
text \<open>
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1171
  Depending on prover markup about file-system path specifications in the
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1172
  source text, e.g.\ for the argument of a load command
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1173
  (\secref{sec:aux-files}), the completion mechanism explores the directory
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1174
  content and offers the result as completion popup. Relative path
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1175
  specifications are understood wrt.\ the \emph{master directory} of the
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1176
  document node (\secref{sec:buffer-node}) of the enclosing editor buffer;
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1177
  this requires a proper theory, not an auxiliary file.
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1178
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1179
  A suffix of slashes may be used to continue the exploration of an already
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1180
  recognized directory name.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1181
\<close>
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1182
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1183
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1184
subsubsection \<open>Spell-checking\<close>
57328
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1185
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1186
text \<open>
57328
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1187
  The spell-checker combines semantic markup from the prover (regions of plain
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1188
  words) with static dictionaries (word lists) that are known to the editor.
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1189
57333
d58b7f7d81db more on "Completion";
wenzelm
parents: 57332
diff changeset
  1190
  Unknown words are underlined in the text, using @{system_option_ref
57328
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1191
  spell_checker_color} (blue by default). This is not an error, but a hint to
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1192
  the user that some action may be taken. The jEdit context menu provides
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1193
  various actions, as far as applicable:
57328
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1194
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1195
  \medskip
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1196
  \begin{tabular}{l}
57329
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
  1197
  @{action_ref "isabelle.complete-word"} \\
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
  1198
  @{action_ref "isabelle.exclude-word"} \\
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
  1199
  @{action_ref "isabelle.exclude-word-permanently"} \\
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
  1200
  @{action_ref "isabelle.include-word"} \\
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
  1201
  @{action_ref "isabelle.include-word-permanently"} \\
57328
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1202
  \end{tabular}
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1203
  \medskip
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1204
57329
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
  1205
  Instead of the specific @{action_ref "isabelle.complete-word"}, it is also
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
  1206
  possible to use the generic @{action_ref "isabelle.complete"} with its
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1207
  default keyboard shortcut @{verbatim "C+b"}.
57328
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1208
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1209
  \medskip Dictionary lookup uses some educated guesses about lower-case,
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1210
  upper-case, and capitalized words. This is oriented on common use in
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1211
  English, where this aspect is not decisive for proper spelling, in contrast
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1212
  to German, for example.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1213
\<close>
57328
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1214
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1215
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1216
subsection \<open>Semantic completion context \label{sec:completion-context}\<close>
57325
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1217
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1218
text \<open>
57325
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1219
  Completion depends on a semantic context that is provided by the prover,
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1220
  although with some delay, because at least a full PIDE protocol round-trip
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1221
  is required. Until that information becomes available in the PIDE
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1222
  document-model, the default context is given by the outer syntax of the
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1223
  editor mode (see also \secref{sec:buffer-node}).
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1224
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1225
  The semantic \emph{language context} provides information about nested
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1226
  sub-languages of Isabelle: keywords are only completed for outer syntax,
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1227
  symbols or antiquotations for languages that support them. E.g.\ there is no
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1228
  symbol completion for ML source, but within ML strings, comments,
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1229
  antiquotations.
57325
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1230
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1231
  The prover may produce \emph{no completion} markup in exceptional
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1232
  situations, to tell that some language keywords should be excluded from
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1233
  further completion attempts. For example, @{verbatim ":"} within accepted
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1234
  Isar syntax looses its meaning as abbreviation for symbol @{text "\<in>"}.
57589
e0e4ac981cf1 always complete explicit symbols;
wenzelm
parents: 57425
diff changeset
  1235
e0e4ac981cf1 always complete explicit symbols;
wenzelm
parents: 57425
diff changeset
  1236
  \medskip The completion context is \emph{ignored} for built-in templates and
e0e4ac981cf1 always complete explicit symbols;
wenzelm
parents: 57425
diff changeset
  1237
  symbols in their explicit form ``@{verbatim "\<foobar>"}''; see also
e0e4ac981cf1 always complete explicit symbols;
wenzelm
parents: 57425
diff changeset
  1238
  \secref{sec:completion-varieties}. This allows to complete within broken
e0e4ac981cf1 always complete explicit symbols;
wenzelm
parents: 57425
diff changeset
  1239
  input that escapes its normal semantic context, e.g.\ antiquotations or
e0e4ac981cf1 always complete explicit symbols;
wenzelm
parents: 57425
diff changeset
  1240
  string literals in ML, which do not allow arbitrary backslash sequences.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1241
\<close>
57325
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1242
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1243
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1244
subsection \<open>Input events \label{sec:completion-input}\<close>
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1245
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1246
text \<open>
57332
da630c4fd92b more on "Completion";
wenzelm
parents: 57331
diff changeset
  1247
  Completion is triggered by certain events produced by the user, with
da630c4fd92b more on "Completion";
wenzelm
parents: 57331
diff changeset
  1248
  optional delay after keyboard input according to @{system_option
da630c4fd92b more on "Completion";
wenzelm
parents: 57331
diff changeset
  1249
  jedit_completion_delay}.
57325
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1250
57332
da630c4fd92b more on "Completion";
wenzelm
parents: 57331
diff changeset
  1251
  \begin{description}
da630c4fd92b more on "Completion";
wenzelm
parents: 57331
diff changeset
  1252
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1253
  \item[Explicit completion] works via action @{action_ref
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1254
  "isabelle.complete"} with keyboard shortcut @{verbatim "C+b"}. This
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1255
  overrides the shortcut for @{action_ref "complete-word"} in jEdit, but it is
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1256
  possible to restore the original jEdit keyboard mapping of @{action
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1257
  "complete-word"} via \emph{Global Options~/ Shortcuts} and invent a
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1258
  different one for @{action "isabelle.complete"}.
57325
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1259
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1260
  \item[Explicit spell-checker completion] works via @{action_ref
57332
da630c4fd92b more on "Completion";
wenzelm
parents: 57331
diff changeset
  1261
  "isabelle.complete-word"}, which is exposed in the jEdit context menu, if
da630c4fd92b more on "Completion";
wenzelm
parents: 57331
diff changeset
  1262
  the mouse points to a word that the spell-checker can complete.
da630c4fd92b more on "Completion";
wenzelm
parents: 57331
diff changeset
  1263
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1264
  \item[Implicit completion] works via regular keyboard input of the editor.
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1265
  It depends on further side-conditions:
57325
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1266
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1267
  \begin{enumerate}
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1268
57329
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
  1269
  \item The system option @{system_option_ref jedit_completion} needs to
57325
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1270
  be enabled (default).
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1271
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1272
  \item Completion of syntax keywords requires at least 3 relevant
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1273
  characters in the text.
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1274
57329
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
  1275
  \item The system option @{system_option_ref jedit_completion_delay}
57332
da630c4fd92b more on "Completion";
wenzelm
parents: 57331
diff changeset
  1276
  determines an additional delay (0.5 by default), before opening a completion
da630c4fd92b more on "Completion";
wenzelm
parents: 57331
diff changeset
  1277
  popup.  The delay gives the prover a chance to provide semantic completion
da630c4fd92b more on "Completion";
wenzelm
parents: 57331
diff changeset
  1278
  information, notably the context (\secref{sec:completion-context}).
57325
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1279
57329
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
  1280
  \item The system option @{system_option_ref jedit_completion_immediate}
57425
625a369b4f32 jedit_completion_immediate is enabled by default: let all users participate in slightly more ambitious symbol insertion;
wenzelm
parents: 57420
diff changeset
  1281
  (enabled by default) controls whether replacement text should be inserted
57332
da630c4fd92b more on "Completion";
wenzelm
parents: 57331
diff changeset
  1282
  immediately without popup, regardless of @{system_option
da630c4fd92b more on "Completion";
wenzelm
parents: 57331
diff changeset
  1283
  jedit_completion_delay}. This aggressive mode of completion is restricted to
da630c4fd92b more on "Completion";
wenzelm
parents: 57331
diff changeset
  1284
  Isabelle symbols and their abbreviations (\secref{sec:symbols}).
57325
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1285
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1286
  \item Completion of symbol abbreviations with only one relevant
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1287
  character in the text always enforces an explicit popup,
57332
da630c4fd92b more on "Completion";
wenzelm
parents: 57331
diff changeset
  1288
  regardless of @{system_option_ref jedit_completion_immediate}.
57325
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1289
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1290
  \end{enumerate}
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1291
57332
da630c4fd92b more on "Completion";
wenzelm
parents: 57331
diff changeset
  1292
  \end{description}
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1293
\<close>
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset