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