src/Doc/System/Misc.thy
author wenzelm
Sat, 05 Apr 2014 15:03:40 +0200
changeset 56421 1ffd7eaa778b
parent 54703 499f92dc6e45
child 56439 95e2656b3b23
permissions -rw-r--r--
updated to jedit_build-20140405: Code2HTML.jar, CommonControls.jar, Console.jar, kappalayout.jar, Navigator.jar, SideKick.jar, doc with jEdit manuals (ant dist-manuals);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     1
theory Misc
43564
9864182c6bad document antiquotations are managed as theory data, with proper name space and entity markup;
wenzelm
parents: 41512
diff changeset
     2
imports Base
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     3
begin
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     4
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     5
chapter {* Miscellaneous tools \label{ch:tools} *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     6
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     7
text {*
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     8
  Subsequently we describe various Isabelle related utilities, given
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
     9
  in alphabetical order.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    10
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    11
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    12
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    13
section {* Resolving Isabelle components \label{sec:tool-components} *}
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    14
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    15
text {*
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    16
  The @{tool_def components} tool resolves Isabelle components:
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    17
\begin{ttbox}
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    18
Usage: isabelle components [OPTIONS] [COMPONENTS ...]
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    19
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    20
  Options are:
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 50132
diff changeset
    21
    -I           init user settings
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    22
    -R URL       component repository
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    23
                 (default $ISABELLE_COMPONENT_REPOSITORY)
53435
wenzelm
parents: 52550
diff changeset
    24
    -a           resolve all missing components
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    25
    -l           list status
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    26
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    27
  Resolve Isabelle components via download and installation.
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    28
  COMPONENTS are identified via base name.
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    29
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    30
  ISABELLE_COMPONENT_REPOSITORY="http://isabelle.in.tum.de/components"
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    31
\end{ttbox}
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    32
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    33
  Components are initialized as described in \secref{sec:components}
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    34
  in a permissive manner, which can mark components as ``missing''.
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    35
  This state is amended by letting @{tool "components"} download and
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    36
  unpack components that are published on the default component
54703
499f92dc6e45 more antiquotations;
wenzelm
parents: 54683
diff changeset
    37
  repository @{url "http://isabelle.in.tum.de/components/"} in
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    38
  particular.
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    39
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    40
  Option @{verbatim "-R"} specifies an alternative component
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    41
  repository.  Note that @{verbatim "file:///"} URLs can be used for
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    42
  local directories.
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    43
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    44
  Option @{verbatim "-a"} selects all missing components to be
53435
wenzelm
parents: 52550
diff changeset
    45
  resolved.  Explicit components may be named as command
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    46
  line-arguments as well.  Note that components are uniquely
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    47
  identified by their base name, while the installation takes place in
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    48
  the location that was specified in the attempt to initialize the
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    49
  component before.
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    50
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    51
  Option @{verbatim "-l"} lists the current state of available and
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    52
  missing components with their location (full name) within the
50653
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 50132
diff changeset
    53
  file-system.
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 50132
diff changeset
    54
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 50132
diff changeset
    55
  Option @{verbatim "-I"} initializes the user settings file to
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 50132
diff changeset
    56
  subscribe to the standard components specified in the Isabelle
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 50132
diff changeset
    57
  repository clone --- this does not make any sense for regular
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 50132
diff changeset
    58
  Isabelle releases.  If the file already exists, it needs to be
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 50132
diff changeset
    59
  edited manually according to the printed explanation.
5c85f8b80b95 simplified quick start via "isabelle components -I";
wenzelm
parents: 50132
diff changeset
    60
*}
48844
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    61
6408fb6f7d81 some explanations on isabelle components;
wenzelm
parents: 48815
diff changeset
    62
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52052
diff changeset
    63
section {* Displaying documents \label{sec:tool-display} *}
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    64
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
    65
text {* The @{tool_def display} tool displays documents in DVI or PDF
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    66
  format:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    67
\begin{ttbox}
54683
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 53435
diff changeset
    68
Usage: isabelle display DOCUMENT
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    69
54683
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 53435
diff changeset
    70
  Display DOCUMENT (in DVI or PDF format).
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    71
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    72
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52052
diff changeset
    73
  \medskip The settings @{setting DVI_VIEWER} and @{setting
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52052
diff changeset
    74
  PDF_VIEWER} determine the programs for viewing the corresponding
54683
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 53435
diff changeset
    75
  file formats.  Normally this opens the document via the desktop
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 53435
diff changeset
    76
  environment, potentially in an asynchronous manner with re-use of
cf48ddc266e5 clarified "isabelle display" and 'display_drafts': re-use file and program instance, open asynchronously via desktop environment;
wenzelm
parents: 53435
diff changeset
    77
  previews views.
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    78
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    79
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    80
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    81
section {* Viewing documentation \label{sec:tool-doc} *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    82
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    83
text {*
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52052
diff changeset
    84
  The @{tool_def doc} tool displays Isabelle documentation:
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    85
\begin{ttbox}
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52052
diff changeset
    86
Usage: isabelle doc [DOC ...]
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    87
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52052
diff changeset
    88
  View Isabelle documentation.
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    89
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    90
  If called without arguments, it lists all available documents. Each
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    91
  line starts with an identifier, followed by a short description. Any
52444
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52052
diff changeset
    92
  of these identifiers may be specified as arguments, in order to
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52052
diff changeset
    93
  display the corresponding document (see also
2cfe6656d6d6 slightly improved "isabelle doc" based on Isabelle/Scala;
wenzelm
parents: 52052
diff changeset
    94
  \secref{sec:tool-display}).
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    95
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    96
  \medskip The @{setting ISABELLE_DOCS} setting specifies the list of
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    97
  directories (separated by colons) to be scanned for documentations.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    98
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
    99
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   100
47828
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   101
section {* Shell commands within the settings environment \label{sec:tool-env} *}
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   102
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   103
text {* The @{tool_def env} tool is a direct wrapper for the standard
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   104
  @{verbatim "/usr/bin/env"} command on POSIX systems, running within
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   105
  the Isabelle settings environment (\secref{sec:settings}).
47828
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   106
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   107
  The command-line arguments are that of the underlying version of
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   108
  @{verbatim env}.  For example, the following invokes an instance of
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   109
  the GNU Bash shell within the Isabelle environment:
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   110
\begin{alltt}
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   111
  isabelle env bash
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   112
\end{alltt}
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   113
*}
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   114
e6e1b670520b some coverage of isabelle env;
wenzelm
parents: 47827
diff changeset
   115
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   116
section {* Getting logic images *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   117
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   118
text {* The @{tool_def findlogics} tool traverses all directories
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   119
  specified in @{setting ISABELLE_PATH}, looking for Isabelle logic
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   120
  images. Its usage is:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   121
\begin{ttbox}
48577
wenzelm
parents: 47828
diff changeset
   122
Usage: isabelle findlogics
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   123
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   124
  Collect heap file names from ISABELLE_PATH.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   125
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   126
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   127
  The base names of all files found on the path are printed --- sorted
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   128
  and with duplicates removed. Also note that lookup in @{setting
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   129
  ISABELLE_PATH} includes the current values of @{setting ML_SYSTEM}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   130
  and @{setting ML_PLATFORM}. Thus switching to another ML compiler
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   131
  may change the set of logic images available.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   132
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   133
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   134
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   135
section {* Inspecting the settings environment \label{sec:tool-getenv} *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   136
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   137
text {* The Isabelle settings environment --- as provided by the
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   138
  site-default and user-specific settings files --- can be inspected
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   139
  with the @{tool_def getenv} tool:
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   140
\begin{ttbox}
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   141
Usage: isabelle getenv [OPTIONS] [VARNAMES ...]
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   142
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   143
  Options are:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   144
    -a           display complete environment
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   145
    -b           print values only (doesn't work for -a)
31497
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   146
    -d FILE      dump complete environment to FILE
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   147
                 (null terminated entries)
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   148
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   149
  Get value of VARNAMES from the Isabelle settings.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   150
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   151
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   152
  With the @{verbatim "-a"} option, one may inspect the full process
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   153
  environment that Isabelle related programs are run in. This usually
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   154
  contains much more variables than are actually Isabelle settings.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   155
  Normally, output is a list of lines of the form @{text
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   156
  name}@{verbatim "="}@{text value}. The @{verbatim "-b"} option
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   157
  causes only the values to be printed.
31497
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   158
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   159
  Option @{verbatim "-d"} produces a dump of the complete environment
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   160
  to the specified file.  Entries are terminated by the ASCII null
5333aa739082 isabelle getenv: option -d;
wenzelm
parents: 28916
diff changeset
   161
  character, i.e.\ the C string terminator.
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   162
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   163
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   164
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   165
subsubsection {* Examples *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   166
48815
wenzelm
parents: 48814
diff changeset
   167
text {* Get the location of @{setting ISABELLE_HOME_USER} where
wenzelm
parents: 48814
diff changeset
   168
  user-specific information is stored:
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   169
\begin{ttbox}
48815
wenzelm
parents: 48814
diff changeset
   170
isabelle getenv ISABELLE_HOME_USER
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   171
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   172
48815
wenzelm
parents: 48814
diff changeset
   173
  \medskip Get the value only of the same settings variable, which is
wenzelm
parents: 48814
diff changeset
   174
particularly useful in shell scripts:
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   175
\begin{ttbox}
28504
7ad7d7d6df47 simplified main Isabelle executables: removed Isabelle and isabelle (replaced by isabelle-process), renamed isatool to isabelle;
wenzelm
parents: 28253
diff changeset
   176
isabelle getenv -b ISABELLE_OUTPUT
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   177
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   178
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   179
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   180
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   181
section {* Installing standalone Isabelle executables \label{sec:tool-install} *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   182
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   183
text {* By default, the main Isabelle binaries (@{executable
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   184
  "isabelle"} etc.)  are just run from their location within the
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   185
  distribution directory, probably indirectly by the shell through its
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   186
  @{setting PATH}.  Other schemes of installation are supported by the
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   187
  @{tool_def install} tool:
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   188
\begin{ttbox}
50132
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   189
Usage: isabelle install [OPTIONS] BINDIR
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   190
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   191
  Options are:
50132
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   192
    -d DISTDIR   refer to DISTDIR as Isabelle distribution
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   193
                 (default ISABELLE_HOME)
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   194
50132
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   195
  Install Isabelle executables with absolute references to the
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   196
  distribution directory.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   197
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   198
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   199
  The @{verbatim "-d"} option overrides the current Isabelle
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   200
  distribution directory as determined by @{setting ISABELLE_HOME}.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   201
50132
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   202
  The @{text BINDIR} argument tells where executable wrapper scripts
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   203
  for @{executable "isabelle-process"} and @{executable isabelle}
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   204
  should be placed, which is typically a directory in the shell's
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   205
  @{setting PATH}, such as @{verbatim "$HOME/bin"}.
48815
wenzelm
parents: 48814
diff changeset
   206
50132
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   207
  \medskip It is also possible to make symbolic links of the main
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   208
  Isabelle executables manually, but making separate copies outside
180d086c30dd simplified command line of "isabelle install";
wenzelm
parents: 49072
diff changeset
   209
  the Isabelle distribution directory will not work!  *}
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   210
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   211
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   212
section {* Creating instances of the Isabelle logo *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   213
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48985
diff changeset
   214
text {* The @{tool_def logo} tool creates instances of the generic
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48985
diff changeset
   215
  Isabelle logo as EPS and PDF, for inclusion in {\LaTeX} documents.
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   216
\begin{ttbox}
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48985
diff changeset
   217
Usage: isabelle logo [OPTIONS] XYZ
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   218
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48985
diff changeset
   219
  Create instance XYZ of the Isabelle logo (as EPS and PDF).
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   220
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   221
  Options are:
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48985
diff changeset
   222
    -n NAME      alternative output base name (default "isabelle_xyx")
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   223
    -q           quiet mode
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   224
\end{ttbox}
48936
e6d9e46ff7bc clarified "isabelle logo";
wenzelm
parents: 48844
diff changeset
   225
49072
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48985
diff changeset
   226
  Option @{verbatim "-n"} specifies an altenative (base) name for the
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48985
diff changeset
   227
  generated files.  The default is @{verbatim "isabelle_"}@{text xyz}
747835eb2782 "isabelle logo" produces EPS and PDF format simultaneously;
wenzelm
parents: 48985
diff changeset
   228
  in lower-case.
48936
e6d9e46ff7bc clarified "isabelle logo";
wenzelm
parents: 48844
diff changeset
   229
e6d9e46ff7bc clarified "isabelle logo";
wenzelm
parents: 48844
diff changeset
   230
  Option @{verbatim "-q"} omits printing of the result file name.
e6d9e46ff7bc clarified "isabelle logo";
wenzelm
parents: 48844
diff changeset
   231
e6d9e46ff7bc clarified "isabelle logo";
wenzelm
parents: 48844
diff changeset
   232
  \medskip Implementors of Isabelle tools and applications are
e6d9e46ff7bc clarified "isabelle logo";
wenzelm
parents: 48844
diff changeset
   233
  encouraged to make derived Isabelle logos for their own projects
e6d9e46ff7bc clarified "isabelle logo";
wenzelm
parents: 48844
diff changeset
   234
  using this template.  *}
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   235
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   236
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   237
section {* Remove awkward symbol names from theory sources *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   238
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   239
text {*
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   240
  The @{tool_def unsymbolize} tool tunes Isabelle theory sources to
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   241
  improve readability for plain ASCII output (e.g.\ in email
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   242
  communication).  Most notably, @{tool unsymbolize} replaces awkward
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   243
  arrow symbols such as @{verbatim "\\"}@{verbatim "<Longrightarrow>"}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   244
  by @{verbatim "==>"}.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   245
\begin{ttbox}
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   246
Usage: isabelle unsymbolize [FILES|DIRS...]
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   247
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   248
  Recursively find .thy/.ML files, removing unreadable symbol names.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   249
  Note: this is an ad-hoc script; there is no systematic way to replace
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   250
  symbols independently of the inner syntax of a theory!
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   251
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   252
  Renames old versions of FILES by appending "~~".
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   253
\end{ttbox}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   254
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   255
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   256
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   257
section {* Output the version identifier of the Isabelle distribution *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   258
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   259
text {*
48602
342ca8f3197b more uniform usage of "isabelle tool";
wenzelm
parents: 48577
diff changeset
   260
  The @{tool_def version} tool displays Isabelle version information:
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   261
\begin{ttbox}
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   262
Usage: isabelle version [OPTIONS]
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   263
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   264
  Options are:
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   265
    -i           short identification (derived from Mercurial id)
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   266
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   267
  Display Isabelle version information.
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   268
\end{ttbox}
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   269
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   270
  \medskip The default is to output the full version string of the
47827
13530d774a21 updated system manual for release;
wenzelm
parents: 44799
diff changeset
   271
  Isabelle distribution, e.g.\ ``@{verbatim "Isabelle2012: May 2012"}.
41511
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   272
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   273
  The @{verbatim "-i"} option produces a short identification derived
2fe62d602681 isabelle version -i;
wenzelm
parents: 40800
diff changeset
   274
  from the Mercurial id of the @{setting ISABELLE_HOME} directory.
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   275
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   276
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   277
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   278
section {* Convert XML to YXML *}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   279
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   280
text {*
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   281
  The @{tool_def yxml} tool converts a standard XML document (stdin)
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   282
  to the much simpler and more efficient YXML format of Isabelle
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   283
  (stdout).  The YXML format is defined as follows.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   284
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   285
  \begin{enumerate}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   286
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   287
  \item The encoding is always UTF-8.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   288
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   289
  \item Body text is represented verbatim (no escaping, no special
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   290
  treatment of white space, no named entities, no CDATA chunks, no
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   291
  comments).
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   292
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   293
  \item Markup elements are represented via ASCII control characters
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   294
  @{text "\<^bold>X = 5"} and @{text "\<^bold>Y = 6"} as follows:
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   295
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   296
  \begin{tabular}{ll}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   297
    XML & YXML \\\hline
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   298
    @{verbatim "<"}@{text "name attribute"}@{verbatim "="}@{text "value \<dots>"}@{verbatim ">"} &
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   299
    @{text "\<^bold>X\<^bold>Yname\<^bold>Yattribute"}@{verbatim "="}@{text "value\<dots>\<^bold>X"} \\
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   300
    @{verbatim "</"}@{text name}@{verbatim ">"} & @{text "\<^bold>X\<^bold>Y\<^bold>X"} \\
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   301
  \end{tabular}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   302
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   303
  There is no special case for empty body text, i.e.\ @{verbatim
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   304
  "<foo/>"} is treated like @{verbatim "<foo></foo>"}.  Also note that
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   305
  @{text "\<^bold>X"} and @{text "\<^bold>Y"} may never occur in
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   306
  well-formed XML documents.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   307
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   308
  \end{enumerate}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   309
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   310
  Parsing YXML is pretty straight-forward: split the text into chunks
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   311
  separated by @{text "\<^bold>X"}, then split each chunk into
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   312
  sub-chunks separated by @{text "\<^bold>Y"}.  Markup chunks start
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   313
  with an empty sub-chunk, and a second empty sub-chunk indicates
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   314
  close of an element.  Any other non-empty chunk consists of plain
44799
1fd0a1276a09 updated file locations;
wenzelm
parents: 43564
diff changeset
   315
  text.  For example, see @{file "~~/src/Pure/PIDE/yxml.ML"} or
1fd0a1276a09 updated file locations;
wenzelm
parents: 43564
diff changeset
   316
  @{file "~~/src/Pure/PIDE/yxml.scala"}.
28224
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   317
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   318
  YXML documents may be detected quickly by checking that the first
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   319
  two characters are @{text "\<^bold>X\<^bold>Y"}.
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   320
*}
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   321
10487d954a8f converted misc.tex;
wenzelm
parents:
diff changeset
   322
end