src/Doc/System/Interfaces.thy
author wenzelm
Fri May 17 19:04:52 2013 +0200 (2013-05-17)
changeset 52056 fc458f304f93
parent 51054 d6de6e81574d
child 52062 4f91262e7f33
permissions -rw-r--r--
added isabelle-process option -o;
wenzelm@28916
     1
theory Interfaces
wenzelm@43564
     2
imports Base
wenzelm@28916
     3
begin
wenzelm@28916
     4
wenzelm@28916
     5
chapter {* User interfaces *}
wenzelm@28916
     6
wenzelm@48573
     7
section {* Isabelle/jEdit Prover IDE \label{sec:tool-jedit} *}
wenzelm@28916
     8
wenzelm@48603
     9
text {* The @{tool_def jedit} tool invokes a version of
wenzelm@48603
    10
  jEdit\footnote{\url{http://www.jedit.org/}} that has been augmented
wenzelm@51054
    11
  with some plugins to provide a fully-featured Prover IDE:
wenzelm@48603
    12
\begin{ttbox} Usage: isabelle jedit [OPTIONS]
wenzelm@48603
    13
  [FILES ...]
wenzelm@28916
    14
wenzelm@28916
    15
  Options are:
wenzelm@48573
    16
    -J OPTION    add JVM runtime option (default JEDIT_JAVA_OPTIONS)
wenzelm@48573
    17
    -b           build only
wenzelm@48791
    18
    -d DIR       include session directory
wenzelm@48573
    19
    -f           fresh build
wenzelm@48573
    20
    -j OPTION    add jEdit runtime option (default JEDIT_OPTIONS)
wenzelm@28916
    21
    -l NAME      logic image name (default ISABELLE_LOGIC)
wenzelm@28916
    22
    -m MODE      add print mode for output
wenzelm@50406
    23
    -n           no build dialog for session image on startup
wenzelm@50406
    24
    -s           system build mode for session image
wenzelm@28916
    25
wenzelm@50550
    26
Start jEdit with Isabelle plugin setup and open theory FILES
wenzelm@50550
    27
(default "\$USER_HOME/Scratch.thy").
wenzelm@28916
    28
\end{ttbox}
wenzelm@28916
    29
wenzelm@48791
    30
  The @{verbatim "-l"} option specifies the session name of the logic
wenzelm@48791
    31
  image to be used for proof processing.  Additional session root
wenzelm@48791
    32
  directories may be included via option @{verbatim "-d"} to augment
wenzelm@48791
    33
  that name space (see also \secref{sec:tool-build}).
wenzelm@48791
    34
wenzelm@50406
    35
  By default, the specified image is checked and built on demand, see
wenzelm@50406
    36
  also @{tool build_dialog}.  The @{verbatim "-s"} determines where to
wenzelm@50406
    37
  store the result session image (see also \secref{sec:tool-build}).
wenzelm@50406
    38
  The @{verbatim "-n"} option bypasses the session build dialog.
wenzelm@50406
    39
wenzelm@51054
    40
  The @{verbatim "-m"} option specifies additional print modes for the
wenzelm@51054
    41
  prover process.
wenzelm@48573
    42
wenzelm@48573
    43
  The @{verbatim "-J"} and @{verbatim "-j"} options allow to pass
wenzelm@48573
    44
  additional low-level options to the JVM or jEdit, respectively.  The
wenzelm@48603
    45
  defaults are provided by the Isabelle settings environment
wenzelm@48603
    46
  (\secref{sec:settings}).
wenzelm@48573
    47
wenzelm@48573
    48
  The @{verbatim "-b"} and @{verbatim "-f"} options control the
wenzelm@48573
    49
  self-build mechanism of Isabelle/jEdit.  This is only relevant for
wenzelm@48573
    50
  building from sources, which also requires an auxiliary @{verbatim
wenzelm@48603
    51
  jedit_build}
wenzelm@48603
    52
  component.\footnote{\url{http://isabelle.in.tum.de/components}} Note
wenzelm@48603
    53
  that official Isabelle releases already include a version of
wenzelm@50406
    54
  Isabelle/jEdit that is built properly.
wenzelm@50406
    55
*}
wenzelm@28916
    56
wenzelm@28916
    57
wenzelm@28916
    58
section {* Proof General / Emacs *}
wenzelm@28916
    59
wenzelm@48572
    60
text {* The @{tool_def emacs} tool invokes a version of Emacs and
wenzelm@48603
    61
  Proof General\footnote{http://proofgeneral.inf.ed.ac.uk/} within the
wenzelm@48603
    62
  regular Isabelle settings environment (\secref{sec:settings}).  This
wenzelm@48603
    63
  is more convenient than starting Emacs separately, loading the Proof
wenzelm@48603
    64
  General LISP files, and then attempting to start Isabelle with
wenzelm@51054
    65
  dynamic @{setting PATH} lookup etc., although it might fail if a
wenzelm@51054
    66
  different version of Proof General is already part of the Emacs
wenzelm@51054
    67
  installation of the operating system.
wenzelm@28916
    68
wenzelm@28916
    69
  The actual interface script is part of the Proof General
wenzelm@48572
    70
  distribution; its usage depends on the particular version.  There
wenzelm@48572
    71
  are some options available, such as @{verbatim "-l"} for passing the
wenzelm@48572
    72
  logic image to be used by default, or @{verbatim "-m"} to tune the
wenzelm@51054
    73
  standard print mode of the prover process.  The following Isabelle
wenzelm@51054
    74
  settings are particularly important for Proof General:
wenzelm@28916
    75
wenzelm@28916
    76
  \begin{description}
wenzelm@28916
    77
wenzelm@28916
    78
  \item[@{setting_def PROOFGENERAL_HOME}] points to the main
wenzelm@48572
    79
  installation directory of the Proof General distribution.  This is
wenzelm@48572
    80
  implicitly provided for versions of Proof General that are
wenzelm@48572
    81
  distributed as Isabelle component, see also \secref{sec:components};
wenzelm@48572
    82
  otherwise it needs to be configured manually.
wenzelm@28916
    83
wenzelm@28916
    84
  \item[@{setting_def PROOFGENERAL_OPTIONS}] is implicitly prefixed to
wenzelm@28916
    85
  the command line of any invocation of the Proof General @{verbatim
wenzelm@48572
    86
  interface} script.  This allows to provide persistent default
wenzelm@48572
    87
  options for the invocation of \texttt{isabelle emacs}.
wenzelm@28916
    88
wenzelm@28916
    89
  \end{description}
wenzelm@28916
    90
*}
wenzelm@28916
    91
wenzelm@47824
    92
wenzelm@48573
    93
section {* Plain TTY interaction \label{sec:tool-tty} *}
wenzelm@47824
    94
wenzelm@48573
    95
text {*
wenzelm@48573
    96
  The @{tool_def tty} tool runs the Isabelle process interactively
wenzelm@48573
    97
  within a plain terminal session:
wenzelm@47824
    98
\begin{ttbox}
wenzelm@48573
    99
Usage: isabelle tty [OPTIONS]
wenzelm@47824
   100
wenzelm@47824
   101
  Options are:
wenzelm@47824
   102
    -l NAME      logic image name (default ISABELLE_LOGIC)
wenzelm@47824
   103
    -m MODE      add print mode for output
wenzelm@48573
   104
    -p NAME      line editor program name (default ISABELLE_LINE_EDITOR)
wenzelm@47824
   105
wenzelm@48573
   106
  Run Isabelle process with plain tty interaction and line editor.
wenzelm@47824
   107
\end{ttbox}
wenzelm@47824
   108
wenzelm@48573
   109
  The @{verbatim "-l"} option specifies the logic image.  The
wenzelm@48573
   110
  @{verbatim "-m"} option specifies additional print modes.  The
wenzelm@48573
   111
  @{verbatim "-p"} option specifies an alternative line editor (such
wenzelm@48573
   112
  as the @{executable_def rlwrap} wrapper for GNU readline); the
wenzelm@48573
   113
  fall-back is to use raw standard input.
wenzelm@47824
   114
wenzelm@48603
   115
  Regular interaction works via the standard Isabelle/Isar toplevel
wenzelm@48603
   116
  loop.  The Isar command @{command exit} drops out into the
wenzelm@48603
   117
  bare-bones ML system, which is occasionally useful for debugging of
wenzelm@48603
   118
  the Isar infrastructure itself.  Invoking @{ML Isar.loop}~@{verbatim
wenzelm@48603
   119
  "();"} in ML will return to the Isar toplevel.  *}
wenzelm@47824
   120
wenzelm@48576
   121
wenzelm@48576
   122
wenzelm@48576
   123
section {* Theory graph browser \label{sec:browse} *}
wenzelm@48576
   124
wenzelm@48576
   125
text {* The Isabelle graph browser is a general tool for visualizing
wenzelm@48576
   126
  dependency graphs.  Certain nodes of the graph (i.e.\ theories) can
wenzelm@48576
   127
  be grouped together in ``directories'', whose contents may be
wenzelm@48576
   128
  hidden, thus enabling the user to collapse irrelevant portions of
wenzelm@48576
   129
  information.  The browser is written in Java, it can be used both as
wenzelm@48814
   130
  a stand-alone application and as an applet.  *}
wenzelm@48576
   131
wenzelm@48576
   132
wenzelm@48576
   133
subsection {* Invoking the graph browser *}
wenzelm@48576
   134
wenzelm@48602
   135
text {* The stand-alone version of the graph browser is wrapped up as
wenzelm@48602
   136
  @{tool_def browser}:
wenzelm@48576
   137
\begin{ttbox}
wenzelm@48602
   138
Usage: isabelle browser [OPTIONS] [GRAPHFILE]
wenzelm@48576
   139
wenzelm@48576
   140
  Options are:
wenzelm@48576
   141
    -b           Admin/build only
wenzelm@48576
   142
    -c           cleanup -- remove GRAPHFILE after use
wenzelm@48576
   143
    -o FILE      output to FILE (ps, eps, pdf)
wenzelm@48576
   144
\end{ttbox}
wenzelm@48576
   145
  When no filename is specified, the browser automatically changes to
wenzelm@48576
   146
  the directory @{setting ISABELLE_BROWSER_INFO}.
wenzelm@48576
   147
wenzelm@48576
   148
  \medskip The @{verbatim "-b"} option indicates that this is for
wenzelm@48576
   149
  administrative build only, i.e.\ no browser popup if no files are
wenzelm@48576
   150
  given.
wenzelm@48576
   151
wenzelm@48576
   152
  The @{verbatim "-c"} option causes the input file to be removed
wenzelm@48576
   153
  after use.
wenzelm@48576
   154
wenzelm@48576
   155
  The @{verbatim "-o"} option indicates batch-mode operation, with the
wenzelm@48576
   156
  output written to the indicated file; note that @{verbatim pdf}
wenzelm@48576
   157
  produces an @{verbatim eps} copy as well.
wenzelm@48576
   158
wenzelm@48576
   159
  \medskip The applet version of the browser is part of the standard
wenzelm@48576
   160
  WWW theory presentation, see the link ``theory dependencies'' within
wenzelm@48576
   161
  each session index.
wenzelm@48576
   162
*}
wenzelm@48576
   163
wenzelm@48576
   164
wenzelm@48576
   165
subsection {* Using the graph browser *}
wenzelm@48576
   166
wenzelm@48576
   167
text {*
wenzelm@48576
   168
  The browser's main window, which is shown in
wenzelm@48576
   169
  \figref{fig:browserwindow}, consists of two sub-windows.  In the
wenzelm@48576
   170
  left sub-window, the directory tree is displayed. The graph itself
wenzelm@48576
   171
  is displayed in the right sub-window.
wenzelm@48576
   172
wenzelm@48576
   173
  \begin{figure}[ht]
wenzelm@48576
   174
  \includegraphics[width=\textwidth]{browser_screenshot}
wenzelm@48576
   175
  \caption{\label{fig:browserwindow} Browser main window}
wenzelm@48576
   176
  \end{figure}
wenzelm@48576
   177
*}
wenzelm@48576
   178
wenzelm@48576
   179
wenzelm@48576
   180
subsubsection {* The directory tree window *}
wenzelm@48576
   181
wenzelm@48576
   182
text {*
wenzelm@48576
   183
  We describe the usage of the directory browser and the meaning of
wenzelm@48576
   184
  the different items in the browser window.
wenzelm@48576
   185
wenzelm@48576
   186
  \begin{itemize}
wenzelm@48576
   187
wenzelm@48576
   188
  \item A red arrow before a directory name indicates that the
wenzelm@48576
   189
  directory is currently ``folded'', i.e.~the nodes in this directory
wenzelm@48576
   190
  are collapsed to one single node. In the right sub-window, the names
wenzelm@48576
   191
  of nodes corresponding to folded directories are enclosed in square
wenzelm@48576
   192
  brackets and displayed in red color.
wenzelm@48576
   193
wenzelm@48576
   194
  \item A green downward arrow before a directory name indicates that
wenzelm@48576
   195
  the directory is currently ``unfolded''. It can be folded by
wenzelm@48576
   196
  clicking on the directory name.  Clicking on the name for a second
wenzelm@48576
   197
  time unfolds the directory again.  Alternatively, a directory can
wenzelm@48576
   198
  also be unfolded by clicking on the corresponding node in the right
wenzelm@48576
   199
  sub-window.
wenzelm@48576
   200
wenzelm@48576
   201
  \item Blue arrows stand before ordinary node names. When clicking on
wenzelm@48576
   202
  such a name (i.e.\ that of a theory), the graph display window
wenzelm@48576
   203
  focuses to the corresponding node. Double clicking invokes a text
wenzelm@48576
   204
  viewer window in which the contents of the theory file are
wenzelm@48576
   205
  displayed.
wenzelm@48576
   206
wenzelm@48576
   207
  \end{itemize}
wenzelm@48576
   208
*}
wenzelm@48576
   209
wenzelm@48576
   210
wenzelm@48576
   211
subsubsection {* The graph display window *}
wenzelm@48576
   212
wenzelm@48576
   213
text {*
wenzelm@48576
   214
  When pointing on an ordinary node, an upward and a downward arrow is
wenzelm@48576
   215
  shown.  Initially, both of these arrows are green. Clicking on the
wenzelm@48576
   216
  upward or downward arrow collapses all predecessor or successor
wenzelm@48576
   217
  nodes, respectively. The arrow's color then changes to red,
wenzelm@48576
   218
  indicating that the predecessor or successor nodes are currently
wenzelm@48576
   219
  collapsed. The node corresponding to the collapsed nodes has the
wenzelm@48576
   220
  name ``@{verbatim "[....]"}''. To uncollapse the nodes again, simply
wenzelm@48576
   221
  click on the red arrow or on the node with the name ``@{verbatim
wenzelm@48576
   222
  "[....]"}''. Similar to the directory browser, the contents of
wenzelm@48576
   223
  theory files can be displayed by double clicking on the
wenzelm@48576
   224
  corresponding node.
wenzelm@48576
   225
*}
wenzelm@48576
   226
wenzelm@48576
   227
wenzelm@48576
   228
subsubsection {* The ``File'' menu *}
wenzelm@48576
   229
wenzelm@48576
   230
text {*
wenzelm@48576
   231
  Due to Java Applet security restrictions this menu is only available
wenzelm@48576
   232
  in the full application version. The meaning of the menu items is as
wenzelm@48576
   233
  follows:
wenzelm@48576
   234
wenzelm@48576
   235
  \begin{description}
wenzelm@48576
   236
wenzelm@48576
   237
  \item[Open \dots] Open a new graph file.
wenzelm@48576
   238
wenzelm@48576
   239
  \item[Export to PostScript] Outputs the current graph in Postscript
wenzelm@48576
   240
  format, appropriately scaled to fit on one single sheet of A4 paper.
wenzelm@48576
   241
  The resulting file can be printed directly.
wenzelm@48576
   242
wenzelm@48576
   243
  \item[Export to EPS] Outputs the current graph in Encapsulated
wenzelm@48576
   244
  Postscript format. The resulting file can be included in other
wenzelm@48576
   245
  documents.
wenzelm@48576
   246
wenzelm@48576
   247
  \item[Quit] Quit the graph browser.
wenzelm@48576
   248
wenzelm@48576
   249
  \end{description}
wenzelm@48576
   250
*}
wenzelm@48576
   251
wenzelm@48576
   252
wenzelm@48576
   253
subsection {* Syntax of graph definition files *}
wenzelm@48576
   254
wenzelm@48576
   255
text {*
wenzelm@48576
   256
  A graph definition file has the following syntax:
wenzelm@48576
   257
wenzelm@48576
   258
  \begin{center}\small
wenzelm@48576
   259
  \begin{tabular}{rcl}
wenzelm@48576
   260
    @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}+"} \\
wenzelm@48576
   261
    @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }*"}
wenzelm@48576
   262
  \end{tabular}
wenzelm@48576
   263
  \end{center}
wenzelm@48576
   264
wenzelm@48576
   265
  The meaning of the items in a vertex description is as follows:
wenzelm@48576
   266
wenzelm@48576
   267
  \begin{description}
wenzelm@48576
   268
wenzelm@48576
   269
  \item[@{text vertex_name}] The name of the vertex.
wenzelm@48576
   270
wenzelm@48576
   271
  \item[@{text vertex_ID}] The vertex identifier. Note that there may
wenzelm@48576
   272
  be several vertices with equal names, whereas identifiers must be
wenzelm@48576
   273
  unique.
wenzelm@48576
   274
wenzelm@48576
   275
  \item[@{text dir_name}] The name of the ``directory'' the vertex
wenzelm@48576
   276
  should be placed in.  A ``@{verbatim "+"}'' sign after @{text
wenzelm@48576
   277
  dir_name} indicates that the nodes in the directory are initially
wenzelm@48576
   278
  visible. Directories are initially invisible by default.
wenzelm@48576
   279
wenzelm@48576
   280
  \item[@{text path}] The path of the corresponding theory file. This
wenzelm@48576
   281
  is specified relatively to the path of the graph definition file.
wenzelm@48576
   282
wenzelm@48576
   283
  \item[List of successor/predecessor nodes] A ``@{verbatim "<"}''
wenzelm@48576
   284
  sign before the list means that successor nodes are listed, a
wenzelm@48576
   285
  ``@{verbatim ">"}'' sign means that predecessor nodes are listed. If
wenzelm@48576
   286
  neither ``@{verbatim "<"}'' nor ``@{verbatim ">"}'' is found, the
wenzelm@48576
   287
  browser assumes that successor nodes are listed.
wenzelm@48576
   288
wenzelm@48576
   289
  \end{description}
wenzelm@48576
   290
*}
wenzelm@48576
   291
wenzelm@28916
   292
end