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