Figure 9: ``Domain Editor'' web page for direct editing of domain definitions. The existing definitions are displayed in a text box and can be changed therein. Before a changed definition is added to the database, it is checked for consistency and errors.
\includegraphics[scale=1.3]{figures/domain-editor.eps}