stex (7apr16)

git-svn-id: svn://tug.org/texlive/trunk@40320 c570f23f-e606-0410-a88d-b1316a301751

2 files changed, 361 insertions, 635 deletions

diff --git a/Master/texmf-dist/source/latex/stex/statements/statements.dtx b/Master/texmf-dist/source/latex/stex/statements/statements.dtx
index 05a9c950a2a..77966fa356c 100644
--- a/Master/texmf-dist/source/latex/stex/statements/statements.dtx
+++ b/Master/texmf-dist/source/latex/stex/statements/statements.dtx
@@ -4,28 +4,28 @@
 %               this file is released under the
 %               LaTeX Project Public License (LPPL)
 %
-% The development version of this file can be found at
-% $HeadURL: https://svn.kwarc.info/repos/stex/trunk/sty/statements/statements.dtx $
+% The original of this file is in the public repository at 
+% http://github.com/KWARC/sTeX/
 % \fi
 %  
 % \iffalse
 %<package>\NeedsTeXFormat{LaTeX2e}[1999/12/01]
-%<package>\ProvidesPackage{statements}[2012/01/28 v1.1 Semantic Markup for Statements]
+%<package>\ProvidesPackage{statements}[2016/04/07 v1.2 Semantic Markup for Statements]
 %
 %<*driver>
 \documentclass{ltxdoc}
 \usepackage{url,array,float,amsfonts}
-\usepackage{statements,modules,presentation}
+\usepackage{statements,presentation}
 \usepackage{paralist}
 \usepackage[show]{ed}
 \usepackage[hyperref=auto,style=alphabetic]{biblatex}
-\bibliography{kwarc}
-\usepackage[eso-foot,today]{svninfo}
+\addbibresource{kwarcpubs.bib}
+\addbibresource{extpubs.bib}
+\addbibresource{kwarccrossrefs.bib}
+\addbibresource{extcrossrefs.bib}
 \usepackage{stex-logo}
-\usepackage{../ctansvn}
+\usepackage{ctangit}
 \usepackage{hyperref}
-\svnInfo $Id: statements.dtx 1999 2012-01-28 07:32:11Z kohlhase $
-\svnKeyword $HeadURL: https://svn.kwarc.info/repos/stex/trunk/sty/statements/statements.dtx $
 \makeindex
 \floatstyle{boxed}
 \newfloat{exfig}{thp}{lop}
@@ -35,7 +35,7 @@
 %</driver>
 % \fi
 % 
-% \CheckSum{597}
+% \CheckSum{809}
 %
 % \changes{v0.9}{2005/06/14}{First Version with Documentation}
 % \changes{v0.9a}{2005/07/01}{Completed Documentation}
@@ -54,6 +54,12 @@
 % \changes{v1.0}{2010/07/13}{adding {\texttt{\textbackslash inlineex}}}
 % \changes{v1.1}{2011/08/25}{renaming all convenience macros for {\texttt{\textbackslash
 % definendum}} and {\texttt{\textbackslash termref}}}
+% \changes{v1.1}{2012/07/06}{adding \texttt{\textbackslash usevocab} to example for importing}
+% \changes{v1.1}{2013/05/17}{more support for types: \texttt{typedec} and
+% \texttt{\textbackslash inlinetypedec}}
+% \changes{v1.2}{2015/04/03}{adding optional last arg to \texttt{\textbackslash \*defi*}}
+% \changes{v1.2}{2015/04/17}{adding \texttt{\textbackslash inlineass}}
+% \changes{v1.2}{2015/09/05}{adding \texttt{\textbackslash defis} and friends}
 % 
 % \GetFileInfo{statements.sty}
 % 
@@ -99,10 +105,10 @@
 % the {\sTeX} sources, or after translation. Even though it is part of the {\stex}
 % collection, it can be used independently, like it's sister package |sproofs|.
 %
-% {\stex}~\cite{Kohlhase:ulsmf08,sTeX:online} is a version of {\TeX/\LaTeX} that allows
-% to markup {\TeX/\LaTeX} documents semantically without leaving the document format,
+% {\stex}~\cite{Kohlhase:ulsmf08,sTeX:online} is a version of {\TeX/\LaTeX} that allows to
+% markup {\TeX/\LaTeX} documents semantically without leaving the document format,
 % essentially turning {\TeX/\LaTeX} into a document format for mathematical knowledge
-% management (MKM). Currently the {\omdoc} format~\cite{Kohlhase:omdoc1.2} is directly
+% management (MKM). Currently the {\omdoc} format~\cite{Kohlhase:OMDoc1.2} is directly
 % supported.
 % 
 % \section{The User Interface}\label{sec:user-interface}
@@ -116,9 +122,11 @@
 %
 % \subsection{Package Options}\label{sec:user:options}
 % 
-% The |statements| package takes a single option: \DescribeMacro{showmeta}|showmeta|. If
-% this is set, then the metadata keys are shown (see~\cite{Kohlhase:metakeys:ctan} for details
-% and customization options).
+% The |statements| package provides the |defindex| option to \sTeX. If this is set, then
+% definienda are automatically passed into the index of the document. Furthermore, the
+% |statements| package passes the \DescribeMacro{showmeta}|showmeta| to the |metakeys|
+% package. If this is set, then the metadata keys are shown
+% (see~\cite{Kohlhase:metakeys:ctan} for details and customization options).
 %
 % \subsection{Statements}\label{sec:statements}
 % 
@@ -133,7 +141,7 @@
 %   with the surrounding text.
 % \end{description}
 % Since they have the same semantic status, they must both be marked up, but styled
-% differently. We distinguis between these two presentational forms with the
+% differently. We distinguish between these two presentational forms with the
 % \DescribeMacro{display=}|display| key, which is allowed on all statement
 % environments. If it has the value |block| (the default), then the statement will be
 % presented in a paragraph of its own, have explicit discourse markers for its begin and
@@ -214,7 +222,11 @@
 %     \multicolumn{2}{|p{12cm}|}{\footnotesize These kinds of assertions
 %       are convenient during the exploration of a mathematical theory. They can be used
 %       and proven later (or assumed as an axiom).}\\\hline\hline
-%     \textbf{observation} & if everything else fails\\\hline
+%     \textbf{rule}
+%     & a normative assertion\\\hline
+%     \multicolumn{2}{|p{12cm}|}{\footnotesize These kinds of assertions can be interpreted
+%     procedurally to trigger actions}\\\hline\hline
+%     \textbf{observation}, \textbf{remark} & if everything else fails\\\hline
 %     \multicolumn{2}{|p{12cm}|}{\footnotesize This type is the catch-all if none of the others
 %       applies.}\\\hline 
 %   \end{tabular}
@@ -301,6 +313,41 @@
 % \caption{Semantic Markup for the Peano Axioms}\label{fig:axioms}
 % \end{exfig}
 %
+% \subsubsection{Types}\label{sec:user:types}
+% 
+% In many cases, we can give additional information for symbols in the form of type
+% assignments. \sTeX does not fix a type system, but allows types to be arbitrary
+% mathematical objects that they can be defined in (imported) modules. The
+% \DescribeMacro{\symtype}|\symtype| macro can be used to assign a type to a symbol: 
+% \begin{quote}
+%   |\symtype[|\meta{keys}|]{|\meta{sym}|}{|\meta{type}|}|
+% \end{quote}
+% assigns the type \meta{type} to a symbol with name \meta{sym}. For instance
+%
+% \begin{center}%
+% |\symtype[id=plus-nat.type,system=sts]{plus}{\fntype{\Nat,\Nat}\Nat}|
+% \end{center}
+% 
+% \noindent assigns the type $\mathbb{N}\times\mathbb{N}\rightarrow\mathbb{N}$ (in the
+% |sts| type system) to the symbol |plus|. This states (type assignments are statements
+% epistemologically) that addition is a binary function on natural numbers. The |\symtype|
+% macro supports the keys |id| (for identifiers) and |system| for the type system.
+% 
+% Often, type assignments occur in informal context, where the type assignment is given by
+% a natural language sentence or phrase. For this, the |statements| package supplies the
+% \DescribeEnv{typedec}|typedec| environment and the
+% \DescribeMacro{\inlinetypedec}|\inlinetypedec| macro. Both take an optional keyval
+% argument followed by the type. The phrase/sentence is the body of the |typedec|
+% environment and the last argument of the |\inlinetypedec| macro. The symbol name is
+% given in via the |for| key. For convenience, the macro
+% \DescribeMacro{\thedectype}|\thedectype| is bound to the type. So we can use
+%\begin{verbatim}
+% \begin{typedec}[for=plus,id=plus-nat.type]{\fntype{\Nat,\Nat}\Nat}
+%   $+:\thedectype$ is a binary function on $\Nat$
+% \end{typedec}
+% \end{verbatim}
+% instead of the |\symtype| above in an informal setting. 
+% 
 % \subsubsection{Definitions, and Definienda}\label{sec:definition}
 % 
 % \DescribeEnv{definition} The |definition| environment is used for marking up
@@ -309,9 +356,9 @@
 % by the |\definiendum| macro, which is used as
 % |\definiendum[|\meta{sysname}|]{|\meta{text}|}|. Here, \meta{text} is the text that is
 % to be emphasized in the presentation and the optional \meta{sysname} is a system name of
-% the symbol defined (for reference via |\term|, see Section~\ref{sec:user:crossref}). If
-% \meta{sysname} is not given, then \meta{text} is used as a system name instead, which is
-% usually sufficient for most situations.
+% the symbol defined (for reference via |\termref|, see
+% Section~\ref{sec:user:crossref}). If \meta{sysname} is not given, then \meta{text} is
+% used as a system name instead, which is usually sufficient for most situations.
 % 
 %\begin{exfig}
 % \begin{verbatim}
@@ -332,33 +379,50 @@
 % \end{module}
 % \caption{A Definition based on Figure {\ref{fig:axioms}}}\label{fig:definition}
 % \end{exfig}
-% The \DescribeMacro{defin}|\defi{|\meta{word}|}| macro combines the functionality of the
+% The \DescribeMacro{defi}|\defi{|\meta{word}|}| macro combines the functionality of the
 % |\definiendum| macro with index markup from the |omdoc|
-% package~\ctancite{Kohlhase:smomdl}: use |\defi[|\meta{name}|]{|\meta{word}|}| to markup
-% a definiendum \meta{word} with system name \meta{name} that appear in the index --- in
-% other words in almost all definitions of single-word concepts. We also have the variants
-% \DescribeMacro{\defii}|\defii| and \DescribeMacro{\defiii}|\defiii| for (adjectivized)
-% two-word compounds. Finally, the varaiants \DescribeMacro{\adefi}|\adefi|,
+% package~\ctancite{Kohlhase:smomdl}: use
+% \begin{center}
+% |\defi[|\meta{name}|]{|\meta{word}|}[|\meta{indexkeys}|]|
+% \end{center}
+% to markup a definiendum \meta{word} with system name \meta{name} that appear in the
+% index (where \meta{indexkeys} are passed to the |\omdoc@index*| macros from the |omtext|
+% package) --- in other words in almost all definitions of single-word concepts.  We also
+% have the variants \DescribeMacro{\defii}|\defii| and \DescribeMacro{\defiii}|\defiii|
+% for (adjectivized) two-word compounds.  Note that if the definiendum contains sematnic
+% macros, then we need to specify the |loadmodules| key and also protect the semantic
+% macro. For instance if |\eset| is the semantic macro for $\emptyset$, then we would use
+% \begin{verbatim}
+% \defii[eset-comp]{$\protect\eset$}{compatible}[loadmodules]
+% \end{verbatim}
+% for the definiendum markup. Finally, the variants \DescribeMacro{\adefi}|\adefi|,
 % \DescribeMacro{\adefii}|\adefii|,and \DescribeMacro{\adefiii}|\adefiii| have an
 % additional first argument that allows to specify an alternative text; see
-% Figure~\ref{fig:defin}
+% Figure~\ref{fig:defin}. The main use of these is to mark up inflected forms as in
+% \begin{verbatim}
+% we speak of \adefi{lemmata}{lemma} in this case. 
+% \end{verbatim}
+% As the greatest number of these are plurals, which tends to be regular (e.g. adding a
+% trailing ``s'' in English), we provide the variants \DescribeMacro{\defis}|\defis|,
+% \DescribeMacro{\defiis}|\defiis|, and \DescribeMacro{\defiiis}|\defiiis| for that case:
+% |\defiis{simple}{group}| is equivalent to much longer |\adefii{simple groups}{simple}{group}|.
 % 
 % \begin{exfig}
 % \begin{tabular}{l|l|l}
-%   \multicolumn{3}{l}{source}\\
-%   system name & result & index \\\hline
-%   \multicolumn{3}{l}{\texttt{\textbackslash defin\{concept\}}}\\
-%   |concept| & concept& concept\\\hline
-%   \multicolumn{3}{l}{\texttt{\textbackslash defin[csymbol]\{concept\}}}\\
-%   |csymbol| & concept & concept\\\hline
-%   \multicolumn{3}{l}{\texttt{\textbackslash definalt[csymbol]\{concepts\}\{concept\}}}\\
-%   |csymbol| & concepts & concept\\\hline
-%   \multicolumn{3}{l}{\texttt{\textbackslash twindef\{concept\}\{group\}}}\\
+%   \multicolumn{3}{l}{source}\\\hline
+%   system name & result & index \\\hline\hline
+%   \multicolumn{3}{l}{\texttt{\textbackslash defi\{concept\}}}\\\hline
+%   |concept| & concept& concept\\\hline\hline
+%   \multicolumn{3}{l}{\texttt{\textbackslash defi[csymbol]\{concept\}}}\\\hline
+%   |csymbol| & concept & concept\\\hline\hline
+%   \multicolumn{3}{l}{\texttt{\textbackslash adefi[csymbol]\{concepts\}\{concept\}}}\\\hline
+%   |csymbol| & concepts & concept\\\hline\hline
+%   \multicolumn{3}{l}{\texttt{\textbackslash defii\{concept\}\{group\}}}\\\hline
 %   |concept-group| & concept group & concept group,  \\
-%   && group - , concept\\\hline
-%   \multicolumn{3}{l}{\texttt{\textbackslash atwindef\{small\}\{concept\}\{group\}}}\\
+%   && group - , concept\\\hline\hline
+%   \multicolumn{3}{l}{\texttt{\textbackslash adefii\{small\}\{concept\}\{group\}}}\\\hline
 %   |small-concept-group| & small concept group &  small concept group,  \\
-%   && concept group - , small\\
+%   && concept group - , small\\\hline
 % \end{tabular}
 % \caption{Some definienda with Index}\label{fig:defin}
 % \end{exfig}
@@ -395,6 +459,7 @@
 % used for inline examples, e.g. ``\ldots mammals, e.g. goats''. Note that we have used an
 % inline example for an inline example.
 %
+%
 % \subsection{Cross-Referencing Symbols and Concepts}\label{sec:user:crossref}
 %
 % If we have defined a concept with the |\definiendum| macro, then we can mark up other
@@ -430,15 +495,16 @@
 % \meta{name}. Concepts defined via |\defii{|\meta{first}|}{|\meta{second}|}| can be
 % referenced by \DescribeMacro{\trefii}|\trefii{|\meta{first}|}{|\meta{second}|}| (with
 % link text ``\meta{first} \meta{second}'') and analogously for |\defiii| and
-% \DescribeMacro{\trefiii}|\trefiii|. Finally, we have variants
-% \DescribeMacro{\atref*}|\atrefi|, |\atrefii|, and |\atrefiii| with alternative link
-% text. For instance |\atrefii{|\meta{text}|{|\meta{first}|}{|\meta{second}|}| references
-% a concept introduced by |\defii{|\meta{first}|}{|\meta{second}|}| but with link text
-% \meta{text}.  Of course, if the system identifier is given explicitly in the optional
-% argument of the definition form, as in
-% |\defii[|\meta{name}|]{|\meta{first}|}{|\meta{second}|}|, then the terms are referenced
-% by |\trefi{|\meta{name}|}|.
-%
+% \DescribeMacro{\trefiii}|\trefiii|.
+% 
+% We have variants \DescribeMacro{\atref*}|\atrefi|, |\atrefii|, and |\atrefiii| with
+% alternative link text. For instance
+% |\atrefii{|\meta{text}|{|\meta{first}|}{|\meta{second}|}| references a concept
+% introduced by |\defii{|\meta{first}|}{|\meta{second}|}| but with link text \meta{text}.
+% Of course, if the system identifier is given explicitly in the optional argument of the
+% definition form, as in |\defii[|\meta{name}|]{|\meta{first}|}{|\meta{second}|}|, then
+% the terms are referenced by |\trefi{|\meta{name}|}|.
+% 
 % For referencing terms outside the current module, the module name can be specified in
 % the first optional argument of the |\*tref*| macros. To specify the |cdbase|, we have to
 % resort to the |\termref| macro with the keyval arguments.
@@ -455,6 +521,18 @@
 % a hyperlink to the relevant definition (i.e. the one that has the declaration
 % |for=|\meta{cseq} in the metadata argument.)
 % 
+% The \DescribeMacro{\term}|\term| macro is a variant of the |\termref| macro that marks
+% up a phrase as a (possible) term reference, which does not have a link \emph{yet}. This
+% macro is a convenient placeholder for authoring, where a |\termref| annotation is
+% (currently) too tedious or the link target has not been authored yet. It facilitates
+% lazy flexiformalization workflows, where definitions for mathematical concepts are
+% supplied or marked up by need (e.g. after a |grep| shows that the number of |\term|
+% annotations of a concept is above a threshold). Editors or active documents can also
+% support the |\term| macro like a wiki-like dangling link: a click on
+% |\term{|\meta{phrase}|}| could generate a new editor buffer with a stub definition (an
+% |definition| environment with |\definiendum| macro and appropriate metadata).\ednote{MK:
+% we probably need multi-part variants for |*tref*|}
+% 
 % \section{Configuration of the Presentation}\label{sec:conf}
 % 
 % \DescribeMacro{\defemph} The |\defemph| macro is a configuration hook that allows to
@@ -481,10 +559,12 @@
 %   have it applied when the reference is constructed. But for that we need to split the
 %   label into keyword and number in package |sref|.}
 % 
-% Finally, we provide configuration hooks in Figure~\ref{fig:hooks} for the statement
-% types provided by the |statement| package. These are mainly intended for package authors
-% building on |statements|, e.g. for multi-language support.\ednote{we might want to
-%   develop an extension \texttt{statements-babel} in the future.}.
+%   Finally, we provide configuration hooks in Figure~\ref{fig:hooks} for the statement
+%   types provided by the |statement| package. These are mainly intended for package
+%   authors building on |statements|, e.g. for multi-language support. The language
+%   bindings are given in the |smultiling|~\cite{KohGin:smss:svn} package not in
+%   |statements| itself.
+% 
 %\begin{exfig}
 % \begin{tabular}{lll}
 % Environment & configuration macro & value\\\hline\hline
@@ -498,6 +578,8 @@
 % \texttt{STobligationAssEnv} & \texttt{\textbackslash st@obligation@kw} & \makeatletter\st@obligation@kw\\\hline
 % \texttt{STassumptionAssEnv} & \texttt{\textbackslash st@assumption@kw} & \makeatletter\st@assumption@kw\\\hline
 % \texttt{STobservationAssEnv} & \texttt{\textbackslash st@observation@kw} & \makeatletter\st@observation@kw\\\hline
+% \texttt{STremarkAssEnv} & \texttt{\textbackslash st@remark@kw} & \makeatletter\st@remark@kw\\\hline
+% \texttt{STruleAssEnv} & \texttt{\textbackslash st@rule@kw} & \makeatletter\st@rule@kw\\\hline
 % \texttt{STexampleEnv} & \texttt{\textbackslash st@example@kw} & \makeatletter\st@example@kw\\\hline
 % \texttt{STaxiomEnv} & \texttt{\textbackslash st@axiom@kw} & \makeatletter\st@axiom@kw\\\hline
 % \texttt{STdefinitionEnv} & \texttt{\textbackslash st@definition@kw} & \makeatletter\st@definition@kw\\\hline
@@ -510,7 +592,7 @@
 % 
 % In this section we document known limitations. If you want to help alleviate them,
 % please feel free to contact the package author. Some of them are currently discussed in
-% the \sTeX TRAC~\cite{sTeX:online}. 
+% the \sTeX GitHub repository~\cite{sTeX:github:on}. 
 % \begin{compactenum}
 % \item none reported yet
 % \end{compactenum}
@@ -519,13 +601,6 @@
 % 
 % \section{The Implementation}\label{sec:impl} 
 % 
-% The |statements| package generates two files: the {\LaTeX} package (all the code between
-% {\textsf{$\langle$*package$\rangle$}} and {\textsf{$\langle$/package$\rangle$}}) and the
-% {\latexml} bindings (between {\textsf{$\langle$*ltxml$\rangle$ and
-%     $\langle$/ltxml$\rangle$}}). We keep the corresponding code fragments together,
-% since the documentation applies to both of them and to prevent them from getting out of
-% sync.
-%
 % \subsection{Package Options}\label{sec:impl:options}
 %
 % We declare some switches which will modify the behavior according to the package
@@ -533,13 +608,10 @@
 % (otherwise they stay false). First we have the general options
 %    \begin{macrocode}
 %<*package>
-\DeclareOption{showmeta}{\PassOptionsToPackage{\CurrentOption}{metakeys}}
-\DeclareOption*{\PassOptionsToPackage{\CurrentOption}{omdoc}}
-%    \end{macrocode}
-%    Finally, we need to declare the end of the option declaration section to {\LaTeX}.
-%    \begin{macrocode}
+\newif\ifdef@index\def@indexfalse
+\DeclareOption{defindex}{\def@indextrue}
+\DeclareOption*{\PassOptionsToPackage{\CurrentOption}{omtext}}
 \ProcessOptions
-%</package>
 %    \end{macrocode}
 % 
 % The next measure is to ensure that some {\sTeX} packages are loaded: |omdoc| for the
@@ -548,87 +620,35 @@
 % initialize the package inclusions, there we do not need |ntheorem|, since the XML does
 % not do the presentation.
 %    \begin{macrocode}
-%<*package>
 \RequirePackage{omtext}
-\RequirePackage{modules}
+\RequirePackage[base]{babel}
 \RequirePackage[hyperref]{ntheorem}
 \theoremstyle{plain}
-%</package>
-%<*ltxml>
-# -*- CPERL -*-
-package LaTeXML::Package::Pool;
-use strict;
-use LaTeXML::Package;
-RequirePackage('omtext');
-RequirePackage('modules');
-%</ltxml>
 %    \end{macrocode}
 % Now, we define an auxiliary function that lowercases strings
 %    \begin{macrocode}
-%<*ltxml>
-sub lowcase {my ($string) = @_; $string ? return lc(ToString($string)) : return('')}#$
-sub dashed { join('-',map($_->toString,@_));}#$
-%</ltxml>
 %    \end{macrocode}
-% Sometimes it is necessary to fallback to symbol names in order to generate xml:id attributes. For this purpose,
-% we define an auxiliary function which ensures the name receives a unique NCName equivalent.\ednote{Hard to be unique here, 
-% e.g. the names "foo\_bar" and "foo bar" would receive the same xml:id attributes... of course we can devise a more complex scheme
-% for the symbol replacement.}
+% Sometimes it is necessary to fallback to symbol names in order to generate xml:id
+% attributes. For this purpose, we define an auxiliary function which ensures the name
+% receives a unique NCName equivalent.\ednote{Hard to be unique here, e.g. the names
+% "foo\_bar" and "foo bar" would receive the same xml:id attributes... of course we can
+% devise a more complex scheme for the symbol replacement.}
 %    \begin{macrocode}
-%<*ltxml>
-sub makeNCName {
-  my ($name) = @_;
-  my $ncname=$name;
-  $ncname=~s/\s/_/g;  #Spaces to underscores
-  $ncname="_$ncname" if $ncname!~/^(\w|_)/;  #Ensure start with letter or underscore
-  ##More to come...
-  $ncname;
-}
-%</ltxml>
 %    \end{macrocode}
 % The following functions are strictly utility functions that makes our life easier later on
 %    \begin{macrocode}
-%<*ltxml>
-sub simple_wrapper {
-  #Deref if array reference
-  my @input;
-  foreach (@_) {
-  if (ref $_ && $_ =~ /ARRAY/ && $_ !~ /LaTeXML/) {
-      @input=(@input,@$_);
-    } else
-      { push (@input,$_); }
-  }
-  return '' if (!@input);
-  @input = map(split(/\s*,\s*/,ToString($_)),@input);
-  my $output=join(" ",@input);
-  $output=~s/(^ )|[{}]//g; #remove leading space and list separator brackets
-  $output||'';
-}
-sub hash_wrapper{
-  #Deref if array reference
-  my @input;
-  foreach (@_) {
-  if (ref $_ && $_ =~ /ARRAY/ && $_ !~ /LaTeXML/) {
-      @input=(@input,@$_);
-    } else
-      { push (@input,$_); }
-  }
-  return '' if (!@input);
-  @input = map(split(/\s*,\s*/,ToString($_)),@input);
-  my $output=join(".sym #",@input);
-  $output=~s/(^\.sym )|[{}]//g; #remove leading space and list separator brackets
-  "#$output"||'';
-}
-%</ltxml>
 %    \end{macrocode}
 % 
+% For the other languages, we set up triggers
+%    \begin{macrocode}
+\AfterBabelLanguage{ngerman}{\input{statements-ngerman.ldf}}
+%    \end{macrocode}
+%
 % \subsection{Statements}\label{sec:impl:statements}
 %
 % \begin{macro}{\STpresent}
 %    \begin{macrocode}
-%<*package>
 \providecommand\STpresent[1]{#1}
-%</package> 
 %    \end{macrocode}
 % \end{macro}
 %
@@ -640,48 +660,39 @@ sub hash_wrapper{
 %    initialize the environment using the appropriate macro. Upon ending the environment,
 %    we just run the respective termination macro.
 %    \begin{macrocode}
-%<*package>
 \def\define@statement@env#1{%
 \newenvironment{#1}[1][]{\metasetkeys{omtext}{##1}\sref@target%
+\@in@omtexttrue%
 \ifx\omtext@display\st@flow\else%
 \ifx\omtext@title\@empty\begin{ST#1Env}\else\begin{ST#1Env}[\omtext@title]\fi%
 \ifx\sref@id\@empty\else\label{#1.\sref@id}\fi
-\csname st@#1@initialize\endcsname\fi
+\csname st@#1@initialize\endcsname\fi% display
 \ifx\sref@id\@empty\sref@label@id{here}\else%
-\sref@label@id{\STpresent{\csname ST#1EnvKeyword\endcsname}~\@currentlabel}\fi}
-{\csname st@#1@terminate\endcsname\ifx\omtext@display\st@flow\else\end{ST#1Env}\fi}}
-%</package>
+\sref@label@id{\STpresent{\csname ST#1EnvKeyword\endcsname}~\@currentlabel}\fi%
+\ignorespaces}
+{\csname st@#1@terminate\endcsname\ifx\omtext@display\st@flow\else\end{ST#1Env}\fi%
+\omtext@post@skip\@in@omtextfalse}}
 %    \end{macrocode}
 % \end{macro}
 %
 % \begin{environment}{assertion}
 %    \begin{macrocode}
-%<*package>
 \newenvironment{assertion}[1][]{\metasetkeys{omtext}{#1}\sref@target%
-\ifx\omtext@display\st@flow\else%
+\@in@omtexttrue%
+\ifx\omtext@display\st@flow\itshape\noindent\ignorespaces%
+\else% display!=flow
 \ifx\omtext@title\@empty\begin{ST\omtext@type AssEnv}%
 \else\begin{ST\omtext@type AssEnv}[\omtext@title]\fi\fi%
 \ifx\omtext@type\@empty\sref@label@id{here}\else%
-\sref@label@id{\STpresent{\csname ST\omtext@type AssEnvKeyword\endcsname}~\@currentlabel}\fi}
-{\ifx\omtext@display\st@flow\else\end{ST\omtext@type AssEnv}\fi}
-%</package>
-%<*ltxml>
-DefEnvironment('{assertion} OptionalKeyVals:omtext',
-  "<omdoc:assertion "
-  .   "?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')() "
-  .   "?&KeyVal(#1,'theory')(theory='&KeyVal(#1,'theory')')() "
-  .   "type='&lowcase(&KeyVal(#1,'type'))'>"
-  .   "?&KeyVal(#1,'title')(<dc:title>&KeyVal(#1,'title')</dc:title>)()"
- .  "<omdoc:CMP>#body"
-  ."</omdoc:assertion>\n");
-%</ltxml>
+\sref@label@id{\STpresent{\csname ST\omtext@type AssEnvKeyword\endcsname}~\@currentlabel}
+\fi}%display=flow
+{\ifx\omtext@display\st@flow\else\end{ST\omtext@type AssEnv}\@in@omtextfalse\fi}
 %    \end{macrocode}
 % \end{environment}
 %
 % \begin{macro}{\st@*@kw}
 %   We configure the default keywords for the various theorem environments. 
 %    \begin{macrocode}
-%<*package>
 \def\st@theorem@kw{Theorem}
 \def\st@lemma@kw{Lemma}
 \def\st@proposition@kw{Proposition}
@@ -691,8 +702,11 @@ DefEnvironment('{assertion} OptionalKeyVals:omtext',
 \def\st@postulate@kw{Postulate}
 \def\st@obligation@kw{Obligation}
 \def\st@assumption@kw{Assumption}
+\def\st@rule@kw{Rule}
 \def\st@observation@kw{Observation}
-%    \end{macrocode}
+\def\st@remark@kw{Remark}
+%    \end{macrocode} 
+%
 % \end{macro}
 % Then we configure the presentation of the theorem environments
 %    \begin{macrocode}
@@ -703,7 +717,7 @@ DefEnvironment('{assertion} OptionalKeyVals:omtext',
 % defined above. They are all numbered together with the section counter.
 % \begin{environment}{ST*AssEnv}
 %    \begin{macrocode}
-\newtheorem{STtheoremAssEnv}{\st@theorem@kw}
+\newtheorem{STtheoremAssEnv}{\st@theorem@kw}[section]
 \newtheorem{STlemmaAssEnv}[STtheoremAssEnv]{\st@lemma@kw}
 \newtheorem{STpropositionAssEnv}[STtheoremAssEnv]{\st@proposition@kw}
 \newtheorem{STcorollaryAssEnv}[STtheoremAssEnv]{\st@corollary@kw}
@@ -713,163 +727,105 @@ DefEnvironment('{assertion} OptionalKeyVals:omtext',
 \newtheorem{STobligationAssEnv}[STtheoremAssEnv]{\st@obligation@kw}
 \newtheorem{STassumptionAssEnv}[STtheoremAssEnv]{\st@assumption@kw}
 \newtheorem{STobservationAssEnv}[STtheoremAssEnv]{\st@observation@kw}
-%</package>
+\theorembodyfont{\rm}
+\newtheorem{STremarkAssEnv}[STtheoremAssEnv]{\st@remark@kw}
+\newtheorem{STruleAssEnv}[STtheoremAssEnv]{\st@rule@kw}
 %    \end{macrocode}
 % \end{environment}
 %
 % \begin{environment}{example}
+%   \ednote{need to do something clever for the OMDoc representation of examples, in
+%   particular, the usevocab should only be defined in example}
 %    \begin{macrocode}
-%<*package>
 \def\st@example@initialize{}\def\st@example@terminate{}
 \define@statement@env{example}
 \def\st@example@kw{Example}
 \theorembodyfont{\upshape}
 \newtheorem{STexampleEnv}[STtheoremAssEnv]{\st@example@kw}
-%</package>
-%<*ltxml>
-DefEnvironment('{example} OptionalKeyVals:omtext',
-       "<omdoc:example "
-       . "?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')() "
-       . "?&KeyVal(#1,'for')(for='&hash_wrapper(&KeyVal(#1,'for'))')()>"
-       . "?&KeyVal(#1,'title')(<dc:title>&KeyVal(#1,'title')</dc:title>)()"
-      . "<omdoc:CMP>#body"
-     . "</omdoc:example>\n");
-%</ltxml>
 %    \end{macrocode}
 % \end{environment}
 %
 % \begin{environment}{axiom}
 %    \begin{macrocode}
-%<*package>
 \def\st@axiom@initialize{}\def\st@axiom@terminate{}
 \define@statement@env{axiom}
 \def\st@axiom@kw{Axiom}
 \theorembodyfont{\upshape}
 \newtheorem{STaxiomEnv}[STtheoremAssEnv]{\st@axiom@kw}
-%</package>
-%<*ltxml>
-DefEnvironment('{axiom} OptionalKeyVals:omtext',
-  "<omdoc:axiom "
-  .   "?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')()>"
-  .   "?&KeyVal(#1,'title')(<dc:title>&KeyVal(#1,'title')</dc:title>)()"
- . "<omdoc:CMP>#body"
-  . "</omdoc:axiom>\n");
-%</ltxml>
 %    \end{macrocode}
 % \end{environment}
 %
 % \begin{environment}{symboldec}
+%   We use |\symdef@type| from the |modules| package as the visual cue. 
 %    \begin{macrocode}
-%<*package>
 \srefaddidkey{symboldec}
 \addmetakey{symboldec}{functions}
 \addmetakey{symboldec}{role}
 \addmetakey*{symboldec}{title}
-\addmetakey{symboldec}{name}
+\addmetakey*{symboldec}{name}
 \addmetakey{symboldec}{subject}
 \addmetakey*{symboldec}{display}
-\def\symboldec@type{Symbol}
 \newenvironment{symboldec}[1][]{\metasetkeys{symboldec}{#1}\sref@target\st@indeftrue%
-\ifx\symboldec@display\st@flow\else{\stDMemph{\symboldec@type} \symboldec@name:}\fi%
+\ifx\symboldec@display\st@flow\else{\noindent\stDMemph{\symdef@type} \symboldec@name:}\fi%
 \ifx\symboldec@title\@empty~\else~(\stDMemph{\symboldec@title})\par\fi}{}
-%</package>
-%<*ltxml>
-DefEnvironment('{symboldec} OptionalKeyVals:symboldec',
-       "<omdoc:symbol "
-      .  "?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')"
-      .                   "(xml:id='&makeNCName(&KeyVal(#1,'name')).def.sym')"
-      .               "name='&KeyVal(#1,'name')'>"
-      .  "?&KeyVal(#1,'title')(<dc:title>&KeyVal(#1,'title')</dc:title>)()"
-      .  "<dc:description>#body"
-      ."</omdoc:symbol>\n");
-%</ltxml>
 %    \end{macrocode}
 % \end{environment}
 % 
-% \begin{macro}{\symtype}
+% \subsubsection{Types}\label{sec:impl:types}
+% 
+% \begin{macro}{\symtype}\ednote{MK@DG; the type element should percolate up.}
 %    \begin{macrocode} 
-%<*package>
-\newcommand{\symtype}[2]{Type (#1): $#2$}
-%</package>
-%<*ltxml>
-DefConstructor('\symtype{}{}',
-  "<omdoc:type system='#1'><ltx:Math><ltx:XMath>#2</ltx:XMath></ltx:Math></omdoc:type>");
-%</ltxml>
+\srefaddidkey{symtype}
+\addmetakey*{symtype}{system}
+\addmetakey*{symtype}{for}
+\newcommand\type@type{Type}
+\newcommand\symtype[3][]{\metasetkeys{symtype}{#1}\sref@target%
+\noindent\type@type \ifx\symtype@\@empty\else (\symtype@system)\fi #2: $#3$}
 %    \end{macrocode}
 % \end{macro}
 %
+% \begin{macro}{\inlinetypedec}
+%    \begin{macrocode} 
+\newcommand\inlinetypedec[3][]{\metasetkeys{symtype}{#1}\sref@target{\def\thedectype{#2}#3}}
+%    \end{macrocode}
+% \end{macro}
+%
+% \begin{environment}{typedec}
+%   We first define a theorem environment 
+%    \begin{macrocode}
+\def\st@typedec@kw{Type Declaration}
+\theorembodyfont{\upshape}
+\newtheorem{STtypedecEnv}[STtheoremAssEnv]{\st@typedec@kw}
+%    \end{macrocode}
+% and then the environment itself.
+%    \begin{macrocode}
+\newenvironment{typedec}[2][]{\metasetkeys{omtext}{#1}\sref@target%
+\def\thedectype{#2}%
+\ifx\omtext@display\st@flow\else%
+\ifx\omtext@title\@empty\begin{STtypedecEnv}\else\begin{STtypedecEnv}[\omtext@title]\fi%
+\ifx\sref@id\@empty\else\label{typedec.\sref@id}\fi
+\ifx\sref@id\@empty\sref@label@id{here}\else%
+\sref@label@id{\STpresent{\csname STtypedecEnvKeyword\endcsname}~\@currentlabel}\fi%
+\ignorespaces}
+{\ifx\omtext@display\st@flow\else\end{STtypedecEnv}\fi\omtext@post@skip}
+%    \end{macrocode}
+% \end{environment}
+%
 % \begin{environment}{definition}
 %   The |definition| environment itself is quite similar to the other's but we need to set
 %   the |\st@indef| switch to suppress warnings from |\st@def@target|.
 %    \begin{macrocode}
-%<*package>
 \newif\ifst@indef\st@indeffalse
 \newenvironment{definition}[1][]{\metasetkeys{omtext}{#1}\sref@target\st@indeftrue%
 \ifx\omtext@display\st@flow\else%
 \ifx\omtext@title\@empty\begin{STdefinitionEnv}\else\begin{STdefinitionEnv}[\omtext@title]\fi\fi%
 \ifx\sref@id\@empty\sref@label@id{here}\else%
-\sref@label@id{\STpresent{\csname STdefinitionEnvKeyword\endcsname}~\@currentlabel}\fi}
+\sref@label@id{\STpresent{\csname STdefinitionEnvKeyword\endcsname}~\@currentlabel}\fi%
+\ignorespaces}
 {\ifx\omtext@display\st@flow\else\end{STdefinitionEnv}\fi}
 \def\st@definition@kw{Definition}
 \theorembodyfont{\upshape}
 \newtheorem{STdefinitionEnv}[STtheoremAssEnv]{\st@definition@kw}
-%</package>
-%<*ltxml>
-sub definitionBody {
-    my ($doc, $keyvals, %props) = @_;
-    my $for = $keyvals->getValue('for') if $keyvals;
-    my $type = $keyvals->getValue('type') if $keyvals;
-   my %for_attr=();
-    if (ToString($for)) {
-      $for = ToString($for);
-      $for =~ s/^{(.+)}$/$1/eg;
-      foreach (split(/,\s*/,$for)) {
-        $for_attr{$_}=1;
-     }}
-   if ($props{theory}) {
-    my @symbols = @{$props{defs} || []};
-    foreach my $symb(@symbols) {
-      next if $for_attr{$symb};
-      $for_attr{$symb}=1;
-      $doc->insertElement('omdoc:symbol', undef, (name=>$symb, "xml:id"=>makeNCName("$symb.def.sym")));
-    }
-   }
-    my %attrs = ();
-    $for = join(" ",(keys %for_attr));
-    $attrs{'for'} = $for if $for;
-    my $id = $keyvals->getValue('id') if $keyvals;
-    $attrs{'xml:id'} = $id if $id;
-    $attrs{'type'} = $type if $type;
-    if ($props{theory}) {
-      $doc->openElement('omdoc:definition', %attrs);
-    } else {
-      $attrs{'type'}='definition';
-      $doc->openElement('omdoc:omtext', %attrs);
-    }
-    my $title = $keyvals->getValue('title') if $keyvals;
-    if ($title) {
-      $doc->openElement('omdoc:metadata');
-      $doc->openElement('dc:title');
-      $doc->absorb($title);
-      $doc->closeElement('dc:title');}
-    $doc->openElement('omdoc:CMP');
-   $doc->absorb($props{body}) if $props{body};
-   $doc->maybeCloseElement('omdoc:CMP');
-    if ($props{theory}) {
-      $doc->closeElement('omdoc:definition');
-    } else {
-      $doc->closeElement('omdoc:omtext');
-    }
-    return; }
-DefEnvironment('{definition} OptionalKeyVals:omtext', sub{definitionBody(@_)},
-  afterDigestBegin=>sub {
-    my ($stomach, $whatsit) = @_;
-    my @symbols = ();
-    $whatsit->setProperty(theory=>LookupValue('current_module'));
-    $whatsit->setProperty(defs=>\@symbols);
-    AssignValue('defs', \@symbols);  return; },
-  afterDigest => sub { AssignValue('defs', undef); return; });#$
-%</ltxml>
 %    \end{macrocode}
 % \end{environment}
 %
@@ -877,26 +833,13 @@ DefEnvironment('{definition} OptionalKeyVals:omtext', sub{definitionBody(@_)},
 %   We initialize the |\def\st@notation@initialize{}| here, and extend it with
 %   functionality below. 
 %    \begin{macrocode}
-%<*package>
-\def\notemph#1{{\bf{#1}}}
+\def\notemph#1{#1}
 \def\st@notation@terminate{}
 \def\st@notation@initialize{}
 \define@statement@env{notation}
 \def\st@notation@kw{Notation}
 \theorembodyfont{\upshape}
 \newtheorem{STnotationEnv}[STtheoremAssEnv]{\st@notation@kw}
-%</package>
-%<*ltxml>
-DefEnvironment('{notation} OptionalKeyVals:omtext',
-  "<omdoc:definition " 
- .   "?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id').not')()"
- .   "?&KeyVal(#1,'for')(for='&simple_wrapper(&KeyVal(#1,'for'))')()>"
- . "?&KeyVal(#1,'title')(<dc:title>&KeyVal(#1,'title')</dc:title>)()"
- . "<omdoc:CMP>#body"
-  . "</omdoc:definition>\n");
-DefConstructor('\notatiendum OptionalKeyVals:notation {}',
-              "<ltx:text class='notatiendum'>#2</ltx:text>");
-%</ltxml>
 %    \end{macrocode}
 % \end{environment}
 %
@@ -905,30 +848,34 @@ DefConstructor('\notatiendum OptionalKeyVals:notation {}',
 %   specialized for the use in the |\definiendum|, |\defi|, |\defii|, and |\defiii|
 %   macros. |\st@def@target{|\meta{opt}|}{|\meta{name}|}| makes a target with label
 %   |sref@|\meta{opt}|@|\meta{modulename}|@target|, if \meta{opt} is non-empty, else with
-%   the label |sref@|\meta{name}|@|\meta{modulename}|@target|. Also it generates the
-%   necessary warnings for a definiendum-like macro.
+%   the label |sref@|\meta{name}|@|\meta{modulename}|@target| (the first time it
+%   encounters this symbol; i.e. if |\sref@|\meta{name}|@|\meta{modulename}|@defined| is
+%   undefined). Also it generates the necessary warnings for a definiendum-like
+%   macro.
 %    \begin{macrocode}
-%<*package>
-\def\st@def@target#1#2{\def\@test{#1}%
+\newcommand\st@def@target[3]{\def\@symname{#1}\def\@verbname{#2}%
 \ifst@indef% if we are in a definition or such
-\ifx\omtext@theory\@empty% if there is no theory attribute
 \@ifundefined{mod@id}% if we are not in a module
 {\PackageWarning{statements}{definiendum in unidentified module\MessageBreak
 \protect\definiendum, \protect\defi,
 \protect\defii, \protect\defiii\MessageBreak
 can only be referenced when called in a module with id key}}%
-{\ifx\@test\@empty%
-\expandafter\sref@target@ifh{sref@#2@\mod@id @target}{}\else%
-\expandafter\sref@target@ifh{sref@#1@\mod@id @target}{}\fi}%
-\else\expandafter\sref@target@ifh{sref@#1@\omtext@theory @target}{}\fi%
-\else\PackageError{statements}%
+{% now we are in a module
+\edef\@@cd{\ifx\omtext@theory\@empty\mod@id\else\omtext@theory\fi}%
+\edef\@@name{\ifx\@symname\@empty\@verbname\else\@symname\fi}%
+\defemph{\@ifundefined{sref@\@@name @\@@cd @defined}%
+{\expandafter\sref@target@ifh{sref@\@@name @\@@cd @target}{#3}}%
+{#3}}%
+\expandafter\gdef\csname sref@\@@name @\@@cd @defined\endcsname{yes}%
+\ifmetakeys@showmeta\metakeys@show@keys{\@@cd}{name:\@@name}\fi}%
+\else% st@indef
+\PackageError{statements}%
 {definiendum outside definition context\MessageBreak
-\protect\definiendum, \protect\defi, 
+\protect\definiendum, \protect\defi,
 \protect\defii, \protect\defiii\MessageBreak
 do not make sense semantically outside a definition.\MessageBreak
 Consider wrapping the defining phrase in a \protect\inlinedef}%
-\fi}
-%</package>
+\fi}% st@indef
 %    \end{macrocode}
 % \end{macro}
 %
@@ -942,33 +889,16 @@ Consider wrapping the defining phrase in a \protect\inlinedef}%
 %   |definition| environments and thus one group level too low. Keeping this for future
 %   reference.
 %    \begin{macrocode}
-%<*package>
 \newcommand\@termdef[2][]{\def\@test{#1}%
 \@ifundefined{mod@id}{}{\ifx\@test\@empty\def\@@name{#2}\else\def\@@name{#1}\fi%
 \termdef{\mod@id @\@@name}{#2}}}
-%</package>
 %    \end{macrocode}
 % \end{macro}
 %
 % \begin{macro}{\definiendum}
 %    \begin{macrocode}
-%<*package>
-%\newcommand\definiendum[2][]{\st@def@target{#1}{#2}\@termdef[#1]{#2}\defemph{#2}}
-\newcommand\definiendum[2][]{\st@def@target{#1}{#2}\defemph{#2}}
-%</package>
-%<*ltxml>
-DefConstructor('\definiendum [] {}',
-       "<omdoc:term role='definiendum' name='#name' cd='#theory'>#2</omdoc:term>",
-       afterDigest => sub {
- my ($stomach, $whatsit) = @_;
- my $addr = LookupValue('defs');
- my $name = $whatsit->getArg(1);
- $name = $whatsit->getArg(2) unless $name;
- $whatsit->setProperty(name=>$name->toString);
- push(@$addr, $name->toString) if ($addr and $name);
- $whatsit->setProperty(theory=>LookupValue('current_module'));
- return; });#$
-%</ltxml>
+%\newcommand\definiendum[2][]{\st@def@target{#1}{#2}\@termdef[#1]{#2}{#2}}
+\newcommand\definiendum[2][]{\st@def@target{#1}{#2}{#2}}
 %    \end{macrocode}
 % \end{macro}
 %
@@ -976,9 +906,7 @@ DefConstructor('\definiendum [] {}',
 %   the |notatiendum| macro also needs to be visible in the |notation| and |definition|
 %   environments
 %    \begin{macrocode}
-%<*package>
-\newcommand{\notatiendum}[2][]{\notemph{#2}}
-%</package>
+\newcommand\notatiendum[2][]{\notemph{#2}}
 %    \end{macrocode}
 % \end{macro}
 %
@@ -986,308 +914,133 @@ DefConstructor('\definiendum [] {}',
 % instances one will be used for the definition and the other for indexing.
 %
 % \begin{macro}{\defi}
+%   We split the |\defi| macro in two: |\defi| does the definiendum bit and |\@defi|
+%   handles the last optional argument and does the indexing. The information flow between
+%   them goes via the local |\@phrase| macro.
 %    \begin{macrocode}
-%<*package>
-\newcommand{\defi}[2][]{\definiendum[#1]{#2}\omdoc@index[#1]{#2}}
-%</package>
-%<*ltxml>
-DefConstructor('\defi[]{}',
-       "<omdoc:idx>"
-      .  "<omdoc:idt>"
-      .     "<omdoc:term role='definiendum' name='?#1(#1)(#2)' cd='#theory'>#2</omdoc:term>"
-      .  "</omdoc:idt>"
-      .  "<omdoc:ide index='default'><omdoc:idp>#2</omdoc:idp></omdoc:ide>"
-      ."</omdoc:idx>",
-       afterDigest => sub {
- my ($stomach, $whatsit) = @_;
- my $addr = LookupValue('defs');
- my $name = $whatsit->getArg(1);
- $name = $whatsit->getArg(2) unless $name;
- push(@$addr, $name->toString) if ($addr and $name);
- $whatsit->setProperty(theory=>LookupValue('current_module'));#$
- return; },
-       alias=>'\defi');
-%</ltxml>
+\newcommand\defi[2][]{\st@def@target{#1}{#2}{#2}\def\@phrase{#2}\@defi}
+\newcommand\@defi[1][]{\ifdef@index\omdoc@indexi[#1]{\@phrase}\fi\xspace}
+\newcommand\defis[2][]{\st@def@target{#1}{#2}{#2s}\def\@phrase{#2}\@defi}
 %    \end{macrocode}
 % \end{macro}
 %
 % \begin{macro}{\adefi}
+%   Again we split the |\adefi| macro into two parts: |\adef| does the definiendum bit and
+%   |\@adefi| handles the last optional argument and does the indexing. 
 %    \begin{macrocode}
-%<*package>
-\newcommand{\adefi}[3][]{\def\@test{#1}%
-\ifx\@test\@empty\definiendum[#3]{#2}%
-\else\definiendum[#1]{#2}\omdoc@index[#1]{#3}\fi}
-%</package>
-%<*ltxml>
-DefConstructor('\adefi[]{}{}',
-       "<omdoc:idx>"
-      .  "<omdoc:idt>"
-      .     "<omdoc:term role='definiendum' name='?#1(#1)(#3)' cd='#theory'>#2</omdoc:term>"
-      .  "</omdoc:idt>"
-      .  "<omdoc:ide index='default'><omdoc:idp>#3</omdoc:idp></omdoc:ide>"
-      ."</omdoc:idx>",
-       afterDigest => sub {
- my ($stomach, $whatsit) = @_;
- my $addr = LookupValue('defs');
- my $name = $whatsit->getArg(1);
- $name = $whatsit->getArg(3) unless $name;
- push(@$addr, $name->toString) if ($addr and $name);
- $whatsit->setProperty(theory=>LookupValue('current_module'));#$
- return; },
-      alias=>'\adefi');
-%</ltxml>
+\newcommand\adefi[3][]{\def\@name{#1}\def\@verb{#3}%
+\st@def@target{#1}{#3}{#2}\@adefi}
+\newcommand\@adefi[1][]{%
+\ifdef@index%
+\ifx\@name\@empty\omdoc@indexi[#1]{\@verb}%
+\else\omdoc@indexi[at=\@name,#1]{\@verb}\fi%
+\fi\xspace}
 %    \end{macrocode}
 % \end{macro}
 %
 % \begin{macro}{\defii}
 %    \begin{macrocode}
-%<*package>
-\newcommand{\defii}[3][]{\st@def@target{#1}{#2-#3}\defemph{#2 #3}\@twin[#1]{#2}{#3}}
-%</package>
-%<*ltxml>
-DefConstructor('\defii[]{}{}',
-       "<omdoc:idx>"
-      .  "<omdoc:idt>"
-      .    "<omdoc:term role='definiendum' name='?#1(#1)(&dashed(#2,#3))' cd='#theory'>"
-      .      "#2 #3"
-      .    "</omdoc:term>"
-      .  "</omdoc:idt>"
-      .  "<omdoc:ide index='default'>"
-      .    "<omdoc:idp>#2</omdoc:idp>"
-      .    "<omdoc:idp>#3</omdoc:idp>"
-      .  "</omdoc:ide>"
-      ."</omdoc:idx>",
-       afterDigest => sub {
- my ($stomach, $whatsit) = @_;
-my $addr = LookupValue('defs');
- my $name = $whatsit->getArg(1);
- $name = $name->toString if $name;
- $name = $whatsit->getArg(2)->toString.'-'.$whatsit->getArg(3)->toString unless $name;
- push(@$addr, $name) if ($addr and $name);
- $whatsit->setProperty(theory=>LookupValue('current_module'));
- return; },
-       alias=>'\defii');#$
-%</ltxml>
+\newcommand\@defii[1][]{\ifdef@index\@twin[#1]{\@pone}{\@ptwo}\fi\xspace}
+\newcommand\defii[3][]{\def\@pone{#2}\def\@ptwo{#3}%
+\st@def@target{#1}{#2-#3}{#2 #3}\@defii}
+\newcommand\defiis[3][]{\def\@pone{#2}\def\@ptwo{#3}%
+\st@def@target{#1}{#2-#3}{#2 #3s}\@defii}
 %    \end{macrocode}
 % \end{macro}
 %
 % \begin{macro}{\adefii}
+%   analogous to |\adefi|
 %    \begin{macrocode}
-%<*package>
-\newcommand{\adefii}[4][]{\def\@test{#1}%
-\ifx\@test\@empty\definiendum[#3-#4]{#2}%
-\else\definiendum[#1]{#2}\@twin[#1]{#3}{#4}\fi}
-%</package>
-%<*ltxml>
-DefConstructor('\adefii[]{}{}{}',
-       "<omdoc:idx>"
-      .  "<omdoc:idt>"
-      .    "<omdoc:term role='definiendum' name='?#1(#1)(&dashed(#3,#4))' cd='#theory'>"
-      .       "#2"
-      .    "</omdoc:term>"
-      .  "</omdoc:idt>"
-      .  "<omdoc:ide index='default'>"
-      .    "<omdoc:idp>#3</omdoc:idp>"
-      .    "<omdoc:idp>#4</omdoc:idp>"
-      .  "</omdoc:ide>"
-      ."</omdoc:idx>",
-       afterDigest => sub {
- my ($stomach, $whatsit) = @_;
- my $addr = LookupValue('defs');
- my $name = $whatsit->getArg(1);
- $name = $name->toString if $name;
- $name = $whatsit->getArg(3)->toString.'-'.$whatsit->getArg(4)->toString unless $name;
- push(@$addr, $name) if ($addr and $name);
- $whatsit->setProperty(theory=>LookupValue('current_module'));
- return; },
-       alias=>'\defii');#$
-%</ltxml>
+\newcommand\adefii[4][]{\def\@name{#1}\def\@pone{#3}\def\@ptwo{#4}%
+\st@def@target{#1}{#3-#4}{#2}\@adefii}
+\newcommand\@adefii[1][]{%
+\ifdef@index%
+\ifx\@name\@empty\@twin[#1]{\@pone}{\@ptwo}%
+\else\@twin[at=\@name,#1]{\@pone}{\@ptwo}\fi%
+\fi\xspace}
 %    \end{macrocode}
 % \end{macro}
 %
 % \begin{macro}{\defiii}
+%   similar to |\defii|
 %    \begin{macrocode}
-%<*package>
-\newcommand{\defiii}[4][]{\st@def@target{#1}{#2-#3-#4}\defemph{#2 #3 #4}\@atwin[#1]{#2}{#3}{#4}}
-%</package>
-%<*ltxml>
-DefConstructor('\defiii[]{}{}{}',
-       "<omdoc:idx>"
-       . "<omdoc:idt>"
-         . "<omdoc:term role='definiendum' cd='#theory' name='?#1(#1)(&dashed(#2,#3,#4))'>#2 #3 #4</omdoc:term>"
-       . "</omdoc:idt>"
-       . "<omdoc:ide index='default'>"
-         . "<omdoc:idp>#2</omdoc:idp>"
-         . "<omdoc:idp>#3</omdoc:idp>"
-         . "<omdoc:idp>#4</omdoc:idp>"
-       . "</omdoc:ide>"
-     . "</omdoc:idx>",
-       afterDigest => sub {
- my ($stomach, $whatsit) = @_;
- my $addr = LookupValue('defs');
- my $name = $whatsit->getArg(1);
- $name = $name->toString if $name;
- $name = $whatsit->getArg(2)->toString.'-'.$whatsit->getArg(3)->toString.'-'.$whatsit->getArg(4)->toString unless $name;
- push(@$addr, $name) if ($addr and $name);
- $whatsit->setProperty(theory=>LookupValue('current_module'));
- return; },
-       alias=>'\defiii');
-%</ltxml>
+\newcommand\defiii[4][]{\def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}%
+\st@def@target{#1}{#2-#3-#4}{#2 #3 #4}\@defiii}
+\newcommand\@defiii[1][]{\ifdef@index\@atwin[#1]{\@pone}{\@ptwo}{\@pthree}\fi\xspace}
+\newcommand\defiiis[4][]{\def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}%
+\st@def@target{#1}{#2-#3-#4}{#2 #3 #4s}\@defiii}
 %    \end{macrocode}
 % \end{macro}
 %
 % \begin{macro}{\adefiii}
 %    \begin{macrocode}
-%<*package>
-\newcommand{\adefiii}[5][]{\def\@test{#1}%
-\ifx\@test\@empty\definiendum[#3-#4-#5]{#2}%
-\else\definiendum[#1]{#2}\@atwin[#1]{#3}{#4}{#5}\fi}
-%</package>
-%<*ltxml>
-DefConstructor('\adefiii[]{}{}{}{}',
-       "<omdoc:idx>"
-       . "<omdoc:idt>"
-       . "<omdoc:term role='definiendum' cd='#theory' name='?#1(#1)(&dashed(#3,#4,#5))'>#2</omdoc:term>"
-       . "</omdoc:idt>"
-       . "<omdoc:ide index='default'>"
-         . "<omdoc:idp>#3</omdoc:idp>"
-         . "<omdoc:idp>#4</omdoc:idp>"
-         . "<omdoc:idp>#5</omdoc:idp>"
-       . "</omdoc:ide>"
-     . "</omdoc:idx>",
-       afterDigest => sub {
- my ($stomach, $whatsit) = @_;
- my $addr = LookupValue('defs');
- my $name = $whatsit->getArg(1);
- $name = $name->toString if $name;
- $name = $whatsit->getArg(3)->toString.'-'.$whatsit->getArg(4)->toString.'-'.$whatsit->getArg(5)->toString unless $name;
- push(@$addr, $name) if ($addr and $name);
- $whatsit->setProperty(theory=>LookupValue('current_module'));
- return; },
-       alias=>'\defiii');
-%</ltxml>
+\newcommand\adefiii[5][]{\def\@name{#1}\def\@pone{#3}\def\@ptwo{#4}\def\@pthree{#3}%
+\st@def@target{#1}{#3-#4-#5}{#2}\@adefiii}
+\newcommand\@adefiii[1][]{%
+\ifdef@index%
+\ifx\@name\@empty\@atwin[#1]{\@pone}{\@ptwo}{\@pthree}%
+\else\@atwin[at=\@name,#1]{\@pone}{\@ptwo}{\@pthree}\fi%
+\fi\xspace}
 %    \end{macrocode}
 % \end{macro}
 %
 % \begin{macro}{\inlineex}
 %    \begin{macrocode}
-%<*package>
-\newcommand{\inlineex}[2][]{\metasetkeys{omtext}{#1}\sref@target\sref@label@id{here}#2}
-%</package>
-%<*ltxml>
-DefConstructor('\inlineex OptionalKeyVals:omtext {}',
-              "<ltx:text class='example'>#2</ltx:text>");
-%</ltxml>
+\newcommand\inlineex[2][]{\metasetkeys{omtext}{#1}%
+\sref@target\sref@label@id{here}#2}
 %    \end{macrocode}
 % \end{macro}
-% \begin{macro}{\inlinedef}
+%
+% \begin{macro}{\inlineass}
 %    \begin{macrocode}
-%<*package>
-\newcommand{\inlinedef}[2][]{\metasetkeys{omtext}{#1}\sref@target\sref@label@id{here}\st@indeftrue #2}
-%</package>
-%<*ltxml>
-DefConstructor('\inlinedef OptionalKeyVals:omtext {}', sub {
- my ($document, $keyvals, $body, %props) = @_;
- my $for = $keyvals->getValue('for') if $keyvals;
- my %for_attr=();
- if (ToString($for)) {
-   $for = ToString($for);
-   $for =~ s/^{(.+)}$/$1/eg;
-   foreach (split(/,\s*/,$for)) {
-     $for_attr{$_}=1;
-   }}
- my @symbols = @{$props{defs} || []};
- #Prepare for symbol insertion -insert before the parent of the closest ancestor CMP element
-  my $original_node = $document->getNode;
- my $xc = XML::LibXML::XPathContext->new( $original_node );
- $xc->registerNs('omdoc', 'http://omdoc.org/ns');
- my ($statement_ancestor) = $xc->findnodes('./ancestor::omdoc:CMP/..');
- foreach my $symb(@symbols) {
-   next if $for_attr{$symb};
-   $for_attr{$symb}=1;
-   my $symbolnode = XML::LibXML::Element->new('symbol');
-   $symbolnode->setAttribute(name=>$symb);
-   $symbolnode->setAttribute("xml:id"=>makeNCName("$symb.def.sym"));
-   $statement_ancestor->parentNode->insertBefore($symbolnode,$statement_ancestor);
- }
- #Restore the insertion point
- $document->setNode($original_node);
- my %attrs = ();
- $for = join(" ",(keys %for_attr));
- $attrs{'for'} = $for if $for;
- my $id = $keyvals->getValue('id') if $keyvals;
- $attrs{'xml:id'} = $id if $id;
-$attrs{'class'} = 'inlinedef';
- $document->openElement('ltx:text',%attrs);
- $document->absorb($body);
-$document->closeElement('ltx:text'); },
- #Prepare 'defs' hooks for \defi and \definiendum symbol names
-  beforeDigest=>sub {
-    my @symbols = ();
-    AssignValue('defs', \@symbols); return; },
- #Adopt collected names as 'defs' property, remove hooks
-  afterDigest=>sub {
-    my ($stomach, $whatsit) = @_;
-    my $defsref = LookupValue('defs');
-    my @defs = @$defsref;
-    $whatsit->setProperty('defs',\@defs);
-    AssignValue('defs',undef);
- return; });
-%</ltxml>
+\newcommand\inlineass[2][]{\metasetkeys{omtext}{#1}%
+\sref@target\sref@label@id{here}#2}
 %    \end{macrocode}
 % \end{macro}
-% 
-% \subsection{Cross-Referencing Symbols and Concepts}\label{sec:impl:crossref}
 %
-% \begin{macro}{\termref@set}
-%   The |term| macro uses the |cd| and |name| keys for hyperlinking to create hyper-refs,
-%   if the |hyperref| package is loaded: We first see if the |cd| key was given, if not we
-%   define it as the local module identifier.
+% \begin{macro}{\inlinedef}
 %    \begin{macrocode}
-%<*package>
-\addmetakey[\mod@id]{termref}{cd}
-\addmetakey{termref}{cdbase}
-\addmetakey{termref}{name}
-\addmetakey{termref}{role}
-\def\termref@set#1#2{\def\termref@name{#2}\metasetkeys{termref}{#1}}
+\newcommand\inlinedef[2][]{\metasetkeys{omtext}{#1}%
+\if@in@omtext\else% we are not in an omtext or statement
+\PackageError{modules}{\protect\inlinedef\space outside a statement!}%
+{Try wrapping the paragraph in a\MessageBreak 
+\protect\begin{omtext}, \protect\begin{assertion}, \protect\begin{axiom}, ... \MessageBreak
+whatever is suitable semantically}\fi%
+\sref@target\sref@label@id{here}\st@indeftrue #2}
 %    \end{macrocode}
 % \end{macro}
+% 
+% \subsection{Cross-Referencing Symbols and Concepts}\label{sec:impl:crossref}
 %
 % \begin{macro}{\termref}
+%   |\termref{|\meta{opt}|}{|\meta{text}|}| makes a hyperlink with link text \meta{text}
+%   to the definitional occurrence of the symbol specified by the |name|, |cd|, and
+%   |cdbase| keys in \meta{opt}. We first set sensible defaults if the keys are not
+%   given. If the symbol is defined in the current document (i.e. if the macro
+%   |\sref@|\meta{name}|@|\meta{cd}|@defined| is defined), then we make a local hyperref,
+%   otherwise we punt to |\mod@termref|.
 %    \begin{macrocode}
-\newcommand{\termref}[2][]{\metasetkeys{termref}{#1}\st@termref{#2}}
-%</package>
-%<*ltxml>
-DefConstructor('\termref OptionalKeyVals:termref {}',
-               "<omdoc:term "
-              .  "?&KeyVal(#1,'cdbase')(cdbase='&KeyVal(#1,'cdbase')')() "
-             .  "cd='?&KeyVal(#1,'cd')(&KeyVal(#1,'cd'))(#module)' "
-              .  "name='&KeyVal(#1,'name')'>"
-              .  "#2"
-              ."</omdoc:term>",
-	      afterDigest=>sub{$_[1]->setProperty(module=>LookupValue('current_module'))});
-%</ltxml>%$
-%    \end{macrocode}
-% \end{macro}
-% The next macro is where the actual work is done. 
-% \begin{macro}{\st@termref}
-%   If the |cdbase| is given, then we make a hyper-reference, otherwise we punt to
-%   |\mod@termref|, which can deal with the case where the cdbase is given by the imported
-%   cd.
-%    \begin{macrocode}
-%<*package>
-\def\st@termref#1{\ifx\termref@name\@empty\def\termref@name{#1}\fi%
-\ifx\termref@cdbase\@empty\mod@termref\termref@cd\termref@name{#1}%
-\else\sref@href@ifh\termref@cdbase{#1}\fi}
-%</package>
+\addmetakey*{termref}{cd}
+\addmetakey*{termref}{cdbase}
+\addmetakey*{termref}{name}
+\addmetakey*{termref}{role}
+\newcommand\termref[2][]{\metasetkeys{termref}{#1}%
+  \ifx\termref@cd\@empty\def\termref@cd{\mod@id}\fi%
+  \ifx\termref@name\@empty\def\termref@name{#2}\fi%
+  \@ifundefined{sref@\termref@name @\termref@cd @defined}
+  {\ifx\termref@cdbase\@empty% external reference
+    \mod@termref\termref@cd\termref@name{#2}%
+    \else\sref@href@ifh\termref@cdbase{#2}%
+    \fi}%
+  {\sref@hlink@ifh{sref@\termref@name @\termref@cd @target}{#2}}%
+}
 %    \end{macrocode}
 % \end{macro}
 %
 % \begin{macro}{\tref*}
 %    \begin{macrocode}
-%<ltxml>RawTeX('
-%<*package|ltxml>
-\newcommand\atrefi[3][]{\def\@test{#1}\ifx\@test\@empty\termref[name=#3]{#2}\else\termref[cd=#1,name=#3]{#2}\fi}
+\newcommand\atrefi[3][]{\def\@test{#1}%
+\ifx\@test\@empty\termref[name=#3]{#2}\else\termref[cd=#1,name=#3]{#2}\fi}
 \newcommand\atrefii[4][]{\atrefi[#1]{#2}{#3-#4}}
 \newcommand\atrefiii[5][]{\atrefi[#1]{#2}{#3-#4-#5}}
 %    \end{macrocode}
@@ -1295,11 +1048,12 @@ DefConstructor('\termref OptionalKeyVals:termref {}',
 %
 % \begin{macro}{\tref*}
 %    \begin{macrocode}
-\newcommand{\trefi}[2][]{\atrefi[#1]{#2}{#2}}
-\newcommand{\trefii}[3][]{\atrefi[#1]{#2 #3}{#2-#3}}
-\newcommand{\trefiii}[4][]{\atrefi[#1]{#2 #3 #4}{#2-#3-#4}}
-%</package|ltxml>
-%<ltxml>');
+\newcommand\trefi[2][]{\atrefi[#1]{#2}{#2}}
+\newcommand\trefii[3][]{\atrefi[#1]{#2 #3}{#2-#3}}
+\newcommand\trefiii[4][]{\atrefi[#1]{#2 #3 #4}{#2-#3-#4}}
+\newcommand\trefis[2][]{\atrefi[#1]{#2s}{#2}}
+\newcommand\trefiis[3][]{\atrefi[#1]{#2 #3s}{#2-#3}}
+\newcommand\trefiiis[4][]{\atrefi[#1]{#2 #3 #4s}{#2-#3-#4}}
 %    \end{macrocode}
 % \end{macro}
 %
@@ -1308,57 +1062,41 @@ DefConstructor('\termref OptionalKeyVals:termref {}',
 % appear in documents, therefore we do not provide {\latexml} bindings for them.
 % \begin{macro}{\*emph}
 %    \begin{macrocode}
-%<*package>
 \providecommand{\termemph}[1]{#1}
 \providecommand{\defemph}[1]{{\textbf{#1}}}
 \providecommand{\stDMemph}[1]{{\textbf{#1}}}
-%</package>
 %    \end{macrocode}
 % \end{macro}
 % 
+% \begin{macro}{\term}
+%   The |\term| macro is used for wiki-style dangling links with editor support.\ednote{MK: document above} 
+%    \begin{macrocode}
+\newcommand\term[2][]{\def\@test{#1}%
+\ifx\@test\@empty\else
+\@ifundefined{module@defs@#1}{\PackageWarning{statements}%
+{{\protect\term} specifies module #1 which is not in
+  scope\MessageBreak import it via e.g. via \protect\importmhmodule}}{}
+\fi%
+\PackageWarning{statements}%
+{Dangling link (\protect\term) for "#2" still needs to be specified}%
+\textcolor{blue}{\underline{#2}}}
+%    \end{macrocode}
+% \end{macro}
 % \begin{macro}{\symref}
 %   The |\symref| macros is quite simple, since we have done all the heavy lifting in the
 %   |modules| package: we simply apply |\mod@symref@|\meta{arg1} to
 %   \meta{arg2}.
 %    \begin{macrocode}
-%<*package>
-\newcommand{\symref}[2]{\@nameuse{mod@symref@#1}{#2}}
-%</package>
-%<*ltxml>
-DefConstructor('\symref{}{}',
-               "<omdoc:term cd='&LookupValue('symdef.#1.cd')' name='&LookupValue('symdef.#1.name')'>"
-              .  "#2"
-              ."</omdoc:term>");
-%</ltxml>
+\newcommand\symref[2]{\@nameuse{mod@symref@#1}{#2}}
 %    \end{macrocode}
 % \end{macro}
 %
-% \subsection{Providing IDs for {\omdoc} Elements}\label{sec:impl:ids}
-%
-% To provide default identifiers, we tag all {\omdoc}
-% elements that allow |xml:id| attributes by executing the |numberIt| procedure from |omdoc.sty.ltxml|.
-% 
-%    \begin{macrocode}
-%<*ltxml>
-Tag('omdoc:assertion',afterOpen=>\&numberIt,afterClose=>\&locateIt);
-Tag('omdoc:definition',afterOpen=>\&numberIt,afterClose=>\&locateIt);
-Tag('omdoc:example',afterOpen=>\&numberIt,afterClose=>\&locateIt);
-Tag('omdoc:requation',afterOpen=>\&numberIt,afterClose=>\&locateIt);
-Tag('omdoc:axiom',afterOpen=>\&numberIt,afterClose=>\&locateIt);
-Tag('omdoc:symbol',afterOpen=>\&numberIt,afterClose=>\&locateIt);
-Tag('omdoc:type',afterOpen=>\&numberIt,afterClose=>\&locateIt);
-Tag('omdoc:term',afterOpen=>\&numberIt,afterClose=>\&locateIt);
-%</ltxml>
-%    \end{macrocode}
-%
 % \subsection{Deprecated Functionality}\label{sec:deprecated}
 %
 % In this section we centralize old interfaces that are only partially supported any
 % more. 
 % \begin{macro}{\*def*}
 %    \begin{macrocode}
-%<ltxml>RawTeX('
-%<*package|ltxml>
 \newcommand\defin[2][]{\defi[#1]{#2}%
 \PackageWarning{statements}{\protect\defin\space is deprecated, use \protect\defi\space instead}}
 \newcommand\twindef[3][]{\defii[#1]{#2}{#3}%
@@ -1380,40 +1118,31 @@ Tag('omdoc:term',afterOpen=>\&numberIt,afterClose=>\&locateIt);
 \PackageWarning{statements}{\protect\twinref\space is deprecated, use \protect\trefii\space instead}}
 \newcommand\atwinref[4][]{\atrefiii[#1]{#2}{#3}{#4}%
 \PackageWarning{statements}{\protect\atwindef\space is deprecated, use \protect\trefiii\space instead}}
-%</package|ltxml>
-%<ltxml>');
+%</package>
 %    \end{macrocode}
 % \end{macro}
-% 
-% \subsection{Finale}
-%
-% Finally, we need to terminate the file with a success mark for perl.
-%    \begin{macrocode}
-%<ltxml>1;
-%    \end{macrocode}
-%
 % \Finale
 %
 \endinput
 % \iffalse
-% LocalWords:  GPL structuresharing STR dtx keyval env envfalse idfalse idtrue
-% LocalWords:  displayfalse envtrue displaytrue forfalse typefalse titlefalse
-% LocalWords:   continuesfalse fortrue fromtrue typetrue titletrue CPERL omdoc
-% LocalWords:   continuestrue symboldec omtext RequirePackage lowcase lc ToString
-% LocalWords:  foreach hyperref href hlink DefEnvironment OptionalKeyVals ne
-% LocalWords:  KeyVal xml CMP simpleDef PatternDef DefEnvironment PatternRule
-% LocalWords:  requation PatternCMP RecDef DefConstructor keyvals defs psymbols
-% LocalWords:  openElement symb closeElement ffor getValue attrs metadata undef
-% LocalWords:  afterDigestBegin setProperty AssignValue afterDigest definiendum
-% LocalWords:  cd addr LookupValue getArg toString idx idt definiendum ide idp
-% LocalWords:  DefMacro args unlist inlinedef uri pdf afterOpen numberIt texttt
-% LocalWords:  iffalse consymb ntheorem textbackslash symref def scsys sc sc kw
-% LocalWords:  mathml openmath latexml activemath fileversion maketitle stex
+% LocalWords:  GPL structuresharing STR dtx keyval env envfalse idfalse idtrue typedec st
+% LocalWords:  displayfalse envtrue displaytrue forfalse typefalse titlefalse filedate eg
+% LocalWords:   continuesfalse fortrue fromtrue typetrue titletrue CPERL omdoc thedectype
+% LocalWords:   continuestrue symboldec omtext RequirePackage lowcase lc ToString termin
+% LocalWords:  foreach hyperref href hlink DefStatement OptionalKeyVals ne NeedsTeXFormat
+% LocalWords:  KeyVal xml CMP simpleDef PatternDef DefStatement PatternRule thedectype
+% LocalWords:  requation PatternCMP RecDef DefConstructor keyvals defs psymbols tref
+% LocalWords:  openElement symb closeElement ffor getValue attrs metadata undef rangle
+% LocalWords:  afterDigestBegin setProperty AssignValue afterDigest definiendum rangle
+% LocalWords:  cd addr LookupValue getArg toString idx idt definiendum ide idp st@flow
+% LocalWords:  DefMacro args unlist inlinedef uri pdf afterOpen numberIt texttt XMath
+% LocalWords:  iffalse consymb ntheorem textbackslash symref def scsys sc sc kw endinput
+% LocalWords:  mathml openmath latexml activemath fileversion maketitle stex importmodule
 % LocalWords:  setcounter tocdepth tableofcontents newpage sproofs ulsmf08 sref
-% LocalWords:  MaySch eltte09 twintoo sref subsubsection exfig vspace vspace
+% LocalWords:  MaySch eltte09 twintoo sref subsubsection exfig vspace vspace usemhvocab
 % LocalWords:  noindent renewtheorem hline textbf textbf footnotesize ple peano
-% LocalWords:  STaxiomEnv symdef medskip succ mathbb ldots stepcounter ednote
-% LocalWords:  STtheoremAssEnv stepcounter STtheoremAssEnv stepcounter defin
+% LocalWords:  STaxiomEnv symdef medskip succ mathbb ldots stepcounter ednote usemhmodule
+% LocalWords:  STtheoremAssEnv stepcounter STtheoremAssEnv stepcounter defin STtypedecEnv
 % LocalWords:  STtheoremAssEnv notatiendum defin smomdl biblatex twindef cdbase
 % LocalWords:  twindef atwindef atwindef adjectivized varaiants twindefalt cseq
 % LocalWords:  twindefalt atwindefalt atwindefalt csymbol definalt termref emph
@@ -1424,16 +1153,21 @@ Tag('omdoc:term',afterOpen=>\&numberIt,afterClose=>\&locateIt);
 % LocalWords:  STfalseconjectureAssEnv STpostulateAssEnv STobligationAssEnv foo
 % LocalWords:  STassumptionAssEnv STobservationAssEnv STexampleEnv textsf ltxml
 % LocalWords:  STdefinitionEnv STnotationEnv printbibliography langle ncname
-% LocalWords:  theoremstyle sym newenvironment ifx csname endcsname
+% LocalWords:  theoremstyle sym newenvironment ifx csname endcsname inlineex
 % LocalWords:  currentlabel theorembodyfont itshape theoremheaderfont bfseries
-% LocalWords:  normalfont newtheorem upshape srefaddidkey 
+% LocalWords:  normalfont newtheorem upshape srefaddidkey  definendum 
 % LocalWords:  newcommand indef newif ifst indeffalse indeftrue attr whatsit
-% LocalWords:  STdefinitionEnvKeyword notemph modulename ifundefined atwin
-% LocalWords:  expandafter providecommand nameuse doctex ctancite funval
+% LocalWords:  STdefinitionEnvKeyword notemph modulename ifundefined atwin defi
+% LocalWords:  expandafter providecommand nameuse doctex ctancite funval defii
 
 %%% Local Variables: 
 %%% mode: doctex
 %%% TeX-master: t
 %%% End: 
 % \fi
-% LocalWords:  funsymbs findnodes symbolnode defsref
+% LocalWords:  funsymbs findnodes symbolnode defsref showmeta showmeta sysname
+% LocalWords:  defii defiii defiii adefi adefi adefii adefii adefiii adefiii
+% LocalWords:  trefi trefii trefiii atref atrefi atrefii atrefiii conf metakeys
+% LocalWords:  compactenum Deref metasetkeys addmetakey symtype ltx ltx sts
+% LocalWords:  ifmetakeys fntype rightarrow inlinetypedec inlinetypedec
+% LocalWords:  ignorespaces usemodule textcolor STtypedecEnvKeyword
diff --git a/Master/texmf-dist/source/latex/stex/statements/statements.ins b/Master/texmf-dist/source/latex/stex/statements/statements.ins
index 98628a07d7c..feb580fc54f 100644
--- a/Master/texmf-dist/source/latex/stex/statements/statements.ins
+++ b/Master/texmf-dist/source/latex/stex/statements/statements.ins
@@ -27,12 +27,4 @@
 \Msg{* And don't forget to refresh your filename database}
 \Msg{* if your TeX distribution uses such a database.}
 \Msg{*}
-
-\nopreamble\nopostamble
-\generate{\file{statements.sty.ltxml}{\from{statements.dtx}{ltxml}}}
-
-\Msg{*}
-\Msg{* You probably need to move the generated ltxml files into a directory searched by LaTeXML.}
-\Msg{*}
-
 \endbatchfile