# HG changeset patch
# User wenzelm
# Date 1207662434 -7200
# Node ID e6511a920168c0ceb1ecc4dbbab89daa556e9a12
# Parent  50f47cc2af72256300a058f3a8058be6fdc0ea11
removed isatool expandshort;
added isatool yxml;

diff -r 50f47cc2af72 -r e6511a920168 doc-src/System/misc.tex
--- 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"