src/Doc/JEdit/JEdit.thy
author wenzelm
Tue, 06 Dec 2016 17:38:46 +0100
changeset 64549 964ac7439a52
parent 64515 29f0b8d2f952
child 64602 8edca3465758
permissions -rw-r--r--
notes on whitespace;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
61656
cfabbc083977 more uniform jEdit properties;
wenzelm
parents: 61574
diff changeset
     1
(*:maxLineLen=78:*)
53981
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>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    12
  Isabelle/jEdit is a Prover IDE that integrates \<^emph>\<open>parallel proof checking\<close>
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    13
  @{cite "Wenzel:2009" and "Wenzel:2013:ITP"} with \<^emph>\<open>asynchronous user
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    14
  interaction\<close> @{cite "Wenzel:2010" and "Wenzel:2012:UITP-EPTCS" and
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    15
  "Wenzel:2014:ITP-PIDE" and "Wenzel:2014:UITP"}, based on a document-oriented
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    16
  approach to \<^emph>\<open>continuous proof processing\<close> @{cite "Wenzel:2011:CICM" and
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    17
  "Wenzel:2012"}. Many concepts and system components are fit together in
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    18
  order to make this work. The main building blocks are as follows.
53769
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    19
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    20
    \<^descr>[Isabelle/ML] is the implementation and extension language of Isabelle,
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    21
    see also @{cite "isabelle-implementation"}. It is integrated into the
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    22
    logical context of Isabelle/Isar and allows to manipulate logical entities
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    23
    directly. Arbitrary add-on tools may be implemented for object-logics such
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    24
    as Isabelle/HOL.
53770
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    25
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    26
    \<^descr>[Isabelle/Scala] is the system programming language of Isabelle. It
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    27
    extends the pure logical environment of Isabelle/ML towards the outer
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    28
    world of graphical user interfaces, text editors, IDE frameworks, web
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    29
    services etc. Special infrastructure allows to transfer algebraic
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    30
    datatypes and formatted text easily between ML and Scala, using
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    31
    asynchronous protocol commands.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
    32
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    33
    \<^descr>[PIDE] is a general framework for Prover IDEs based on Isabelle/Scala. It
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    34
    is built around a concept of parallel and asynchronous document
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    35
    processing, which is supported natively by the parallel proof engine that
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    36
    is implemented in Isabelle/ML. The traditional prover command loop is
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    37
    given up; instead there is direct support for editing of source text, with
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    38
    rich formal markup for GUI rendering.
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    39
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
    40
    \<^descr>[jEdit] is a sophisticated text editor\<^footnote>\<open>\<^url>\<open>http://www.jedit.org\<close>\<close>
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
    41
    implemented in Java\<^footnote>\<open>\<^url>\<open>http://www.java.com\<close>\<close>. It is easily extensible by
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
    42
    plugins written in any language that works on the JVM. In the context of
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
    43
    Isabelle this is always Scala\<^footnote>\<open>\<^url>\<open>http://www.scala-lang.org\<close>\<close>.
53770
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    44
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    45
    \<^descr>[Isabelle/jEdit] is the main application of the PIDE framework and the
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    46
    default user-interface for Isabelle. It targets both beginners and
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    47
    experts. Technically, Isabelle/jEdit consists of the original jEdit code
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    48
    base with minimal patches and a special plugin for Isabelle. This is
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    49
    integrated as a desktop application for the main operating system
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    50
    families: Linux, Windows, Mac OS X.
53770
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    51
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    52
  End-users of Isabelle download and run a standalone application that exposes
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    53
  jEdit as a text editor on the surface. Thus there is occasionally a tendency
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    54
  to apply the name ``jEdit'' to any of the Isabelle Prover IDE aspects,
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    55
  without proper differentiation. When discussing these PIDE building blocks
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    56
  in public forums, mailing lists, or even scientific publications, it is
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    57
  particularly important to distinguish Isabelle/ML versus Standard ML,
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    58
  Isabelle/Scala versus Scala, Isabelle/jEdit versus jEdit.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
    59
\<close>
53770
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    60
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    61
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
    62
section \<open>The Isabelle/jEdit Prover IDE\<close>
53770
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
text \<open>
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    65
  \begin{figure}[!htb]
54331
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
    66
  \begin{center}
57312
afbc20986435 updated screenshots;
wenzelm
parents: 57311
diff changeset
    67
  \includegraphics[scale=0.333]{isabelle-jedit}
54331
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
    68
  \end{center}
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
    69
  \caption{The Isabelle/jEdit Prover IDE}
54357
157b6eee6a76 more screenshots;
wenzelm
parents: 54356
diff changeset
    70
  \label{fig:isabelle-jedit}
54331
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
    71
  \end{figure}
53773
36703fcea740 added canonical screenshot;
wenzelm
parents: 53771
diff changeset
    72
57337
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    73
  Isabelle/jEdit (\figref{fig:isabelle-jedit}) consists of some plugins for
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    74
  the jEdit text editor, while preserving its general look-and-feel as far as
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    75
  possible. The main plugin is called ``Isabelle'' and has its own menu
61477
e467ae7aa808 more control symbols;
wenzelm
parents: 61458
diff changeset
    76
  \<^emph>\<open>Plugins~/ Isabelle\<close> with access to several panels (see also
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    77
  \secref{sec:dockables}), as well as \<^emph>\<open>Plugins~/ Plugin Options~/ Isabelle\<close>
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    78
  (see also \secref{sec:options}).
53770
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
    79
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    80
  The options allow to specify a logic session name, but the same selector is
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    81
  also accessible in the \<^emph>\<open>Theories\<close> panel (\secref{sec:theories}). After
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    82
  application startup, the selected logic session image is provided
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    83
  automatically by the Isabelle build tool @{cite "isabelle-system"}: if it is
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    84
  absent or outdated wrt.\ its sources, the build process updates it while the
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    85
  text editor is running. Prover IDE functionality is only activated after
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    86
  successful termination of the build process. A failure may require changing
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    87
  some options and restart the application. Changing the logic session, or the
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    88
  underlying ML system platform (32\,bit versus 64\,bit) requires a restart of
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
    89
  the application to take effect.
53769
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
    90
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
    91
  \<^medskip>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    92
  The main job of the Prover IDE is to manage sources and their changes,
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    93
  taking the logical structure as a formal document into account (see also
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
    94
  \secref{sec:document-model}). The editor and the prover are connected
57337
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    95
  asynchronously in a lock-free manner. The prover is free to organize the
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    96
  checking of the formal text in parallel on multiple cores, and provides
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
    97
  feedback via markup, which is rendered in the editor via colors, boxes,
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
    98
  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
    99
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   100
  Using the mouse together with the modifier key \<^verbatim>\<open>CONTROL\<close> (Linux, Windows)
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   101
  or \<^verbatim>\<open>COMMAND\<close> (Mac OS X) exposes formal content via tooltips and/or
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   102
  hyperlinks (see also \secref{sec:tooltips-hyperlinks}). Output (in popups
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   103
  etc.) may be explored recursively, using the same techniques as in the
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   104
  editor source buffer.
53770
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
   105
57337
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
   106
  Thus the Prover IDE gives an impression of direct access to formal content
8b46b57008ea misc tuning;
wenzelm
parents: 57336
diff changeset
   107
  of the prover within the editor, but in reality only certain aspects are
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   108
  exposed, according to the possibilities of the prover and its add-on tools.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   109
\<close>
53769
036e80175bdd basic setup for Isabelle/jEdit documentation;
wenzelm
parents:
diff changeset
   110
53770
db362319d766 added/updated material from src/Tools/jEdit/README.html;
wenzelm
parents: 53769
diff changeset
   111
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   112
subsection \<open>Documentation\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   113
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   114
text \<open>
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   115
  The \<^emph>\<open>Documentation\<close> panel of Isabelle/jEdit provides access to some example
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   116
  theory files and the standard Isabelle documentation. PDF files are opened
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   117
  by regular desktop operations of the underlying platform. The section
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   118
  ``Original jEdit Documentation'' contains the original \<^emph>\<open>User's Guide\<close> of
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   119
  this sophisticated text editor. The same is accessible via the \<^verbatim>\<open>Help\<close> menu
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   120
  or \<^verbatim>\<open>F1\<close> keyboard shortcut, using the built-in HTML viewer of Java/Swing.
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   121
  The latter also includes \<^emph>\<open>Frequently Asked Questions\<close> and documentation of
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   122
  individual plugins.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   123
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   124
  Most of the information about jEdit is relevant for Isabelle/jEdit as well,
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   125
  but one needs to keep in mind that defaults sometimes differ, and the
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   126
  official jEdit documentation does not know about the Isabelle plugin with
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   127
  its support for continuous checking of formal source text: jEdit is a plain
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   128
  text editor, but Isabelle/jEdit is a Prover IDE.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   129
\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   130
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   131
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   132
subsection \<open>Plugins\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   133
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   134
text \<open>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   135
  The \<^emph>\<open>Plugin Manager\<close> of jEdit allows to augment editor functionality by JVM
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   136
  modules (jars) that are provided by the central plugin repository, which is
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   137
  accessible via various mirror sites.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   138
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   139
  Connecting to the plugin server-infrastructure of the jEdit project allows
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   140
  to update bundled plugins or to add further functionality. This needs to be
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   141
  done with the usual care for such an open bazaar of contributions. Arbitrary
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   142
  combinations of add-on features are apt to cause problems. It is advisable
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   143
  to start with the default configuration of Isabelle/jEdit and develop some
64513
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   144
  sense how it is meant to work, before loading too many other plugins.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   145
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   146
  \<^medskip>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   147
  The main \<^emph>\<open>Isabelle\<close> plugin is an integral part of Isabelle/jEdit and needs
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   148
  to remain active at all times! A few additional plugins are bundled with
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   149
  Isabelle/jEdit for convenience or out of necessity, notably \<^emph>\<open>Console\<close> with
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   150
  its Isabelle/Scala sub-plugin (\secref{sec:scala-console}) and \<^emph>\<open>SideKick\<close>
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   151
  with some Isabelle-specific parsers for document tree structure
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   152
  (\secref{sec:sidekick}). The \<^emph>\<open>Navigator\<close> plugin is particularly important
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   153
  for hyperlinks within the formal document-model
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   154
  (\secref{sec:tooltips-hyperlinks}). Further plugins (e.g.\ \<^emph>\<open>ErrorList\<close>,
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   155
  \<^emph>\<open>Code2HTML\<close>) are included to saturate the dependencies of bundled plugins,
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   156
  but have no particular use in Isabelle/jEdit.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   157
\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   158
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   159
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   160
subsection \<open>Options \label{sec:options}\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   161
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   162
text \<open>
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   163
  Both jEdit and Isabelle have distinctive management of persistent options.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   164
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   165
  Regular jEdit options are accessible via the dialogs \<^emph>\<open>Utilities~/ Global
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   166
  Options\<close> or \<^emph>\<open>Plugins~/ Plugin Options\<close>, with a second chance to flip the
63669
256fc20716f2 clarified antiquotations;
wenzelm
parents: 62969
diff changeset
   167
  two within the central options dialog. Changes are stored in @{path
63749
4fe8cfaeb1fc clarified important directories;
wenzelm
parents: 63680
diff changeset
   168
  "$JEDIT_SETTINGS/properties"} and @{path "$JEDIT_SETTINGS/keymaps"}.
57310
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
63669
256fc20716f2 clarified antiquotations;
wenzelm
parents: 62969
diff changeset
   171
  in @{path "$ISABELLE_HOME_USER/etc/preferences"}, independently of
60270
wenzelm
parents: 60264
diff changeset
   172
  other jEdit properties. See also @{cite "isabelle-system"}, 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
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   176
  Those Isabelle options that are declared as \<^verbatim>\<open>public\<close> are configurable in
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   177
  Isabelle/jEdit via \<^emph>\<open>Plugin Options~/ Isabelle~/ General\<close>. Moreover, there
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   178
  are various options for rendering of document content, which are
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   179
  configurable via \<^emph>\<open>Plugin Options~/ Isabelle~/ Rendering\<close>. Thus \<^emph>\<open>Plugin
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   180
  Options~/ Isabelle\<close> in jEdit provides a view on a subset of Isabelle system
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   181
  options. Note that some of these options affect general parameters that are
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   182
  relevant outside Isabelle/jEdit as well, e.g.\ @{system_option threads} or
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   183
  @{system_option parallel_proofs} for the Isabelle build tool @{cite
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   184
  "isabelle-system"}, but it is possible to use the settings variable
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   185
  @{setting ISABELLE_BUILD_OPTIONS} to change defaults for batch builds
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   186
  without affecting the Prover IDE.
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
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   191
  \<^medskip>
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   192
  Options are usually loaded on startup and saved on shutdown of
63669
256fc20716f2 clarified antiquotations;
wenzelm
parents: 62969
diff changeset
   193
  Isabelle/jEdit. Editing the machine-generated @{path
63749
4fe8cfaeb1fc clarified important directories;
wenzelm
parents: 63680
diff changeset
   194
  "$JEDIT_SETTINGS/properties"} or @{path
57310
da107539996f misc tuning and updates;
wenzelm
parents: 56466
diff changeset
   195
  "$ISABELLE_HOME_USER/etc/preferences"} manually while the application is
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   196
  running is likely to cause surprise due to lost update!
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   197
\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   198
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   199
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   200
subsection \<open>Keymaps\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   201
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   202
text \<open>
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   203
  Keyboard shortcuts are managed as a separate concept of \<^emph>\<open>keymap\<close> that is
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   204
  configurable via \<^emph>\<open>Global Options~/ Shortcuts\<close>. The \<^verbatim>\<open>imported\<close> keymap is
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   205
  derived from the initial environment of properties that is available at the
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   206
  first start of the editor; afterwards the keymap file takes precedence and
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   207
  is no longer affected by change of default properties.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   208
64513
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   209
  Users may change their keymap later, but need to keep its content @{path
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   210
  "$JEDIT_SETTINGS/keymaps"} in sync with \<^verbatim>\<open>shortcut\<close> properties in
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   211
  \<^file>\<open>$JEDIT_HOME/src/jEdit.props\<close>.
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   212
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   213
  \<^medskip>
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   214
  The action @{action_def "isabelle.keymap-merge"} helps to resolve pending
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   215
  Isabelle keymap changes that are in conflict with the current jEdit keymap;
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   216
  non-conflicting changes are always applied implicitly. This action is
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   217
  automatically invoked on Isabelle/jEdit startup.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   218
\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   219
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   220
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   221
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
   222
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   223
text \<open>
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   224
  Isabelle/jEdit is normally invoked as a single-instance desktop application,
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   225
  based on platform-specific executables for Linux, Windows, Mac OS X.
62014
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   226
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   227
  It is also possible to invoke the Prover IDE on the command-line, with some
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   228
  extra options and environment settings. The command-line usage of @{tool_def
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   229
  jedit} is as follows:
61408
9020a3ba6c9a @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61199
diff changeset
   230
  @{verbatim [display]
9020a3ba6c9a @{verbatim [display]} supersedes old alltt/ttbox;
wenzelm
parents: 61199
diff changeset
   231
\<open>Usage: isabelle jedit [OPTIONS] [FILES ...]
57320
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   232
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   233
  Options are:
62039
a77f4a9037d4 clarified isabelle jedit command-line;
wenzelm
parents: 62036
diff changeset
   234
    -D NAME=X    set JVM system property
61132
70029aae9a9f clarified JEDIT_JAVA_SYSTEM_OPTIONS;
wenzelm
parents: 60296
diff changeset
   235
    -J OPTION    add JVM runtime option
57320
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   236
    -b           build only
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   237
    -d DIR       include session directory
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   238
    -f           fresh build
61132
70029aae9a9f clarified JEDIT_JAVA_SYSTEM_OPTIONS;
wenzelm
parents: 60296
diff changeset
   239
    -j OPTION    add jEdit runtime option
70029aae9a9f clarified JEDIT_JAVA_SYSTEM_OPTIONS;
wenzelm
parents: 60296
diff changeset
   240
    -l NAME      logic image name
57320
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   241
    -m MODE      add print mode for output
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   242
    -n           no build of session image on startup
63987
ac96fe9224f6 just one option is enough -- "isabelle jedit" java process may be prefixed directly in the shell;
wenzelm
parents: 63871
diff changeset
   243
    -p CMD       ML process command prefix (process policy)
57320
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   244
    -s           system build mode for session image
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   245
61512
933463440449 more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents: 61506
diff changeset
   246
  Start jEdit with Isabelle plugin setup and open FILES
933463440449 more uniform command-line for "isabelle jedit" and the isabelle.Main app wrapper;
wenzelm
parents: 61506
diff changeset
   247
  (default "$USER_HOME/Scratch.thy" or ":" for empty buffer).\<close>}
57320
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   248
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   249
  The \<^verbatim>\<open>-l\<close> option specifies the session name of the logic image to be used
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   250
  for proof processing. Additional session root directories may be included
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   251
  via option \<^verbatim>\<open>-d\<close> to augment that name space of @{tool build} @{cite
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   252
  "isabelle-system"}.
57320
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   253
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   254
  By default, the specified image is checked and built on demand. The \<^verbatim>\<open>-s\<close>
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   255
  option determines where to store the result session image of @{tool build}.
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   256
  The \<^verbatim>\<open>-n\<close> option bypasses the implicit build process for the selected
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   257
  session image.
57320
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   258
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   259
  The \<^verbatim>\<open>-m\<close> option specifies additional print modes for the prover process.
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   260
  Note that the system option @{system_option_ref jedit_print_mode} allows to
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   261
  do the same persistently (e.g.\ via the \<^emph>\<open>Plugin Options\<close> dialog of
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   262
  Isabelle/jEdit), without requiring command-line invocation.
57320
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   263
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   264
  The \<^verbatim>\<open>-J\<close> and \<^verbatim>\<open>-j\<close> options allow to pass additional low-level options to
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   265
  the JVM or jEdit, respectively. The defaults are provided by the Isabelle
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   266
  settings environment @{cite "isabelle-system"}, but note that these only
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   267
  work for the command-line tool described here, and not the regular
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   268
  application.
57320
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   269
62039
a77f4a9037d4 clarified isabelle jedit command-line;
wenzelm
parents: 62036
diff changeset
   270
  The \<^verbatim>\<open>-D\<close> option allows to define JVM system properties; this is passed
a77f4a9037d4 clarified isabelle jedit command-line;
wenzelm
parents: 62036
diff changeset
   271
  directly to the underlying \<^verbatim>\<open>java\<close> process.
a77f4a9037d4 clarified isabelle jedit command-line;
wenzelm
parents: 62036
diff changeset
   272
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   273
  The \<^verbatim>\<open>-b\<close> and \<^verbatim>\<open>-f\<close> options control the self-build mechanism of
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   274
  Isabelle/jEdit. This is only relevant for building from sources, which also
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   275
  requires an auxiliary \<^verbatim>\<open>jedit_build\<close> component from
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   276
  \<^url>\<open>http://isabelle.in.tum.de/components\<close>. The official Isabelle release
62014
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   277
  already includes a pre-built version of Isabelle/jEdit.
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   278
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   279
  \<^bigskip>
62014
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   280
  It is also possible to connect to an already running Isabelle/jEdit process
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   281
  via @{tool_def jedit_client}:
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   282
  @{verbatim [display]
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   283
\<open>Usage: isabelle jedit_client [OPTIONS] [FILES ...]
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   284
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   285
  Options are:
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   286
    -c           only check presence of server
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   287
    -n           only report server name
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   288
    -s NAME      server name (default Isabelle)
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   289
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   290
  Connect to already running Isabelle/jEdit instance and open FILES\<close>}
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   291
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   292
  The \<^verbatim>\<open>-c\<close> option merely checks the presence of the server, producing a
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   293
  process return code accordingly.
62014
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   294
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   295
  The \<^verbatim>\<open>-n\<close> option reports the server name, and the \<^verbatim>\<open>-s\<close> option provides a
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   296
  different server name. The default server name is the official distribution
64513
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   297
  name (e.g.\ \<^verbatim>\<open>Isabelle2016-1\<close>). Thus @{tool jedit_client} can connect to the
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   298
  Isabelle desktop application without further options.
62014
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   299
63987
ac96fe9224f6 just one option is enough -- "isabelle jedit" java process may be prefixed directly in the shell;
wenzelm
parents: 63871
diff changeset
   300
  The \<^verbatim>\<open>-p\<close> option allows to override the implicit default of the system
ac96fe9224f6 just one option is enough -- "isabelle jedit" java process may be prefixed directly in the shell;
wenzelm
parents: 63871
diff changeset
   301
  option @{system_option_ref ML_process_policy} for ML processes started by
ac96fe9224f6 just one option is enough -- "isabelle jedit" java process may be prefixed directly in the shell;
wenzelm
parents: 63871
diff changeset
   302
  the Prover IDE, e.g. to control CPU affinity on multiprocessor systems.
ac96fe9224f6 just one option is enough -- "isabelle jedit" java process may be prefixed directly in the shell;
wenzelm
parents: 63871
diff changeset
   303
62036
773cb226738c provide server name uniformly on all platforms;
wenzelm
parents: 62014
diff changeset
   304
  The JVM system property \<^verbatim>\<open>isabelle.jedit_server\<close> provides a different server
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   305
  name, e.g.\ use \<^verbatim>\<open>isabelle jedit -Disabelle.jedit_server=\<close>\<open>name\<close> and
62036
773cb226738c provide server name uniformly on all platforms;
wenzelm
parents: 62014
diff changeset
   306
  \<^verbatim>\<open>isabelle jedit_client -s\<close>~\<open>name\<close> to connect later on.
62014
446fcbadc6bf documentation for "isabelle jedit_client";
wenzelm
parents: 61960
diff changeset
   307
\<close>
57320
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   308
00f2c8d1aa0b more on command-line invocation -- moved material from system manual;
wenzelm
parents: 57319
diff changeset
   309
60291
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   310
section \<open>GUI rendering\<close>
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   311
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   312
subsection \<open>Look-and-feel \label{sec:look-and-feel}\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   313
60291
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   314
text \<open>
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   315
  jEdit is a Java/AWT/Swing application with some ambition to support
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   316
  ``native'' look-and-feel on all platforms, within the limits of what Oracle
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   317
  as Java provider and major operating system distributors allow (see also
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   318
  \secref{sec:problems}).
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   319
54329
e0fa4bd16c80 misc tuning;
wenzelm
parents: 54323
diff changeset
   320
  Isabelle/jEdit enables platform-specific look-and-feel by default as
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   321
  follows.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   322
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   323
    \<^descr>[Linux:] The platform-independent \<^emph>\<open>Metal\<close> is used by default.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   324
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   325
    The Linux-specific \<^emph>\<open>GTK+\<close> also works under the side-condition that the
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   326
    overall GTK theme and options are selected in a way that works with Java
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   327
    AWT/Swing. The JVM has no direct influence of GTK rendering.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   328
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   329
    \<^descr>[Windows:] Regular \<^emph>\<open>Windows\<close> is used by default.
54372
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
   330
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   331
    \<^descr>[Mac OS X:] Regular \<^emph>\<open>Mac OS X\<close> is used by default.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   332
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   333
    The bundled \<^emph>\<open>MacOSX\<close> plugin provides various functions that are expected
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   334
    from applications on that particular platform: quit from menu or dock,
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   335
    preferences menu, drag-and-drop of text files on the application,
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   336
    full-screen mode for main editor windows. It is advisable to have the
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   337
    \<^emph>\<open>MacOSX\<close> plugin enabled all the time on that platform.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   338
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   339
  Users may experiment with different Swing look-and-feels, but need to keep
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   340
  in mind that this extra variance of GUI functionality is unlikely to work in
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   341
  arbitrary combinations. The platform-independent \<^emph>\<open>Metal\<close> and \<^emph>\<open>Nimbus\<close>
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   342
  should always work on all platforms, although they are technically and
62212
8addfff5965a clarified -- this is available on Mac OS X, too;
wenzelm
parents: 62185
diff changeset
   343
  stylistically outdated. The historic \<^emph>\<open>CDE/Motif\<close> should be ignored.
54372
2d61935eed4a misc tuning;
wenzelm
parents: 54362
diff changeset
   344
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   345
  After changing the look-and-feel in \<^emph>\<open>Global Options~/ Appearance\<close>,
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   346
  Isabelle/jEdit should be restarted to take full effect.
60291
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   347
\<close>
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   348
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   349
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   350
subsection \<open>Displays with very high resolution \label{sec:hdpi}\<close>
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   351
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   352
text \<open>
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   353
  In distant past, displays with $1024 \times 768$ or $1280 \times 1024$
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   354
  pixels were considered ``high resolution'' and bitmap fonts with 12 or 14
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   355
  pixels as adequate for text rendering. In 2016, we routinely see much higher
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   356
  resolutions, e.g. ``Full HD'' at $1920 \times 1080$ pixels or ``Ultra HD'' /
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   357
  ``4K'' at $3840 \times 2160$.
60291
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   358
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   359
  GUI frameworks are usually lagging behind, with hard-wired icon sizes and
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   360
  tiny fonts. Java and jEdit do provide reasonable support for very high
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   361
  resolution, but this requires manual adjustments as described below.
60291
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   362
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   363
  \<^medskip>
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   364
  The \<^bold>\<open>operating-system\<close> usually provides some configuration for global
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   365
  scaling of text fonts, e.g.\ $120\%$--$250\%$ on Windows. This impacts
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   366
  regular GUI elements, when used with native look-and-feel: Linux \<^emph>\<open>GTK+\<close>,
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   367
  \<^emph>\<open>Windows\<close>, \<^emph>\<open>Mac OS X\<close>, respectively. Alternatively, it is possible to use
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   368
  the platform-independent \<^emph>\<open>Metal\<close> look-and-feel and readjust its main font
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   369
  sizes via jEdit options explained below. The Isabelle/jEdit \<^bold>\<open>application\<close>
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   370
  provides further options to adjust font sizes in particular GUI elements.
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   371
  Here is a summary of all relevant font properties:
60291
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   372
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   373
    \<^item> \<^emph>\<open>Global Options / Text Area / Text font\<close>: the main text area font,
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   374
    which is also used as reference point for various derived font sizes,
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   375
    e.g.\ the \<^emph>\<open>Output\<close> (\secref{sec:output}) and \<^emph>\<open>State\<close>
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   376
    (\secref{sec:state-output}) panels.
60291
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   377
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   378
    \<^item> \<^emph>\<open>Global Options / Gutter / Gutter font\<close>: the font for the gutter area
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   379
    left of the main text area, e.g.\ relevant for display of line numbers
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   380
    (disabled by default).
60291
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   381
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   382
    \<^item> \<^emph>\<open>Global Options / Appearance / Button, menu and label font\<close> as well as
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   383
    \<^emph>\<open>List and text field font\<close>: this specifies the primary and secondary font
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   384
    for the \<^emph>\<open>Metal\<close> look-and-feel (\secref{sec:look-and-feel}).
60291
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   385
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   386
    \<^item> \<^emph>\<open>Plugin Options / Isabelle / General / Reset Font Size\<close>: the main text
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   387
    area font size for action @{action_ref "isabelle.reset-font-size"}, e.g.\
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   388
    relevant for quick scaling like in common web browsers.
60291
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   389
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   390
    \<^item> \<^emph>\<open>Plugin Options / Console / General / Font\<close>: the console window font,
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   391
    e.g.\ relevant for Isabelle/Scala command-line.
60291
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   392
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   393
  In \figref{fig:isabelle-jedit-hdpi} the \<^emph>\<open>Metal\<close> look-and-feel is configured
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   394
  with custom fonts at 30 pixels, and the main text area and console at 36
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   395
  pixels. This leads to decent rendering quality, despite the old-fashioned
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   396
  appearance of \<^emph>\<open>Metal\<close>.
60291
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   397
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   398
  \begin{figure}[!htb]
60291
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   399
  \begin{center}
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   400
  \includegraphics[width=\textwidth]{isabelle-jedit-hdpi}
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   401
  \end{center}
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   402
  \caption{Metal look-and-feel with custom fonts for very high resolution}
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   403
  \label{fig:isabelle-jedit-hdpi}
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   404
  \end{figure}
4335ee20014e more on displays with very high resolution;
wenzelm
parents: 60270
diff changeset
   405
\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   406
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   407
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   408
chapter \<open>Augmented jEdit functionality\<close>
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   409
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   410
section \<open>Dockable windows \label{sec:dockables}\<close>
57316
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   411
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   412
text \<open>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   413
  In jEdit terminology, a \<^emph>\<open>view\<close> is an editor window with one or more \<^emph>\<open>text
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   414
  areas\<close> that show the content of one or more \<^emph>\<open>buffers\<close>. A regular view may
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   415
  be surrounded by \<^emph>\<open>dockable windows\<close> that show additional information in
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   416
  arbitrary format, not just text; a \<^emph>\<open>plain view\<close> does not allow dockables.
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   417
  The \<^emph>\<open>dockable window manager\<close> of jEdit organizes these dockable windows,
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   418
  either as \<^emph>\<open>floating\<close> windows, or \<^emph>\<open>docked\<close> panels within one of the four
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   419
  margins of the view. There may be any number of floating instances of some
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   420
  dockable window, but at most one docked instance; jEdit actions that address
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   421
  \<^emph>\<open>the\<close> dockable window of a particular kind refer to the unique docked
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   422
  instance.
57316
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   423
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   424
  Dockables are used routinely in jEdit for important functionality like
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   425
  \<^emph>\<open>HyperSearch Results\<close> or the \<^emph>\<open>File System Browser\<close>. Plugins often provide
62184
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   426
  a central dockable to access their main functionality, which may be opened
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   427
  by the user on demand. The Isabelle/jEdit plugin takes this approach to the
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   428
  extreme: its plugin menu provides the entry-points to many panels that are
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   429
  managed as dockable windows. Some important panels are docked by default,
62184
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   430
  e.g.\ \<^emph>\<open>Documentation\<close>, \<^emph>\<open>State\<close>, \<^emph>\<open>Theories\<close> \<^emph>\<open>Output\<close>, \<^emph>\<open>Query\<close>. The user
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   431
  can change this arrangement easily and persistently.
57316
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   432
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   433
  Compared to plain jEdit, dockable window management in Isabelle/jEdit is
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   434
  slightly augmented according to the the following principles:
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   435
61477
e467ae7aa808 more control symbols;
wenzelm
parents: 61458
diff changeset
   436
  \<^item> Floating windows are dependent on the main window as \<^emph>\<open>dialog\<close> in
57316
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   437
  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
   438
  which is particularly important in full-screen mode. The desktop environment
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   439
  of the underlying platform may impose further policies on such dependent
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   440
  dialogs, in contrast to fully independent windows, e.g.\ some window
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   441
  management functions may be missing.
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   442
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   443
  \<^item> Keyboard focus of the main view vs.\ a dockable window is carefully
57316
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   444
  managed according to the intended semantics, as a panel mainly for output or
62184
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   445
  input. For example, activating the \<^emph>\<open>Output\<close> (\secref{sec:output}) or State
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   446
  (\secref{sec:state-output}) panel via the dockable window manager returns
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   447
  keyboard focus to the main text area, but for \<^emph>\<open>Query\<close> (\secref{sec:query})
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   448
  or \<^emph>\<open>Sledgehammer\<close> \secref{sec:sledgehammer} the focus is given to the main
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   449
  input field of that panel.
57316
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   450
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   451
  \<^item> Panels that provide their own text area for output have an additional
61477
e467ae7aa808 more control symbols;
wenzelm
parents: 61458
diff changeset
   452
  dockable menu item \<^emph>\<open>Detach\<close>. This produces an independent copy of the
e467ae7aa808 more control symbols;
wenzelm
parents: 61458
diff changeset
   453
  current output as a floating \<^emph>\<open>Info\<close> window, which displays that content
57316
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   454
  independently of ongoing changes of the PIDE document-model. Note that
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   455
  Isabelle/jEdit popup windows (\secref{sec:tooltips-hyperlinks}) provide a
61477
e467ae7aa808 more control symbols;
wenzelm
parents: 61458
diff changeset
   456
  similar \<^emph>\<open>Detach\<close> operation as an icon.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   457
\<close>
57316
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   458
134d3b6c135e more on dockable windows;
wenzelm
parents: 57315
diff changeset
   459
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   460
section \<open>Isabelle symbols \label{sec:symbols}\<close>
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   461
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   462
text \<open>
61477
e467ae7aa808 more control symbols;
wenzelm
parents: 61458
diff changeset
   463
  Isabelle sources consist of \<^emph>\<open>symbols\<close> that extend plain ASCII to allow
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   464
  infinitely many mathematical symbols within the formal sources. This works
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   465
  without depending on particular encodings and varying Unicode
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   466
  standards.\<^footnote>\<open>Raw Unicode characters within formal sources would compromise
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   467
  portability and reliability in the face of changing interpretation of
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   468
  special features of Unicode, such as Combining Characters or Bi-directional
62184
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   469
  Text.\<close> See @{cite "Wenzel:2011:CICM"}.
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   470
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   471
  For the prover back-end, formal text consists of ASCII characters that are
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   472
  grouped according to some simple rules, e.g.\ as plain ``\<^verbatim>\<open>a\<close>'' or symbolic
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   473
  ``\<^verbatim>\<open>\<alpha>\<close>''. For the editor front-end, a certain subset of symbols is rendered
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   474
  physically via Unicode glyphs, in order to show ``\<^verbatim>\<open>\<alpha>\<close>'' as ``\<open>\<alpha>\<close>'', for
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   475
  example. This symbol interpretation is specified by the Isabelle system
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   476
  distribution in \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> and may be augmented by the
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   477
  user in @{path "$ISABELLE_HOME_USER/etc/symbols"}.
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   478
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   479
  The appendix of @{cite "isabelle-isar-ref"} gives an overview of the
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   480
  standard interpretation of finitely many symbols from the infinite
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   481
  collection. Uninterpreted symbols are displayed literally, e.g.\
61503
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   482
  ``\<^verbatim>\<open>\<foobar>\<close>''. Overlap of Unicode characters used in symbol
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   483
  interpretation with informal ones (which might appear e.g.\ in comments)
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   484
  needs to be avoided. Raw Unicode characters within prover source files
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   485
  should be restricted to informal parts, e.g.\ to write text in non-latin
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   486
  alphabets in comments.
61506
wenzelm
parents: 61504
diff changeset
   487
\<close>
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   488
61506
wenzelm
parents: 61504
diff changeset
   489
paragraph \<open>Encoding.\<close>
62184
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   490
text \<open>Technically, the Unicode interpretation of Isabelle symbols is an
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   491
  \<^emph>\<open>encoding\<close> called \<^verbatim>\<open>UTF-8-Isabelle\<close> in jEdit (\<^emph>\<open>not\<close> in the underlying
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   492
  JVM). It is provided by the Isabelle/jEdit plugin and enabled by default for
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   493
  all source files. Sometimes such defaults are reset accidentally, or
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   494
  malformed UTF-8 sequences in the text force jEdit to fall back on a
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   495
  different encoding like \<^verbatim>\<open>ISO-8859-15\<close>. In that case, verbatim ``\<^verbatim>\<open>\<alpha>\<close>'' will
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   496
  be shown in the text buffer instead of its Unicode rendering ``\<open>\<alpha>\<close>''. The
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   497
  jEdit menu operation \<^emph>\<open>File~/ Reload with Encoding~/ UTF-8-Isabelle\<close> helps
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   498
  to resolve such problems (after repairing malformed parts of the text). \<close>
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   499
61506
wenzelm
parents: 61504
diff changeset
   500
paragraph \<open>Font.\<close>
wenzelm
parents: 61504
diff changeset
   501
text \<open>Correct rendering via Unicode requires a font that contains glyphs for
62184
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   502
  the corresponding codepoints. There are also various unusual symbols with
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   503
  particular purpose in Isabelle, e.g.\ control symbols and very long arrows.
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   504
  Isabelle/jEdit prefers its own application fonts \<^verbatim>\<open>IsabelleText\<close>, which
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   505
  ensures that standard collection of Isabelle symbols is actually shown on
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   506
  the screen (or printer) as expected.
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   507
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   508
  Note that a Java/AWT/Swing application can load additional fonts only if
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   509
  they are not installed on the operating system already! Some outdated
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   510
  version of \<^verbatim>\<open>IsabelleText\<close> that happens to be provided by the operating
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   511
  system would prevent Isabelle/jEdit to use its bundled version. This could
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   512
  lead to missing glyphs (black rectangles), when the system version of
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   513
  \<^verbatim>\<open>IsabelleText\<close> is older than the application version. This problem can be
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   514
  avoided by refraining to ``install'' any version of \<^verbatim>\<open>IsabelleText\<close> in the
62184
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   515
  first place, although it might be tempting to use the same font in other
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   516
  applications.
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   517
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   518
  HTML pages generated by Isabelle refer to the same \<^verbatim>\<open>IsabelleText\<close> font as a
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   519
  server-side resource. Thus a web-browser can use that without requiring a
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   520
  locally installed copy.
61506
wenzelm
parents: 61504
diff changeset
   521
\<close>
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   522
61506
wenzelm
parents: 61504
diff changeset
   523
paragraph \<open>Input methods.\<close>
wenzelm
parents: 61504
diff changeset
   524
text \<open>In principle, Isabelle/jEdit could delegate the problem to produce
wenzelm
parents: 61504
diff changeset
   525
  Isabelle symbols in their Unicode rendering to the underlying operating
wenzelm
parents: 61504
diff changeset
   526
  system and its \<^emph>\<open>input methods\<close>. Regular jEdit also provides various ways to
wenzelm
parents: 61504
diff changeset
   527
  work with \<^emph>\<open>abbreviations\<close> to produce certain non-ASCII characters. Since
wenzelm
parents: 61504
diff changeset
   528
  none of these standard input methods work satisfactorily for the
wenzelm
parents: 61504
diff changeset
   529
  mathematical characters required for Isabelle, various specific
wenzelm
parents: 61504
diff changeset
   530
  Isabelle/jEdit mechanisms are provided.
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   531
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   532
  This is a summary for practically relevant input methods for Isabelle
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   533
  symbols.
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   534
61504
wenzelm
parents: 61503
diff changeset
   535
  \<^enum> The \<^emph>\<open>Symbols\<close> panel: some GUI buttons allow to insert certain symbols in
wenzelm
parents: 61503
diff changeset
   536
  the text buffer. There are also tooltips to reveal the official Isabelle
wenzelm
parents: 61503
diff changeset
   537
  representation with some additional information about \<^emph>\<open>symbol
wenzelm
parents: 61503
diff changeset
   538
  abbreviations\<close> (see below).
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   539
61504
wenzelm
parents: 61503
diff changeset
   540
  \<^enum> Copy/paste from decoded source files: text that is rendered as Unicode
wenzelm
parents: 61503
diff changeset
   541
  already can be re-used to produce further text. This also works between
wenzelm
parents: 61503
diff changeset
   542
  different applications, e.g.\ Isabelle/jEdit and some web browser or mail
62184
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   543
  client, as long as the same Unicode interpretation of Isabelle symbols is
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   544
  used.
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   545
61504
wenzelm
parents: 61503
diff changeset
   546
  \<^enum> Copy/paste from prover output within Isabelle/jEdit. The same principles
wenzelm
parents: 61503
diff changeset
   547
  as for text buffers apply, but note that \<^emph>\<open>copy\<close> in secondary Isabelle/jEdit
wenzelm
parents: 61503
diff changeset
   548
  windows works via the keyboard shortcuts \<^verbatim>\<open>C+c\<close> or \<^verbatim>\<open>C+INSERT\<close>, while jEdit
wenzelm
parents: 61503
diff changeset
   549
  menu actions always refer to the primary text area!
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   550
62184
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   551
  \<^enum> Completion provided by the Isabelle plugin (see \secref{sec:completion}).
61504
wenzelm
parents: 61503
diff changeset
   552
  Isabelle symbols have a canonical name and optional abbreviations. This can
wenzelm
parents: 61503
diff changeset
   553
  be used with the text completion mechanism of Isabelle/jEdit, to replace a
wenzelm
parents: 61503
diff changeset
   554
  prefix of the actual symbol like \<^verbatim>\<open>\<lambda>\<close>, or its name preceded by backslash
wenzelm
parents: 61503
diff changeset
   555
  \<^verbatim>\<open>\lambda\<close>, or its ASCII abbreviation \<^verbatim>\<open>%\<close> by the Unicode rendering.
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   556
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   557
  The following table is an extract of the information provided by the
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   558
  standard \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> file:
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   559
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   560
  \<^medskip>
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   561
  \begin{tabular}{lll}
61477
e467ae7aa808 more control symbols;
wenzelm
parents: 61458
diff changeset
   562
    \<^bold>\<open>symbol\<close> & \<^bold>\<open>name with backslash\<close> & \<^bold>\<open>abbreviation\<close> \\\hline
61503
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   563
    \<open>\<lambda>\<close> & \<^verbatim>\<open>\lambda\<close> & \<^verbatim>\<open>%\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   564
    \<open>\<Rightarrow>\<close> & \<^verbatim>\<open>\Rightarrow\<close> & \<^verbatim>\<open>=>\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   565
    \<open>\<Longrightarrow>\<close> & \<^verbatim>\<open>\Longrightarrow\<close> & \<^verbatim>\<open>==>\<close> \\[0.5ex]
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   566
    \<open>\<And>\<close> & \<^verbatim>\<open>\And\<close> & \<^verbatim>\<open>!!\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   567
    \<open>\<equiv>\<close> & \<^verbatim>\<open>\equiv\<close> & \<^verbatim>\<open>==\<close> \\[0.5ex]
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   568
    \<open>\<forall>\<close> & \<^verbatim>\<open>\forall\<close> & \<^verbatim>\<open>!\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   569
    \<open>\<exists>\<close> & \<^verbatim>\<open>\exists\<close> & \<^verbatim>\<open>?\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   570
    \<open>\<longrightarrow>\<close> & \<^verbatim>\<open>\longrightarrow\<close> & \<^verbatim>\<open>-->\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   571
    \<open>\<and>\<close> & \<^verbatim>\<open>\and\<close> & \<^verbatim>\<open>&\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   572
    \<open>\<or>\<close> & \<^verbatim>\<open>\or\<close> & \<^verbatim>\<open>|\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   573
    \<open>\<not>\<close> & \<^verbatim>\<open>\not\<close> & \<^verbatim>\<open>~\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   574
    \<open>\<noteq>\<close> & \<^verbatim>\<open>\noteq\<close> & \<^verbatim>\<open>~=\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   575
    \<open>\<in>\<close> & \<^verbatim>\<open>\in\<close> & \<^verbatim>\<open>:\<close> \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   576
    \<open>\<notin>\<close> & \<^verbatim>\<open>\notin\<close> & \<^verbatim>\<open>~:\<close> \\
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   577
  \end{tabular}
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   578
  \<^medskip>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   579
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   580
  Note that the above abbreviations refer to the input method. The logical
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   581
  notation provides ASCII alternatives that often coincide, but sometimes
62184
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   582
  deviate. This occasionally causes user confusion with old-fashioned Isabelle
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   583
  source that use ASCII replacement notation like \<^verbatim>\<open>!\<close> or \<^verbatim>\<open>ALL\<close> directly in
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   584
  the text.
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   585
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   586
  On the other hand, coincidence of symbol abbreviations with ASCII
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   587
  replacement syntax syntax helps to update old theory sources via explicit
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   588
  completion (see also \<^verbatim>\<open>C+b\<close> explained in \secref{sec:completion}).
61506
wenzelm
parents: 61504
diff changeset
   589
\<close>
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   590
61506
wenzelm
parents: 61504
diff changeset
   591
paragraph \<open>Control symbols.\<close>
wenzelm
parents: 61504
diff changeset
   592
text \<open>There are some special control symbols to modify the display style of a
wenzelm
parents: 61504
diff changeset
   593
  single symbol (without nesting). Control symbols may be applied to a region
wenzelm
parents: 61504
diff changeset
   594
  of selected text, either using the \<^emph>\<open>Symbols\<close> panel or keyboard shortcuts or
wenzelm
parents: 61504
diff changeset
   595
  jEdit actions. These editor operations produce a separate control symbol for
wenzelm
parents: 61504
diff changeset
   596
  each symbol in the text, in order to make the whole text appear in a certain
wenzelm
parents: 61504
diff changeset
   597
  style.
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   598
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   599
  \<^medskip>
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   600
  \begin{tabular}{llll}
61477
e467ae7aa808 more control symbols;
wenzelm
parents: 61458
diff changeset
   601
    \<^bold>\<open>style\<close> & \<^bold>\<open>symbol\<close> & \<^bold>\<open>shortcut\<close> & \<^bold>\<open>action\<close> \\\hline
61503
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   602
    superscript & \<^verbatim>\<open>\<^sup>\<close> & \<^verbatim>\<open>C+e UP\<close> & @{action_ref "isabelle.control-sup"} \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   603
    subscript & \<^verbatim>\<open>\<^sub>\<close> & \<^verbatim>\<open>C+e DOWN\<close> & @{action_ref "isabelle.control-sub"} \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   604
    bold face & \<^verbatim>\<open>\<^bold>\<close> & \<^verbatim>\<open>C+e RIGHT\<close> & @{action_ref "isabelle.control-bold"} \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   605
    emphasized & \<^verbatim>\<open>\<^emph>\<close> & \<^verbatim>\<open>C+e LEFT\<close> & @{action_ref "isabelle.control-emph"} \\
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   606
    reset & & \<^verbatim>\<open>C+e BACK_SPACE\<close> & @{action_ref "isabelle.control-reset"} \\
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   607
  \end{tabular}
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   608
  \<^medskip>
61483
07c8d5d8acab added action "isabelle-emph";
wenzelm
parents: 61477
diff changeset
   609
07c8d5d8acab added action "isabelle-emph";
wenzelm
parents: 61477
diff changeset
   610
  To produce a single control symbol, it is also possible to complete on
61504
wenzelm
parents: 61503
diff changeset
   611
  \<^verbatim>\<open>\sup\<close>, \<^verbatim>\<open>\sub\<close>, \<^verbatim>\<open>\bold\<close>, \<^verbatim>\<open>\emph\<close> as for regular symbols.
61483
07c8d5d8acab added action "isabelle-emph";
wenzelm
parents: 61477
diff changeset
   612
62184
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   613
  The emphasized style only takes effect in document output (when used with a
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   614
  cartouche), but not in the editor.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   615
\<close>
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   616
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   617
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   618
section \<open>Scala console \label{sec:scala-console}\<close>
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   619
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   620
text \<open>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   621
  The \<^emph>\<open>Console\<close> plugin manages various shells (command interpreters), e.g.\
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   622
  \<^emph>\<open>BeanShell\<close>, which is the official jEdit scripting language, and the
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   623
  cross-platform \<^emph>\<open>System\<close> shell. Thus the console provides similar
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   624
  functionality than the Emacs buffers \<^verbatim>\<open>*scratch*\<close> and \<^verbatim>\<open>*shell*\<close>.
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   625
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   626
  Isabelle/jEdit extends the repertoire of the console by \<^emph>\<open>Scala\<close>, which is
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   627
  the regular Scala toplevel loop running inside the same JVM process as
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   628
  Isabelle/jEdit itself. This means the Scala command interpreter has access
57603
0f58af858813 more default imports;
wenzelm
parents: 57589
diff changeset
   629
  to the JVM name space and state of the running Prover IDE application. The
61503
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   630
  default environment imports the full content of packages \<^verbatim>\<open>isabelle\<close> and
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   631
  \<^verbatim>\<open>isabelle.jedit\<close>.
57603
0f58af858813 more default imports;
wenzelm
parents: 57589
diff changeset
   632
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   633
  For example, \<^verbatim>\<open>PIDE\<close> refers to the Isabelle/jEdit plugin object, and \<^verbatim>\<open>view\<close>
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   634
  to the current editor view of jEdit. The Scala expression
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   635
  \<^verbatim>\<open>PIDE.snapshot(view)\<close> makes a PIDE document snapshot of the current buffer
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   636
  within the current editor view.
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   637
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   638
  This helps to explore Isabelle/Scala functionality interactively. Some care
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   639
  is required to avoid interference with the internals of the running
62184
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   640
  application.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   641
\<close>
57319
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   642
3ca8216f4a96 clarified section structure;
wenzelm
parents: 57318
diff changeset
   643
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   644
section \<open>File-system access\<close>
57318
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   645
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   646
text \<open>
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   647
  File specifications in jEdit follow various formats and conventions
61477
e467ae7aa808 more control symbols;
wenzelm
parents: 61458
diff changeset
   648
  according to \<^emph>\<open>Virtual File Systems\<close>, which may be also provided by
61503
28e788ca2c5d more control symbols;
wenzelm
parents: 61493
diff changeset
   649
  additional plugins. This allows to access remote files via the \<^verbatim>\<open>http:\<close>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   650
  protocol prefix, for example. Isabelle/jEdit attempts to work with the
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   651
  file-system model of jEdit as far as possible. In particular, theory sources
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   652
  are passed directly from the editor to the prover, without indirection via
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   653
  physical files.
57318
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   654
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   655
  Despite the flexibility of URLs in jEdit, local files are particularly
62184
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   656
  important and are accessible without protocol prefix. The file path notation
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   657
  is that of the Java Virtual Machine on the underlying platform. On Windows
62184
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   658
  the preferred form uses backslashes, but happens to accept forward slashes
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   659
  like Unix/POSIX as well. Further differences arise due to Windows drive
60257
wenzelm
parents: 60256
diff changeset
   660
  letters and network shares.
57318
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   661
57331
wenzelm
parents: 57329
diff changeset
   662
  The Java notation for files needs to be distinguished from the one of
61477
e467ae7aa808 more control symbols;
wenzelm
parents: 61458
diff changeset
   663
  Isabelle, which uses POSIX notation with forward slashes on \<^emph>\<open>all\<close>
62184
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   664
  platforms. Isabelle/ML on Windows uses Unix-style path notation, too, and
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   665
  driver letter representation as in Cygwin (e.g.\ \<^verbatim>\<open>/cygdrive/c\<close>). Moreover,
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   666
  environment variables from the Isabelle process may be used freely, e.g.\
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   667
  \<^file>\<open>$ISABELLE_HOME/etc/symbols\<close> or \<^file>\<open>$POLYML_HOME/README\<close>. There are special
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   668
  shortcuts: \<^dir>\<open>~\<close> for \<^dir>\<open>$USER_HOME\<close> and \<^dir>\<open>~~\<close> for \<^dir>\<open>$ISABELLE_HOME\<close>.
57318
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   669
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   670
  \<^medskip>
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   671
  Since jEdit happens to support environment variables within file
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   672
  specifications as well, it is natural to use similar notation within the
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   673
  editor, e.g.\ in the file-browser. This does not work in full generality,
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   674
  though, due to the bias of jEdit towards platform-specific notation and of
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   675
  Isabelle towards POSIX. Moreover, the Isabelle settings environment is not
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   676
  yet active when starting Isabelle/jEdit via its standard application
60257
wenzelm
parents: 60256
diff changeset
   677
  wrapper, in contrast to @{tool jedit} run from the command line
wenzelm
parents: 60256
diff changeset
   678
  (\secref{sec:command-line}).
57318
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   679
63749
4fe8cfaeb1fc clarified important directories;
wenzelm
parents: 63680
diff changeset
   680
  Isabelle/jEdit imitates important system settings within the Java process
4fe8cfaeb1fc clarified important directories;
wenzelm
parents: 63680
diff changeset
   681
  environment, in order to allow easy access to these important places from
4fe8cfaeb1fc clarified important directories;
wenzelm
parents: 63680
diff changeset
   682
  the editor: \<^verbatim>\<open>$ISABELLE_HOME\<close>, \<^verbatim>\<open>$ISABELLE_HOME_USER\<close>, \<^verbatim>\<open>$JEDIT_HOME\<close>,
4fe8cfaeb1fc clarified important directories;
wenzelm
parents: 63680
diff changeset
   683
  \<^verbatim>\<open>$JEDIT_SETTINGS\<close>. The file browser of jEdit also includes \<^emph>\<open>Favorites\<close> for
4fe8cfaeb1fc clarified important directories;
wenzelm
parents: 63680
diff changeset
   684
  these two important locations.
57318
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   685
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   686
  \<^medskip>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   687
  Path specifications in prover input or output usually include formal markup
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   688
  that turns it into a hyperlink (see also \secref{sec:tooltips-hyperlinks}).
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   689
  This allows to open the corresponding file in the text editor, independently
62184
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   690
  of the path notation. If the path refers to a directory, the jEdit file
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   691
  browser is opened on it.
57318
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   692
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   693
  Formally checked paths in prover input are subject to completion
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   694
  (\secref{sec:completion}): partial specifications are resolved via directory
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   695
  content and possible completions are offered in a popup.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   696
\<close>
57318
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   697
2b89a3a34cc3 clarified section structure;
wenzelm
parents: 57317
diff changeset
   698
64515
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   699
section \<open>Indentation\<close>
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   700
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   701
text \<open>
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   702
  Isabelle/jEdit augments the existing indentation facilities of jEdit to take
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   703
  the structure of theory and proof texts into account. There is also special
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   704
  support for unstructured proof scripts.
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   705
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   706
    \<^descr>[Syntactic indentation] follows the outer syntax of Isabelle/Isar.
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   707
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   708
    Action @{action "indent-lines"} (shortcut \<^verbatim>\<open>C+i\<close>) indents the current line
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   709
    according to command keywords and some command substructure: this
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   710
    approximation may need further manual tuning.
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   711
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   712
    Action @{action "isabelle.newline"} (shortcut \<^verbatim>\<open>ENTER\<close>) indents the old
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   713
    and the new line according to command keywords only: this leads to precise
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   714
    alignment of the main Isar language elements. This depends on option
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   715
    @{system_option_def "jedit_indent_newline"} (enabled by default).
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   716
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   717
    \<^descr>[Semantic indentation] adds additional white space to unstructured proof
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   718
    scripts (\<^theory_text>\<open>apply\<close> etc.) via number of subgoals. This requires information
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   719
    of ongoing document processing and may thus lag behind, when the user is
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   720
    editing too quickly; see also option @{system_option_def
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   721
    "jedit_script_indent"} and @{system_option_def
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   722
    "jedit_script_indent_limit"}.
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   723
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   724
  The above options are accessible in the menu \<^emph>\<open>Plugins / Plugin Options /
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   725
  Isabelle / General\<close>.
64549
964ac7439a52 notes on whitespace;
wenzelm
parents: 64515
diff changeset
   726
964ac7439a52 notes on whitespace;
wenzelm
parents: 64515
diff changeset
   727
  \<^medskip> Automatic indentation has a tendency to produce trailing whitespace. That
964ac7439a52 notes on whitespace;
wenzelm
parents: 64515
diff changeset
   728
  can be purged manually with the jEdit action @{action "remove-trailing-ws"}
964ac7439a52 notes on whitespace;
wenzelm
parents: 64515
diff changeset
   729
  (shortcut \<^verbatim>\<open>C+e r\<close>). Moreover, the \<^emph>\<open>WhiteSpace\<close> plugin provides some
964ac7439a52 notes on whitespace;
wenzelm
parents: 64515
diff changeset
   730
  aggressive options to trim whitespace on buffer-save.
64515
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   731
\<close>
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   732
29f0b8d2f952 more on "Indentation";
wenzelm
parents: 64514
diff changeset
   733
62184
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   734
section \<open>SideKick parsers \label{sec:sidekick}\<close>
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   735
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   736
text \<open>
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   737
  The \<^emph>\<open>SideKick\<close> plugin provides some general services to display buffer
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   738
  structure in a tree view. Isabelle/jEdit provides SideKick parsers for its
64513
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   739
  main mode for theory files, ML files, as well as some minor modes for the
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   740
  \<^verbatim>\<open>NEWS\<close> file (see \figref{fig:sidekick}), session \<^verbatim>\<open>ROOT\<close> files, system
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   741
  \<^verbatim>\<open>options\<close>, and Bib{\TeX} files (\secref{sec:bibtex}).
62184
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   742
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   743
  \begin{figure}[!htb]
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   744
  \begin{center}
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   745
  \includegraphics[scale=0.333]{sidekick}
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   746
  \end{center}
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   747
  \caption{The Isabelle NEWS file with SideKick tree view}
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   748
  \label{fig:sidekick}
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   749
  \end{figure}
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   750
64513
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   751
  The default SideKick parser for theory files is \<^verbatim>\<open>isabelle\<close>: it provides a
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   752
  tree-view on the formal document structure, with section headings at the top
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   753
  and formal specification elements at the bottom. The alternative parser
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   754
  \<^verbatim>\<open>isabelle-context\<close> shows nesting of context blocks according to \<^theory_text>\<open>begin \<dots>
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   755
  end\<close> structure.
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   756
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   757
  \<^medskip>
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   758
  Isabelle/ML files are structured according to semi-formal comments that are
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   759
  explained in @{cite "isabelle-implementation"}. This outline is turned into
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   760
  a tree-view by default, by using the \<^verbatim>\<open>isabelle-ml\<close> parser. There is also a
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   761
  folding mode of the same name, for hierarchic text folds within ML files.
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   762
56972c755027 misc tuning and updates;
wenzelm
parents: 64512
diff changeset
   763
  \<^medskip>
62184
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   764
  The special SideKick parser \<^verbatim>\<open>isabelle-markup\<close> exposes the uninterpreted
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   765
  markup tree of the PIDE document model of the current buffer. This is
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   766
  occasionally useful for informative purposes, but the amount of displayed
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   767
  information might cause problems for large buffers.
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   768
\<close>
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   769
3764797dd6fc misc updates and tuning;
wenzelm
parents: 62183
diff changeset
   770
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   771
chapter \<open>Prover IDE functionality \label{sec:document-model}\<close>
57315
d0f34f328ffa clarified section structure;
wenzelm
parents: 57314
diff changeset
   772
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   773
section \<open>Document model \label{sec:document-model}\<close>
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   774
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   775
text \<open>
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   776
  The document model is central to the PIDE architecture: the editor and the
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   777
  prover have a common notion of structured source text with markup, which is
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   778
  produced by formal processing. The editor is responsible for edits of
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   779
  document source, as produced by the user. The prover is responsible for
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   780
  reports of document markup, as produced by its processing in the background.
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   781
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   782
  Isabelle/jEdit handles classic editor events of jEdit, in order to connect
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   783
  the physical world of the GUI (with its singleton state) to the mathematical
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   784
  world of multiple document versions (with timeless and stateless updates).
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   785
\<close>
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   786
54322
9d156ded3c2a more documentation;
wenzelm
parents: 54321
diff changeset
   787
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   788
subsection \<open>Editor buffers and document nodes \label{sec:buffer-node}\<close>
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   789
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   790
text \<open>
61477
e467ae7aa808 more control symbols;
wenzelm
parents: 61458
diff changeset
   791
  As a regular text editor, jEdit maintains a collection of \<^emph>\<open>buffers\<close> to
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   792
  store text files; each buffer may be associated with any number of visible
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   793
  \<^emph>\<open>text areas\<close>. Buffers are subject to an \<^emph>\<open>edit mode\<close> that is determined
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   794
  from the file name extension. The following modes are treated specifically
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   795
  in Isabelle/jEdit:
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   796
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   797
  \<^medskip>
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   798
  \begin{tabular}{lll}
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   799
  \<^bold>\<open>mode\<close> & \<^bold>\<open>file name\<close> & \<^bold>\<open>content\<close> \\\hline
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   800
  \<^verbatim>\<open>isabelle\<close> & \<^verbatim>\<open>*.thy\<close> & theory source \\
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   801
  \<^verbatim>\<open>isabelle-ml\<close> & \<^verbatim>\<open>*.ML\<close> & Isabelle/ML source \\
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   802
  \<^verbatim>\<open>sml\<close> & \<^verbatim>\<open>*.sml\<close> or \<^verbatim>\<open>*.sig\<close> & Standard ML source \\
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   803
  \<^verbatim>\<open>isabelle-root\<close> & \<^verbatim>\<open>ROOT\<close> & session root \\
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   804
  \<^verbatim>\<open>isabelle-options\<close> & & Isabelle options \\
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   805
  \<^verbatim>\<open>isabelle-news\<close> & & Isabelle NEWS \\
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   806
  \end{tabular}
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   807
  \<^medskip>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   808
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   809
  All jEdit buffers are automatically added to the PIDE document-model as
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   810
  \<^emph>\<open>document nodes\<close>. The overall document structure is defined by the theory
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   811
  nodes in two dimensions:
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   812
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   813
    \<^enum> via \<^bold>\<open>theory imports\<close> that are specified in the \<^emph>\<open>theory header\<close> using
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   814
    concrete syntax of the @{command_ref theory} command @{cite
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   815
    "isabelle-isar-ref"};
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   816
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   817
    \<^enum> via \<^bold>\<open>auxiliary files\<close> that are loaded into a theory by special \<^emph>\<open>load
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   818
    commands\<close>, notably @{command_ref ML_file} and @{command_ref SML_file}
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   819
    @{cite "isabelle-isar-ref"}.
54322
9d156ded3c2a more documentation;
wenzelm
parents: 54321
diff changeset
   820
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   821
  In any case, source files are managed by the PIDE infrastructure: the
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   822
  physical file-system only plays a subordinate role. The relevant version of
60257
wenzelm
parents: 60256
diff changeset
   823
  source text is passed directly from the editor to the prover, using internal
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   824
  communication channels.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   825
\<close>
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   826
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   827
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   828
subsection \<open>Theories \label{sec:theories}\<close>
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   829
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   830
text \<open>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   831
  The \<^emph>\<open>Theories\<close> panel (see also \figref{fig:theories}) provides an overview
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   832
  of the status of continuous checking of theory nodes within the document
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   833
  model. Unlike batch sessions of @{tool build} @{cite "isabelle-system"},
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   834
  theory nodes are identified by full path names; this allows to work with
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   835
  multiple (disjoint) Isabelle sessions simultaneously within the same editor
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   836
  session.
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   837
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   838
  \begin{figure}[!htb]
57339
3bb94256e0ed added screenshot;
wenzelm
parents: 57338
diff changeset
   839
  \begin{center}
3bb94256e0ed added screenshot;
wenzelm
parents: 57338
diff changeset
   840
  \includegraphics[scale=0.333]{theories}
3bb94256e0ed added screenshot;
wenzelm
parents: 57338
diff changeset
   841
  \end{center}
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   842
  \caption{Theories panel with an overview of the document-model, and jEdit
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   843
  text areas as editable views on some of the document nodes}
57339
3bb94256e0ed added screenshot;
wenzelm
parents: 57338
diff changeset
   844
  \label{fig:theories}
3bb94256e0ed added screenshot;
wenzelm
parents: 57338
diff changeset
   845
  \end{figure}
3bb94256e0ed added screenshot;
wenzelm
parents: 57338
diff changeset
   846
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   847
  Certain events to open or update editor buffers cause Isabelle/jEdit to
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   848
  resolve dependencies of theory imports. The system requests to load
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   849
  additional files into editor buffers, in order to be included in the
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   850
  document model for further checking. It is also possible to let the system
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   851
  resolve dependencies automatically, according to the system option
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   852
  @{system_option jedit_auto_load}.
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
   853
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   854
  \<^medskip>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   855
  The visible \<^emph>\<open>perspective\<close> of Isabelle/jEdit is defined by the collective
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   856
  view on theory buffers via open text areas. The perspective is taken as a
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   857
  hint for document processing: the prover ensures that those parts of a
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   858
  theory where the user is looking are checked, while other parts that are
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   859
  presently not required are ignored. The perspective is changed by opening or
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   860
  closing text area windows, or scrolling within a window.
54322
9d156ded3c2a more documentation;
wenzelm
parents: 54321
diff changeset
   861
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   862
  The \<^emph>\<open>Theories\<close> panel provides some further options to influence the process
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   863
  of continuous checking: it may be switched off globally to restrict the
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   864
  prover to superficial processing of command syntax. It is also possible to
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   865
  indicate theory nodes as \<^emph>\<open>required\<close> for continuous checking: this means
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   866
  such nodes and all their imports are always processed independently of the
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   867
  visibility status (if continuous checking is enabled). Big theory libraries
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   868
  that are marked as required can have significant impact on performance!
54322
9d156ded3c2a more documentation;
wenzelm
parents: 54321
diff changeset
   869
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   870
  \<^medskip>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   871
  Formal markup of checked theory content is turned into GUI rendering, based
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   872
  on a standard repertoire known from mainstream IDEs for programming
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   873
  languages: colors, icons, highlighting, squiggly underlines, tooltips,
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   874
  hyperlinks etc. For outer syntax of Isabelle/Isar there is some traditional
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   875
  syntax-highlighting via static keywords and tokenization within the editor;
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   876
  this buffer syntax is determined from theory imports. In contrast, the
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   877
  painting of inner syntax (term language etc.)\ uses semantic information
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   878
  that is reported dynamically from the logical context. Thus the prover can
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   879
  provide additional markup to help the user to understand the meaning of
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   880
  formal text, and to produce more text with some add-on tools (e.g.\
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   881
  information messages with \<^emph>\<open>sendback\<close> markup by automated provers or
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   882
  disprovers in the background). \<close>
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   883
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   884
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   885
subsection \<open>Auxiliary files \label{sec:aux-files}\<close>
57322
88d7e3eca84b more on "Document model";
wenzelm
parents: 57321
diff changeset
   886
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   887
text \<open>
57329
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   888
  Special load commands like @{command_ref ML_file} and @{command_ref
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
   889
  SML_file} @{cite "isabelle-isar-ref"} refer to auxiliary files within some
57329
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   890
  theory. Conceptually, the file argument of the command extends the theory
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   891
  source by the content of the file, but its editor buffer may be loaded~/
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   892
  changed~/ saved separately. The PIDE document model propagates changes of
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   893
  auxiliary file content to the corresponding load command in the theory, to
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   894
  update and process it accordingly: changes of auxiliary file content are
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
   895
  treated as changes of the corresponding load command.
57323
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   896
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   897
  \<^medskip>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   898
  As a concession to the massive amount of ML files in Isabelle/HOL itself,
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   899
  the content of auxiliary files is only added to the PIDE document-model on
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   900
  demand, the first time when opened explicitly in the editor. There are
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   901
  further tricks to manage markup of ML files, such that Isabelle/HOL may be
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   902
  edited conveniently in the Prover IDE on small machines with only 8\,GB of
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   903
  main memory. Using \<^verbatim>\<open>Pure\<close> as logic session image, the exploration may start
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   904
  at the top \<^file>\<open>$ISABELLE_HOME/src/HOL/Main.thy\<close> or the bottom
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   905
  \<^file>\<open>$ISABELLE_HOME/src/HOL/HOL.thy\<close>, for example.
57323
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   906
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   907
  Initially, before an auxiliary file is opened in the editor, the prover
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   908
  reads its content from the physical file-system. After the file is opened
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   909
  for the first time in the editor, e.g.\ by following the hyperlink
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   910
  (\secref{sec:tooltips-hyperlinks}) for the argument of its @{command
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   911
  ML_file} command, the content is taken from the jEdit buffer.
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   912
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   913
  The change of responsibility from prover to editor counts as an update of
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   914
  the document content, so subsequent theory sources need to be re-checked.
57420
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   915
  When the buffer is closed, the responsibility remains to the editor: the
8103a3f6f342 misc tuning;
wenzelm
parents: 57415
diff changeset
   916
  file may be opened again without causing another document update.
57323
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   917
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   918
  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
   919
  not, is presently inactive in the document model. A file that is loaded via
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   920
  multiple load commands is associated to an arbitrary one: this situation is
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   921
  morally unsupported and might lead to confusion.
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   922
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   923
  \<^medskip>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   924
  Output that refers to an auxiliary file is combined with that of the
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   925
  corresponding load command, and shown whenever the file or the command are
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   926
  active (see also \secref{sec:output}).
57323
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   927
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   928
  Warnings, errors, and other useful markup is attached directly to the
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   929
  positions in the auxiliary file buffer, in the manner of standard IDEs. By
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   930
  using the load command @{command SML_file} as explained in
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
   931
  \<^file>\<open>$ISABELLE_HOME/src/Tools/SML/Examples.thy\<close>, Isabelle/jEdit may be used as
57323
3c66ca9b425b more on "Auxiliary files";
wenzelm
parents: 57322
diff changeset
   932
  fully-featured IDE for Standard ML, independently of theory or proof
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   933
  development: the required theory merely serves as some kind of project file
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   934
  for a collection of SML source modules.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   935
\<close>
54322
9d156ded3c2a more documentation;
wenzelm
parents: 54321
diff changeset
   936
54352
7557f9f1d4aa misc tuning and clarification;
wenzelm
parents: 54351
diff changeset
   937
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   938
section \<open>Output \label{sec:output}\<close>
54353
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   939
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
   940
text \<open>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   941
  Prover output consists of \<^emph>\<open>markup\<close> and \<^emph>\<open>messages\<close>. Both are directly
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   942
  attached to the corresponding positions in the original source text, and
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   943
  visualized in the text area, e.g.\ as text colours for free and bound
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   944
  variables, or as squiggly underlines for warnings, errors etc.\ (see also
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   945
  \figref{fig:output}). In the latter case, the corresponding messages are
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   946
  shown by hovering with the mouse over the highlighted text --- although in
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   947
  many situations the user should already get some clue by looking at the
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   948
  position of the text highlighting, without seeing the message body itself.
54357
157b6eee6a76 more screenshots;
wenzelm
parents: 54356
diff changeset
   949
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
   950
  \begin{figure}[!htb]
54357
157b6eee6a76 more screenshots;
wenzelm
parents: 54356
diff changeset
   951
  \begin{center}
57312
afbc20986435 updated screenshots;
wenzelm
parents: 57311
diff changeset
   952
  \includegraphics[scale=0.333]{output}
54357
157b6eee6a76 more screenshots;
wenzelm
parents: 54356
diff changeset
   953
  \end{center}
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   954
  \caption{Multiple views on prover output: gutter with icon, text area with
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   955
  popup, text overview column, \<^emph>\<open>Theories\<close> panel, \<^emph>\<open>Output\<close> panel}
54357
157b6eee6a76 more screenshots;
wenzelm
parents: 54356
diff changeset
   956
  \label{fig:output}
157b6eee6a76 more screenshots;
wenzelm
parents: 54356
diff changeset
   957
  \end{figure}
54353
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   958
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   959
  The ``gutter'' on the left-hand-side of the text area uses icons to
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   960
  provide a summary of the messages within the adjacent text line. Message
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
   961
  priorities are used to prefer errors over warnings, warnings over
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   962
  information messages; other output is ignored.
54353
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   963
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   964
  The ``text overview column'' on the right-hand-side of the text area uses
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   965
  similar information to paint small rectangles for the overall status of the
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   966
  whole text buffer. The graphics is scaled to fit the logical buffer length
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   967
  into the given window height. Mouse clicks on the overview area move the
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   968
  cursor approximately to the corresponding text line in the buffer.
54353
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   969
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   970
  The \<^emph>\<open>Theories\<close> panel provides another course-grained overview, but without
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   971
  direct correspondence to text positions. The coloured rectangles represent
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   972
  the amount of messages of a certain kind (warnings, errors, etc.) and the
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   973
  execution status of commands. A double-click on one of the theory entries
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   974
  with their status overview opens the corresponding text buffer, without
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   975
  moving the cursor to a specific point.
54353
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   976
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
   977
  \<^medskip>
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   978
  The \<^emph>\<open>Output\<close> panel displays prover messages that correspond to a given
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   979
  command, within a separate window. The cursor position in the presently
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   980
  active text area determines the prover command whose cumulative message
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   981
  output is appended and shown in that window (in canonical order according to
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   982
  the internal execution of the command). There are also control elements to
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   983
  modify the update policy of the output wrt.\ continued editor movements:
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   984
  \<^emph>\<open>Auto update\<close> and \<^emph>\<open>Update\<close>. This is particularly useful for multiple
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   985
  instances of the \<^emph>\<open>Output\<close> panel to look at different situations.
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   986
  Alternatively, the panel can be turned into a passive \<^emph>\<open>Info\<close> window via the
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   987
  \<^emph>\<open>Detach\<close> menu item.
54353
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   988
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   989
  Proof state is handled separately (\secref{sec:state-output}), but it is
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   990
  also possible to tick the corresponding checkbox to append it to regular
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   991
  output (\figref{fig:output-including-state}). This is a globally persistent
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   992
  option: it affects all open panels and future editor sessions.
54353
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
   993
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   994
  \begin{figure}[!htb]
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   995
  \begin{center}
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   996
  \includegraphics[scale=0.333]{output-including-state}
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   997
  \end{center}
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   998
  \caption{Proof state display within the regular output panel}
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
   999
  \label{fig:output-including-state}
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1000
  \end{figure}
54353
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
  1001
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
  1002
  \<^medskip>
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1003
  Following the IDE principle, regular messages are attached to the original
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1004
  source in the proper place and may be inspected on demand via popups. This
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1005
  excludes messages that are somehow internal to the machinery of proof
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1006
  checking, notably \<^emph>\<open>proof state\<close> and \<^emph>\<open>tracing\<close>.
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1007
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1008
  In any case, the same display technology is used for small popups and big
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1009
  output windows. The formal text contains markup that may be explored
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1010
  recursively via further popups and hyperlinks (see
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1011
  \secref{sec:tooltips-hyperlinks}), or clicked directly to initiate certain
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1012
  actions (see \secref{sec:auto-tools} and \secref{sec:sledgehammer}).
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1013
\<close>
54353
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
  1014
6692c355ebc1 more on prover output;
wenzelm
parents: 54352
diff changeset
  1015
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1016
section \<open>Proof state \label{sec:state-output}\<close>
62154
b855771b3979 updated old screenshots, added new screenshots;
wenzelm
parents: 62039
diff changeset
  1017
b855771b3979 updated old screenshots, added new screenshots;
wenzelm
parents: 62039
diff changeset
  1018
text \<open>
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1019
  The main purpose of the Prover IDE is to help the user editing proof
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1020
  documents, with ongoing formal checking by the prover in the background.
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1021
  This can be done to some extent in the main text area alone, especially for
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1022
  well-structured Isar proofs.
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1023
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1024
  Nonetheless, internal proof state needs to be inspected in many situations
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1025
  of exploration and ``debugging''. The \<^emph>\<open>State\<close> panel shows exclusively such
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1026
  proof state messages without further distraction, while all other messages
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1027
  are displayed in \<^emph>\<open>Output\<close> (\secref{sec:output}).
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1028
  \Figref{fig:output-and-state} shows a typical GUI layout where both panels
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1029
  are open.
62154
b855771b3979 updated old screenshots, added new screenshots;
wenzelm
parents: 62039
diff changeset
  1030
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
  1031
  \begin{figure}[!htb]
62154
b855771b3979 updated old screenshots, added new screenshots;
wenzelm
parents: 62039
diff changeset
  1032
  \begin{center}
b855771b3979 updated old screenshots, added new screenshots;
wenzelm
parents: 62039
diff changeset
  1033
  \includegraphics[scale=0.333]{output-and-state}
b855771b3979 updated old screenshots, added new screenshots;
wenzelm
parents: 62039
diff changeset
  1034
  \end{center}
b855771b3979 updated old screenshots, added new screenshots;
wenzelm
parents: 62039
diff changeset
  1035
  \caption{Separate proof state display (right) and other output (bottom).}
b855771b3979 updated old screenshots, added new screenshots;
wenzelm
parents: 62039
diff changeset
  1036
  \label{fig:output-and-state}
b855771b3979 updated old screenshots, added new screenshots;
wenzelm
parents: 62039
diff changeset
  1037
  \end{figure}
b855771b3979 updated old screenshots, added new screenshots;
wenzelm
parents: 62039
diff changeset
  1038
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1039
  Another typical arrangement has more than one \<^emph>\<open>State\<close> panel open (as
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1040
  floating windows), with \<^emph>\<open>Auto update\<close> disabled to look at an old situation
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1041
  while the proof text in the vicinity is changed. The \<^emph>\<open>Update\<close> button
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1042
  triggers an explicit one-shot update; this operation is also available via
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1043
  the action @{action "isabelle.update-state"} (keyboard shortcut \<^verbatim>\<open>S+ENTER\<close>).
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1044
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1045
  On small screens, it is occasionally useful to have all messages
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1046
  concatenated in the regular \<^emph>\<open>Output\<close> panel, e.g.\ see
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1047
  \figref{fig:output-including-state}.
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1048
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1049
  \<^medskip>
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1050
  The mechanics of \<^emph>\<open>Output\<close> versus \<^emph>\<open>State\<close> are slightly different:
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1051
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1052
    \<^item> \<^emph>\<open>Output\<close> shows information that is continuously produced and already
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1053
    present when the GUI wants to show it. This is implicitly controlled by
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1054
    the visible perspective on the text.
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1055
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1056
    \<^item> \<^emph>\<open>State\<close> initiates a real-time query on demand, with a full round trip
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1057
    including a fresh print operation on the prover side. This is controlled
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1058
    explicitly when the cursor is moved to the next command (\<^emph>\<open>Auto update\<close>)
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1059
    or the \<^emph>\<open>Update\<close> operation is triggered.
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1060
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1061
  This can make a difference in GUI responsibility and resource usage within
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1062
  the prover process. Applications with very big proof states that are only
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1063
  inspected in isolation work better with the \<^emph>\<open>State\<close> panel.
62154
b855771b3979 updated old screenshots, added new screenshots;
wenzelm
parents: 62039
diff changeset
  1064
\<close>
b855771b3979 updated old screenshots, added new screenshots;
wenzelm
parents: 62039
diff changeset
  1065
62185
155d30f721dd misc updates and tuning;
wenzelm
parents: 62184
diff changeset
  1066
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1067
section \<open>Query \label{sec:query}\<close>
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1068
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1069
text \<open>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1070
  The \<^emph>\<open>Query\<close> panel provides various GUI forms to request extra information
62249
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1071
  from the prover, as a replacement of old-style diagnostic commands like
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1072
  @{command find_theorems}. There are input fields and buttons for a
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1073
  particular query command, with output in a dedicated text area.
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1074
62249
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1075
  The main query modes are presented as separate tabs: \<^emph>\<open>Find Theorems\<close>,
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1076
  \<^emph>\<open>Find Constants\<close>, \<^emph>\<open>Print Context\<close>, e.g.\ see \figref{fig:query}. As usual
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1077
  in jEdit, multiple \<^emph>\<open>Query\<close> windows may be active at the same time: any
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1078
  number of floating instances, but at most one docked instance (which is used
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1079
  by default).
57313
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
  1080
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
  1081
  \begin{figure}[!htb]
57313
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
  1082
  \begin{center}
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
  1083
  \includegraphics[scale=0.333]{query}
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
  1084
  \end{center}
62154
b855771b3979 updated old screenshots, added new screenshots;
wenzelm
parents: 62039
diff changeset
  1085
  \caption{An instance of the Query panel: find theorems}
57313
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
  1086
  \label{fig:query}
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
  1087
  \end{figure}
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1088
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
  1089
  \<^medskip>
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
  1090
  The following GUI elements are common to all query modes:
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1091
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1092
    \<^item> The spinning wheel provides feedback about the status of a pending query
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1093
    wrt.\ the evaluation of its context and its own operation.
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1094
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1095
    \<^item> The \<^emph>\<open>Apply\<close> button attaches a fresh query invocation to the current
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1096
    context of the command where the cursor is pointing in the text.
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1097
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1098
    \<^item> The \<^emph>\<open>Search\<close> field allows to highlight query output according to some
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1099
    regular expression, in the notation that is commonly used on the Java
63680
6e1e8b5abbfa more symbols;
wenzelm
parents: 63669
diff changeset
  1100
    platform.\<^footnote>\<open>\<^url>\<open>https://docs.oracle.com/javase/8/docs/api/java/util/regex/Pattern.html\<close>\<close>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1101
    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
  1102
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1103
    \<^item> The \<^emph>\<open>Zoom\<close> box controls the font size of the output area.
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1104
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1105
  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
  1106
  evaluation of the document for the query context, nor for the query
61477
e467ae7aa808 more control symbols;
wenzelm
parents: 61458
diff changeset
  1107
  operation itself. Query output may be detached as independent \<^emph>\<open>Info\<close>
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1108
  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
  1109
  result usually provides sufficient clues about the original query, with some
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1110
  hyperlink to its context (via markup of its head line).
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1111
\<close>
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1112
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1113
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1114
subsection \<open>Find theorems\<close>
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1115
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1116
text \<open>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1117
  The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Theorems\<close> mode retrieves facts from the theory
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1118
  or proof context matching all of given criteria in the \<^emph>\<open>Find\<close> text field. A
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1119
  single criterium has the following syntax:
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1120
57313
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
  1121
  @{rail \<open>
62969
9f394a16c557 eliminated "xname" and variants;
wenzelm
parents: 62917
diff changeset
  1122
    ('-'?) ('name' ':' @{syntax name} | 'intro' | 'elim' | 'dest' |
57313
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
  1123
      'solves' | 'simp' ':' @{syntax term} | @{syntax term})
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
  1124
  \<close>}
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
  1125
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1126
  See also the Isar command @{command_ref find_theorems} in @{cite
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1127
  "isabelle-isar-ref"}.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1128
\<close>
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1129
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1130
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1131
subsection \<open>Find constants\<close>
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1132
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1133
text \<open>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1134
  The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Find Constants\<close> mode prints all constants whose type
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1135
  meets all of the given criteria in the \<^emph>\<open>Find\<close> text field. A single
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1136
  criterium has the following syntax:
57313
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
  1137
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
  1138
  @{rail \<open>
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
  1139
    ('-'?)
62969
9f394a16c557 eliminated "xname" and variants;
wenzelm
parents: 62917
diff changeset
  1140
      ('name' ':' @{syntax name} | 'strict' ':' @{syntax type} | @{syntax type})
57313
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
  1141
  \<close>}
c66832858f43 more on Query panel;
wenzelm
parents: 57312
diff changeset
  1142
58554
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
  1143
  See also the Isar command @{command_ref find_consts} in @{cite
423202f05a43 prefer @{cite} antiquotation;
wenzelm
parents: 57869
diff changeset
  1144
  "isabelle-isar-ref"}.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1145
\<close>
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1146
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1147
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1148
subsection \<open>Print context\<close>
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1149
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1150
text \<open>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1151
  The \<^emph>\<open>Query\<close> panel in \<^emph>\<open>Print Context\<close> mode prints information from the
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1152
  theory or proof context, or proof state. See also the Isar commands
57329
397062213224 added Index;
wenzelm
parents: 57328
diff changeset
  1153
  @{command_ref print_context}, @{command_ref print_cases}, @{command_ref
62249
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1154
  print_term_bindings}, @{command_ref print_theorems}, described in @{cite
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1155
  "isabelle-isar-ref"}.
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1156
\<close>
57311
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1157
550b704d665e more on Query panel -- updated Find Theorems;
wenzelm
parents: 57310
diff changeset
  1158
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1159
section \<open>Tooltips and hyperlinks \label{sec:tooltips-hyperlinks}\<close>
54352
7557f9f1d4aa misc tuning and clarification;
wenzelm
parents: 54351
diff changeset
  1160
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1161
text \<open>
62249
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1162
  Formally processed text (prover input or output) contains rich markup that
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1163
  can be explored by using the \<^verbatim>\<open>CONTROL\<close> modifier key on Linux and Windows,
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1164
  or \<^verbatim>\<open>COMMAND\<close> on Mac OS X. Hovering with the mouse while the modifier is
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1165
  pressed reveals a \<^emph>\<open>tooltip\<close> (grey box over the text with a yellow popup)
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1166
  and/or a \<^emph>\<open>hyperlink\<close> (black rectangle over the text with change of mouse
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1167
  pointer); see also \figref{fig:tooltip}.
54331
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
  1168
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
  1169
  \begin{figure}[!htb]
54331
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
  1170
  \begin{center}
57312
afbc20986435 updated screenshots;
wenzelm
parents: 57311
diff changeset
  1171
  \includegraphics[scale=0.5]{popup1}
54331
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
  1172
  \end{center}
54356
9538f51da542 more screenshots;
wenzelm
parents: 54355
diff changeset
  1173
  \caption{Tooltip and hyperlink for some formal entity}
54350
wenzelm
parents: 54349
diff changeset
  1174
  \label{fig:tooltip}
54331
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
  1175
  \end{figure}
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
  1176
62249
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1177
  Tooltip popups use the same rendering technology as the main text area, and
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1178
  further tooltips and/or hyperlinks may be exposed recursively by the same
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1179
  mechanism; see \figref{fig:nested-tooltips}.
54323
d521407f8d0f more documentation;
wenzelm
parents: 54322
diff changeset
  1180
62183
7fdcc25c5c35 misc updates and tuning;
wenzelm
parents: 62154
diff changeset
  1181
  \begin{figure}[!htb]
54331
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
  1182
  \begin{center}
57312
afbc20986435 updated screenshots;
wenzelm
parents: 57311
diff changeset
  1183
  \includegraphics[scale=0.5]{popup2}
54331
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
  1184
  \end{center}
54356
9538f51da542 more screenshots;
wenzelm
parents: 54355
diff changeset
  1185
  \caption{Nested tooltips over formal entities}
54350
wenzelm
parents: 54349
diff changeset
  1186
  \label{fig:nested-tooltips}
54331
9e944630be0c more screenshots;
wenzelm
parents: 54330
diff changeset
  1187
  \end{figure}
54350
wenzelm
parents: 54349
diff changeset
  1188
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1189
  The tooltip popup window provides some controls to \<^emph>\<open>close\<close> or \<^emph>\<open>detach\<close> the
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1190
  window, turning it into a separate \<^emph>\<open>Info\<close> window managed by jEdit. The
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1191
  \<^verbatim>\<open>ESCAPE\<close> key closes \<^emph>\<open>all\<close> popups, which is particularly relevant when
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1192
  nested tooltips are stacking up.
54352
7557f9f1d4aa misc tuning and clarification;
wenzelm
parents: 54351
diff changeset
  1193
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
  1194
  \<^medskip>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1195
  A black rectangle in the text indicates a hyperlink that may be followed by
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1196
  a mouse click (while the \<^verbatim>\<open>CONTROL\<close> or \<^verbatim>\<open>COMMAND\<close> modifier key is still
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1197
  pressed). Such jumps to other text locations are recorded by the
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1198
  \<^emph>\<open>Navigator\<close> plugin, which is bundled with Isabelle/jEdit and enabled by
62249
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1199
  default. There are usually navigation arrows in the main jEdit toolbar.
54352
7557f9f1d4aa misc tuning and clarification;
wenzelm
parents: 54351
diff changeset
  1200
62249
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1201
  Note that the link target may be a file that is itself not subject to formal
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1202
  document processing of the editor session and thus prevents further
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1203
  exploration: the chain of hyperlinks may end in some source file of the
62249
c1d6dfd645e2 misc tuning;
wenzelm
parents: 62212
diff changeset
  1204
  underlying logic image, or within the ML bootstrap sources of Isabelle/Pure.
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1205
\<close>
54321
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
  1206
41951f427ac7 more documentation;
wenzelm
parents: 54320
diff changeset
  1207
64514
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1208
section \<open>Formal scopes and semantic selection\<close>
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1209
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1210
text \<open>
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1211
  Formal entities are semantically annotated in the source text as explained
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1212
  in \secref{sec:tooltips-hyperlinks}. A \<^emph>\<open>formal scope\<close> consists of the
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1213
  defining position with all its referencing positions. This correspondence is
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1214
  highlighted in the text according to the cursor position, see also
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1215
  \figref{fig:scope1}. Here the referencing positions are rendered with an
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1216
  additional border, in reminiscence to a hyperlink: clicking there moves the
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1217
  cursor to the original defining position.
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1218
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1219
  \begin{figure}[!htb]
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1220
  \begin{center}
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1221
  \includegraphics[scale=0.5]{scope1}
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1222
  \end{center}
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1223
  \caption{Scope of formal entity: defining vs.\ referencing positions}
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1224
  \label{fig:scope1}
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1225
  \end{figure}
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1226
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1227
  The action @{action_def "isabelle.select-entity"} (shortcut \<^verbatim>\<open>CS+ENTER\<close>)
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1228
  supports semantic selection of all occurrences of the formal entity at the
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1229
  caret position. This facilitates systematic renaming, using regular jEdit
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1230
  editing of a multi-selection, see also \figref{fig:scope2}.
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1231
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1232
  \begin{figure}[!htb]
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1233
  \begin{center}
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1234
  \includegraphics[scale=0.5]{scope2}
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1235
  \end{center}
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1236
  \caption{The result of semantic selection and systematic renaming}
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1237
  \label{fig:scope2}
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1238
  \end{figure}
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1239
\<close>
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1240
27914a4f8c70 more on "Formal scopes and semantic selection";
wenzelm
parents: 64513
diff changeset
  1241
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1242
section \<open>Completion \label{sec:completion}\<close>
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1243
58618
782f0b662cae more cartouches;
wenzelm
parents: 58556
diff changeset
  1244
text \<open>
61477
e467ae7aa808 more control symbols;
wenzelm
parents: 61458
diff changeset
  1245
  Smart completion of partial input is the IDE functionality \<^emph>\<open>par
e467ae7aa808 more control symbols;
wenzelm
parents: 61458
diff changeset
  1246
  excellance\<close>. Isabelle/jEdit combines several sources of information to
57328
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1247
  achieve that. Despite its complexity, it should be possible to get some idea
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1248
  how completion works by experimentation, based on the overview of completion
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1249
  varieties in \secref{sec:completion-varieties}. The remaining subsections
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1250
  explain concepts around completion more systematically.
57325
5e7488f4309e more on "Completion";
wenzelm
parents: 57324
diff changeset
  1251
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
  1252
  \<^medskip>
61477
e467ae7aa808 more control symbols;
wenzelm
parents: 61458
diff changeset
  1253
  \<^emph>\<open>Explicit completion\<close> is triggered by the action @{action_ref
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1254
  "isabelle.complete"}, which is bound to the keyboard shortcut \<^verbatim>\<open>C+b\<close>, and
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1255
  thus overrides the jEdit default for @{action_ref "complete-word"}.
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1256
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1257
  \<^emph>\<open>Implicit completion\<close> hooks into the regular keyboard input stream of the
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1258
  editor, with some event filtering and optional delays.
54361
wenzelm
parents: 54360
diff changeset
  1259
61415
55e73b352287 more symbols;
wenzelm
parents: 61408
diff changeset
  1260
  \<^medskip>
61574
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1261
  Completion options may be configured in \<^emph>\<open>Plugin Options~/ Isabelle~/
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1262
  General~/ Completion\<close>. These are explained in further detail below, whenever
e717f152d2a8 tuned whitespace;
wenzelm
parents: 61573
diff changeset
  1263
  relevant. There is also a summary of options in
57328
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1264
  \secref{sec:completion-options}.
5765ce647ca4 more on "Completion";
wenzelm
parents: 57327
diff changeset
  1265
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1266
  The asynchronous nature of PIDE interaction means that information from the
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1267
  prover is delayed --- at least by a full round-trip of the document update
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1268
  protocol. The default options already take this into account, with a
57324
8c0322732f3e more on "Completion";
wenzelm
parents: 57323
diff changeset
  1269
  sufficiently long completion delay to speculate on the availability of all
57335
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1270
  relevant information from the editor and the prover, before completing text
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1271
  immediately or producing a popup. Although there is an inherent danger of
f911187ada43 misc tuning;
wenzelm
parents: 57334
diff changeset
  1272
  non-deterministic behaviour due to such real-time paramete