removed isatool expandshort;
authorwenzelm
Tue Apr 08 15:47:14 2008 +0200 (2008-04-08)
changeset 26578e6511a920168
parent 26577 50f47cc2af72
child 26579 13bbc72fda45
removed isatool expandshort;
added isatool yxml;
doc-src/System/misc.tex
     1.1 --- a/doc-src/System/misc.tex	Tue Apr 08 15:47:12 2008 +0200
     1.2 +++ b/doc-src/System/misc.tex	Tue Apr 08 15:47:14 2008 +0200
     1.3 @@ -63,26 +63,6 @@
     1.4  viewing \texttt{dvi} files is determined by the \texttt{DVI_VIEWER} setting.
     1.5  
     1.6  
     1.7 -\section{Tuning proof scripts --- \texttt{isatool expandshort}}
     1.8 -
     1.9 -The \tooldx{expandshort} utility tunes {\ML} proof scripts to enhance
    1.10 -readability:
    1.11 -\begin{ttbox}
    1.12 -Usage: expandshort [FILES|DIRS...]
    1.13 -
    1.14 -  Recursively find .ML files, expand shorthand goal commands.  Also
    1.15 -  contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
    1.16 -  forward_tac, rewrite_goals_tac on 1-element lists; furthermore
    1.17 -  expands tabs, which are forbidden in SML string constants.
    1.18 -
    1.19 -  Renames old versions of files by appending "~~".
    1.20 -\end{ttbox}
    1.21 -In the files or directories supplied as arguments, all occurrences of the
    1.22 -shorthand commands \texttt{br}, \texttt{be} etc.\ in proof scripts are
    1.23 -replaced with the corresponding full commands.  The old versions of the files
    1.24 -are renamed to have the suffix ``\verb'~~'''.
    1.25 -
    1.26 -
    1.27  \section{Getting logic images --- \texttt{isatool findlogics}}
    1.28  
    1.29  The \tooldx{findlogics} utility traverses all directories specified in
    1.30 @@ -304,6 +284,44 @@
    1.31    November 2007}''.  There are no options nor arguments.
    1.32  
    1.33  
    1.34 +\section{Convert XML to YXML --- \texttt{isatool yxml}}
    1.35 +
    1.36 +The \tooldx{yxml} utility converts a standard XML document (stdin) to
    1.37 +the much simpler and more efficient YXML format of Isabelle (stdout).
    1.38 +The YXML format is defined as follows.
    1.39 +
    1.40 +\begin{enumerate}
    1.41 +
    1.42 +\item The encoding is always UTF-8.
    1.43 +
    1.44 +\item Body text is represented verbatim (no escaping, no named
    1.45 +  entities, no CDATA chunks, no comments).
    1.46 +
    1.47 +\item Markup elements are represented via ASCII control characters $X
    1.48 +  = 5$ and $Y = 6$ as follows:
    1.49 +
    1.50 +  \begin{tabular}{ll}
    1.51 +    XML & YXML \\\hline
    1.52 +    \verb,<,\emph{name}~\emph{attribute}\verb,=,\emph{value}~\dots\verb,>, &
    1.53 +    \emph{X\,Y\,name\,Y\,attribute}\verb,=,\emph{value}\dots\emph{X} \\
    1.54 +    \verb,</,\emph{name}\verb,>, & \emph{X\,Y\,X} \\
    1.55 +  \end{tabular}
    1.56 +
    1.57 +  There is no special case for empty body text, i.e.\ \verb,<foo/>, is
    1.58 +  treated like \verb,<foo></foo>,.  Also note that \emph{X} and
    1.59 +  \emph{Y} may never occur in well-formed XML documents.
    1.60 +
    1.61 +\end{enumerate}
    1.62 +
    1.63 +Parsing YXML is pretty straight-forward: split the text into chunks
    1.64 +separated by \emph{X}, then split each chunk into sub-chunks separated
    1.65 +by \emph{Y}.  Markup chunks start with an empty sub-chunk, and a
    1.66 +second empty sub-chunk indicates close of an element.  Any other chunk
    1.67 +consists of plain text.
    1.68 +
    1.69 +YXML documents may be detected quickly by checking that the first two
    1.70 +characters are \emph{X\,Y}.
    1.71 +
    1.72  %%% Local Variables: 
    1.73  %%% mode: latex
    1.74  %%% TeX-master: "system"