59 corresponding document displayed. |
59 corresponding document displayed. |
60 |
60 |
61 \medskip The \texttt{ISABELLE_DOCS} setting specifies the list of directories |
61 \medskip The \texttt{ISABELLE_DOCS} setting specifies the list of directories |
62 (separated by colons) to be scanned for documentations. The program for |
62 (separated by colons) to be scanned for documentations. The program for |
63 viewing \texttt{dvi} files is determined by the \texttt{DVI_VIEWER} setting. |
63 viewing \texttt{dvi} files is determined by the \texttt{DVI_VIEWER} setting. |
64 |
|
65 |
|
66 \section{Tuning proof scripts --- \texttt{isatool expandshort}} |
|
67 |
|
68 The \tooldx{expandshort} utility tunes {\ML} proof scripts to enhance |
|
69 readability: |
|
70 \begin{ttbox} |
|
71 Usage: expandshort [FILES|DIRS...] |
|
72 |
|
73 Recursively find .ML files, expand shorthand goal commands. Also |
|
74 contracts uses of resolve_tac, dresolve_tac, eresolve_tac, |
|
75 forward_tac, rewrite_goals_tac on 1-element lists; furthermore |
|
76 expands tabs, which are forbidden in SML string constants. |
|
77 |
|
78 Renames old versions of files by appending "~~". |
|
79 \end{ttbox} |
|
80 In the files or directories supplied as arguments, all occurrences of the |
|
81 shorthand commands \texttt{br}, \texttt{be} etc.\ in proof scripts are |
|
82 replaced with the corresponding full commands. The old versions of the files |
|
83 are renamed to have the suffix ``\verb'~~'''. |
|
84 |
64 |
85 |
65 |
86 \section{Getting logic images --- \texttt{isatool findlogics}} |
66 \section{Getting logic images --- \texttt{isatool findlogics}} |
87 |
67 |
88 The \tooldx{findlogics} utility traverses all directories specified in |
68 The \tooldx{findlogics} utility traverses all directories specified in |
302 The \tooldx{version} utility outputs the full version string of the |
282 The \tooldx{version} utility outputs the full version string of the |
303 Isabelle distribution being used, e.g.\ ``\texttt{Isabelle2007: |
283 Isabelle distribution being used, e.g.\ ``\texttt{Isabelle2007: |
304 November 2007}''. There are no options nor arguments. |
284 November 2007}''. There are no options nor arguments. |
305 |
285 |
306 |
286 |
|
287 \section{Convert XML to YXML --- \texttt{isatool yxml}} |
|
288 |
|
289 The \tooldx{yxml} utility converts a standard XML document (stdin) to |
|
290 the much simpler and more efficient YXML format of Isabelle (stdout). |
|
291 The YXML format is defined as follows. |
|
292 |
|
293 \begin{enumerate} |
|
294 |
|
295 \item The encoding is always UTF-8. |
|
296 |
|
297 \item Body text is represented verbatim (no escaping, no named |
|
298 entities, no CDATA chunks, no comments). |
|
299 |
|
300 \item Markup elements are represented via ASCII control characters $X |
|
301 = 5$ and $Y = 6$ as follows: |
|
302 |
|
303 \begin{tabular}{ll} |
|
304 XML & YXML \\\hline |
|
305 \verb,<,\emph{name}~\emph{attribute}\verb,=,\emph{value}~\dots\verb,>, & |
|
306 \emph{X\,Y\,name\,Y\,attribute}\verb,=,\emph{value}\dots\emph{X} \\ |
|
307 \verb,</,\emph{name}\verb,>, & \emph{X\,Y\,X} \\ |
|
308 \end{tabular} |
|
309 |
|
310 There is no special case for empty body text, i.e.\ \verb,<foo/>, is |
|
311 treated like \verb,<foo></foo>,. Also note that \emph{X} and |
|
312 \emph{Y} may never occur in well-formed XML documents. |
|
313 |
|
314 \end{enumerate} |
|
315 |
|
316 Parsing YXML is pretty straight-forward: split the text into chunks |
|
317 separated by \emph{X}, then split each chunk into sub-chunks separated |
|
318 by \emph{Y}. Markup chunks start with an empty sub-chunk, and a |
|
319 second empty sub-chunk indicates close of an element. Any other chunk |
|
320 consists of plain text. |
|
321 |
|
322 YXML documents may be detected quickly by checking that the first two |
|
323 characters are \emph{X\,Y}. |
|
324 |
307 %%% Local Variables: |
325 %%% Local Variables: |
308 %%% mode: latex |
326 %%% mode: latex |
309 %%% TeX-master: "system" |
327 %%% TeX-master: "system" |
310 %%% End: |
328 %%% End: |