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