src/Doc/System/Misc.thy
author wenzelm
Wed Mar 25 11:39:52 2015 +0100 (2015-03-25)
changeset 59809 87641097d0f3
parent 58618 782f0b662cae
child 61406 eb2463fc4d7b
permissions -rw-r--r--
tuned signature;
wenzelm@28224
     1
theory Misc
wenzelm@43564
     2
imports Base
wenzelm@28224
     3
begin
wenzelm@28224
     4
wenzelm@58618
     5
chapter \<open>Miscellaneous tools \label{ch:tools}\<close>
wenzelm@28224
     6
wenzelm@58618
     7
text \<open>
wenzelm@28224
     8
  Subsequently we describe various Isabelle related utilities, given
wenzelm@28224
     9
  in alphabetical order.
wenzelm@58618
    10
\<close>
wenzelm@28224
    11
wenzelm@28224
    12
wenzelm@58618
    13
section \<open>Theory graph browser \label{sec:browse}\<close>
wenzelm@57330
    14
wenzelm@58618
    15
text \<open>The Isabelle graph browser is a general tool for visualizing
wenzelm@57330
    16
  dependency graphs.  Certain nodes of the graph (i.e.\ theories) can
wenzelm@57330
    17
  be grouped together in ``directories'', whose contents may be
wenzelm@57330
    18
  hidden, thus enabling the user to collapse irrelevant portions of
wenzelm@57330
    19
  information.  The browser is written in Java, it can be used both as
wenzelm@58618
    20
  a stand-alone application and as an applet.\<close>
wenzelm@57330
    21
wenzelm@57330
    22
wenzelm@58618
    23
subsection \<open>Invoking the graph browser\<close>
wenzelm@57330
    24
wenzelm@58618
    25
text \<open>The stand-alone version of the graph browser is wrapped up as
wenzelm@57330
    26
  @{tool_def browser}:
wenzelm@57330
    27
\begin{ttbox}
wenzelm@57330
    28
Usage: isabelle browser [OPTIONS] [GRAPHFILE]
wenzelm@57330
    29
wenzelm@57330
    30
  Options are:
wenzelm@57330
    31
    -b           Admin/build only
wenzelm@57330
    32
    -c           cleanup -- remove GRAPHFILE after use
wenzelm@57330
    33
    -o FILE      output to FILE (ps, eps, pdf)
wenzelm@57330
    34
\end{ttbox}
wenzelm@57330
    35
  When no file name is specified, the browser automatically changes to
wenzelm@57330
    36
  the directory @{setting ISABELLE_BROWSER_INFO}.
wenzelm@57330
    37
wenzelm@57330
    38
  \medskip The @{verbatim "-b"} option indicates that this is for
wenzelm@57330
    39
  administrative build only, i.e.\ no browser popup if no files are
wenzelm@57330
    40
  given.
wenzelm@57330
    41
wenzelm@57330
    42
  The @{verbatim "-c"} option causes the input file to be removed
wenzelm@57330
    43
  after use.
wenzelm@57330
    44
wenzelm@57330
    45
  The @{verbatim "-o"} option indicates batch-mode operation, with the
wenzelm@57330
    46
  output written to the indicated file; note that @{verbatim pdf}
wenzelm@57330
    47
  produces an @{verbatim eps} copy as well.
wenzelm@57330
    48
wenzelm@57330
    49
  \medskip The applet version of the browser is part of the standard
wenzelm@57330
    50
  WWW theory presentation, see the link ``theory dependencies'' within
wenzelm@57330
    51
  each session index.
wenzelm@58618
    52
\<close>
wenzelm@57330
    53
wenzelm@57330
    54
wenzelm@58618
    55
subsection \<open>Using the graph browser\<close>
wenzelm@57330
    56
wenzelm@58618
    57
text \<open>
wenzelm@57330
    58
  The browser's main window, which is shown in
wenzelm@57330
    59
  \figref{fig:browserwindow}, consists of two sub-windows.  In the
wenzelm@57330
    60
  left sub-window, the directory tree is displayed. The graph itself
wenzelm@57330
    61
  is displayed in the right sub-window.
wenzelm@57330
    62
wenzelm@57330
    63
  \begin{figure}[ht]
wenzelm@57330
    64
  \includegraphics[width=\textwidth]{browser_screenshot}
wenzelm@57330
    65
  \caption{\label{fig:browserwindow} Browser main window}
wenzelm@57330
    66
  \end{figure}
wenzelm@58618
    67
\<close>
wenzelm@57330
    68
wenzelm@57330
    69
wenzelm@58618
    70
subsubsection \<open>The directory tree window\<close>
wenzelm@57330
    71
wenzelm@58618
    72
text \<open>
wenzelm@57330
    73
  We describe the usage of the directory browser and the meaning of
wenzelm@57330
    74
  the different items in the browser window.
wenzelm@57330
    75
wenzelm@57330
    76
  \begin{itemize}
wenzelm@57330
    77
wenzelm@57330
    78
  \item A red arrow before a directory name indicates that the
wenzelm@57330
    79
  directory is currently ``folded'', i.e.~the nodes in this directory
wenzelm@57330
    80
  are collapsed to one single node. In the right sub-window, the names
wenzelm@57330
    81
  of nodes corresponding to folded directories are enclosed in square
wenzelm@57330
    82
  brackets and displayed in red color.
wenzelm@57330
    83
wenzelm@57330
    84
  \item A green downward arrow before a directory name indicates that
wenzelm@57330
    85
  the directory is currently ``unfolded''. It can be folded by
wenzelm@57330
    86
  clicking on the directory name.  Clicking on the name for a second
wenzelm@57330
    87
  time unfolds the directory again.  Alternatively, a directory can
wenzelm@57330
    88
  also be unfolded by clicking on the corresponding node in the right
wenzelm@57330
    89
  sub-window.
wenzelm@57330
    90
wenzelm@57330
    91
  \item Blue arrows stand before ordinary node names. When clicking on
wenzelm@57330
    92
  such a name (i.e.\ that of a theory), the graph display window
wenzelm@57330
    93
  focuses to the corresponding node. Double clicking invokes a text
wenzelm@57330
    94
  viewer window in which the contents of the theory file are
wenzelm@57330
    95
  displayed.
wenzelm@57330
    96
wenzelm@57330
    97
  \end{itemize}
wenzelm@58618
    98
\<close>
wenzelm@57330
    99
wenzelm@57330
   100
wenzelm@58618
   101
subsubsection \<open>The graph display window\<close>
wenzelm@57330
   102
wenzelm@58618
   103
text \<open>
wenzelm@57330
   104
  When pointing on an ordinary node, an upward and a downward arrow is
wenzelm@57330
   105
  shown.  Initially, both of these arrows are green. Clicking on the
wenzelm@57330
   106
  upward or downward arrow collapses all predecessor or successor
wenzelm@57330
   107
  nodes, respectively. The arrow's color then changes to red,
wenzelm@57330
   108
  indicating that the predecessor or successor nodes are currently
wenzelm@57330
   109
  collapsed. The node corresponding to the collapsed nodes has the
wenzelm@57330
   110
  name ``@{verbatim "[....]"}''. To uncollapse the nodes again, simply
wenzelm@57330
   111
  click on the red arrow or on the node with the name ``@{verbatim
wenzelm@57330
   112
  "[....]"}''. Similar to the directory browser, the contents of
wenzelm@57330
   113
  theory files can be displayed by double clicking on the
wenzelm@57330
   114
  corresponding node.
wenzelm@58618
   115
\<close>
wenzelm@57330
   116
wenzelm@57330
   117
wenzelm@58618
   118
subsubsection \<open>The ``File'' menu\<close>
wenzelm@57330
   119
wenzelm@58618
   120
text \<open>
wenzelm@57330
   121
  Due to Java Applet security restrictions this menu is only available
wenzelm@57330
   122
  in the full application version. The meaning of the menu items is as
wenzelm@57330
   123
  follows:
wenzelm@57330
   124
wenzelm@57330
   125
  \begin{description}
wenzelm@57330
   126
wenzelm@57330
   127
  \item[Open \dots] Open a new graph file.
wenzelm@57330
   128
wenzelm@57330
   129
  \item[Export to PostScript] Outputs the current graph in Postscript
wenzelm@57330
   130
  format, appropriately scaled to fit on one single sheet of A4 paper.
wenzelm@57330
   131
  The resulting file can be printed directly.
wenzelm@57330
   132
wenzelm@57330
   133
  \item[Export to EPS] Outputs the current graph in Encapsulated
wenzelm@57330
   134
  Postscript format. The resulting file can be included in other
wenzelm@57330
   135
  documents.
wenzelm@57330
   136
wenzelm@57330
   137
  \item[Quit] Quit the graph browser.
wenzelm@57330
   138
wenzelm@57330
   139
  \end{description}
wenzelm@58618
   140
\<close>
wenzelm@57330
   141
wenzelm@57330
   142
wenzelm@58618
   143
subsection \<open>Syntax of graph definition files\<close>
wenzelm@57330
   144
wenzelm@58618
   145
text \<open>
wenzelm@57330
   146
  A graph definition file has the following syntax:
wenzelm@57330
   147
wenzelm@57330
   148
  \begin{center}\small
wenzelm@57330
   149
  \begin{tabular}{rcl}
wenzelm@57330
   150
    @{text graph} & @{text "="} & @{text "{ vertex"}~@{verbatim ";"}~@{text "}+"} \\
wenzelm@57330
   151
    @{text vertex} & @{text "="} & @{text "vertex_name vertex_ID dir_name ["}~@{verbatim "+"}~@{text "] path ["}~@{verbatim "<"}~@{text "|"}~@{verbatim ">"}~@{text "] { vertex_ID }*"}
wenzelm@57330
   152
  \end{tabular}
wenzelm@57330
   153
  \end{center}
wenzelm@57330
   154
wenzelm@57330
   155
  The meaning of the items in a vertex description is as follows:
wenzelm@57330
   156
wenzelm@57330
   157
  \begin{description}
wenzelm@57330
   158
wenzelm@57330
   159
  \item[@{text vertex_name}] The name of the vertex.
wenzelm@57330
   160
wenzelm@57330
   161
  \item[@{text vertex_ID}] The vertex identifier. Note that there may
wenzelm@57330
   162
  be several vertices with equal names, whereas identifiers must be
wenzelm@57330
   163
  unique.
wenzelm@57330
   164
wenzelm@57330
   165
  \item[@{text dir_name}] The name of the ``directory'' the vertex
wenzelm@57330
   166
  should be placed in.  A ``@{verbatim "+"}'' sign after @{text
wenzelm@57330
   167
  dir_name} indicates that the nodes in the directory are initially
wenzelm@57330
   168
  visible. Directories are initially invisible by default.
wenzelm@57330
   169
wenzelm@57330
   170
  \item[@{text path}] The path of the corresponding theory file. This
wenzelm@57330
   171
  is specified relatively to the path of the graph definition file.
wenzelm@57330
   172
wenzelm@57330
   173
  \item[List of successor/predecessor nodes] A ``@{verbatim "<"}''
wenzelm@57330
   174
  sign before the list means that successor nodes are listed, a
wenzelm@57330
   175
  ``@{verbatim ">"}'' sign means that predecessor nodes are listed. If
wenzelm@57330
   176
  neither ``@{verbatim "<"}'' nor ``@{verbatim ">"}'' is found, the
wenzelm@57330
   177
  browser assumes that successor nodes are listed.
wenzelm@57330
   178
wenzelm@57330
   179
  \end{description}
wenzelm@58618
   180
\<close>
wenzelm@57330
   181
wenzelm@57330
   182
wenzelm@58618
   183
section \<open>Resolving Isabelle components \label{sec:tool-components}\<close>
wenzelm@48844
   184
wenzelm@58618
   185
text \<open>
wenzelm@48844
   186
  The @{tool_def components} tool resolves Isabelle components:
wenzelm@48844
   187
\begin{ttbox}
wenzelm@48844
   188
Usage: isabelle components [OPTIONS] [COMPONENTS ...]
wenzelm@48844
   189
wenzelm@48844
   190
  Options are:
wenzelm@50653
   191
    -I           init user settings
wenzelm@48844
   192
    -R URL       component repository
wenzelm@48844
   193
                 (default $ISABELLE_COMPONENT_REPOSITORY)
wenzelm@53435
   194
    -a           resolve all missing components
wenzelm@48844
   195
    -l           list status
wenzelm@48844
   196
wenzelm@48844
   197
  Resolve Isabelle components via download and installation.
wenzelm@48844
   198
  COMPONENTS are identified via base name.
wenzelm@48844
   199
wenzelm@48844
   200
  ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"
wenzelm@48844
   201
\end{ttbox}
wenzelm@48844
   202
wenzelm@48844
   203
  Components are initialized as described in \secref{sec:components}
wenzelm@48844
   204
  in a permissive manner, which can mark components as ``missing''.
wenzelm@48844
   205
  This state is amended by letting @{tool "components"} download and
wenzelm@48844
   206
  unpack components that are published on the default component
wenzelm@54703
   207
  repository @{url "http://isabelle.in.tum.de/components/"} in
wenzelm@48844
   208
  particular.
wenzelm@48844
   209
wenzelm@48844
   210
  Option @{verbatim "-R"} specifies an alternative component
wenzelm@48844
   211
  repository.  Note that @{verbatim "file:///"} URLs can be used for
wenzelm@48844
   212
  local directories.
wenzelm@48844
   213
wenzelm@48844
   214
  Option @{verbatim "-a"} selects all missing components to be
wenzelm@53435
   215
  resolved.  Explicit components may be named as command
wenzelm@48844
   216
  line-arguments as well.  Note that components are uniquely
wenzelm@48844
   217
  identified by their base name, while the installation takes place in
wenzelm@48844
   218
  the location that was specified in the attempt to initialize the
wenzelm@48844
   219
  component before.
wenzelm@48844
   220
wenzelm@48844
   221
  Option @{verbatim "-l"} lists the current state of available and
wenzelm@48844
   222
  missing components with their location (full name) within the
wenzelm@50653
   223
  file-system.
wenzelm@50653
   224
wenzelm@50653
   225
  Option @{verbatim "-I"} initializes the user settings file to
wenzelm@50653
   226
  subscribe to the standard components specified in the Isabelle
wenzelm@50653
   227
  repository clone --- this does not make any sense for regular
wenzelm@50653
   228
  Isabelle releases.  If the file already exists, it needs to be
wenzelm@50653
   229
  edited manually according to the printed explanation.
wenzelm@58618
   230
\<close>
wenzelm@48844
   231
wenzelm@48844
   232
wenzelm@58618
   233
section \<open>Raw ML console\<close>
wenzelm@57439
   234
wenzelm@58618
   235
text \<open>
wenzelm@57439
   236
  The @{tool_def console} tool runs the Isabelle process with raw ML console:
wenzelm@57439
   237
\begin{ttbox}
wenzelm@57439
   238
Usage: isabelle console [OPTIONS]
wenzelm@57439
   239
wenzelm@57439
   240
  Options are:
wenzelm@57439
   241
    -d DIR       include session directory
wenzelm@57439
   242
    -l NAME      logic session name (default ISABELLE_LOGIC)
wenzelm@57439
   243
    -m MODE      add print mode for output
wenzelm@57439
   244
    -n           no build of session image on startup
wenzelm@57439
   245
    -o OPTION    override Isabelle system OPTION (via NAME=VAL or NAME)
wenzelm@57439
   246
    -s           system build mode for session image
wenzelm@57439
   247
wenzelm@57439
   248
  Run Isabelle process with raw ML console and line editor
wenzelm@57439
   249
  (default ISABELLE_LINE_EDITOR).
wenzelm@57439
   250
\end{ttbox}
wenzelm@57439
   251
wenzelm@57439
   252
  The @{verbatim "-l"} option specifies the logic session name. By default,
wenzelm@57439
   253
  its heap image is checked and built on demand, but the option @{verbatim
wenzelm@57439
   254
  "-n"} skips that.
wenzelm@57439
   255
wenzelm@57439
   256
  Options @{verbatim "-d"}, @{verbatim "-o"}, @{verbatim "-s"} are passed
wenzelm@57439
   257
  directly to @{tool build} (\secref{sec:tool-build}).
wenzelm@57439
   258
wenzelm@57439
   259
  Options @{verbatim "-m"}, @{verbatim "-o"} are passed directly to the
wenzelm@57439
   260
  underlying Isabelle process (\secref{sec:isabelle-process}).
wenzelm@57439
   261
wenzelm@57439
   262
  The Isabelle process is run through the line editor that is specified via
wenzelm@57439
   263
  the settings variable @{setting ISABELLE_LINE_EDITOR} (e.g.\
wenzelm@57439
   264
  @{executable_def rlwrap} for GNU readline); the fall-back is to use plain
wenzelm@57439
   265
  standard input/output.
wenzelm@57439
   266
wenzelm@57439
   267
  Interaction works via the raw ML toplevel loop: this is neither
wenzelm@57439
   268
  Isabelle/Isar nor Isabelle/ML within the usual formal context. Some useful
wenzelm@57439
   269
  ML commands at this stage are @{ML cd}, @{ML pwd}, @{ML use}, @{ML use_thy},
wenzelm@57439
   270
  @{ML use_thys}.
wenzelm@58618
   271
\<close>
wenzelm@57439
   272
wenzelm@57439
   273
wenzelm@58618
   274
section \<open>Displaying documents \label{sec:tool-display}\<close>
wenzelm@28224
   275
wenzelm@58618
   276
text \<open>The @{tool_def display} tool displays documents in DVI or PDF
wenzelm@28224
   277
  format:
wenzelm@28224
   278
\begin{ttbox}
wenzelm@54683
   279
Usage: isabelle display DOCUMENT
wenzelm@28224
   280
wenzelm@54683
   281
  Display DOCUMENT (in DVI or PDF format).
wenzelm@28224
   282
\end{ttbox}
wenzelm@28224
   283
wenzelm@52444
   284
  \medskip The settings @{setting DVI_VIEWER} and @{setting
wenzelm@52444
   285
  PDF_VIEWER} determine the programs for viewing the corresponding
wenzelm@54683
   286
  file formats.  Normally this opens the document via the desktop
wenzelm@54683
   287
  environment, potentially in an asynchronous manner with re-use of
wenzelm@54683
   288
  previews views.
wenzelm@58618
   289
\<close>
wenzelm@28224
   290
wenzelm@28224
   291
wenzelm@58618
   292
section \<open>Viewing documentation \label{sec:tool-doc}\<close>
wenzelm@28224
   293
wenzelm@58618
   294
text \<open>
wenzelm@52444
   295
  The @{tool_def doc} tool displays Isabelle documentation:
wenzelm@28224
   296
\begin{ttbox}
wenzelm@52444
   297
Usage: isabelle doc [DOC ...]
wenzelm@28224
   298
wenzelm@52444
   299
  View Isabelle documentation.
wenzelm@28224
   300
\end{ttbox}
wenzelm@28224
   301
  If called without arguments, it lists all available documents. Each
wenzelm@28224
   302
  line starts with an identifier, followed by a short description. Any
wenzelm@52444
   303
  of these identifiers may be specified as arguments, in order to
wenzelm@52444
   304
  display the corresponding document (see also
wenzelm@52444
   305
  \secref{sec:tool-display}).
wenzelm@28224
   306
wenzelm@28224
   307
  \medskip The @{setting ISABELLE_DOCS} setting specifies the list of
wenzelm@28224
   308
  directories (separated by colons) to be scanned for documentations.
wenzelm@58618
   309
\<close>
wenzelm@28224
   310
wenzelm@28224
   311
wenzelm@58618
   312
section \<open>Shell commands within the settings environment \label{sec:tool-env}\<close>
wenzelm@47828
   313
wenzelm@58618
   314
text \<open>The @{tool_def env} tool is a direct wrapper for the standard
wenzelm@48602
   315
  @{verbatim "/usr/bin/env"} command on POSIX systems, running within
wenzelm@48602
   316
  the Isabelle settings environment (\secref{sec:settings}).
wenzelm@47828
   317
wenzelm@47828
   318
  The command-line arguments are that of the underlying version of
wenzelm@47828
   319
  @{verbatim env}.  For example, the following invokes an instance of
wenzelm@47828
   320
  the GNU Bash shell within the Isabelle environment:
wenzelm@47828
   321
\begin{alltt}
wenzelm@47828
   322
  isabelle env bash
wenzelm@47828
   323
\end{alltt}
wenzelm@58618
   324
\<close>
wenzelm@47828
   325
wenzelm@47828
   326
wenzelm@58618
   327
section \<open>Inspecting the settings environment \label{sec:tool-getenv}\<close>
wenzelm@28224
   328
wenzelm@58618
   329
text \<open>The Isabelle settings environment --- as provided by the
wenzelm@28224
   330
  site-default and user-specific settings files --- can be inspected
wenzelm@48602
   331
  with the @{tool_def getenv} tool:
wenzelm@28224
   332
\begin{ttbox}
wenzelm@48602
   333
Usage: isabelle getenv [OPTIONS] [VARNAMES ...]
wenzelm@28224
   334
wenzelm@28224
   335
  Options are:
wenzelm@28224
   336
    -a           display complete environment
wenzelm@28224
   337
    -b           print values only (doesn't work for -a)
wenzelm@31497
   338
    -d FILE      dump complete environment to FILE
wenzelm@31497
   339
                 (null terminated entries)
wenzelm@28224
   340
wenzelm@28224
   341
  Get value of VARNAMES from the Isabelle settings.
wenzelm@28224
   342
\end{ttbox}
wenzelm@28224
   343
wenzelm@28224
   344
  With the @{verbatim "-a"} option, one may inspect the full process
wenzelm@28224
   345
  environment that Isabelle related programs are run in. This usually
wenzelm@28224
   346
  contains much more variables than are actually Isabelle settings.
wenzelm@28224
   347
  Normally, output is a list of lines of the form @{text
wenzelm@28224
   348
  name}@{verbatim "="}@{text value}. The @{verbatim "-b"} option
wenzelm@28224
   349
  causes only the values to be printed.
wenzelm@31497
   350
wenzelm@31497
   351
  Option @{verbatim "-d"} produces a dump of the complete environment
wenzelm@31497
   352
  to the specified file.  Entries are terminated by the ASCII null
wenzelm@31497
   353
  character, i.e.\ the C string terminator.
wenzelm@58618
   354
\<close>
wenzelm@28224
   355
wenzelm@28224
   356
wenzelm@58618
   357
subsubsection \<open>Examples\<close>
wenzelm@28224
   358
wenzelm@58618
   359
text \<open>Get the location of @{setting ISABELLE_HOME_USER} where
wenzelm@48815
   360
  user-specific information is stored:
wenzelm@28224
   361
\begin{ttbox}
wenzelm@48815
   362
isabelle getenv ISABELLE_HOME_USER
wenzelm@28224
   363
\end{ttbox}
wenzelm@28224
   364
wenzelm@48815
   365
  \medskip Get the value only of the same settings variable, which is
wenzelm@48815
   366
particularly useful in shell scripts:
wenzelm@28224
   367
\begin{ttbox}
wenzelm@28504
   368
isabelle getenv -b ISABELLE_OUTPUT
wenzelm@28224
   369
\end{ttbox}
wenzelm@58618
   370
\<close>
wenzelm@28224
   371
wenzelm@28224
   372
wenzelm@58618
   373
section \<open>Installing standalone Isabelle executables \label{sec:tool-install}\<close>
wenzelm@28224
   374
wenzelm@58618
   375
text \<open>By default, the main Isabelle binaries (@{executable
wenzelm@48602
   376
  "isabelle"} etc.)  are just run from their location within the
wenzelm@48602
   377
  distribution directory, probably indirectly by the shell through its
wenzelm@48602
   378
  @{setting PATH}.  Other schemes of installation are supported by the
wenzelm@48602
   379
  @{tool_def install} tool:
wenzelm@28224
   380
\begin{ttbox}
wenzelm@50132
   381
Usage: isabelle install [OPTIONS] BINDIR
wenzelm@28224
   382
wenzelm@28224
   383
  Options are:
wenzelm@50132
   384
    -d DISTDIR   refer to DISTDIR as Isabelle distribution
wenzelm@28224
   385
                 (default ISABELLE_HOME)
wenzelm@28224
   386
wenzelm@50132
   387
  Install Isabelle executables with absolute references to the
wenzelm@28224
   388
  distribution directory.
wenzelm@28224
   389
\end{ttbox}
wenzelm@28224
   390
wenzelm@28224
   391
  The @{verbatim "-d"} option overrides the current Isabelle
wenzelm@28224
   392
  distribution directory as determined by @{setting ISABELLE_HOME}.
wenzelm@28224
   393
wenzelm@50132
   394
  The @{text BINDIR} argument tells where executable wrapper scripts
wenzelm@56439
   395
  for @{executable "isabelle_process"} and @{executable isabelle}
wenzelm@50132
   396
  should be placed, which is typically a directory in the shell's
wenzelm@50132
   397
  @{setting PATH}, such as @{verbatim "$HOME/bin"}.
wenzelm@48815
   398
wenzelm@50132
   399
  \medskip It is also possible to make symbolic links of the main
wenzelm@50132
   400
  Isabelle executables manually, but making separate copies outside
wenzelm@58618
   401
  the Isabelle distribution directory will not work!\<close>
wenzelm@28224
   402
wenzelm@28224
   403
wenzelm@58618
   404
section \<open>Creating instances of the Isabelle logo\<close>
wenzelm@28224
   405
wenzelm@58618
   406
text \<open>The @{tool_def logo} tool creates instances of the generic
wenzelm@49072
   407
  Isabelle logo as EPS and PDF, for inclusion in {\LaTeX} documents.
wenzelm@28224
   408
\begin{ttbox}
wenzelm@49072
   409
Usage: isabelle logo [OPTIONS] XYZ
wenzelm@28224
   410
wenzelm@49072
   411
  Create instance XYZ of the Isabelle logo (as EPS and PDF).
wenzelm@28224
   412
wenzelm@28224
   413
  Options are:
wenzelm@49072
   414
    -n NAME      alternative output base name (default "isabelle_xyx")
wenzelm@28224
   415
    -q           quiet mode
wenzelm@28224
   416
\end{ttbox}
wenzelm@48936
   417
wenzelm@49072
   418
  Option @{verbatim "-n"} specifies an altenative (base) name for the
wenzelm@49072
   419
  generated files.  The default is @{verbatim "isabelle_"}@{text xyz}
wenzelm@49072
   420
  in lower-case.
wenzelm@48936
   421
wenzelm@48936
   422
  Option @{verbatim "-q"} omits printing of the result file name.
wenzelm@48936
   423
wenzelm@48936
   424
  \medskip Implementors of Isabelle tools and applications are
wenzelm@48936
   425
  encouraged to make derived Isabelle logos for their own projects
wenzelm@58618
   426
  using this template.\<close>
wenzelm@28224
   427
wenzelm@28224
   428
wenzelm@58618
   429
section \<open>Output the version identifier of the Isabelle distribution\<close>
wenzelm@28224
   430
wenzelm@58618
   431
text \<open>
wenzelm@48602
   432
  The @{tool_def version} tool displays Isabelle version information:
wenzelm@41511
   433
\begin{ttbox}
wenzelm@41511
   434
Usage: isabelle version [OPTIONS]
wenzelm@41511
   435
wenzelm@41511
   436
  Options are:
wenzelm@41511
   437
    -i           short identification (derived from Mercurial id)
wenzelm@41511
   438
wenzelm@41511
   439
  Display Isabelle version information.
wenzelm@41511
   440
\end{ttbox}
wenzelm@41511
   441
wenzelm@41511
   442
  \medskip The default is to output the full version string of the
wenzelm@47827
   443
  Isabelle distribution, e.g.\ ``@{verbatim "Isabelle2012: May 2012"}.
wenzelm@41511
   444
wenzelm@41511
   445
  The @{verbatim "-i"} option produces a short identification derived
wenzelm@41511
   446
  from the Mercurial id of the @{setting ISABELLE_HOME} directory.
wenzelm@58618
   447
\<close>
wenzelm@28224
   448
wenzelm@28224
   449
wenzelm@58618
   450
section \<open>Convert XML to YXML\<close>
wenzelm@28224
   451
wenzelm@58618
   452
text \<open>
wenzelm@28224
   453
  The @{tool_def yxml} tool converts a standard XML document (stdin)
wenzelm@28224
   454
  to the much simpler and more efficient YXML format of Isabelle
wenzelm@28224
   455
  (stdout).  The YXML format is defined as follows.
wenzelm@28224
   456
wenzelm@28224
   457
  \begin{enumerate}
wenzelm@28224
   458
wenzelm@28224
   459
  \item The encoding is always UTF-8.
wenzelm@28224
   460
wenzelm@28224
   461
  \item Body text is represented verbatim (no escaping, no special
wenzelm@28224
   462
  treatment of white space, no named entities, no CDATA chunks, no
wenzelm@28224
   463
  comments).
wenzelm@28224
   464
wenzelm@28224
   465
  \item Markup elements are represented via ASCII control characters
wenzelm@28224
   466
  @{text "\<^bold>X = 5"} and @{text "\<^bold>Y = 6"} as follows:
wenzelm@28224
   467
wenzelm@28224
   468
  \begin{tabular}{ll}
wenzelm@28224
   469
    XML & YXML \\\hline
wenzelm@28224
   470
    @{verbatim "<"}@{text "name attribute"}@{verbatim "="}@{text "value \<dots>"}@{verbatim ">"} &
wenzelm@28224
   471
    @{text "\<^bold>X\<^bold>Yname\<^bold>Yattribute"}@{verbatim "="}@{text "value\<dots>\<^bold>X"} \\
wenzelm@28224
   472
    @{verbatim "</"}@{text name}@{verbatim ">"} & @{text "\<^bold>X\<^bold>Y\<^bold>X"} \\
wenzelm@28224
   473
  \end{tabular}
wenzelm@28224
   474
wenzelm@28224
   475
  There is no special case for empty body text, i.e.\ @{verbatim
wenzelm@28224
   476
  "<foo/>"} is treated like @{verbatim "<foo></foo>"}.  Also note that
wenzelm@28224
   477
  @{text "\<^bold>X"} and @{text "\<^bold>Y"} may never occur in
wenzelm@28224
   478
  well-formed XML documents.
wenzelm@28224
   479
wenzelm@28224
   480
  \end{enumerate}
wenzelm@28224
   481
wenzelm@28224
   482
  Parsing YXML is pretty straight-forward: split the text into chunks
wenzelm@28224
   483
  separated by @{text "\<^bold>X"}, then split each chunk into
wenzelm@28224
   484
  sub-chunks separated by @{text "\<^bold>Y"}.  Markup chunks start
wenzelm@28224
   485
  with an empty sub-chunk, and a second empty sub-chunk indicates
wenzelm@28224
   486
  close of an element.  Any other non-empty chunk consists of plain
wenzelm@44799
   487
  text.  For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or
wenzelm@44799
   488
  @{file "~~/src/Pure/PIDE/yxml.scala"}.
wenzelm@28224
   489
wenzelm@28224
   490
  YXML documents may be detected quickly by checking that the first
wenzelm@28224
   491
  two characters are @{text "\<^bold>X\<^bold>Y"}.
wenzelm@58618
   492
\<close>
wenzelm@28224
   493
wenzelm@28224
   494
end