% \iffalse meta-comment
% An Infrastructure for Semantic Macros and Module Scoping
% Copyright (C) 2004-2013 Michael Kohlhase, all rights reserved
%               this file is released under the
%               LaTeX Project Public License (LPPL)
%
% 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{modules}[2019/03/20 v1.4 Semantic Markup]
%
%<*driver>
\documentclass{ltxdoc}
\usepackage[utf8]{inputenc}
\usepackage[T1]{fontenc}
\usepackage{stex-logo,modules}
\usepackage{url,array,float,textcomp}
\usepackage[show]{ed}
\usepackage[hyperref=auto,style=alphabetic]{biblatex}
\addbibresource{kwarcpubs.bib}
\addbibresource{extpubs.bib}
\addbibresource{kwarccrossrefs.bib}
\addbibresource{extcrossrefs.bib}
\usepackage{listings}
\usepackage{amsfonts}
\usepackage{ctangit}
\usepackage{xspace}
\usepackage{hyperref}
\makeindex
\floatstyle{boxed}
\newfloat{exfig}{thp}{lop}
\floatname{exfig}{Example}
\def\githubissue#1{\cite{sTeX:github:on}, \hyperlink{https://github.com/KWARC/sTeX/issues/#1}{issue #1}}
\begin{document}
\RecordChanges
\DocInput{modules.dtx}
\end{document} 
%</driver>
% \fi
% 
% \CheckSum{802}
%
% \changes{v0.9}{2005/06/14}{First Version with Documentation}
% \changes{v0.9a}{2005/07/01}{Completed Documentation}
% \changes{v0.9b}{2005/08/06}{Complete functionality and Updated Documentation}
% \changes{v0.9c}{2006/01/13}{more packaging}
% \changes{v0.9d}{2007/12/12}{fixing double loading of .tex and .sms}
% \changes{v0.9e}{2008/06/17}{fixing LaTeXML}
% \changes{v0.9f}{2008/06/17}{remove unused options uses and usesqualified}
% \changes{v0.9g}{2009/05/02}{adding resymdef functionality}
% \changes{v0.9g}{2009/08/12}{adding importOMDocmodule}
% \changes{v0.9h}{2010/01/19}{using {\texttt{\textbackslash mod@newcommand}} instead of
% {\texttt{\textbackslash providecommand}} for more intuitive inheritance.}
% \changes{v0.9h}{2010/03/05}{adding {\texttt{\textbackslash metalanguage}}}
% \changes{v1.0}{2010/06/18}{minor fixes}
% \changes{v1.1}{2010/12/30}{adding optional arguments to semantic macros for display
%   variants. The resymdef functionality introduced in 0.9g is now deprecated. It was hardly
%   used.}
% \changes{v1.1}{2012/06/25}{adding additional keys for the \texttt{\textbackslash symdef}
%   macro and exporting them to OMDoc}
% \changes{v1.1}{2012/07/06}{exporting requiremodules to the \texttt{aux} file, so that
%   they are preloaded (pre-required) so semantic macros in section titles can work.}
% \changes{v1.1}{2012/11/09}{Moving LaTeXML bindings into \texttt{modules.sty.ltxml} and
% disabling generation}
% \changes{v1.2}{2013/08/25}{No longer loading the aux file at the end of the document}
% \changes{v1.3}{2013/12/12}{adding MathHub support}
% \changes{v1.4}{2015/03/31}{Completely revamped importing modules this is much faster now,
% but can no longer do relative paths.}
% \changes{v1.4}{2015/04/02}{deprecated \texttt {\textbackslash sinput} and \texttt {\textbackslash sinputref}}
% \changes{v1.5}{2015/11/02}{Moved MH Versions to a separate \texttt{mathhub} package}
% \changes{v1.5}{2018/06/15}{``unidentified cd'' in termref is now an error.}
% 
% \GetFileInfo{modules.sty}
% 
% \MakeShortVerb{\|}
%\def\scsys#1{{{\sc #1}}\index{#1@{\sc #1}}\xspace}
% \def\xml{\scsys{Xml}}
% \def\mathml{\scsys{MathML}}
% \def\omdoc{\scsys{OMDoc}}
% \def\openmath{\scsys{OpenMath}}
% \def\latexml{\scsys{LaTeXML}}
% \def\perl{\scsys{Perl}}
% \def\cmathml{Content-{\sc MathML}\index{Content {\sc MathML}}\index{MathML@{\sc MathML}!content}}
% \def\activemath{\scsys{ActiveMath}}
% \def\twin#1#2{\index{#1!#2}\index{#2!#1}}
% \def\twintoo#1#2{{#1 #2}\twin{#1}{#2}}
% \def\atwin#1#2#3{\index{#1!#2!#3}\index{#3!#2 (#1)}}
% \def\atwintoo#1#2#3{{#1 #2 #3}\atwin{#1}{#2}{#3}}
% \def\cT{\mathcal{T}}\def\cD{\mathcal{D}}
% \title{{\texttt{modules.sty}}: Semantic Macros and Module Scoping   in {\stex}\thanks{Version {\fileversion} (last revised
% {\filedate})}}
% \author{Michael Kohlhase\\
%    FAU Erlangen-N\"urnberg\\
%    \url{http://kwarc.info/kohlhase}\and
%    Deyan Ginev\\Authorea\and 
%    Rares Ambrus\\Jacobs University Bremen}
% \maketitle
%
% \begin{abstract}
%   The |modules| package is a central part of the {\stex} collection, 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).
%
%   This package supplies a definition mechanism for semantic macros and a non-standard
%   scoping construct for them, which is oriented at the semantic dependency relation
%   rather than the document structure. This structure can be used by MKM systems for
%   added-value services, either directly from the {\sTeX} sources, or after translation.
% \end{abstract}
%
% \newpage\setcounter{tocdepth}{2}\tableofcontents\newpage
%
% \section{Introduction}\label{sec:intro}
% 
% Following general practice in the {\TeX/\LaTeX} community, we use the term ``semantic
% macro'' for a macro whose expansion stands for a mathematical object, and whose name
% (the command sequence) is inspired by the name of the mathematical object.  This can
% range from simple definitions like |\def\Reals{\mathbb{R}}| for individual mathematical
% objects to more complex (functional) ones object constructors like
% |\def\SmoothFunctionsOn#1{\mathcal{C}^\infty(#1,#1)}|. Semantic macros are traditionally
% used to make {\TeX/\LaTeX} code more portable. However, the {\TeX/\LaTeX} scoping model
% (macro definitions are scoped either in the local group or until the rest of the
% document), does not mirror mathematical practice, where notations are scoped by
% mathematical environments like statements, theories, or such. For an in-depth discussion
% of semantic macros and scoping we refer the reader~\cite{Kohlhase:ulsmf08}.
% 
% The |modules| package provides a {\LaTeX}-based markup infrastructure for defining
% module-scoped semantic macros and {\latexml} bindings~\cite{Miller:latexml:online} to
% create {\omdoc}~\cite{Kohlhase:OMDoc1.2} from {\stex} documents. In the {\stex} world
% semantic macros have a special status, since they allow the transformation of
% {\TeX/\LaTeX} formulae into a content-oriented markup format like
% {\openmath}~\cite{BusCapCar:2oms04} and (strict) content
% {\mathml}~\cite{CarlisleEd:MathML3}; see Figure~\ref{fig:omsemmac} for an example, where
% the semantic macros above have been defined by the |\symdef| macros (see
% Section~\ref{sec:symdef}) in the scope of a |\begin{module}[id=calculus]| (see
% Section~\ref{sec:modules}).
% 
% \begin{exfig}\lstset{basicstyle=\scriptsize,aboveskip=-.5em,belowskip=-1.5em}
% \begin{tabular}{l|p{9.7cm}}
% \LaTeX  & \verb|\SmoothFunctionsOn\Reals| \\\hline
% PDF/DVI & ${\mathcal{C}^\infty(\mathbb{R},\mathbb{R})}$\\\hline
%  {\openmath} & \lstset{morekeywords={OMA,OMS}}
% \begin{lstlisting}
% <OMA>
%   <OMS cd="calculus" name="SmoothFunctionsOn"/>
%   <OMS cd="calculus" name="Reals"/>
% </OMA>\end{lstlisting}\\\hline
% {\mathml}  & \lstset{morekeywords={apply,csymbol}}
% \begin{lstlisting}
% <apply>
%   <csymbol cd="calculus">SmoothFunctionsOn</csymbol>
%   <csymbol cd="calculus">Reals</csymbol>
% </apply>\end{lstlisting}\\
% \end{tabular}
% \caption{{\openmath} and {\mathml} generated from Semantic Macros}\label{fig:omsemmac}
% \end{exfig}
% 
% \section{The User Interface}
%
% The main contributions of the |modules| package are the |module| environment, which
% allows for lexical scoping of semantic macros with inheritance and the |\symdef| macro
% for declaration of semantic macros that underly the |module| scoping.
% 
% \subsection{Package Options}\label{sec:options}
%
% The |modules| package takes six options: If we set
% \DescribeMacro{showmods}|showmods|\ednote{This mechanism does not work yet, since we
% cannot disable it when importing modules and that leads to unwanted boxes. What we need
% to do instead is to tweak the sms utility to use an internal version that never shows
% anything during sms reading.}, then the views (see Section~\ref{sec:user:views}) are
% shown. If we set the \DescribeMacro{qualifiedimports}|qualifiedimports| option, then
% qualified imports are enabled. Qualified imports give more flexibility in module
% inheritance, but consume more internal memory. As qualified imports are not fully
% implemented at the moment, they are turned off by default see
% Limitation~\ref{sec:limitations:qualified-imports}. The option
% \DescribeMacro{noauxreq}|noauxreq| prohibits the registration of |\@requiremodules|
% commands in the |aux| file. They are necessary for preloading the module signatures so
% that entries in the table of contents can have semantic macros; but as they sometimes
% cause trouble the option allows to turn off preloading. 
% 
% If the \DescribeMacro{showmeta}|showmeta| optin is set, then the metadata keys are shown
% (see~\cite{Kohlhase:metakeys:ctan} for details and customization options).
%
% The \texttt{mh} option enables MathHub support; see~\cite{Kohlhase:mss:ctan}.
%
% Finally, if the \DescribeMacro{trwarn}|trwrn| is given, then the |modules| package only
% gives warnings instead of hard errors when term references are unknown. 
% 
% \subsection{Semantic Macros}\label{sec:symdef}
%
% The \DescribeMacro{\symdef} is the main constructor for semantic macros in {\sTeX}. A
% call to the |\symdef| macro has the general form
% \begin{quote}
% |\symdef[|\meta{keys}|]{|\meta{cseq}|}[|\meta{args}|]{|\meta{definiens}|}|
% \end{quote}
% where {\meta{cseq}} is a control sequence (the name of the semantic macro) {\meta{args}}
% is a number between 0 and 9 for the number of arguments {\meta{definiens}} is the token
% sequence used in macro expansion for {\meta{cseq}}. Finally {\meta{keys}} is a keyword
% list that further specifies the semantic status of the defined macro.
% 
% The two semantic macros in Figure~\ref{fig:omsemmac} would have been declared by
% invocations of the |\symdef| macro of the form:
% \begin{verbatim}
% \symdef{Reals}{\mathbb{R}}
% \symdef{SmoothFunctionsOn}[1]{\mathcal{C}^\infty(#1,#1)}
% \end{verbatim}
% 
% Note that both semantic macros correspond to {\openmath} or {\mathml} ``symbols'',
% i.e. named representations of mathematical concepts (the real numbers and the
% constructor for the space of smooth functions over a set); we call these names the
% \textbf{symbol name} of a semantic macro. Normally, the symbol name of a semantic macro
% declared by a |\symdef| directive is just \meta{cseq}. The key-value pair
% \DescribeMacro{name}|name=|\meta{symname} can be used to override this behavior and
% specify a differing name. There are two main use cases for this.
% 
% The first one is shown in Example~\ref{fig:symvariant}, where we define semantic macros
% for the ``exclusive or'' operator. Note that we define two semantic macros: |\xorOp| and
% |\xor| for the applied form and the operator. As both relate to the same mathematical
% concept, their symbol names should be the same, so we specify |name=xor| on the
% definition of |\xorOp|.
% 
% A key \DescribeMacro{local}|local| can be added to {\meta{keys}} to specify that the
% symbol is local to the module and is invisible outside. Note that even though |\symdef|
% has no advantage over |\def| for defining local semantic macros, it is still considered
% good style to use |\symdef| and |\abbrdef|, if only to make switching between local and
% exported semantic macros easier.
% 
% Finally, the key \DescribeMacro{primary}|primary| (no value) can be given for primary
% symbols.
% 
% \DescribeMacro{\abbrdef}The |\abbrdef| macro is a variant of |\symdef| that is only
% different in semantics, not in presentation. An abbreviative macro is like a semantic
% macro, and underlies the same scoping and inheritance rules, but it is just an
% abbreviation that is meant to be expanded, it does not stand for an atomic mathematical
% object.
%
% We will use a simple module for natural number arithmetics as a running example. It
% defines exponentiation and summation as new concepts while drawing on the basic
% operations like $+$ and $-$ from {\LaTeX}. In our example, we will define a semantic
% macro for summation |\Sumfromto|, which will allow us to express an expression like
% $\sum{i=1}^nx^i$ as |\Sumfromto{i}1n{2i-1}| (see Example~\ref{fig:semmodule} for an
% example). In this example we have also made use of a local semantic symbol for $n$,
% which is treated as an arbitrary (but fixed) symbol.
%
%\begin{exfig}
% \begin{verbatim}
% \begin{module}[id=arith]
%   \symdef{Sumfromto}[4]{\sum_{#1=#2}^{#3}{#4}}
%   \symdef[local]{arbitraryn}{n}
%   What is the sum of the first $\arbitraryn$ odd numbers, i.e.
%   $\Sumfromto{i}1\arbitraryn{2i-1}?$
% \end{module}
% \end{verbatim}
% \vspace*{-3.5ex}\hrule\vspace*{1ex}
% \begin{module}[id=arith]
% \symdef{Sumfromto}[4]{\sum_{#1=#2}^{#3}{#4}}
% \symdef[local]{arbitraryn}{n}
% What is the sum of the first $\arbitraryn$ odd numbers, i.e.
% $\Sumfromto{i}1\arbitraryn{2i-1}?$
% \end{module}
% \caption{Semantic Markup in a {\texttt{module}} Context}\label{fig:semmodule}
% \end{exfig}
%
% The \DescribeMacro{\symvariant}|\symvariant| macro can be used to define presentation
% variants for semantic macros previously defined via the |\symdef| directive. In an
% invocation 
% \begin{quote}
% |\symdef[|\meta{keys}|]{|\meta{cseq}|}[|\meta{args}|]{|\meta{pres}|}|\\
% |\symvariant{|\meta{cseq}|}[|\meta{args}|]{|\meta{var}|}{|\meta{varpres}|}|
% \end{quote}
% the first line defines the semantic macro |\|\meta{cseq} that when applied to
% \meta{args} arguments is presented as \meta{pres}. The second line allows the semantic
% macro to be called with an optional argument \meta{var}: |\|\meta{cseq}|[var]| (applied
% to \meta{args} arguments) is then presented as \meta{varpres}. We can define a variant
% presentation for |\xor|; see Figure~\ref{fig:symvariant} for an example.
%
%\begin{exfig}
% \begin{verbatim}
% \begin{module}[id=xbool]
%   \symdef[name=xor]{xorOp}{\oplus}
%   \symvariant{xorOp}{uvee}{\underline{\vee}}
%   \symdef{xor}[2]{#1\xorOp #2}
%   \symvariant{xor}[2]{uvee}{#1\xorOp[uvee] #2}
%   Exclusive disjunction is commutative: $\xor{p}q=\xor{q}p$\\
%   Some authors also write exclusive or with the $\xorOp[uvee]$ operator, 
%   then the formula above is $\xor[uvee]{p}q=\xor[uvee]{q}p$
% \end{module}
% \end{verbatim}
% \vspace*{-3.5ex}\hrule\vspace*{1ex}
% \begin{module}[id=xbool]
%   \symdef[name=xor]{xorOp}{\oplus}
%   \symvariant{xorOp}{uvee}{\underline{\vee}}
%   \symdef{xor}[2]{#1\xorOp #2}
%   \symvariant{xor}[2]{uvee}{#1\xorOp[uvee] #2}
%   Exclusive disjunction is commutative: $\xor{p}q=\xor{q}p$\\
%   Some authors also write exclusive or with the $\xorOp[uvee]$ operator, 
%   then the formula above is $\xor[uvee]{p}q=\xor[uvee]{q}p$
% \end{module}
% \caption{Presentation Variants of a Semantic Macro}\label{fig:symvariant}
% \end{exfig}
%
% Version 1.0 of the |modules| package had the \DescribeMacro{\resymdef}|\resymdef| macro
% that allowed to locally redefine the presentation of a macro. But this did not interact
% well with the |beamer| package and was less useful than the |\symvariant|
% functionality. Therefore it is deprecated now and leads to an according error message.
% \subsection{Testing Semantic Macros}\label{sec:user:testing}
% 
% One of the problems in managing large module graphs with many semantic macros, so the
% |module| package gives an infrastructure for unit testing.  The first macro is
% \DescribeMacro{\symtest}|\symtest|, which allows the author of a semantic macro to
% generate test output (if the |symtest| option is set) see figure~\ref{fig:symtest} for a
% ``tested semantic macro definition''.
% \begin{exfig}
% \begin{verbatim}
% \symdef[name=setst]{SetSt}[2]{\{#1\,\vert\,#2\}}
% \symtest[name=setst]{SetSt}{\SetSt{a}{a>0}}
% \end{verbatim}
% \vspace*{-2em} generates the output 
% \begin{module}[id=foo]
% \symdef[name=setst]{SetSt}[2]{\{#1\,\vert\,#2\}}
% \symtest[name=setst]{SetSt}{\SetSt{a}{a>0}}
% \end{module}
% \caption{A Semantic Macro Definition with Test}\label{fig:symtest}
% \end{exfig}
% Note that the language in this purely generated, so that it can be adapted (tbd).
% 
% The \DescribeMacro{\abbrtest}|\abbrtest| macro gives the analogous functionality for
% |\abbrdef|. 
%
% \subsection{Axiomatic Assumptions}\label{sec:user:assumptions}
% 
% In many ways, axioms and assumptions in definitions behave a lot like symbols
% (see~\cite{RabKoh:WSMSML13} for discussion). Therefore we provide the macro
% \DescribeMacro{\assdef}|\assdef| that can be used to mark up assumptions. Given a phrase
% \meta{phrase} in a definition\ednote{only definitions?}, we can use
% |\assdef{|\meta{name}|}{|\meta{phrase}|}| to give this the symbol name
% \meta{name}.\ednote{continue}
%
% \subsection{Semantic Macros for Variables}\label{sec:user:semvars}
%
% Up to now, the semantic macros generated \openmath and \mathml markup where the heads of
% the semantic macros become constants (the |OMS| and |csymbol| elements in
% Figure~\ref{fig:omsemmac}). But sometimes we want to have semantic macros for variables,
% e.g. to associate special notation conventions. For instance, if we want to define
% mathematical structures from components as in Figure~\ref{fig:monoid}, where the
% semigroup operation $\circ$ is a variable epistemologically, but is a $n$-ary
% associative operator -- we are in a semigroup after all. Let us call such variables
% \textbf{semantic variables} to contrast them from \textbf{semantic constants} generated
% by |\symdef| and |\symvariant|.
%
%\begin{exfig}
%  \textbf{Definition 3.17} Let $\langle G,\circ\rangle$ be a semigroup, then we call
%  $e\in G$ a \textbf{unit}, iff $e\circ x=x\circ e=x$. A semigroup with unit $\langle
%  G,\circ,e\rangle$ is called a \textbf{monoid}.
%  \caption{A Definition of a Structure with ``semantic
%  variables''.}\label{fig:monoid}
% \end{exfig}
%
% Semantic variables differ from semantic constants in two ways:
% \begin{enumerate}
% \item they do not participate
% in the imports mechanism and
% \item they generate markup with variables.
% \end{enumerate}
%  In the case of
% Figure~\ref{fig:monoid} we (want to) have the \xml markup in Figure~\ref{fig:omsemvar}.
% To associate the notation to the variables, we define semantic macros for them, here the
% macro |\op| for the (semigroup) operation via the \DescribeMacro{\vardef}|\vardef|
% macro. |\vardef| works exactly like, except
% \begin{enumerate}
% \item semantic variables are local to the current {\TeX} group and 
% \item they generate variable markup in the \xml
% \end{enumerate}
% 
% \begin{exfig}\lstset{basicstyle=\scriptsize,aboveskip=-.5em,belowskip=-1.5em}
% \begin{tabular}{l|p{9.7cm}}
% \sTeX   & \verb|\vardef{op}[1]{\assoc\circ{#1}}|\\\hline
% \omdoc & 
% \begin{lstlisting}
% <notation>
%   <prototype>
%     <OMA>
%       <OMV name="op"/>
%       <expr name="a1"/>
%       <expr name="a2"/>
%      </OMA>
%   </prototype>
%   <rendering>
%     <mrow>
%       <render name="a1"/>
%       <mo>&#x2384;</mo>
%       <render name="a2"/>
%     </mrow>
%   </rendering>
% </notation>\end{lstlisting}\\\hline
% \LaTeX  & \verb|\op{x,e}| \\\hline
% PDF/DVI & $x\circ e$\\\hline
%  {\openmath} & \lstset{morekeywords={OMA,OMV}}
% \begin{lstlisting}
% <OMA><OMV name="op"/><OMV name="x"/><OMV name="e"/></OMA>\end{lstlisting}\\\hline
% {\mathml}  & \lstset{morekeywords={apply,ci}}
% \begin{lstlisting}
% <apply><ci>op</ci><ci>x</ci><ci>e</ci></apply>\end{lstlisting}\\
% \end{tabular}
% \caption{Semantic Variables in {\openmath} and {\mathml}}\label{fig:omsemvar}
% \end{exfig}
% 
% \subsection{Symbol and Concept Names}\label{sec:user:termdef}
% 
% Just as the |\symdef| declarations define semantic macros for mathematical symbols, the
% |modules| package provides an infrastructure for {\emph{mathematical concepts}} that are
% expressed in mathematical vernacular. The key observation here is that concept names
% like ``finite symplectic group'' follow the same scoping rules as mathematical symbols,
% i.e. they are module-scoped. The \DescribeMacro{\termdef}|\termdef| macro is an analogue
% to |\symdef| that supports this: use
% |\termdef[|\meta{keys}|]{|\meta{cseq}|}{|\meta{concept}|}| to declare the macro
% |\|\meta{cseq} that expands to \meta{concept}. See Figure~\ref{fig:termref} for an
% example, where we use the \DescribeMacro{\capitalize}|\capitalize| macro to adapt
% \meta{concept} to the sentence beginning.\ednote{continue, describe \meta{keys}, they
% will have to to with plurals,\ldots once implemented}. The main use of the
% |\termdef|-defined concepts lies in automatic cross-referencing facilities via the
% \DescribeMacro{\termref}|\termref| and \DescribeMacro{\symref}|\symref| macros provided
% by the |statements| package~\ctancite{Kohlhase:smms}. Together with the |hyperref|
% package~\cite{RahObe:hmlmh10}, this provide cross-referencing to the definitions of the
% symbols and concepts. As discussed in section~\ref{sec:limitations:crossref}, the
% |\symdef| and |\termdef| declarations must be on top-level in a module, so the
% infrastructure provided in the |modules| package alone cannot be used to locate the
% definitions, so we use the infrastructure for mathematical statements for that.
%
%\begin{exfig}
% \begin{verbatim}
%   \termdef[name=xor]{xdisjunction}{exclusive disjunction}
%   \capitalize\xdisjunction is commutative: $\xor{p}q=\xor{q}p$
% \end{verbatim}
% \vspace*{-3.5ex}
% \caption{Extending Example~\ref{fig:symvariant} with Term References}\label{fig:termref}
% \end{exfig}
%
% \subsection{Modules and Inheritance}\label{sec:modules}
%
% The\DescribeEnv{module}|module| environment takes an optional |KeyVal|
% argument. Currently, only the |id| key is supported for specifying the identifier of a
% module (also called the {\twintoo{module}{name}}).  A module introduced by
% |\begin{module}[id=foo]| restricts the scope the semantic macros defined by the
%   |\symdef| form to the end of this module given by the corresponding |\end{module}|,
% and to any other |module| environments that import them by a |\importmodule{foo}|
% directive. If the module |foo| contains |\importmodule| directives of its own, these are
% also exported to the importing module.
%
% Thus the \DescribeMacro{\importmodule}|\importmodule| declarations induce the
% {\atwintoo{semantic}{inheritance}{relation}}. Figure~\ref{exf:importmodule} shows a
% module that imports the semantic macros from three others. In the simplest form,
% |\importmodule{|\meta{mod}|}| will activate the semantic macros and concepts declared by
% |\symdef| and |\termdef| in module \meta{mod} in the current module\footnote{Actually,
% in the current {\TeX} group, therefore \texttt{\textbackslash importmodule} should be
% placed directly after the \texttt{\textbackslash begin\{module\}}.}. To understand the
% mechanics of this, we need to understand a bit of the internals. The |module|
% environment sets up an internal macro pool, to which all the macros defined by the
% |\symdef| and |\termdef| declarations are added; |\importmodule| only activates this
% macro pool. Therefore |\importmodule{|\meta{mod}|}| can only work, if the {\TeX} parser
% --- which linearly goes through the {\sTeX} sources --- already came across the module
% \meta{mod}. In many situations, this is not obtainable; e.g. for ``semantic forward
% references'', where symbols or concepts are previewed or motivated to knowledgeable
% readers before they are formally introduced or for modularizations of documents into
% multiple files. To enable situations like these, the |module| package uses auxiliary
% files called {\textbf{\sTeX module signatures}}. For any file, \meta{file}|.tex|, we
% generate a corresponding \sTeX module signature \meta{file}|.sms| with the |sms| utility
% (see also Limitation~\ref{sec:limitations:sms}), which contains (copies of) all
% |\begin|/|\end{module}|, |\importmodule|, |\symdef|, and |\termdef| invocations in
% \meta{file}|.tex|. The value of an \sTeX module signature is that it can be loaded
% instead its corresponding \sTeX document, if we are only interested in the semantic
% macros. So |\importmodule[|load=\meta{filepath}|]{|\meta{mod}|}| will load the \sTeX
% module signature \meta{filepath}|.sms| (if it exists and has not been loaded before) and
% activate the semantic macros from module \meta{mod} (which was supposedly defined in
% \meta{filepath}|.tex|). Note that since \meta{filepath}|.sms| contains all
% |\importmodule| statements that \meta{filepath}|.tex| does, an |\importmodule|
% recursively loads all necessary files to supply the semantic macros inherited by the
% current module.\ednote{MK: document the other keys of |module|}
% 
% The \DescribeMacro{\metalanguage}|\metalanguage| macro is a variant of
% \lstinline|importmodule| that imports the meta language, i.e. the language in which the
% meaning of the new symbols is expressed. For mathematics this is often first-order logic
% with some set theory; see~\cite{RabKoh:WSMSML13} for discussion. 
% 
% \subsection{Dealing with multiple Files}\label{sec:user:multiple}
%
% The infrastructure presented above works well if we are dealing with small files or
% small collections of modules. In reality, collections of modules tend to grow, get
% re-used, etc, making it much more difficult to keep everything in one file. This general
% trend towards increasing entropy is aggravated by the fact that modules are very
% self-contained objects that are ideal for re-used. Therefore in the absence of a
% content management system for {\LaTeX} document (fragments), module collections tend to
% develop towards the ``one module one file'' rule, which leads to situations with lots
% and lots of little files.
%
% Moreover, most mathematical documents are not self-contained, i.e. they do not build up
% the theory from scratch, but pre-suppose the knowledge (and notation) from other
% documents. In this case we want to make use of the semantic macros from these
% prerequisite documents without including their text into the current document. One way
% to do this would be to have {\LaTeX} read the prerequisite documents without producing
% output. For efficiency reasons, {\stex} chooses a different route. It comes with a
% utility |sms| (see Section~\ref{sec:limitations:sms}) that exports the modules and macros
% defined inside them from a particular document and stores them inside |.sms| files. This
% way we can avoid overloading LaTeX with useless information, while retaining the
% important information which can then be imported in a more efficient way.
%
% \DescribeMacro{\importmodule} For such situations, the |\importmodule| macro can be
% given an optional first argument that is a path to a file that contains a path to the
% module file, whose module definition (the |.sms| file) is read. Note that the
% |\importmodule| macro can be used to make module files truly self-contained. To arrive
% at a file-based content management system, it is good practice to reuse the module
% identifiers as module names and to prefix module files with corresponding
% |\importmodule| statements that pre-load the corresponding module files.
%
%\begin{exfig}
% \begin{verbatim}
% \begin{module}[id=foo]
% \importmodule[load=../other/bar]{bar}
% \importmodule[load=../mycolleaguesmodules]{baz}
% \importmodule[load=../other/bar]{foobar}
%   ...
% \end{module}
% \end{verbatim}
% \vspace{-1.7em}
% \caption{Self-contained Modules via {\texttt{importmodule}}}\label{exf:importmodule}
% \end{exfig}
%
% In Example~\ref{exf:importmodule}, we have shown the typical setup of a module
% file. The |\importmodule| macro takes great care that files are only read once, as
% {\sTeX} allows multiple inheritance and this setup would lead to an exponential (in the
% module inheritance depth) number of file loads.
%
% Sometimes we want to import an existing {\omdoc} theory\footnote{{\omdoc} theories are
%   the counterpart of {\stex} modules.} $\widehat\cT$ into (the {\omdoc} document
% $\widehat\cD$ generated from) a {\stex} document $\cD$. Naturally, we have to provide an
% {\stex} stub module $\cT$ that provides |\symdef| declarations for all symbols we use in
% $\cD$. In this situation, we use\DescribeMacro{\importOMDocmodule}
% |\importOMDocmodule[|\meta{spath}|]{|\meta{OURI}|}{|\meta{name}|}|, where \meta{spath}
% is the file system path to $\cT$ (as in |\importmodule|, this argument must not contain
% the file extension), \meta{OURI} is the URI to the {\omdoc} module (this time with
% extension), and \meta{name} is the name of the theory $\widehat\cT$ and the module in
% $\cT$ (they have to be identical for this to work). Note that since the \meta{spath}
% argument is optional, we can make ``local imports'', where the stub $\cT$ is in $\cD$
% and only contains the |\symdef|s needed there.
%
% Note that the recursive (depth-first) nature of the file loads induced by this setup is
% very natural, but can lead to problems with the depth of the file stack in the {\TeX}
% formatter (it is usually set to something like 15\footnote{If you have sufficient rights
% to change your {\TeX} installation, you can also increase the variable
% {\texttt{max\_in\_open}} in the relevant {\texttt{texmf.cnf}} file. Setting it to 50
% usually suffices}). Therefore, it may be necessary to circumvent the recursive load
% pattern providing (logically spurious) |\importmodule| commands. Consider for instance
% module |bar| in Example~\ref{exf:importmodule}, say that |bar| already has load depth
% 15, then we cannot naively import it in this way. If module |bar| depended say on a
% module |base| on the critical load path, then we could add a statement
% \DescribeMacro{\requiremodules} |\requiremodules{../base}| in the second line.  This
% would load the modules from |../base.sms| in advance (uncritical, since it has load
% depth 10) without activating them, so that it would not have to be re-loaded in the
% critical path of the module |foo|. Solving the load depth problem.
% 
% The \DescribeMacro{\inputref}|\inputref| macro behaves just like |\input| in the
% {\LaTeX} workflow, but in the {\latexml} conversion process creates a reference to the
% transformed version of the input file instead.
% 
% \subsection{Using Semantic Macros in Narrative Structures}\label{sec:user:using}
% 
% The |\importmodule| macro establishes the inheritance relation, a transitive relation
% among modules that governs visibility of semantic macros. In particular, it can only be
% used in modules (and has to be used at the top-level, otherwise it is hindered by
% {\LaTeX} groups). In many cases, we only want to \emph{use} the semantic macros in an
% environment (and not re-export them). Indeed, this is the normal situation for most
% parts of mathematical documents. For that \sTeX provides the
% \DescribeMacro{\usemodule}|\usemodule| macro, which takes the same arguments as
% |\importmodule|, but is treated differently in the \sTeX module signatures. A typical
% situation is shown in Figure~\ref{fig:use-ring}, where we open the module |ring| (see
% Figure~\ref{fig:ring}) and use its semantic macros (in the |omtext| environment). In
% earlier versions of \sTeX, we would have to wrap the |omtext| environment in an
% anonymous |module| environment to prevent re-export. 
% 
%\begin{exfig}
% \begin{verbatim}
% \begin{omtext}
%   \usemodule[load=../algebra/rings.tex]{ring}
%   We $R$ be a ring $(\rbase,\rplus,\rzero,\rminusOp,\rtimes,\rone)$, ...
% \end{omtext}
% \end{verbatim}
% \caption{Using Semantic Macros in Narrative Structures}\label{fig:use-ring}
% \end{exfig}
%
% \subsection{Including Externally Defined Semantic Macros }
% 
% In some cases, we use an existing {\LaTeX} macro package for typesetting objects that
% have a conventionalized mathematical meaning. In this case, the macros are ``semantic''
% even though they have not been defined by a |\symdef|. This is no problem, if we are
% only interested in the {\LaTeX} workflow. But if we want to e.g. transform them to
% {\omdoc} via {\latexml}, the {\latexml} bindings will need to contain references to an
% {\omdoc} theory that semantically corresponds to the {\LaTeX} package. In particular,
% this theory will have to be imported in the generated {\omdoc} file to make it
% {\omdoc}-valid. 
%
% \DescribeMacro{\requirepackage} To deal with this situation, the |modules| package
% provides the |\requirepackage| macro. It takes two arguments: a package name, and a URI
% of the corresponding {\omdoc} theory. In the {\LaTeX} workflow this macro behaves like a
% |\usepackage| on the first argument, except that it can --- and should --- be used
% outside the {\LaTeX} preamble. In the {\latexml} workflow, this loads the {\latexml}
% bindings of the package specified in the first argument and generates an appropriate
% |imports| element using the URI in the second argument.
%
% \section{Limitations \& Extensions}\label{sec:limitations}
% 
% In this section we will discuss limitations and possible extensions of the |modules|
% package. Any contributions and extension ideas are welcome; please discuss ideas,
% requests, fixes, etc on the {\sTeX} TRAC~\cite{sTeX:github:on}.
% 
% \subsection{Perl Utility \texttt{sms}}\label{sec:limitations:sms}
% 
% Currently we have to use an external perl utility |sms| to extract \sTeX module
% signatures from \sTeX files. This considerably adds to the complexity of the \sTeX
% installation and workflow. If we can solve security setting problems that allows us to
% write to \sTeX module signatures outside the current directory, writing them from \sTeX
% may be an avenue of future development see~\cite[issue \#1522]{sTeX:github:on} for a
% discussion.
% 
% \subsection{Qualified Imports}\label{sec:limitations:qualified-imports}
% 
% In an earlier version of the \texttt{modules} package we used the \texttt{usesqualified}
% for importing macros with a disambiguating prefix (this is used whenever we have
% conflicting names for macros inherited from different modules). This is not accessible
% from the current interface. We need something like a |\importqualified| macro for this;
% see~\cite[issue \#1505]{sTeX:github:on}. Until this is implemented the infrastructure is
% turned off by default, but we have already introduced the
% \DescribeMacro{qualifiedimports}|qualifiedimports| option for the future.
% 
% \subsection{Error Messages}\label{sec:limitations:errormsg}
% 
% The error messages generated by the |modules| package are still quite bad. For instance
% if |thyA| does note exists we get the cryptic error message 
% \begin{verbatim}
% ! Undefined control sequence.
% \module@defs@thyA ...hy 
%                        \expandafter \mod@newcomma...
% l.490 ...ortmodule{thyA}
% \end{verbatim}
% This should definitely be improved. 
% 
% \subsection{Crossreferencing}\label{sec:limitations:crossref}
% 
% Note that the macros defined by |\symdef| are still subject to the normal {\TeX} scoping
% rules. Thus they have to be at the top level of a module to be visible throughout the
% module as intended. As a consequence, the location of the |\symdef| elements cannot be
% used as targets for crossreferencing, which is currently supplied by the |statement|
% package~\ctancite{Kohlhase:smms}. A way around this limitation would be to import
% the current module from the \sTeX module signature (see Section~\ref{sec:modules}) via
% the |\importmodule| declaration.
% 
% \subsection{No Forward Imports}\label{sec:limitations:forward-imports}
% 
% {\sTeX} allows imports in the same file via |\importmodule{|\meta{mod}|}|, but due to
% the single-pass linear processing model of {\TeX}, \meta{mod} must be the name of a
% module declared {\emph{before}} the current point. So we cannot have forward imports as
% in \ednote{usemodule should work here; revise}
% \begin{verbatim}
% \begin{module}[id=foo]
%   \importmodule{mod}
%   ...
% \end{module}
% ... 
% \begin{module}[id=mod]
%   ... 
% \end{module}
% \end{verbatim}
% a workaround, we can extract the module \meta{mod} into a file {{{mod.tex}}} and replace
% it with |\sinput{mod}|, as in
% \begin{verbatim}
% \begin{module}[id=foo]
%   \importmodule[load=mod]{mod}
%   ...
% \end{module}
% ... 
% \sinput{mod}
% \end{verbatim}
% then the |\importmodule| command can read |mod.sms| (created via the |sms| utility)
% without having to wait for the module \meta{mod} to be defined.
% 
% \StopEventually{\newpage\PrintIndex\newpage\PrintChanges\newpage\printbibliography}\newpage
%
% \section{The Implementation} 
%
% The |modules| package generates two files: the {\LaTeX} package (all the code between
% {\textlangle\textsf{*package}\textrangle} and {\textsf{\textlangle/package\textrangle}})
% and the {\latexml} bindings (between {\textsf{\textlangle*ltxml\textrangle}} and
% {\textsf{\textlangle/ltxml\textrangle}}). 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
% options. Generally, an option |xxx| will just set the appropriate switches to true
% (otherwise they stay false). The options we are not using, we pass on to the |sref|
% package we require next.
%    \begin{macrocode}
%<*package>
\newif\if@modules@mh@\@modules@mh@false
\DeclareOption{mh}{\@modules@mh@true}
\newif\ifmod@show\mod@showfalse
\DeclareOption{showmods}{\mod@showtrue}
\newif\ifaux@req\aux@reqtrue
\DeclareOption{noauxreq}{\aux@reqfalse}
\newif\ifmod@qualified\mod@qualifiedfalse
\DeclareOption{qualifiedimports}{\mod@qualifiedtrue}
\newif\if@trwarn\@trwarnfalse
\DeclareOption{trwarn}{\@trwarntrue}
\newif\if@mmt\@mmtfalse 
\DeclareOption{mmt}{\@mmttrue}
\DeclareOption*{\PassOptionsToPackage{\CurrentOption}{sref}}
\ProcessOptions
%    \end{macrocode}
%
% {\latexml} does not support module options yet, so we do not have to do anything here
% for the {\latexml} bindings. We only set up the {\perl} packages (and tell {\texttt{emacs}}
% about the appropriate mode for convenience  
% 
% The next measure is to ensure that the |sref| and |xcomment| packages are loaded (in the
% right version). For {\latexml}, we also initialize the package inclusions.
%    \begin{macrocode}
\RequirePackage{sref}
\if@modules@mh@\RequirePackage{modules-mh}\fi
\if@mmt\RequirePackage{mmt}\fi
\RequirePackage{xspace}
\RequirePackage{mdframed}
\RequirePackage{pathsuris}
%    \end{macrocode}
%
% \subsection{Modules and Inheritance}\label{sec:impl:modules}
% 
% We define the keys for the |module| environment and the actions that are undertaken,
% when the keys are encountered.
%
% \begin{macro}{module:cd}
%    This |KeyVal| key is only needed for {\latexml} at the moment; use this to specify a
%    content dictionary name that is different from the module name.
%    \begin{macrocode}
\addmetakey{module}{cd}% no longer used
\addmetakey{module}{load}% ignored
\addmetakey*{module}{title}
\addmetakey*{module}{creators}
\addmetakey*{module}{contributors}
\addmetakey*{module}{srccite}
\addmetakey*{module}{align}[WithTheModuleOfTheSameName]
\addmetakey*{module}{noalign}[true]
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{module:id}
%   For a module with |[id=|\meta{name}|]|, we have a macro |\module@defs@|\meta{name}
%   that acts as a repository for semantic macros of the current module. I will be called
%   by |\importmodule| to activate them. We will add the internal forms of the semantic
%   macros whenever |\symdef| is invoked. To do this, we will need an unexpended form
%   |\this@module| that expands to |\module@defs@|\meta{name}; we define it first and then
%   initialize |\module@defs@|\meta{name} as empty. Then we do the same for qualified
%   imports as well (if the |qualifiedimports| option was specified). Furthermore, we save
%   the module name in the token register |\mod@id|.
%    \begin{macrocode}
\define@key{module}{id}{%
  \edef\this@module{%
    \expandafter\noexpand\csname module@defs@#1\endcsname%
  }%
  \csgdef{module@defs@#1}{}%
  \ifmod@qualified%
    \edef\this@qualified@module{%
      \expandafter\noexpand\csname module@defs@#1\endcsname%
    }%
    \csgdef{module@defs@qualified@#1}{}%
  \fi%
  \def\mod@id{#1}%
}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{module@heading}
%   Then we make a convenience macro for the module heading. This can be customized. 
%    \begin{macrocode}
\ifdef{\thesection}{\newcounter{module}[section]}{\newcounter{module}}%
\newrobustcmd\module@heading{%
  \stepcounter{module}%
  \ifmod@show%
    \noindent{\textbf{Module} \thesection.\themodule [\mod@id]}%
    \sref@label@id{Module \thesection.\themodule [\mod@id]}%
    \ifx\module@title\@empty :\quad\else\quad(\module@title)\hfill\\\fi%
  \fi%
}% mod@show
%    \end{macrocode}
% \end{macro}
%
% \begin{environment}{module}
%   Finally, we define the begin module command for the module environment. Much of the
%   work has already been done in the keyval bindings, so this is quite simple. We store
%   the file name (without extension) and extension of the module file in the global
%   macros |\module@|\meta{name}|@path| and |\module@|\meta{name}|@ext|, so that we can
%   use them later. The source of these two macros, |\mod@path| and |\mod@ext|, are
%   defined in |\requiremodules|.
%    \begin{macrocode}
\newenvironment{module}[1][]{%
  \begin{@module}[#1]%
  \ifcsundef{mod@id}{}{% only define if components are!
    \ifcsundef{mod@path}{}{\csxdef{module@\mod@id @path}{\mod@path}}%
    \ifcsundef{mod@ext}{}{\csxdef{module@\mod@id @ext}{\mod@ext}}%
  }%
  \if@mmt\if@importing\else\mmtheory{\mod@id}{????}\fi\fi%
  \module@heading% make the headings
  \ignorespaces}{%
  \if@mmt\if@importing\else\mmtheoryend\fi\fi%
  \end{@module}%
  \ignorespacesafterend%
}%
\ifmod@show\surroundwithmdframed{module}\fi%
%    \end{macrocode}
% \end{environment}
%
% \begin{environment}{@module}
%   A variant of the |module| environment that does not create printed representations (in
%   particular no frames) 
%    \begin{macrocode}
\newenvironment{@module}[1][]{\metasetkeys{module}{#1}}{}%
%    \end{macrocode}
% \end{environment}
%
% \begin{macro}{\activate@defs}
%   To activate the |\symdef|s from a given module \meta{mod}, we call the macro
%   |\module@defs@|\meta{mod}. But to make sure that every module is activated only once,
%   we only activate if the macro |\module@defs@|\meta{mod} is undefined, and define it
%   directly afterwards to prohibit further activations.
%    \begin{macrocode}
\def\activate@defs#1{%
  \ifcsundef{module@#1@activated}{\csname module@defs@#1\endcsname}{}%
  \@namedef{module@#1@activated}{true}%
}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\export@defs}
%   |\export@defs{|\meta{mod}|}| exports all the |\symdef|s from module \meta{mod} to the
%   current module (if it has the name \meta{currmod}), by adding a call to
%   |\module@defs@|\meta{mod} to the registry |\module@defs@|\meta{currmod}.\ednote{MK: I
%   have the feeling that we may be exporting modules multiple times here, is that a
%   problem?}\ednote{Jinbo: This part of code is extremely easy to generate bugs, cautiously edit this part of code.}\newline
%   Naive understanding of this code: |#1| be will be expanded first, then |\this@module|, then |\active@defs|, then |\g@addto@macro|. 
%    \begin{macrocode}
\def\export@defs#1{\@ifundefined{mod@id}{}{%
\expandafter\expandafter\expandafter\g@addto@macro%
\expandafter\this@module\expandafter{\activate@defs{#1}}}}%
%    \end{macrocode}
% \end{macro}
%
% Now we come to the implementation of |\importmodule|, but before we do, we define 
% conditional and an auxiliary macro: 
% \begin{macro}{\if@importing} 
%   |\if@importing| can be used to shut up macros in an import situation. 
%    \begin{macrocode}
\newif\if@importing\@importingfalse
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\update@used@modules}
%   This updates the register |\used@modules|
%    \begin{macrocode}
\newcommand\update@used@modules[1]{%
  \ifx\used@modules\@empty%
    \edef\used@modules{#1}%
  \else%
    \edef\used@modules{\used@modules,#1}%
  \fi}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\importmodule} 
%   The |\importmodule[|\meta{file}|]{|\meta{mod}|}| macro is an interface macro that
%   loads \meta{file} and activates and re-exports the |\symdef|s from module
%   \meta{mod}. As we will (probably) need to keep a record of the currently imported modules
%   (top-level only), we divide the functionality into a user-visible macro that records
%   modules in the |\used@modules| register and an internal one (|\@importmodule|)
%   that does the actual work.
%    \begin{macrocode}
\gdef\used@modules{}
\srefaddidkey{importmodule}
\addmetakey{importmodule}{load}
\addmetakey[sms]{importmodule}{ext}
\addmetakey[false]{importmodule}{conservative}[true]
\newcommand\importmodule[2][]{%
  \metasetkeys{importmodule}{#1}%
  \update@used@modules{#2}%
  \@importmodule[\importmodule@load]{#2}{\importmodule@ext}{export}%
  \ignorespacesandpars%
}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\@importmodule} 
%   |\@importmodule[|\meta{filepath}|]{|\meta{mod}|}{|\meta{ext}|}{|\meta{export?}|}|
%   loads \meta{filepath}|.|\meta{ext} (if it is given) and activates the module
%   \meta{mod}. If \meta{export?} is |export|, then it also re-exports the |\symdef|s from
%   \meta{mod}.
%
%   First |\@load| will store the base file name with full path, then check if
%   |\module@|\meta{mod}|@path| is defined. If this macro is defined, a module of this
%   name has already been loaded, so we check whether the paths coincide, if they do, all
%   is fine and we do nothing otherwise we give a suitable error. If this macro is
%   undefined we load the path by |\requiremodules|.
%    \begin{macrocode}
\newcommand\@importmodule[4][]{%
  {\@importingtrue% to shut up macros while in the group opened here
  \edef\@load{#1}%
  \ifx\@load\@empty%
    \relax%
  \else%
    \ifcsundef{module@#2@path}{%
      \requiremodules{#1}{#3}%
    }{%
      \edef\@path{\csname module@#2@path\endcsname}%
      \IfStrEq\@load\@path{% if the known path is the same as the requested one
        \relax% do nothing, it has already been loaded, else signal an error
	  }{%
        \PackageError{modules}
        {Module Name Clash\MessageBreak
        A module with name #2 was already loaded under the path "\@path"\MessageBreak
        The imported path "\@load" is probably a different module with the\MessageBreak
        same name; this is dangerous -- not importing}%
        {Check whether the Module name is correct}%
      }%
    }%
  \fi}%
  \activate@defs{#2}% activate the module
  \edef\@export{#4}\def\@@export{export}%prepare comparison
  \ifx\@export\@@export\export@defs{#2}\fi% export the module
  \if@importing\else\if@mmt\mmtinclude{#1?#2}\fi\fi%
}%
%    \end{macrocode}
% \end{macro}
% 
% \begin{macro}{\usemodule} 
%   |\usemodule| acts like |\importmodule|, except that the |sms| utility does not
%   transfer it to the module signatures and it does not re-export the symdefs.
%    \begin{macrocode}
\newcommand\usemodule[2][]{%
  \metasetkeys{importmodule}{#1}%
  \update@used@modules{#2}%
  \@importmodule[\importmodule@load]{#2}{\importmodule@ext}{noexport}%
  \ignorespacesandpars%
}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\withusedmodules} 
%   This variant just imports all the modules in a comma-separated list (usually
%   |\used@modules|)
%    \begin{macrocode}
\newcommand\withusedmodules[2]{{\@for\@I:=#1\do{\activate@defs\@I}{#2}}}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\importOMDocmodule} 
%   for the {\LaTeX} side we can just re-use |\importmodule|, for the {\latexml} side we
%   have a full URI anyways. So things are easy.\ednote{MK@DG: this macro is seldom used,
%   maybe I should just switch arguments.}
%    \begin{macrocode}
\newrobustcmd\importOMDocmodule[3][]{\importmodule[#1]{#3}}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\metalanguage} 
%   |\metalanguage| behaves exactly like |\importmodule| for formatting. For {\latexml},
%   we only add the |type| attribute.
%    \begin{macrocode}
\let\metalanguage=\importmodule%
%    \end{macrocode}
% \end{macro}
%
% \subsection{Semantic Macros}\label{sec:impl:symdef}
% 
% \begin{macro}{\mod@newcommand}
%   We first hack the {\LaTeX} kernel macros to obtain a version of the |\newcommand|
%   macro that does not check for definedness.
%    \begin{macrocode}
\let\mod@newcommand=\providerobustcmd%
%    \end{macrocode}
% \end{macro}
% 
% Now we define the optional KeyVal arguments for the |\symdef| form and the actions that
% are taken when they are encountered.
%
% \begin{environment}{conceptdef}
%    \begin{macrocode}
\srefaddidkey{conceptdef}%
\addmetakey*{conceptdef}{title}%
\addmetakey{conceptdef}{subject}%
\addmetakey*{conceptdef}{display}%
\def\conceptdef@type{Symbol}%
\newrobustcmd\conceptdef[2][]{%
  \metasetkeys{conceptdef}{#1}%
  \ifx\conceptdef@display\st@flow\else{\stDMemph{\conceptdef@type} #2:}\fi%
  \ifx\conceptdef@title\@empty~\else~(\stDMemph{\conceptdef@title})\par\fi%
}%
%    \end{macrocode}
% \ednote{MK@DG: maybe we need to add DefKeyVals here?}
% \end{environment}
% 
% \begin{macro}{symdef:keys}
%   The optional argument local specifies the scope of the function to be defined. If
%   local is not present as an optional argument then |\symdef| assumes the scope of the
%   function is global and it will include it in the pool of macros of the current
%   module. Otherwise, if local is present then the function will be defined only locally
%   and it will not be added to the current module (i.e. we cannot inherit a local
%   function).  Note, the optional key local does not need a value: we write
%   |\symdef[local]{somefunction}[0]{some expansion}|. The other keys are not used in the
%   {\LaTeX} part. 
%    \begin{macrocode}
\newif\if@symdeflocal%
\srefaddidkey{symdef}%
\define@key{symdef}{local}[true]{\@symdeflocaltrue}%
\define@key{symdef}{noverb}[all]{}%
\define@key{symdef}{align}[WithTheSymbolOfTheSameName]{}%
\define@key{symdef}{specializes}{}%
\addmetakey*{symdef}{noalign}[true]
\define@key{symdef}{primary}[true]{}%
\define@key{symdef}{assocarg}{}%
\define@key{symdef}{bvars}{}%
\define@key{symdef}{bargs}{}%
\addmetakey{symdef}{name}%
\addmetakey*{symdef}{title}%
\addmetakey*{symdef}{description}%
\addmetakey{symdef}{subject}%
\addmetakey*{symdef}{display}%
%    \end{macrocode}
% \end{macro}
% \ednote{MK@MK: we need to document the binder keys above.}
% \begin{macro}{\symdef}
%    The the |\symdef|, and |\@symdef| macros just handle optional arguments.
%    \begin{macrocode}
\def\symdef{\@ifnextchar[{\@symdef}{\@symdef[]}}%
\def\@symdef[#1]#2{\@ifnextchar[{\@@symdef[#1]{#2}}{\@@symdef[#1]{#2}[0]}}%
%    \end{macrocode}
% \end{macro}
%
% next we locally abbreviate |\mod@newcommand| to simplify argument passing.
%    \begin{macrocode}
\def\@mod@nc#1{\mod@newcommand{#1}[1]}%
%    \end{macrocode}
% and we copy a very useful piece of code from
% \url{http://tex.stackexchange.com/questions/23100/looking-for-an-ignorespacesandpars},
% it ignores spaces and following implicit paragraphs (double newlines), explicit |\par|s
% are respected however
%    \begin{macrocode}
\def\ignorespacesandpars{%
  \begingroup
  \catcode13=10
  \@ifnextchar\relax
    {\endgroup}%
    {\endgroup}%
}
%    \end{macrocode}
% and more adapted from \url{http://tex.stackexchange.com/questions/179016/ignore-spaces-and-pars-after-an-environment}
%    \begin{macrocode}
\def\ignorespacesandparsafterend#1\ignorespaces\fi{#1\fi\ignorespacesandpars}
\def\ignorespacesandpars{
  \ifhmode\unskip\fi%
  \@ifnextchar\par%
    {\expandafter\ignorespacesandpars\@gobble}%
    {}%
}
%    \end{macrocode}
% 
% \begin{macro}{\@@symdef}
%    now comes the real meat: the |\@@symdef| macro does two things, it adds the macro
%    definition to the macro definition pool of the current module and also provides it.
%    \begin{macrocode}
\def\@@symdef[#1]#2[#3]#4{%
%    \end{macrocode}
% We use a switch to keep track of the local optional argument. We initialize the switch
% to false and set all the keys that have been provided as arguments: |name|, |local|.
%    \begin{macrocode}
  \@symdeflocalfalse%
  \metasetkeys{symdef}{#1}%
%    \end{macrocode}
% If the |mmt| option is set and we are not importing, then we write out the constant
% declaration for this symdef\ednote{eventually we may want to do something about the
% notations. This would pass \#4 to MMT via a macro that makes the \# (argumentmarkers)
% active and empty. I am not clear how well this works, so we leave out notations.}
%    \begin{macrocode}
 \if@mmt\if@importing\else%
\ifx\symdef@name\@empty\mmtconstdec{#2}\else\mmtconstdec{\symdef@name}\fi%
\fi\fi%
%    \end{macrocode}
% First, using |\mod@newcommand| we initialize the intermediate macro
% |\module@|\meta{sym}|@pres@|, the one that can be extended with |\symvariant|
%    \begin{macrocode}
  \expandafter\mod@newcommand\csname modules@#2@pres@\endcsname[#3]{#4}%
%    \end{macrocode}
% and then we define the actual semantic macro, which when invoked with an optional
% argument \meta{opt} calls |\modules@|\meta{sym}|@pres@|\meta{opt} provided by the
% |\symvariant| macro.
%    \begin{macrocode}
  \expandafter\mod@newcommand\csname #2\endcsname[1][]%
  {\csname modules@#2@pres@##1\endcsname}%
%    \end{macrocode}
% Finally, we prepare the internal macro to be used in the |\symref| call.
%    \begin{macrocode}
  \expandafter\@mod@nc\csname mod@symref@#2\expandafter\endcsname\expandafter%
  {\expandafter\mod@termref\expandafter{\mod@id}{#2}{##1}}%
%    \end{macrocode}
% We check if the switch for the local scope is set: if it is we are done, since this
% function has a local scope. Similarly, if we are not inside a module, which we could
% export from.  
%    \begin{macrocode}
  \if@symdeflocal%
  \else%
    \ifcsundef{mod@id}{}{%
%    \end{macrocode}
% Otherwise, we add three functions to the module's pool of defined macros using
% |\g@addto@macro|. We first add the definition of the intermediate function
% |\modules@|\meta{sym}|@pres@|.
%    \begin{macrocode}
      \expandafter\g@addto@macro\this@module%
      {\expandafter\mod@newcommand\csname modules@#2@pres@\endcsname[#3]{#4}}%
%    \end{macrocode}
% Then we add add the definition of |\|\meta{sym}  which calls the intermediate
% function and handles the optional argument.
%    \begin{macrocode}
      \expandafter\g@addto@macro\this@module%
      {\expandafter\mod@newcommand\csname #2\endcsname[1][]%
      {\csname modules@#2@pres@##1\endcsname}}%
%    \end{macrocode}
% We also add |\mod@symref@|\meta{sym} macro to the macro pool so that the |\symref| macro
% can pick it up.
%    \begin{macrocode}
      \expandafter\g@addto@macro\csname  module@defs@\mod@id\expandafter\endcsname\expandafter%
      {\expandafter\@mod@nc\csname mod@symref@#2\expandafter\endcsname\expandafter%
      {\expandafter\mod@termref\expandafter{\mod@id}{#2}{##1}}}%
%    \end{macrocode}
% Finally, using |\g@addto@macro| we add the two functions to the qualified version of the
% module if the |qualifiedimports| option was set.
%    \begin{macrocode}
      \ifmod@qualified%
        \expandafter\g@addto@macro\this@qualified@module%
        {\expandafter\mod@newcommand\csname modules@#2@pres@qualified\endcsname[#3]{#4}}%
        \expandafter\g@addto@macro\this@qualified@module%
        {\expandafter\def\csname#2@qualified\endcsname{\csname modules@#2@pres@qualified\endcsname}}%
      \fi%
    }% mod@qualified
  \fi% symdeflocal
%    \end{macrocode}
% So now we only need to show the data in the symdef, if the options allow. 
%    \begin{macrocode}
  \ifmod@show%
    \ifx\symdef@display\st@flow\else{\noindent\stDMemph{\symdef@type} #2:}\fi%
    \ifx\symdef@title\@empty~\else~(\stDMemph{\symdef@title})\par\fi%
  \fi%
  \ignorespacesandpars%
}% mod@show
\def\symdef@type{Symbol}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\symvariant}
%   |\symvariant{|\meta{sym}|}[|\meta{args}|]{|\meta{var}|}{|\meta{cseq}|}| just extends
%   the internal macro |\modules@|\meta{sym}|@pres@| defined by
%   |\symdef{|\meta{sym}|}[|\meta{args}|]{|\ldots|}| with a variant
%   |\modules@|\meta{sym}|@pres@|\meta{var} which expands to \meta{cseq}. Recall that this
%   is called by the macro |\|\meta{sym}|[|\meta{var}|]| induced by the
%   |\symdef|.\ednote{MK@DG: this needs to be implemented in LaTeXML}
%    \begin{macrocode}
\def\symvariant#1{%
  \@ifnextchar[{\@symvariant{#1}}{\@symvariant{#1}[0]}%
  }%
\def\@symvariant#1[#2]#3#4{%
  \expandafter\mod@newcommand\csname modules@#1@pres@#3\endcsname[#2]{#4}%
%    \end{macrocode}
% and if we are in a named module, then we need to export the function
% |\modules@|\meta{sym}|@pres@|\meta{opt} just as we have done that in |\symdef|.
%    \begin{macrocode}
  \ifcsundef{mod@id}{}{%
    \expandafter\g@addto@macro\this@module%
    {\expandafter\mod@newcommand\csname modules@#1@pres@#3\endcsname[#2]{#4}}%
  }%
\ignorespacesandpars}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\resymdef}
%   This is now deprecated.
%    \begin{macrocode}
\def\resymdef{%
  \@ifnextchar[{\@resymdef}{\@resymdef[]}%
}%
\def\@resymdef[#1]#2{%
  \@ifnextchar[{\@@resymdef[#1]{#2}}{\@@resymdef[#1]{#2}[0]}%
}%
\def\@@resymdef[#1]#2[#3]#4{%
  \PackageError{modules}%
  {The \protect\resymdef macro is deprecated}{use the \protect\symvariant instead!}%
}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\abbrdef}
%   The |\abbrdef| macro is a variant of |\symdef| that does the same on the {\LaTeX}
%   level.
%    \begin{macrocode}
\let\abbrdef\symdef%
%    \end{macrocode}
% \end{macro}
%
% \subsection{Defining Math Operators}\label{sec:impl:defmathop}
%
% \begin{macro}{\DefMathOp} 
% |\DefMathOp[|\meta{key pair}|]{definition}| will take 2 arguments. ||\meta{key pair}|| should be something like |[name=...]|, for example, |[name=equal]|. Though |\setkeys|, |\defmathop@name| will be set. Further definition will be done by |\symdef|.
%    \begin{macrocode}
\define@key{DefMathOp}{name}{%
  \def\defmathop@name{#1}%
}%
\newrobustcmd\DefMathOp[2][]{%
  \setkeys{DefMathOp}{#1}%
  \symdef[#1]{\defmathop@name}{#2}%
}%
%    \end{macrocode}
% \end{macro}
%
%
% \subsection{Axiomatic Assumptions}\label{sec:impl:assumptions}
% 
% \begin{macro}{\assdef} 
%   We fake it for now, not clear what we should do on the {\LaTeX} side.
%    \begin{macrocode}
\newcommand\assdef[2][]{#2}
%    \end{macrocode}
% \end{macro}
%
% \subsection{Semantic Macros for Variables}\label{sec:impl:semvars}
%
% \begin{macro}{\vardef} 
%   We do the argument parsing like in |\symdef| above, but add the |local| key. All the
%   other changes are in the \latexml binding exclusively.
%    \begin{macrocode}
\def\vardef{\@ifnextchar[{\@vardef}{\@vardef[]}}%
\def\@vardef[#1]#2{%
  \@ifnextchar[{\@@vardef[#1]{#2}}{\@@vardef[#1]{#2}[0]}}
\def\@@vardef[#1]#2[#3]#4{%
  \def\@test{#1}%
  \ifx\@test\@empty%
    \@@symdef[local]{#2}[#3]{#4}%
  \else%
    \symdef[local,#1]{#2}[#3]{#4}%
  \fi%
  \ignorespacesandpars}%
%    \end{macrocode}
% \end{macro}
%
% \subsection{Testing Semantic Macros}\label{sec:impl:testing}
%
% \begin{macro}{\symtest}
%   Allows to test a |\symdef| in place, this shuts up when being imported.
%    \begin{macrocode}
\addmetakey{symtest}{name}%
\addmetakey{symtest}{variant}%
\newrobustcmd\symtest[3][]{%
  \if@importing%
  \else%
    \metasetkeys{symtest}{#1}%
    \par\noindent \textbf{Symbol}~%
    \ifx\symtest@name\@empty\texttt{#2}\else\texttt{\symtest@name}\fi%
    \ifx\symtest@variant\@empty\else\ (variant \texttt{\symtest@variant})\fi%
    \ with semantic macro %
    \texttt{\textbackslash #2\ifx\symtest@variant\@empty\else[\symtest@variant]\fi}%
    : used e.g. in \ensuremath{#3}%
  \fi%
  \ignorespacesandpars%
}%
%    \end{macrocode}
% \end{macro}
% 
% \begin{macro}{\abbrtest}
%    \begin{macrocode}
\addmetakey{abbrtest}{name}%
\newrobustcmd\abbrtest[3][]{%
  \if@importing%
  \else%
    \metasetkeys{abbrtest}{#1}%
    \par\noindent \textbf{Abbreviation}~%
    \ifx\abbrtest@name\@empty\texttt{#2}\else\texttt{\abbrtest@name}\fi%
    : used e.g. in \ensuremath{#3}%
  \fi%
  \ignorespacesandpars}%
%    \end{macrocode}
% \end{macro}
% 
% \subsection{Symbol and Concept Names}\label{sec:impl:concepts}
%
% \begin{macro}{\termdef} 
%    \begin{macrocode}
\def\mod@true{true}%
\addmetakey[false]{termdef}{local}%
\addmetakey{termdef}{name}%
\newrobustcmd\termdef[3][]{%
  \metasetkeys{termdef}{#1}%
  \expandafter\mod@newcommand\csname#2\endcsname[0]{#3\xspace}%
  \ifx\termdef@local\mod@true%
  \else%
    \ifcsundef{mod@id}{}{%
      \expandafter\g@addto@macro\this@module%
      {\expandafter\mod@newcommand\csname#2\endcsname[0]{#3\xspace}}%
    }%
  \fi%
}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\capitalize} 
%    \begin{macrocode}
\def\@capitalize#1{\uppercase{#1}}%
\newrobustcmd\capitalize[1]{\expandafter\@capitalize #1}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\module@component}
%   This macro computes the module component identifier for external links on term
%   references. It is initially empty, but can be redefined later (e.g.in the |smultiling|
%   package).
%    \begin{macrocode}
\newcommand\mod@component[1]{}
%    \end{macrocode}
% \end{macro}
% 
% \begin{macro}{\mod@termref} 
%   |\mod@termref{|\meta{module}|}{|\meta{name}|}{|\meta{nl}|}| determines whether the
%   macro |\module@|\meta{module}|@path| is defined. If it is, we make it the prefix of a
%   URI reference in the local macro |\@uri|, which we compose to the hyper-reference,
%   otherwise we give a warning.\ednote{MK: this should be rethought, in particular the
%   local reference does not work!}
%    \begin{macrocode}
\newcommand\mod@termref[3]{\def\@test{#3}%
  \@ifundefined{module@defs@#1}{%
    \protect\G@refundefinedtrue%
    \if@trwarn
      \PackageWarning{modules}{`\protect\termref' with unidentified cd "#1":\MessageBreak
        the cd key must reference an active module}%
    \else
      \PackageError{modules}{`\protect\termref' with unidentified cd "#1"}
      {the cd key must reference an active module}%
    \fi}%
  {\def\@label{sref@#2@#1\mod@component{#1}@target}%
    \@ifundefined{module@#1@path}% local reference
    {\sref@hlink@ifh{\@label}{\ifx\@test\@empty #2\else #3\fi}%
%      \footnote{sTeX mod@termref: local reference to\\ \@label}
    }%
    {\def\@uri{\csname module@#1@path\endcsname\mod@component{#1}.pdf\#\@label}%
      \sref@href@ifh{\@uri}{\ifx\@test\@empty #2\else #3\fi}%
%      \footnote{sTeX mod@termref: external reference to \\\@uri}
}%
  }}%
%    \end{macrocode}
% \end{macro}
%
% \subsection{Dealing with Multiple Files}\label{sec:impl:multiple}
%
% We use the |pathsuris| package deals with the canonicalization of paths. |\@cpath| will
% canonicalize a path and store the result into |\@CanPath|. To print a canoncalized path,
% simply use |\cpath{|\meta{path}|}|.
% 
% \begin{macro}{\@rinput}
%   |\@rinput{|\meta{path to the current file without extension}|}{|\meta{extension}|}| allows loading 
%   modules with relative path. For example, |\@rinput{foo/bar/B}{tex}| will load |foo/bar/B.tex|.
%   \ednote{Jinbo: How to handle |mod@path|?}
%    \begin{macrocode}
\def\CurrentDir{}%
\newrobustcmd{\@rinput}[2]{%
  \@cpath{\CurrentDir#1}%
  \StrCut[\value{RealAddrNum}]{/\@CanPath}{/}\@TempPath\@Rubbish%
  \StrCut[1]{\@TempPath/}{/}\@Rubbish\@DirPath%
  \edef\CurrentDir{\@DirPath}%
%  \edef\mod@path{}% what should I put in here???
%  \edef\mod@ext{}%
  \input{\@CanPath.#2}%
  \def\CurrentDir{}%
}%
%    \end{macrocode}
% \end{macro} 
%
% \subsection{Loading Module Signatures}
%
% \subsubsection{Selective Inclusion}
%
% \begin{macro}{\requiremodules}
%   this macro loads the modules in a file and makes sure that no text is deposited (we
%   set the flags |\mod@showfalse| and |\@importingtrue| in the local group). It also
%   remembers the file name and extension in |\mod@path| and |\mod@ext| so that
%   |\begin{module}| can pick them up later.
%    \begin{macrocode}
\newrobustcmd\requiremodules[2]{%
  \mod@showfalse%
  \@importingtrue% save state and ensure silence while reading sms
  \edef\mod@path{#1}%
  \edef\mod@ext{#2}% set up path/ext
  \input{#1.#2}%
}%
%    \end{macrocode}
% \end{macro}
% 
% \begin{macro}{\@requiremodules}
%   the internal version of |\requiremodules| for use in the |*.aux| file. We disable it
%   at the end of the document, so that when the |aux| file is read again, nothing is
%   loaded.
%    \begin{macrocode}
\newrobustcmd\@requiremodules[2]{%
  \if@tempswa\requiremodules{#1}{#2}\fi%
}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\inputref}
%   |\inputref{|\meta{path to the current file without extension}|}| supports both
%   absolute path and relative path, meanwhile, records the path and the extension (not
%   for relative path).  \ednote{MK: the first (optional) argument is not used. Maybe do
%   something with a non-standard (i.e. non-\texttt{tex}) extension with an optional
%   argument?}
%    \begin{macrocode}
\newrobustcmd\inputref[2][]{%
  \def\@Slash{/}
  \edef\@load{#2}%
  \StrChar{\@load}{1}[\@testchar]
  \ifx\@testchar\@Slash%
    \edef\mod@path{#2}%
    \edef\mod@ext{tex}%
    \input{#2}%
  \else%
    \@rinput{#2}{tex}%
  \fi%
}%
%    \end{macrocode}
% \end{macro}
% 
% \subsection{Including Externally Defined Semantic Macros }\label{sec:impl:packages}
% 
% \begin{macro}{\requirepackage}
%    \begin{macrocode}
\def\requirepackage#1#2{\makeatletter\input{#1.sty}\makeatother}%
%    \end{macrocode}
% \end{macro}
% 
% \subsection{Deprecated Functionality}\label{sec:impl:deprecated}
%
% \begin{macro}{\sinput*}
%    \begin{macrocode}
\newrobustcmd\sinput[1]{%
  \PackageError{modules}%
  {The `\protect\sinput' macro is deprecated}{use the \protect\input instead!}%
}%
\newrobustcmd\sinputref[1]{%
  \PackageError{modules}%
  {The \protect\sinputref macro is deprecated}{use the \protect\inputref instead!}%
}%
%    \end{macrocode}
% \end{macro}
%
% In this section we centralize old interfaces that are only partially supported any more. 
% \begin{macro}{module:uses}
%   For each the module name |xxx| specified in the |uses| key, we activate their symdefs
%   and we export the local symdefs.\ednote{this issue is deprecated, it will be removed
%     before 1.0.}
%    \begin{macrocode}
\define@key{module}{uses}{%
  \@for\module@tmp:=#1\do{\activate@defs\module@tmp\export@defs\module@tmp}%
}%
%    \end{macrocode}
% \end{macro}
% 
% \begin{macro}{module:usesqualified}
%   This option operates similarly to the module:uses option defined above. The only
%   difference is that here we import modules with a prefix. This is useful when two
%   modules provide a macro with the same name.
%    \begin{macrocode}
\define@key{module}{usesqualified}{%
  \@for\module@tmp:=#1\do{\activate@defs{qualified@\module@tmp}\export@defs\module@tmp}%
}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\coolurion/off}
%    \begin{macrocode}
\def\coolurion{\PackageWarning{modules}{coolurion is obsolete, please remove}}%
\def\coolurioff{\PackageWarning{modules}{coolurioff is obsolete, please remove}}%
%    \end{macrocode}
% \end{macro}
%
% \subsection{Experiments}
% In this section we develop experimental functionality. Currently support for complex
% expressions, see
% \url{https://svn.kwarc.info/repos/stex/doc/blue/comlex_semmacros/note.pdf} for details.
%
% \begin{macro}{\csymdef}
% For the {\LaTeX} we use |\symdef| and forget the last argument. The code here is just
% needed for parsing the (non-standard) argument structure. 
%    \begin{macrocode}
\def\csymdef{\@ifnextchar[{\@csymdef}{\@csymdef[]}}%
\def\@csymdef[#1]#2{%
  \@ifnextchar[{\@@csymdef[#1]{#2}}{\@@csymdef[#1]{#2}[0]}%
}%
\def\@@csymdef[#1]#2[#3]#4#5{%
  \@@symdef[#1]{#2}[#3]{#4}%
}%
%    \end{macrocode}
% \end{macro}
% 
% \begin{macro}{\notationdef}
% For the {\LaTeX} side, we just make |\notationdef| invisible.
%    \begin{macrocode}
\def\notationdef[#1]#2#3{}
%    \end{macrocode}
% \end{macro}
% 
% The code for avoiding duplicate loading is very very complex and brittle (and does not
% quite work). Therefore I would like to replace it with something better. It has two
% parts: 
% \begin{itemize}
% \item keeping a registry of file paths, and only loading when the file path has not been
%   mentioned in that, and
% \item dealing with relative paths (for that we have to string together prefixes and pass
%   them one)
% \end{itemize}
% For the first problem, there is a very nice and efficient solution using |etoolbox| which
% I document below. If I decide to do away with relative paths, this would be it.
% 
% \begin{macro}{\reqmodules}
%   We keep a file path registry |\@register| and only load a module signature, if it is
%   not in there.
%    \begin{macrocode}
\newrobustcmd\reqmodules[2]{%
  \ifinlist{#1}{\@register}{}{\listadd\@register{#1}\input{#1.#2}}%
}%
%    \end{macrocode}
% \end{macro}
% for the relative paths, I have to find out the directory prefix and the file name. Here
% are two helper functions, which work well, but do not survive being called in an
% |\edef|, which is what we would need. First some preparation: we set up a path parser
%    \begin{macrocode}
\newcounter{@pl}
\DeclareListParser*{\forpathlist}{/}
%    \end{macrocode}
%
% \begin{macro}{\file@name}
%   |\file@name| selects the filename of the file path: |\file@name{/foo/bar/baz.tex}| is
%   |baz.tex|.
%    \begin{macrocode}
\def\file@name#1{%
  \setcounter{@pl}{0}%
  \forpathlist{\stepcounter{@pl}\listadd\@pathlist}{#1}
  \def\do##1{%
    \ifnumequal{\value{@pl}}{1}{##1}{\addtocounter{@pl}{-1}}
  }%
  \dolistloop{\@pathlist}%
}%
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\file@path}
%   |\file@path| selects the path of the file path |\file@path{/foo/bar/baz.tex}| is
%   |/foo/bar|
%    \begin{macrocode}
\def\file@path#1{%
  \setcounter{@pl}{0}%
  \forpathlist{\stepcounter{@pl}\listadd\@pathlist}{#1}%
  \def\do##1{%
    \ifnumequal{\value{@pl}}{1}{}{%
      \addtocounter{@pl}{-1}%
      \ifnumequal{\value{@pl}}{1}{##1}{##1/}%
    }%
  }%
  \dolistloop{\@pathlist}%
}%
%</package>
%    \end{macrocode}
% \end{macro}
% what I would really like to do in this situation is 
% \begin{macro}{\NEWrequiremodules}
%   but this does not work, since the |\file@name| and |\file@path| do not survive the
%   |\edef|.
%    \begin{macrocode}
\def\@NEWcurrentprefix{}
\def\NEWrequiremodules#1{%
  \def\@pref{\file@path{#1}}%
  \ifx\@pref\@empty%
  \else%
    \xdef\@NEWcurrentprefix{\@NEWcurrentprefix/\@pref}%
  \fi%
  \edef\@input@me{\@NEWcurrentprefix/\file@name{#1}}%
  \message{requiring \@input@me}\reqmodule{\@input@me}%
}%
%    \end{macrocode}
% \end{macro}
% \Finale
\endinput
%%% Local Variables: 
%%% mode: doctex
%%% TeX-master: t
%%% End: 
% LocalWords:  GPL structuresharing STR dtx env envfalse idfalse displayfalse filedate nl
% LocalWords:  usesfalse usesqualified usesqualifiedfalse envtrue idtrue CPERL Rares pres
% LocalWords:  usestrue displaytrue usesqualifiedtrue RequirePackage keyval tmp 2oms04 eg
% LocalWords:  defs foreach LookupValue activateScope DefEnvironment keyvals cd varpres
% LocalWords:  OptionalKeyVals getValue toString AssignValue openElement omdoc uvee vee
% LocalWords:  closeElement beforeDigest useTheoryItemizations afterDigestBegin symtest
% LocalWords:  whatsit setProperty getArg qw symdef  iffalse importOMDocmodule symtest ci
% LocalWords:  DefKeyVal Semiverbatim symdeflocal atqualified DefMacro STDERR setst spath
% LocalWords:  args unlist DefPrimitive nargs Stringify eq attr omcd ltx XMTok abbrtest
% LocalWords:  convertLaTeXArgs scriptpos XMApp OMA XMArg simpl abbrtest 2oms04 circ ary
% LocalWords:  blaaaa savedprefix aaa simplhelp tust tist tost reguse spath baz rangle
% LocalWords:  updatedpre ReturnAfterFi updateall updatedpost updatesms bgroup includeref
% LocalWords:  texclude tinclude getGullet requiredmodule tex sms egroup pmml sincluderef
% LocalWords:  toks mixfixi mixfixa mixfixii mixfixia mixfixai mixfixiii arg cr OPaths
% LocalWords:  undef tok PARAM thyid BerFieMas inparaenum omsemvar vardef vardef mhview
% LocalWords:  getString showfalse showtrue xcomment stex srcref KeyVal omext osslepsdl13
% LocalWords:  beginItemize getProperty introdcue afterOpen numberIt Tokenize mathhub mmt
% LocalWords:  OptionalSemiverbatim omdocmod PushValue assocarg getStomach prs HorIacJuc
% LocalWords:  begingroup beginMode endMode endgroup insertElement resymdef sym cscpnrr11
% LocalWords:  updir nargkey PresFormatters mixfixaii formatters argname expr behavior
% LocalWords:  getSymmdefProperties XMath mcdcr exprlist recurse texttt scsys foobar mrow
% LocalWords:  textbackslash newcommand providecommand sc sc mathml openmath nx st@flow
% LocalWords:  latexml cmathml activemath twintoo atwin atwintoo mathcal Deyan viewsketch
% LocalWords:  mathcal fileversion Ginev maketitle  newpage infty ulsmf08 exfig endinput
% LocalWords:  omsemmac lstset basicstyle scriptsize aboveskip belowskip hline mh-variant
% LocalWords:  morekeywords lstlisting csymbol showmods foo exf cseq mdframed usemhmodule
% LocalWords:  qualifiedimports qualifiedimports termdef textbf filepath RabKoh mhinput
% LocalWords:  symname varSmoothfunctionsOn ednote abbrdef Sumfromto semmodule mhinputref
% LocalWords:  vspace hrule vspace arith arbitraryn xbool oplus xdisjunction tw mhinput
% LocalWords:  emph capitalize ldots termref termref symref symref ctancite nc mhinputref
% LocalWords:  smms hyperref RahObe hmlmh10 widehat texmf.cnf requiremodules cs 2oms04
% LocalWords:  sinput sinputref sinputref cname csname 2oms04 if@mmt modules-mh pathsuris
% LocalWords:  OPhats usepackage importqualified Crossreferencing jobname ltxml etoolbox
% LocalWords:  jobname printbibliography textsf langle textsf langle textlangle listadd
% LocalWords:  textrangle textlangle newif ifmod qualifiedfalse qualifiedtrue usemhmodule
% LocalWords:  sref xspace expandafter noexpand endcsname namedef setkeys ifx mh-variants
% LocalWords:  newenvironment parentmod usemodule ifundefined coolurion cooluri reqmodule
% LocalWords:  coolurioff cwd ouri ifdefinable testopt ifnextchar xargdef bvars 2oms04
% LocalWords:  argdef yargdef somefunction symdeflocaltrue bvar xpath assoc qr reqmodules
% LocalWords:  symdeflocalfalse localpres isbound symdefs COMPLEXTOKEN localp  fromrepos
% LocalWords:  findnodes localname carg renewcommand bbb showmeta showmeta exp ifnumequal
% LocalWords:  refundefinedtrue subsubsection blaaa makeatletter makeatother rm ifinlist
% LocalWords:  ifmodules gdef xdef xdef modulestrue modulesfalse pathpostfix abbreviative
% LocalWords:  updatedsms newreg xref texorpdfstring srefaddidkey newsavebox importmodule
% LocalWords:  viewbox newcounter thesection theview theproblem hfill lrbox req torepos
% LocalWords:  stepcounter textwidth hbox noindent smallskip fbox vbox usebox forpathlist
% LocalWords:  smallskip newxcomment vassign ensuremath mapsto doctex tocdepth dolistloop
% LocalWords:  setcounter tableofcontents mathbb symvariant importmodulevia  assdef Jinbo
% LocalWords:  importmodulevia compactdesc tassign tassign tname source-tname frompath
% LocalWords:  ttassign metakeys addmetakey themodule metasetkeys aftergroup addtocounter
% LocalWords:  groupling requation IMPORTCD CURRENTCD bindargs defmathop cnode topath
% LocalWords:  icvariant aftercounter prestok inputref oref loadfrom loadto customization
% LocalWords:  csymdef notationdef noauxreq noauxreq rinput ifaux reqtrue bargs assdef
% LocalWords:  reqfalse currmod importmoduleenv conceptdef stDMemph  tempswa mhviewsketch
% LocalWords:  auxout omtext surroundwithmdframed ignorespaces NeedsTeXFormat lstinline
%  LocalWords:  modularizations conventionalized initialize xstring srccite csgdef csxdef
%  LocalWords:  customized newrobustcmd ifcsundef definedness providerobustcmd cpath
%  LocalWords:  canonicalization canonicalize canoncalized RealAddrNum itemize mmtheory
%  LocalWords:  NEWrequiremodules mmtheoryend ignorespacesafterend ignorespacesandpars
%  LocalWords:  mmtinclude noexport withusedmodules catcode13 ignorespacesandparsafterend
%  LocalWords:  ifhmode unskip mmtconstdec mmtconstdec

% \endinput
% Local Variables:
% mode: doctex
% TeX-master: t
% End: