--- a/doc-src/System/misc.tex Tue Apr 08 15:47:12 2008 +0200
+++ b/doc-src/System/misc.tex Tue Apr 08 15:47:14 2008 +0200
@@ -63,26 +63,6 @@
viewing \texttt{dvi} files is determined by the \texttt{DVI_VIEWER} setting.
-\section{Tuning proof scripts --- \texttt{isatool expandshort}}
-
-The \tooldx{expandshort} utility tunes {\ML} proof scripts to enhance
-readability:
-\begin{ttbox}
-Usage: expandshort [FILES|DIRS...]
-
- Recursively find .ML files, expand shorthand goal commands. Also
- contracts uses of resolve_tac, dresolve_tac, eresolve_tac,
- forward_tac, rewrite_goals_tac on 1-element lists; furthermore
- expands tabs, which are forbidden in SML string constants.
-
- Renames old versions of files by appending "~~".
-\end{ttbox}
-In the files or directories supplied as arguments, all occurrences of the
-shorthand commands \texttt{br}, \texttt{be} etc.\ in proof scripts are
-replaced with the corresponding full commands. The old versions of the files
-are renamed to have the suffix ``\verb'~~'''.
-
-
\section{Getting logic images --- \texttt{isatool findlogics}}
The \tooldx{findlogics} utility traverses all directories specified in
@@ -304,6 +284,44 @@
November 2007}''. There are no options nor arguments.
+\section{Convert XML to YXML --- \texttt{isatool yxml}}
+
+The \tooldx{yxml} utility converts a standard XML document (stdin) to
+the much simpler and more efficient YXML format of Isabelle (stdout).
+The YXML format is defined as follows.
+
+\begin{enumerate}
+
+\item The encoding is always UTF-8.
+
+\item Body text is represented verbatim (no escaping, no named
+ entities, no CDATA chunks, no comments).
+
+\item Markup elements are represented via ASCII control characters $X
+ = 5$ and $Y = 6$ as follows:
+
+ \begin{tabular}{ll}
+ XML & YXML \\\hline
+ \verb,<,\emph{name}~\emph{attribute}\verb,=,\emph{value}~\dots\verb,>, &
+ \emph{X\,Y\,name\,Y\,attribute}\verb,=,\emph{value}\dots\emph{X} \\
+ \verb,</,\emph{name}\verb,>, & \emph{X\,Y\,X} \\
+ \end{tabular}
+
+ There is no special case for empty body text, i.e.\ \verb,<foo/>, is
+ treated like \verb,<foo></foo>,. Also note that \emph{X} and
+ \emph{Y} may never occur in well-formed XML documents.
+
+\end{enumerate}
+
+Parsing YXML is pretty straight-forward: split the text into chunks
+separated by \emph{X}, then split each chunk into sub-chunks separated
+by \emph{Y}. Markup chunks start with an empty sub-chunk, and a
+second empty sub-chunk indicates close of an element. Any other chunk
+consists of plain text.
+
+YXML documents may be detected quickly by checking that the first two
+characters are \emph{X\,Y}.
+
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "system"