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