Commit 30889940 authored by Michael Banken's avatar Michael Banken

added xml spec

parent 75721da1
......@@ -113,3 +113,30 @@ The functionality of the buttons remains the same as in the case above.
\subsection{XML}
\label{sec:xml}
As mentioned above the method toXML serves to transcribe the suggested changes into a human readable form.
The output is an xml subset generated by the following grammar.
\begin{lstlisting}
SUGGESTIONS ::= THEORY_SUGGESTIONS
THEORY_SUGGESTIONS ::= <theory MPath = MPATH> SUGGESTIONSBODY </theory>
SUGGESTIONSBODY ::= REMOVE
\| REPLACE
REMOVE ::= <removeInclusion MPath = MPATH>
REPLACE ::= <replaceInclusion MPath = MPATH>REPLACMENT</replaceInclusion>
REPLACEMENT ::= <replacement MPath = MPATH>
\end{lstlisting}
MPATH should be a valid MPath addressing a theory.
The MPath attribute of the theory tag names the theory where the changes should occur.
The removeInclusion tags mark a theory that can be removed entirely, ie. a simply redundant or purely superfluous inclusion. Again the MPath attribute names the theory to be removed.
The replaceInclusion tags contain any number of replacements tags. The MPath attributes of replaceInclusion tags name the theory to be replaced, while the attributes of the replacement tags name the theories with which that theory is to be replaced.
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment