% \iffalse meta-comment
% An Infrastructure for Semantic Macros and Module Scoping
% Copyright (C) 2004-2010 Michael Kohlhase, all rights reserved
%               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/modules/modules.dtx $
% \fi
%  
% \iffalse
%<package>\NeedsTeXFormat{LaTeX2e}[1999/12/01]
%<package>\ProvidesPackage{modules}[2010/06/25 v1.0 Semantic Markup]
%
%<*driver>
\documentclass{ltxdoc}
\usepackage{stex-logo,modules}
\usepackage{url,array,float,textcomp}
\usepackage[show]{ed}
\usepackage[hyperref=auto,style=alphabetic]{biblatex}
\usepackage{listings}
\usepackage{amsfonts}
\bibliography{kwarc}
\usepackage[eso-foot,today]{svninfo}
\svnInfo $Id: modules.dtx 1676 2010-11-08 09:53:09Z kohlhase $
\svnKeyword $HeadURL: https://svn.kwarc.info/repos/stex/trunk/sty/modules/modules.dtx $
\usepackage{../ctansvn}
\usepackage{hyperref} 
\makeindex
\floatstyle{boxed}
\newfloat{exfig}{thp}{lop}
\floatname{exfig}{Example}
\def\tracissue#1{\cite{sTeX:online}, \hyperlink{http://trac.kwarc.info/sTeX/ticket/#1}{issue #1}}
\begin{document}\DocInput{modules.dtx}\end{document} 
%</driver>
% \fi
% 
% \iffalse\CheckSum{787}\fi
%
% \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}
% 
% \GetFileInfo{modules.sty}
% 
% \MakeShortVerb{\|}
%\def\scsys#1{{{\sc #1}}\index{#1@{\sc #1}}}
% \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 \& Deyan Ginev \& Rares Ambrus\\
%            Jacobs University, Bremen\\
%            \url{http://kwarc.info/kohlhase}}
% \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 two options: If we set \DescribeMacro{showviews}|showviews|,
% 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}.
% 
% If the \DescribeMacro{showmeta}|showmeta| is set, then the metadata keys are shown
% (see~\cite{Kohlhase:metakeys:ctan} for details and customization options).
% 
% \subsection{Modules and Inheritance}\label{sec:modules}
%
% \DescribeEnv{module} The |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 (see
%   Section~\ref{sec:symdef}) 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[|\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.
% 
% 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:WSMSML10} for discussion. 
% 
% \subsection{Semantic Macros and Module Scoping}\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:resymdef}, 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.
% 
% \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}
%
% To locally change the presentation of a semantic macro, we can use the
% \DescribeMacro{\resymdef}|\resymdef| macro\footnote{For some reason, this does not
% interact very well with the {\texttt{beamer}} class, if used in side a {\texttt{frame}}
% environment, the option {\texttt{[fragile]}} should be given of {\texttt{frame}}.}. It
% takes the same arguments as the |\symdef| macro described above, but locally redefines
% the presentation. Consider for instance the situation in Figure~\ref{fig:resymdef}
%
%\begin{exfig}
% \begin{verbatim}
% \begin{module}[id=xbool]
%   \symdef[name=xor]{xorOp}{\oplus}
%   \symdef{xor}[2]{#1\xorOp #2}
%   \termdef[name=xor]{xdisjunction}{exclusive disjunction}
%   \captitalize\xdisjunction is commutative: $\xor{p}q=\xor{q}p$\\
%   \resymdef[name=xor]{xorOp}{\underline{\vee}}
%   Some authors also write exclusive or with the $\xorOp$ operator, 
%   then the formula above is $\xor{p}q=\xor{q}p$
% \end{module}
% \end{verbatim}
% \vspace*{-3.5ex}\hrule\vspace*{1ex}
% \begin{module}[id=xbool]
%   \symdef[name=xor]{xorOp}{\oplus}
%   \symdef{xor}[2]{#1\oplus#2}
%   \termdef[name=xor]{xdisjunction}{exclusive disjunction}
%   \capitalize\xdisjunction is communtative: $\xor{p}q=\xor{q}p$\\
%   \resymdef[name=xor]{xorOp}{\underline{\vee}}
%   Some authors also write exclusive or with the $\xorOp$ operator,
%   then the formula above is $\xor{p}q=\xor{q}p$
% \end{module}
% \caption{Redefining the Presentation of a Semantic Macro}\label{fig:resymdef}
% \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:resymdef} for an
% example, where we use the \DescribeMacro{\capitalize}|\captitalize| 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.
%
% \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:utilities}) 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[../other/bar]{bar}
% \importmodule[../mycolleaguesmodules]{baz}
% \importmodule[../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.}). 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), so that it would not
% have to be re-loaded in the critical path of the module |foo|. Solving the load depth
% problem.
% 
% \DescribeMacro{\sinput} In all of the above, we do not want to load an |sms| file, if
% the corresponding file has already been loaded, since the semantic macros are already in
% memory. Therefore the |modules| package supplies a semantic variant of the |\input|
% macro, which records in an internal register that the modules in the file have already
% been loaded. Thus if we consistently use |\sinput| instead of |\input| or |\include| for
% files that contain modules\footnote{files without modules should be treated by the
%   regular {\LaTeX} input mechanism, since they do not need to be registered.}, we can
% prevent double loading of files and therefore gain efficiency. The
% \DescribeMacro{\sinputref} |\sinputref| macro behaves just like |\sinput| in the
% {\LaTeX} workflow, but in the {\latexml} conversion process creates a reference to the
% transformed version of the input file instead.
% 
% Finally, the separation of documents into multiple modules often profits from a symbolic
% management of file paths. To simplify this, the |modules| package supplies the
% \DescribeMacro{\defpath}|\defpath| macro: |\defpath{|\meta{cname}|}{|\meta{path}|}|
% defines a command, so that |\|\meta{csname}|{|\meta{name}|}| expands to
% \meta{path}|/|\meta{name}. So we could have used
% \begin{lstlisting}
% \defpath{OPaths}{../other}
% \importmodule[\OPhats{bar}]{bar}
% \end{lstlisting}
% instead of the second line in Example~\ref{exf:importmodule}. The variant |\OPaths| has
% the big advantage that we can get around the fact that {\TeX/\LaTeX} does not set the
% current directory in |\input|, so that we can use systematically deployed
% |\defpath|-defined path macros to make modules relocatable by defining the path macros
% locally.
% 
% \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.
%
% \subsection{Views}\label{sec:user:views}
% 
% \ednote{Document and make Examples}
%
% \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:online}.
% 
% \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:online} 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:online}. 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 
% \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[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.
% 
%
% \section{Limitations}\label{sec:limitations}
% 
% 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}. 
% \begin{compactenum}
% \item none reported yet
% \end{compactenum}
% 
% \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).
%    \begin{macrocode}
%<*package>
\DeclareOption{showmeta}{\PassOptionsToPackage{\CurrentOption}{metakeys}}
\newif\ifmod@show\mod@showfalse
\DeclareOption{show}{\mod@showtrue}
\newif\ifmod@qualified\mod@qualifiedfalse
\DeclareOption{qualifiedimports}{\mod@qualifiedtrue}
%    \end{macrocode}
% Finally, we need to declare the end of the option declaration section to {\LaTeX}.
%    \begin{macrocode}
\ProcessOptions
%</package>
%    \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}
%<*package>
\RequirePackage{sref}
\RequirePackage{xspace}
\RequirePackage{xcomment}
%</package>
%<*ltxml>
# -*- CPERL -*-
package LaTeXML::Package::Pool;
use strict;
use LaTeXML::Global;
use LaTeXML::Package;
%</ltxml>
%    \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}
%<*package>
\define@key{module}{cd}{}
%</package>
%    \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 |\mod@id| and the module path in |\|\meta{name}|@cd@file@base|
%   which we add to |\module@defs@|\meta{name}, so that we can use it in the importing
%   module.
%    \begin{macrocode}
%<*package>
\define@key{module}{id}{%
\edef\this@module{\expandafter\noexpand\csname module@defs@#1\endcsname}%
\global\@namedef{module@defs@#1}{}%
\ifmod@qualified
\edef\this@qualified@module{\expandafter\noexpand\csname module@defs@qualified@#1\endcsname}%
\global\@namedef{module@defs@qualified@#1}{}%
\fi
\def\mod@id{#1}%
\expandafter\edef\csname #1@cd@file@base\endcsname{\mod@path}%
\expandafter\g@addto@macro\csname module@defs@#1\expandafter\endcsname\expandafter%
{\expandafter\def\csname #1@cd@file@base\expandafter\endcsname\expandafter{\mod@path}}}
%</package>
%    \end{macrocode}
% \end{macro}
%
% \begin{environment}{module}
%    finally, we define the begin module command for the module environment. All the work
%    has already been done in the keyval bindings, so this is very simple.
%    \begin{macrocode}
%<*package>
\newenvironment{module}[1][]{\setkeys{module}{#1}}{}
%</package>
%    \end{macrocode}
% for the {\latexml} bindings, we have to do the work all at once. 
%    \begin{macrocode}
%<*ltxml>
DefEnvironment('{module} OptionalKeyVals:Module',
	       "?#excluded()(<omdoc:theory "
             . "?&defined(&KeyVal(#1,'id'))(xml:id='&KeyVal(#1,'id')')(xml:id='#id')>#body</omdoc:theory>)", 
#     beforeDigest=>\&useTheoryItemizations,
       afterDigestBegin=>sub {
       my($stomach, $whatsit)=@_;
       $whatsit->setProperty(excluded=>LookupValue('excluding_modules'));

       my $keys = $whatsit->getArg(1);
       my($id, $cd)=$keys
  && map(ToString($keys->getValue($_)),qw(id cd));       
       	#make sure we have an id or give a stub one otherwise:
	if (not $id) {
		#do magic to get a unique id for this theory
		$whatsit->setProperties(beginItemize('theory'));
		$id = ToString($whatsit->getProperty('id'));
	}
       $cd = $id unless $cd;
       # update the catalog with paths for modules
       my $module_paths = LookupValue('module_paths') || {};
       $module_paths->{$id} = LookupValue('last_module_path');
       AssignValue('module_paths', $module_paths, 'global');
       
       #Update the current module position
       AssignValue(current_module => $id);
       AssignValue(module_cd => $cd) if $cd;

       #activate the module in our current scope
       $STATE->activateScope("module:".$id);

       #Activate parent scope, if present
       my $parentmod = LookupValue('parent_module');
       use_module($parentmod) if $parentmod;
       #Update the current parent module
       AssignValue("parent_of_$id"=>$parentmod,'global');
       AssignValue("parent_module" => $id);
       return; },
     afterDigest => sub {
       #Move a step up on the module ancestry
       AssignValue("parent_module" => LookupValue("parent_of_".LookupValue("parent_module")));
       return;
     });
%</ltxml>
%    \end{macrocode}
% \end{environment}
%
%
% \begin{macro}{usemodule}
%   The |use_module| subroutine performs depth-first load of definitions of the used
%   modules
%    \begin{macrocode}
%<*ltxml>
sub use_module {
  my($module,%ancestors)=@_;
  $module = ToString($module);
  if (defined $ancestors{$module})  {
    Fatal(":module \"$module\" leads to import cycle!");
  }
  $ancestors{$module}=1;
  # Depth-first load definitions from used modules, disregarding cycles
  foreach my $used_module (@{ LookupValue("module_${module}_uses") || []}){
    use_module($used_module,%ancestors);
  }
  # then load definitions for this module
  $STATE->activateScope("module:$module"); }#$
%</ltxml>
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\activate@defs}
%    To activate the |\symdef|s from a given module xxx, we call the macro |\module@defs@xxx|. 
%    \begin{macrocode}
%<*package>
\def\activate@defs#1{\csname module@defs@#1\endcsname}
%</package>
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\export@defs}
%   To export a the |\symdef|s from the current module, we all the macros
%   |\module@defs@|\meta{mod} to |\module@defs@|\meta{mod} (if the current module has a
%   name and it is \meta{mod})
%    \begin{macrocode}
%<*package>
\def\export@defs#1{\@ifundefined{mod@id}{}%
{\expandafter\expandafter\expandafter\g@addto@macro\expandafter%
\this@module\expandafter{\csname module@defs@#1\endcsname}}}
%</package>
%    \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}. It also remembers the file name in |\mod@path|.
%    \begin{macrocode}
%<*package>
\def\coolurion{}
\def\coolurioff{}
\newcommand{\importmodule}[2][]{{\def\mod@path{#1}%
\ifx\mod@path\@empty\else\requiremodules{#1}\fi}%
\activate@defs{#2}\export@defs{#2}}
%</package>
%<*ltxml>
DefMacro('\coolurion',sub {AssignValue('cooluri'=>1);});
DefMacro('\coolurioff',sub {AssignValue('cooluri'=>0);});
sub omext {
  my ($mod)=@_; my $dest='';
  if (ToString($mod)) {
    #We need a constellation of abs_path invocations
    # to make sure that all symbolic links get resolved
    my ($d,$f,$t) = pathname_split(abs_path(ToString($mod)));
    $d = pathname_relative(abs_path($d),abs_path(cwd()));
    $dest=$d."/".$f;
  }
  $dest.=".omdoc" if (ToString($mod) && !LookupValue('cooluri')); 
  return Tokenize($dest);}
sub importmoduleI {
   my($stomach,$whatsit)=@_;
   my $file = $whatsit->getArg(1);
   my $omdocmod = $file.".omdoc" if $file;
   my $module = $whatsit->getArg(2);
   $module = ToString($module);
   my $containing_module = LookupValue('current_module');
   #set the relation between the current module and the one to be imported
   PushValue("module_".$containing_module."_uses"=>$module) if $containing_module;
  #check if we've already loaded this module file or no file path given
  if((!$file) || (LookupValue('file_'.$module.'_loaded'))) {use_module($module);} #if so activate it!
  else {
    #if not:
    my $gullet = $stomach->getGullet;
    #1) mark as loaded
    AssignValue('file_'.$module.'_loaded' => 1, 'global');
    #open a group for its definitions so that they are localized
    $stomach->bgroup;
    #update the last module path
    AssignValue('last_module_path', $file);
    #queue the closing tag for this module in the gullet where it will be executed
    #after all other definitions of the imported module have been taken care of
    $gullet->unread(Invocation(T_CS('\end@requiredmodule'), T_OTHER($module))->unlist);
    #we only need to load the sms definitions without generating any xml output, so we set the flag to 1
    AssignValue('excluding_modules' => 1);
    #queue this module's sms file in the gullet so that its definitions are imported
    $gullet->input($file,['sms']);
   }
   return;}
DefConstructor('\importmodule OptionalSemiverbatim {}',
   "<omdoc:imports from='?#1(&omext(#1))\##2'/>",
   afterDigest=>sub{ importmoduleI(@_)});
%</ltxml>
%    \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.
%    \begin{macrocode}
%<*package>
\newcommand{\importOMDocmodule}[3][]{\importmodule[#1]{#3}}
%</package>
%<*ltxml>
DefConstructor('\importOMDocmodule OptionalSemiverbatim {}{}',"<omdoc:imports from='#3\##2'/>",
afterDigest=>sub{ 
  #Same as \importmodule, just switch second and third argument.
  my ($stomach,$whatsit) = @_;
  my $path = $whatsit->getArg(1);
  my $ouri = $whatsit->getArg(2);
  my $module = $whatsit->getArg(3);
  $whatsit->setArgs(($path, $module,$ouri));
  importmoduleI($stomach,$whatsit);
  return;
});
%</ltxml>
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\metalanguage} 
%   |\metalanguage| behaves exactly like |\importmodule| for formatting. For {\latexml},
%   we only add the |type| attribute.
%    \begin{macrocode}
%<*package>
\let\metalanguage=\importmodule
%</package>
%<*ltxml>
DefConstructor('\metalanguage OptionalSemiverbatim {}',
   "<omdoc:imports type='metalanguage' from='?#1(&omext(#1))\##2'/>",
   afterDigest=>sub{ importmoduleI(@_)});
%</ltxml>
%    \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. This is just a copy of the code from
%   |latex.ltx| where I have removed the |\@ifdefinable| check.\footnote{Someone must have
%     done this before, I would be very happy to hear about a package that provides this.}
%    \begin{macrocode}
%<*package>
\def\mod@newcommand{\@star@or@long\mod@new@command}
\def\mod@new@command#1{\@testopt{\@mod@newcommand#1}0}
\def\@mod@newcommand#1[#2]{\kernel@ifnextchar [{\mod@xargdef#1[#2]}{\mod@argdef#1[#2]}}
\long\def\mod@argdef#1[#2]#3{\@yargdef#1\@ne{#2}{#3}}
\long\def\mod@xargdef#1[#2][#3]#4{\expandafter\def\expandafter#1\expandafter{%
\expandafter\@protected@testopt\expandafter #1\csname\string#1\endcsname{#3}}%
\expandafter\@yargdef\csname\string#1\endcsname\tw@{#2}{#4}}
%</package>
%    \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{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}
%<*package>
\define@key{symdef}{local}[true]{\@symdeflocaltrue}
\define@key{symdef}{name}{}
\define@key{symdef}{assocarg}{}
\define@key{symdef}{bvars}{}
\define@key{symdef}{bvar}{}
%</package>
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\symdef}
%    The the |\symdef|, and |\@symdef| macros just handle optional arguments.
%    \begin{macrocode}
%<*package>
\newif\if@symdeflocal
\def\symdef{\@ifnextchar[{\@symdef}{\@symdef[]}}
\def\@symdef[#1]#2{\@ifnextchar[{\@@symdef[#1]{#2}}{\@@symdef[#1]{#2}[0]}}
%    \end{macrocode}
% next we locally abbreviate |\mod@newcommand| to make the argument passing simpler.
%    \begin{macrocode}
\def\@mod@nc#1{\mod@newcommand{#1}[1]}
%    \end{macrocode}
%    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 check for the local keyword. Then we set all the keys that have been
% provided as arguments: |name|, |local|. First, using |\mod@newcommand| we initialize the
% intermediate function, the one that can be changed internally with |\resymdef| and then
% we link the actual function to it, again with |\mod@newcommand|. 
%    \begin{macrocode}
\@symdeflocalfalse\setkeys{symdef}{#1}%
\expandafter\mod@newcommand\csname modules@#2@pres\endcsname[#3]{#4}%
\expandafter\def\csname#2\endcsname{\csname modules@#2@pres\endcsname}%
\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.  Otherwise, we add two functions to the module's pool of defined macros
% using |\g@addto@macro|. We add both functions so that we can keep the link between the
% real and the intermediate function whenever we inherit the module. Finally we also add
% |\mod@symref@|\meta{sym} macro to the macro pool.
%    \begin{macrocode}
\if@symdeflocal\else%
\@ifundefined{mod@id}{}{%
\expandafter\g@addto@macro\this@module%
{\expandafter\mod@newcommand\csname modules@#2@pres\endcsname[#3]{#4}}%
\expandafter\g@addto@macro\this@module%
{\expandafter\def\csname#2\endcsname{\csname modules@#2@pres\endcsname}}%
\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#2atqualified\endcsname{\csname modules@#2@pres@qualified\endcsname}}%
\fi%
%    \end{macrocode}
% So now we only need to close all brackets and the macro is done. 
%    \begin{macrocode}
}\fi}
%</package>
%    \end{macrocode}
% In the {\latexml} bindings, we have a top-level macro that delegates the work to two
% internal macros: |\@symdef|, which defines the content macro and |\@symdef@pres|, which
% generates the {\omdoc} |symbol| and |presentation| elements (see
% Section~\ref{sec:impl:presentation}).
%    \begin{macrocode}
%<*package>
\define@key{DefMathOp}{name}{\def\defmathop@name{#1}}
\newcommand\DefMathOp[2][]{%
\setkeys{DefMathOp}{#1}%
\symdef[#1]{\defmathop@name}{#2}}
%</package>
%<*ltxml>
DefMacro('\DefMathOp OptionalKeyVals:symdef {}',
 sub {
   my($self,$keyval,$pres)=@_;
   my $name = KeyVal($keyval,'name') if $keyval;
   #Rewrite this token
   my $scopes = $STATE->getActiveScopes;
   DefMathRewrite(xpath=>'descendant-or-self::ltx:XMath',match=>ToString($pres),
        replace=>sub{
          map {$STATE->activateScope($_);} @$scopes;
          $_[0]->absorb(Digest("\\".ToString($name)));
        });
   #Invoke symdef
   (Invocation(T_CS('\symdef'),$keyval,$name,undef,undef,$pres)->unlist);
 });
DefMacro('\symdef OptionalKeyVals:symdef {}[][]{}',
      sub {
  my($self,@args)=@_;
  ((Invocation(T_CS('\@symdef'),@args)->unlist),
   (LookupValue('excluding_modules') ? ()
     : (Invocation(T_CS('\@symdef@pres'), @args)->unlist))); });

#Current list of recognized formatter command sequences:
our @PresFormatters = qw (infix prefix postfix assoc mixfixi mixfixa mixfixii mixfixia mixfixai mixfixaii mixfixiii);
DefPrimitive('\@symdef OptionalKeyVals:symdef {}[][]{}', sub {
  my($stomach,$keys,$cs,$nargs,$opt,$presentation)=@_;
  my($name,$cd,$role,$bvars,$bvar)=$keys 
    && map($_ && $_->toString,map($keys->getValue($_), qw(name cd role
    bvars bvar)));
  $cd = LookupValue('module_cd') unless $cd;
  $name = $cs unless $name;
  #Store for later lookup
  AssignValue("symdef.".ToString($cs).".cd"=>ToString($cd),'global');
  AssignValue("symdef.".ToString($cs).".name"=>ToString($name),'global');
  $nargs = (ref $nargs ? $nargs->toString : $nargs || 0);
  my $module = LookupValue('current_module');
  my $scope = (($keys && ($keys->getValue('local') || '' eq 'true')) ? 'module_local' : 'module').":".$module;

 #The DefConstructorI Factory is responsible for creating the \symbol command sequences as dictated by the \symdef
 DefConstructorI("\\".$cs->toString,convertLaTeXArgs($nargs,$opt), sub {
    my ($document,@args) = @_;
    my @props = @args;
    my $localpres = $presentation;
    @args = splice(@props,0,$nargs);
    my %prs = @props;
    $prs{isbound} = "BINDER" if ($bvars || $bvar);
    my $wrapped;
    my $parent=$document->getNode;
    if(! defined $parent->lookupNamespacePrefix("http://omdoc.org/ns")){ # namespace not already declared?
      $document->getDocument->documentElement->setNamespace("http://omdoc.org/ns","omdoc",0); }
    my $symdef_scope=$parent->exists('ancestor::omdoc:rendering'); #Are we in a \symdef rendering?
    if (($localpres =~/^LaTeXML::Token/) && $symdef_scope) {
      #Note: We should probably ask Bruce whether this maneuver makes sense
      # We jump back to digestion, at a processing stage where it has been already completed
      # Hence need to reinitialize all scopes and make a new group. This is probably expensive to do.

      my @toks = $localpres->unlist;
      while(@toks && $toks[0]->equals(T_SPACE)){ shift(@toks); }  # Remove leading space
      my $formatters = join("|",@PresFormatters);
      $formatters = qr/$formatters/;
      $wrapped = (@toks && ($toks[0]->toString =~ /^\\($formatters)$/));
      $localpres = Invocation(T_CS('\@use'),$localpres) unless $wrapped;
      # Plug in the provided arguments, doing a nasty reversion:
      my @sargs = map (Tokens($_->revert),  @args);
      $localpres = Tokens(LaTeXML::Expandable::substituteTokens($localpres,@sargs)) if $nargs>0;
      #Digest:
      my $stomach = $STATE->getStomach;
      $stomach->beginMode('inline-math');
      $STATE->activateScope($scope);
      use_module($module);
      use_module(LookupValue("parent_of_".$module)) if LookupValue("parent_of_".$module);
      $localpres=$stomach->digest($localpres);
      $stomach->endMode('inline-math');
    }
    else { #Some are already digested to Whatsit, usually when dropped from a wrapping constructor
    }
    if ($nargs == 0) {
      if (!$symdef_scope) { #Simple case - discourse flow, only a single XMTok
        #Referencing XMTok when not in \symdefs:
        $document->insertElement('ltx:XMTok',undef,(name=>$cs->toString, meaning=>$name,omcd=>$cd,role => $role,scriptpos=>$prs{'scriptpos'}));
      }
      else {
        if ($symdef_scope && ($localpres =~/^LaTeXML::Whatsit/) && (!$wrapped)) {#1. Simple case: converts to a single token
          $localpres->setProperties((name=>$cs->toString, meaning=>$name,omcd=>$cd,role => $role,scriptpos=>$prs{'scriptpos'}));
        }
        else {
          #Experimental treatment - COMPLEXTOKEN
          #$role=$role||'COMPLEXTOKEN';
          #$document->openElement('ltx:XMApp',role=>'COMPLEXTOKEN');
          #$document->insertElement('ltx:XMTok',undef,(name=>$cs->toString, meaning=>$name, omcd=>$cd, role=>$role, scriptpos=>$prs{'scriptpos'}));
          #$document->openElement('ltx:XMWrap');
          #$document->absorb($localpres);
          #$document->closeElement('ltx:XMWrap');
          #$document->closeElement('ltx:XMApp');
        }
        #We need expanded presentation when invoked in \symdef scope:

        #Suppress errors from rendering attributes when absorbing.
        #This is bad style, but we have no way around it due to the digestion acrobatics.
        my $verbosity = $LaTeXML::Global::STATE->lookupValue('VERBOSITY');
        my $errors = $LaTeXML::Global::STATE->getStatus('error');
        $LaTeXML::Global::STATE->assignValue('VERBOSITY',-5);

        #Absorb presentation:
        $document->absorb($localpres);

        #Return to original verbosity and error state:
        $LaTeXML::Global::STATE->assignValue('VERBOSITY',$verbosity);
        $LaTeXML::Global::STATE->setStatus('error',$errors);

        #Strip all/any <rendering><Math><XMath> wrappers:
        #TODO: Ugly LibXML work, possibly do something smarter
        my $parent = $document->getNode;
        my @renderings=$parent->findnodes(".//omdoc:rendering");
        foreach my $render(@renderings) {
          my $content=$render;
          while ($content && $content->localname =~/^rendering|[X]?Math/) {
            $content = $content->firstChild;
          }
          my $sibling = $content->parentNode->lastChild;
          my $localp = $render->parentNode;
          while ((defined $sibling) && (!$sibling->isSameNode($content))) {
            my $clone = $sibling->cloneNode(1);
            $localp->insertAfter($clone,$render);
            $sibling = $sibling->previousSibling;
          }
          $render->replaceNode($content);
        }
      }
    }
    else {#2. Constructors with arguments
      if (!$symdef_scope) { #2.1 Simple case, outside of \symdef declarations:
        #Referencing XMTok when not in \symdefs:
        $document->openElement('ltx:XMApp',scriptpos=>$prs{'scriptpos'},role=>$prs{'isbound'});
        $document->insertElement('ltx:XMTok',undef,(name=>$cs->toString, meaning=>$name, omcd=>$cd, role=>$role, scriptpos=>$prs{'operator_scriptpos'}));
        foreach my $carg (@args) {
          if ($carg =~/^LaTeXML::Token/) {
            my $stomach = $STATE->getStomach;
            $stomach->beginMode('inline-math');
            $carg=$stomach->digest($carg);
            $stomach->endMode('inline-math');
          }
          $document->openElement('ltx:XMArg');
          $document->absorb($carg);
          $document->closeElement('ltx:XMArg');
        }
        $document->closeElement('ltx:XMApp');
      }
      else { #2.2 Complex case, inside a \symdef declaration
        #We need expanded presentation when invoked in \symdef scope:

        #Suppress errors from rendering attributes when absorbing.
        #This is bad style, but we have no way around it due to the digestion acrobatics.
        my $verbosity = $LaTeXML::Global::STATE->lookupValue('VERBOSITY');
        my $errors = $LaTeXML::Global::STATE->getStatus('error');
        $LaTeXML::Global::STATE->assignValue('VERBOSITY',-5);

        #Absorb presentation:
        $document->absorb($localpres);

        #Return to original verbosity and error state:
        $LaTeXML::Global::STATE->assignValue('VERBOSITY',$verbosity);
        $LaTeXML::Global::STATE->setStatus('error',$errors);

        #Strip all/any <rendering><Math><XMath> wrappers:
        #TODO: Ugly LibXML work, possibly do something smarter?
        my $parent = $document->getNode;
        if(! defined $parent->lookupNamespacePrefix("http://omdoc.org/ns")){ # namespace not already declared?
          $document->getDocument->documentElement->setNamespace("http://omdoc.org/ns","omdoc",0); }
        my @renderings=$parent->findnodes(".//omdoc:rendering");
        foreach my $render(@renderings) {
          my $content=$render;
          while ($content && $content->localname =~/^rendering|[X]?Math/) {
            $content = $content->firstChild;
          }
          my $sibling = $content->parentNode->lastChild;
          my $localp = $render->parentNode;
          while ((defined $sibling) && (!$sibling->isSameNode($content))) {
            my $clone = $sibling->cloneNode(1);
            $localp->insertAfter($clone,$render);
            $sibling = $sibling->previousSibling;
          }
          $render->replaceNode($content);
        }
      }
    }},
  properties => {name=>$cs->toString, meaning=>$name,omcd=>$cd,role => $role},
  scope=>$scope);
  return; });
%</ltxml>%$ 
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\resymdef}
%   We can use this function to redefine our intermediate presentational function inside
%   the modules\ednote{We have already prepared the argument parsing for an optional first
%     argument, but this is not looked at yet. }\ednote{does not seem to have a {\latexml}
%     counterpart yet!}
%    \begin{macrocode}
%<*package>
\def\resymdef{\@ifnextchar[{\@resymdef}{\@resymdef[]}}
\def\@resymdef[#1]#2{\@ifnextchar[{\@@resymdef[#1]{#2}}{\@@resymdef[#1]{#2}[0]}}
\def\@@resymdef[#1]#2[#3]#4{\expandafter\renewcommand\csname modules@#2@pres\endcsname[#3]{#4}}
%</package>
%    \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}
%<*package>
\let\abbrdef\symdef
%</package>
%<*ltxml>
DefPrimitive('\abbrdef OptionalKeyVals:symdef {}[][]{}', sub {
  my($stomach,$keys,$cs,$nargs,$opt,$presentation)=@_;
  my $module = LookupValue('current_module');
  my $scope = (($keys && ($keys->getValue('local') || '' eq 'true')) ? 'module_local' : 'module').":$module";
  DefMacroI("\\".$cs->toString,convertLaTeXArgs($nargs,$opt),$presentation,
	   scope=>$scope);
  return; });
%</ltxml>
%    \end{macrocode}
% \end{macro}
%
% \subsection{Symbol and Concept Names}\label{sec:impl:concepts}
%
% \begin{macro}{\mod@path} 
%   the |\mod@path| macro is used to remember the local path, so that the |module|
%   environment can set it for later cross-referencing of the modules. If |\mod@path| is
%   empty, then it signifies the local file.
%    \begin{macrocode}
%<*package>
\def\mod@path{}
%</package>
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\termdef} 
%    \begin{macrocode}
%<*package>
\def\mod@true{true}
\addmetakey[false]{termdef}{local}
\addmetakey{termdef}{name}
\newcommand{\termdef}[3][]{\metasetkeys{termdef}{#1}%
\expandafter\mod@newcommand\csname#2\endcsname[0]{#3\xspace}
\ifx\termdef@local\mod@true\else%
\@ifundefined{mod@id}{}{\expandafter\g@addto@macro\this@module%
{\expandafter\mod@newcommand\csname#2\endcsname[0]{#3\xspace}}}
\fi}
%</package>
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\capitalize} 
%    \begin{macrocode}
%<*package>
\def\@captitalize#1{\uppercase{#1}}
\newcommand\capitalize[1]{\expandafter\@captitalize #1}
%</package>
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\mod@termref} 
%   |\mod@termref{|\meta{module}|}{|\meta{name}|}{|\meta{nl}|}| determines whether the
%   macro |\|\meta{module}|@cd@file@base| 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.
%    \begin{macrocode}
%<*package>
\def\mod@termref#1#2#3{\def\@test{#3}
\@ifundefined{#1@cd@file@base}
    {\protect\G@refundefinedtrue
      \@latex@warning{\protect\termref with unidentified cd "#1": the cd key must
        reference an active module}
      \def\@label{sref@#2 @target}}
  {\def\@label{sref@#2@#1@target}}%
\expandafter\ifx\csname #1@cd@file@base\endcsname\@empty% local reference
\sref@hlink@ifh{\@label}{\ifx\@test\@empty #2\else #3\fi}\else%
\def\@uri{\csname #1@cd@file@base\endcsname.pdf\#\@label}%
\sref@href@ifh{\@uri}{\ifx\@test\@empty #2\else #3\fi}\fi}
%</package>
%    \end{macrocode}
% \end{macro}
%
% \subsection{Dealing with Multiple Files}\label{sec:impl:multiple}
%
% Before we can come to the functionality we want to offer, we need some auxiliary
% functions that deal with path names. 
% 
% \subsubsection{Simplifying Path Names}
% 
% The |\mod@simplify| macro is used for simplifying
% path names by removing \meta{xxx}|/..| from a string. eg:
% \meta{aaa}|/|\meta{bbb}|/../|\meta{ddd} goes to \meta{aaa}|/|\meta{ddd} unless
% \meta{bbb} is |..|. This is used to normalize relative path names below.
%
% \begin{macro}{\mod@simplify}
%   The macro |\mod@simplify| recursively runs over the path collecting the result in the
%   internal |\mod@savedprefix| macro.
%    \begin{macrocode}
%<*package>
\def\mod@simplify#1{\expandafter\mod@simpl#1/\relax}
%    \end{macrocode}
% It is based on the |\mod@simpl| macro\ednote{what does the mod@blaaa do?}
%    \begin{macrocode}
\def\mod@simpl#1/#2\relax{\def\@second{#2}%
\ifx\mod@blaaaa\@empty\edef\mod@savedprefix{}\def\mod@blaaaa{aaa}\else\fi%
\ifx\@second\@empty\edef\mod@savedprefix{\mod@savedprefix#1}%
\else\mod@simplhelp#1/#2\relax\fi}
%    \end{macrocode}
%    which in turn is based on a helper macro
%    \begin{macrocode}
\def\mod@updir{..}
\def\mod@simplhelp#1/#2/#3\relax{\def\@first{#1}\def\@second{#2}\def\@third{#3}%
%\message{mod@simplhelp: first=\@first, second=\@second, third=\@third, result=\mod@savedprefix.}
\ifx\@third\@empty% base case
\ifx\@second\mod@updir\else%
\ifx\mod@second\@empty\edef\mod@savedprefix{\mod@savedprefix#1}%
\else\edef\mod@savedprefix{\mod@savedprefix#1/#2}%
\fi%
\fi%
\else%
\ifx\@first\mod@updir%
\edef\mod@savedprefix{\mod@savedprefix#1/}\mod@simplhelp#2/#3\relax%
\else%
\ifx\@second\mod@updir\mod@simpl#3\relax%
\else\edef\mod@savedprefix{\mod@savedprefix#1/}\mod@simplhelp#2/#3\relax%
\fi%
\fi%
\fi}%
%</package>
%    \end{macrocode}
% \end{macro}
%
% We directly test the simplification: \makeatletter
% \def\mod@simpl@test#1{\def\mod@savedprefix{}\mod@simplify{#1}\mod@savedprefix}
% \begin{center}
% \begin{tabular}{|l|l|l|}\hline
%   source       & result                          & should be \\\hline\hline
% ../../aaa      & \mod@simpl@test{../../aaa}      &  ../../aaa\\\hline
% aaa/bbb        & \mod@simpl@test{aaa/bbb}        & aaa/bbb\\\hline
% aaa/..         & \mod@simpl@test{aaa/..}         & \\\hline
% ../../aaa/bbb  & \mod@simpl@test{../../aaa/bbb}  & ../../aaa/bbb\\\hline
% ../aaa/../bbb  & \mod@simpl@test{../aaa/../bbb}  &  ../bbb\\\hline
% ../aaa/bbb  & \mod@simpl@test{../aaa/bbb}  &  ../aaa/bbb\\\hline
% aaa/bbb/../ddd & \mod@simpl@test{aaa/bbb/../ddd} & aaa/ddd\\\hline
% \end{tabular}
% \end{center}
% \makeatother
%
% \begin{macro}{\defpath}
%    \begin{macrocode}
%<*package>
\newcommand{\defpath}[2]{\expandafter\newcommand\csname #1\endcsname[1]{#2/##1}}
%</package>
%<*ltxml>
DefMacro('\defpath{}{}', sub {
	   my ($gullet,$arg1,$arg2)=@_;
	   $arg1 = ToString($arg1);
	   $arg2 = ToString($arg2);
	   my $paths = LookupValue('defpath')||{};
	   $$paths{"$arg1"}=$arg2;
	   AssignValue('defpath'=>$paths,'global');
	   DefMacro('\\'.$arg1.' Semiverbatim',$arg2."/#1");
	 });#$
%</ltxml>
%    \end{macrocode}
% \end{macro}
%
% \subsection{Loading Module Signatures}
%
% We will need a switch\ednote{explain why?}
%    \begin{macrocode}
%<*package>
\newif\ifmodules
%    \end{macrocode}
% and a ``registry'' macro whose expansion represents the list of added macros (or files)
% \begin{macro}{\mod@reg}
%    We initialize the |\mod@reg| macro with the empty string.
%    \begin{macrocode}
\gdef\mod@reg{}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\mod@update}
%     This macro provides special append functionality. It takes a string and appends it
%     to the expansion of the |\mod@reg| macro in the following way:  |string@\mod@reg|.
%    \begin{macrocode}
\def\mod@update#1{\ifx\mod@reg\@empty\xdef\mod@reg{#1}\else\xdef\mod@reg{#1@\mod@reg}\fi}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\mod@check}
%   The |\mod@check| takes as input a file path (arg 3), and searches the registry. If the
%   file path is not in the registry it means it means it has not been already added, so
%   we make |\ifmodules| true, otherwise make |\ifmodules| false. The macro |\mod@search|
%   will look at |\ifmodules| and update the registry for |\modulestrue| or do nothing for
%   |\modulesfalse|.
%    \begin{macrocode}
\def\mod@check#1@#2///#3\relax{%
\def\mod@one{#1}\def\mod@two{#2}\def\mod@three{#3}%
%    \end{macrocode}
%    Define a few intermediate macros so that we can split the registry into separate file
%    paths and compare to the new one
%    \begin{macrocode}
\expandafter%
\ifx\mod@three\mod@one\modulestrue%
\else%
\ifx\mod@two\@empty\modulesfalse\else\mod@check#2///#3\relax\fi%
\fi}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\mod@search}
%    Macro for updating the registry after the execution of |\mod@check|
%    \begin{macrocode}
\def\mod@search#1{%
%    \end{macrocode}
%    We put the registry as the first argument for |\mod@check| and the other
%    argument is the new file path.
%    \begin{macrocode}
\modulesfalse\expandafter\mod@check\mod@reg @///#1\relax%
%    \end{macrocode}
%    We run |\mod@check| with these arguments and the check |\ifmodules| for
%    the result
%    \begin{macrocode}
\ifmodules\else\mod@update{#1}\fi}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\mod@reguse}
%   The macro operates almost as the |mod@search| function, but it does not update the
%   registry. Its purpose is to check whether some file is or not inside the registry but
%   without updating it. Will be used before deciding on a new sms file
%    \begin{macrocode}
\def\mod@reguse#1{\modulesfalse\expandafter\mod@check\mod@reg @///#1\relax}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\mod@prefix}
% This is a local macro for storing the path prefix, we initialize it as the empty
% string.
%    \begin{macrocode}
\def\mod@prefix{}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\mod@updatedpre}
%    This macro updates the path prefix |\mod@prefix| with the last word in the path given
%    in its argument. 
%    \begin{macrocode}
\def\mod@updatedpre#1{%
\edef\mod@prefix{\mod@prefix\mod@pathprefix@check#1/\relax}}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\mod@pathprefix@check}
%   |\mod@pathprefix@check| returns the last word in a string composed of words separated
%   by slashes
%    \begin{macrocode}
\def\mod@pathprefix@check#1/#2\relax{%
\ifx\\#2\\% no slash in string
\else\mod@ReturnAfterFi{#1/\mod@pathprefix@help#2\relax}%
\fi}
%    \end{macrocode}
% It needs two helper macros:
%    \begin{macrocode}
\def\mod@pathprefix@help#1/#2\relax{%
\ifx\\#2\\% end of recursion
\else\mod@ReturnAfterFi{#1/\mod@pathprefix@help#2\relax}%
\fi}
\long\def\mod@ReturnAfterFi#1\fi{\fi#1}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\mod@pathpostfix@check}
%    |\mod@pathpostfix@check| takes a string composed of words separated by slashes and
%    returns the part of the string until the last slash
%    \begin{macrocode}
\def\mod@pathpostfix@check#1/#2\relax{% slash
\ifx\\#2\\%no slash in string
#1\else\mod@ReturnAfterFi{\mod@pathpostfix@help#2\relax}%
\fi}
%    \end{macrocode}
% Helper function for the |\pathpostfix@check| macro defined above
%    \begin{macrocode}
\def\mod@pathpostfix@help#1/#2\relax{%
\ifx\\#2\\%
#1\else\mod@ReturnAfterFi{\mod@pathpostfix@help#2\relax}%
\fi}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\mod@updatedpost}
%    This macro updates |\mod@savedprefix| with leading path (all but the last word) in the path given
%    in its argument. 
%    \begin{macrocode}
\def\mod@updatedpost#1{%
\edef\mod@savedprefix{\mod@savedprefix\mod@pathpostfix@check#1/\relax}}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\mod@updatedsms}
% Finally: A macro that will add a |.sms| extension to a path. Will be used when adding a |.sms| file
%    \begin{macrocode}
\def\mod@updatesms{\edef\mod@savedprefix{\mod@savedprefix.sms}}
%</package>
%    \end{macrocode}
% \end{macro}
% 
% \subsubsection{Selective Inclusion}
%
% \begin{macro}{\requiremodules}
%    \begin{macrocode}
%<*package>
\newcommand{\requiremodules}[1]{%
{\mod@updatedpre{#1}% add the new file to the already existing path
\let\mod@savedprefix\mod@prefix% add the path to the new file to the prefix
\mod@updatedpost{#1}%
\def\mod@blaaaa{}% macro used in the simplify function (remove .. from the prefix)
\mod@simplify{\mod@savedprefix}% remove |xxx/..| from the path (in case it exists)
\mod@reguse{\mod@savedprefix}%
\ifmodules\else%
\mod@updatesms% update the file to contain the .sms extension
\let\newreg\mod@reg% use to compare, in case the .sms file was loaded before
\mod@search{\mod@savedprefix}% update registry
\ifx\newreg\mod@reg\else\input{\mod@savedprefix}\fi% check if the registry was updated and load if necessary
\fi}}
%</package>
%<*ltxml>
DefPrimitive('\requiremodules{}', sub {
  my($stomach,$module)=@_;
  my $GULLET = $stomach->getGullet;
  $module = Digest($module)->toString;
  if(LookupValue('file_'.$module.'_loaded')) {}
  else {
    AssignValue('file_'.$module.'_loaded' => 1, 'global');
    $stomach->bgroup;
    AssignValue('last_module_path', $module);
    $GULLET->unread(T_CS('\end@requiredmodule'));
    AssignValue('excluding_modules' => 1);
    $GULLET->input($module,['sms']);
       }
  return;});

DefPrimitive('\end@requiredmodule{}',sub {
 #close the group
 $_[0]->egroup;
 #print STDERR "END: ".ToString(Digest($_[1])->toString);
 #Take care of any imported elements in this current module by activating it and all its dependencies
 #print STDERR "Important: ".ToString(Digest($_[1])->toString)."\n";
 use_module(ToString(Digest($_[1])->toString)); 
 return; });#$
%</ltxml>
%    \end{macrocode}
% \end{macro}
% 
% \begin{macro}{\sinput}
%    \begin{macrocode}
%<*package>
\def\sinput#1{
{\mod@updatedpre{#1}% add the new file to the already existing path
\let\mod@savedprefix\mod@prefix% add the path to the new file to the prefix
\mod@updatedpost{#1}%
\def\mod@blaaaa{}% macro used in the simplify function (remove .. from the prefix)
\mod@simplify{\mod@savedprefix}% remove |xxx/..| from the path (in case it exists)
\mod@reguse{\mod@savedprefix}%
\let\newreg\mod@reg% use to compare, in case the .sms file was loaded before
\mod@search{\mod@savedprefix}% update registry
\ifx\newreg\mod@reg%\message{This file has been previously introduced}
\else\input{\mod@savedprefix}%
\fi}}
%</package>
%<*ltxml>
DefPrimitive('\sinput Semiverbatim', sub {
  my($stomach,$module)=@_;
  my $GULLET = $stomach->getGullet;
  $module = Digest($module)->toString;
  AssignValue('file_'.$module.'_loaded' => 1, 'global');
  $stomach->bgroup;
  AssignValue('last_module_path', $module);
  $GULLET->unread(Invocation(T_CS('\end@requiredmodule'),T_OTHER($module))->unlist);
  $GULLET->input($module,['tex']);
  return;});#$
%</ltxml>
%    \end{macrocode}
% \end{macro}
% \ednote{the sinput macro is just faked, it should be more like requiremodules, except
% that the tex file is inputted; I wonder if this can be simplified.}
%
%    \begin{macrocode}
%<*package>
\let\sinputref=\sinput
\let\inputref=\input
%</package>
%<*ltxml> 
DefConstructor('\sinputref{}',"<omdoc:ref xref='#1.omdoc' type='cite' class='expandable'/>");
DefConstructor('\inputref{}',"<omdoc:ref xref='#1.omdoc' type='cite' class='expandable'/>");
%</ltxml>
%    \end{macrocode}
% 
% \subsubsection{Generating {\texorpdfstring\omdoc{OMDoc}} Presentation Elements}\label{sec:impl:presentation}
%
% Additional bundle of code to generate presentation encodings. Redefined to an expandable
% (macro) so that we can add conversions.
% 
%    \begin{macrocode}
%<*ltxml>
DefMacro('\@symdef@pres  OptionalKeyVals:symdef {}[][]{}', sub {
  my($self,$keys, $cs,$nargs,$opt,$presentation)=@_;

  my($name,$cd,$role)=$keys
   && map($_ && $_->toString,map($keys->getValue($_), qw(name cd role)));
  $cd = LookupValue('module_cd') unless $cd;
  $name = $cs unless $name;
  AssignValue('module_name'=>$name) if $name;
  $nargs = 0 unless ($nargs);
  my $nargkey = ToString($name).'_args';
  AssignValue($nargkey=>ToString($nargs)) if $nargs;
  $name=ToString($name);
  
  Invocation(T_CS('\@symdef@pres@aux'),
     $cs,
     ($nargs || Tokens(T_OTHER(0))),
     symdef_presentation_pmml($cs,ToString($nargs)||0,$presentation),
#     symdef_presentation_TeX($presentation),
     (Tokens(T_OTHER($name))),
     (Tokens(T_OTHER($cd))),
     $keys)->unlist; });#$
%    \end{macrocode}
% Generate the expansion of a symdef's macro using special arguments.
%
% Note that the |symdef_presentation_pmml| subroutine is responsible for preserving the
% rendering structure of the original definition. Hence, we keep a
% collection of all known formatters in the |@PresFormatters| array,
% which should be updated whenever the list of allowed formatters has
% been altered.
%
%    \begin{macrocode}
sub symdef_presentation_pmml {
  my($cs,$nargs,$presentation)=@_;
  my @toks = $presentation->unlist;
  while(@toks && $toks[0]->equals(T_SPACE)){ shift(@toks); }  # Remove leading space
  $presentation = Tokens(@toks);
  # Wrap with \@use, unless already has a recognized formatter.
  my $formatters = join("|",@PresFormatters);
  $formatters = qr/$formatters/;
  $presentation = Invocation(T_CS('\@use'),$presentation)
    unless (@toks && ($toks[0]->toString =~ /^\\($formatters)$/));
  # Low level substitution.
  my @args = map(Invocation(T_CS('\@SYMBOL'),T_OTHER("arg:".($_))),1..$nargs);
  $presentation = Tokens(LaTeXML::Expandable::substituteTokens($presentation,@args));
  $presentation; }#$
%    \end{macrocode}
% The |\@use| macro just generates the contents of the notation element
%    \begin{macrocode}
sub  getSymmdefProperties {
  my $cd = LookupValue('module_cd');
  my $name = LookupValue('module_name');
  my $nargkey = ToString($name).'_args';
  my $nargs = LookupValue($nargkey);
  $nargs = 0 unless ($nargs);
  my %props = ('cd'=>$cd,'name'=>$name,'nargs'=>$nargs);
  return %props;}
DefConstructor('\@use{}', sub{
  my ($document,$args,%properties) = @_;
  #Notation created at \@symdef@pres@aux
  #Create the rendering:
  $document->openElement('omdoc:rendering');
  $document->openElement('ltx:Math');
  $document->openElement('ltx:XMath');
  if ($args->isMath) {$document->absorb($args);}
  else {  $document->insertElement('ltx:XMText',$args);}
  $document->closeElement('ltx:XMath');
  $document->closeElement('ltx:Math');
  $document->closeElement('omdoc:rendering');
},
properties=>sub { getSymmdefProperties($_[1]);},
               mode=>'inline_math');
%    \end{macrocode}
% The |get_cd| procedure reads of the cd from our list of keys.
%    \begin{macrocode}
sub get_cd {
   my($name,$cd,$role)=@_;
   return $cd;}
%    \end{macrocode}
% The |\@symdef@pres@aux| creates the |symbol| element and the outer layer of the of the
% |notation| element. The content of the latter is generated by applying the {\latexml} to
% the definiens of the |\symdef| form. 
%    \begin{macrocode}
DefConstructor('\@symdef@pres@aux{}{}{}{}{} OptionalKeyVals:symdef', sub {
   my ($document,$cs,$nargs,$pmml,$name,$cd,$keys)=@_;
   my $assocarg = ToString($keys->getValue('assocarg')) if $keys;
   $assocarg = $assocarg||"0";
   my $bvars = ToString($keys->getValue('bvars')) if $keys;
   $bvars = $bvars||"0";
   my $bvar = ToString($keys->getValue('bvar')) if $keys;
   $bvar = $bvar||"0";
   my $appElement = 'om:OMA'; $appElement = 'om:OMBIND' if ($bvars || $bvar);

   $document->insertElement("omdoc:symbol",undef,(name=>$cs,"xml:id"=>ToString($cs).".sym"));
   $document->openElement("omdoc:notation",(name=>$name,cd=>$cd));
   #First, generate prototype:
   $nargs = ToString($nargs)||0;
   $document->openElement('omdoc:prototype');
   $document->openElement($appElement) if $nargs;
   my $cr="fun" if $nargs;
   $document->insertElement('om:OMS',undef,
    (cd=>$cd,
     name=>$name,
     "cr"=>$cr));
   if ($bvar || $bvars) {
     $document->openElement('om:OMBVAR');
     if ($bvar) {
       $document->insertElement('omdoc:expr',undef,(name=>"arg$bvar"));
     } else {
       $document->openElement('omdoc:exprlist',(name=>"args"));
       $document->insertElement('omdoc:expr',undef,(name=>"arg"));
       $document->closeElement('omdoc:exprlist');       
     }
     $document->closeElement('om:OMBVAR');
   }
   for my $id(1..$nargs) {
     next if ($id==$bvars || $id==$bvar);
     if ($id!=$assocarg) {
       my $argname="arg$id";
       $document->insertElement('omdoc:expr',undef,(name=>"$argname"));
     }
     else {
       $document->openElement('omdoc:exprlist',(name=>"args"));
       $document->insertElement('omdoc:expr',undef,(name=>"arg"));
       $document->closeElement('omdoc:exprlist');
     }
   }
   $document->closeElement($appElement) if $nargs;
   $document->closeElement('omdoc:prototype');
   #Next, absorb rendering:
   $document->absorb($pmml);
   $document->closeElement("omdoc:notation");
 }, afterDigest=>sub { my ($stomach, $whatsit) = @_;
  my $keys = $whatsit->getArg(6);
  my $module = LookupValue('current_module');
  $whatsit->setProperties(for=>ToString($whatsit->getArg(1)));
  $whatsit->setProperty(role=>($keys ? $keys->getValue('role')
       : (ToString($whatsit->getArg(2)) ? 'applied'
  : undef))); });
%    \end{macrocode}
% Convert a macro body (tokens with parameters |#1|,..) into a Presentation |style=TeX| form.
% walk through the tokens, breaking into chunks of neutralized (|T_OTHER|) tokens and
% parameter specs.
%    \begin{macrocode}
sub symdef_presentation_TeX {
  my($presentation)=@_;
  my @tokens = $presentation->unlist;
  my(@frag,@frags) = ();
  while(my $tok = shift(@tokens)){
    if($tok->equals(T_PARAM)){
      push(@frags,Invocation(T_CS('\@symdef@pres@text'),Tokens(@frag))) if @frag;
      @frag=();
      my $n = shift(@tokens)->getString;
      push(@frags,Invocation(T_CS('\@symdef@pres@arg'),T_OTHER($n+1))); }
    else {
      push(@frag,T_OTHER($tok->getString)); }} # IMPORTANT! Neutralize the tokens!
  push(@frags,Invocation(T_CS('\@symdef@pres@text'),Tokens(@frag))) if @frag;
  Tokens(map($_->unlist,@frags)); }
DefConstructor('\@symdef@pres@arg{}', "<omdoc:recurse select='#select'/>",
	       afterDigest=>sub { my ($stomach, $whatsit) = @_;
				  my $select = $whatsit->getArg(1);
				  $select = ref $select ? $select->toString : '';
				  $whatsit->setProperty(select=>"*[".$select."]"); });
DefConstructor('\@symdef@pres@text{}', "<omdoc:text>#1</omdoc:text>");
%</ltxml>#$
%    \end{macrocode}
%
% 
% \subsection{Including Externally Defined Semantic Macros }\label{sec:impl:packages}
% 
% \begin{macro}{\requirepackage}
%    \begin{macrocode}
%<*package>
\def\requirepackage#1#2{\makeatletter\input{#1.sty}\makeatother}
%</package>
%<*ltxml>
DefConstructor('\requirepackage{} Semiverbatim',"<omdoc:imports from='#2'/>",
       afterDigest=>sub { my ($stomach, $whatsit) = @_;
  my $select = $whatsit->getArg(1);
  RequirePackage($select->toString); });#$
%</ltxml>
%    \end{macrocode}
% \end{macro}
% 
% \subsection{Views}\label{sec:impl:views}
%
%    \begin{macrocode}
%<*package>
\srefaddidkey{view}
\addmetakey{view}{from}
\addmetakey{view}{to}
\addmetakey*{view}{title}
\ifmod@show 
\newsavebox{\viewbox}
\newcounter{view}[section]
\def\view@heading{{\textbf{View} \thesection.\theview}
  \sref@label@id{View \thesection.\theproblem}
  \@ifundefined{view@title}{:\quad}{\quad(\view@title)\hfill\\}}
\newenvironment{view}[1][]{\metasetkeys{view}{#1}\sref@target\stepcounter{view}
\begin{lrbox}{\viewbox}\begin{minipage}{.9\textwidth}\importmodule{\view@to}}
{\end{minipage}\end{lrbox}
\setbox0=\hbox{\begin{minipage}{.9\textwidth}%
\noindent\view@heading\rm%
\end{minipage}}
\smallskip\noindent\fbox{\vbox{\box0\vspace*{.2em}\usebox\viewbox}}\smallskip}
\else\newxcomment[]{view}\fi
\def\vassign#1#2{#1\ensuremath{\mapsto #2}}
%</package>
%    \end{macrocode}
%
% \subsection{Deprecated Functionality}\label{sec:impl:deprecated}
%
% 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}
%<*package>
\define@key{module}{uses}{%
\@for\module@tmp:=#1\do{\activate@defs\module@tmp\export@defs\module@tmp}}
%</package>
%    \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}
%<*package>
\define@key{module}{usesqualified}{%
\@for\module@tmp:=#1\do{\activate@defs{qualified@\module@tmp}\export@defs\module@tmp}}
%</package>
%    \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 below.
% 
%    \begin{macrocode}
%<*ltxml>
Tag('omdoc:recurse',afterOpen=>\&numberIt,afterClose=>\&locateIt);
Tag('omdoc:imports',afterOpen=>\&numberIt,afterClose=>\&locateIt);
Tag('omdoc:theory',afterOpen=>\&numberIt,afterClose=>\&locateIt);
%</ltxml>
%    \end{macrocode}
%
% \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}
%<*package>
\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}}
%</package>
%<*ltxml>
%</ltxml>
%    \end{macrocode}
% \end{macro}
% 
% \begin{macro}{\notationdef}
% For the {\LaTeX} side, we just make |\notationdef| invisible.
%    \begin{macrocode}
%<*package>
\def\notationdef[#1]#2#3{}
%</package>
%<*ltxml>
%</ltxml>
%    \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
%%% Local Variables: 
%%% mode: doctex
%%% TeX-master: t
%%% End: 
% LocalWords:  GPL structuresharing STR dtx env envfalse idfalse displayfalse
% LocalWords:  usesfalse usesqualified usesqualifiedfalse envtrue idtrue CPERL
% LocalWords:  usestrue displaytrue usesqualifiedtrue RequirePackage keyval tmp
% LocalWords:  defs foreach LookupValue activateScope DefEnvironment keyvals cd
% LocalWords:  OptionalKeyVals getValue toString AssignValue openElement omdoc
% LocalWords:  closeElement beforeDigest useTheoryItemizations afterDigestBegin
% LocalWords:  whatsit setProperty getArg qw symdef  iffalse importOMDocmodule
% LocalWords:  DefKeyVal Semiverbatim symdeflocal atqualified DefMacro STDERR
% LocalWords:  args unlist DefPrimitive nargs Stringify eq attr omcd ltx XMTok
% LocalWords:  DefConstructorI convertLaTeXArgs scriptpos XMApp OMA XMArg simpl
% LocalWords:  DefMacroI blaaaa savedprefix aaa simplhelp tust tist tost reguse
% LocalWords:  updatedpre ReturnAfterFi updateall updatedpost updatesms bgroup
% LocalWords:  texclude tinclude getGullet requiredmodule tex sms egroup pmml
% LocalWords:  toks mixfixi mixfixa mixfixii mixfixia mixfixai mixfixiii arg cr
% LocalWords:  DefConstructor afterDigest setProperties undef tok PARAM locator
% LocalWords:  getString showfalse showtrue xcomment stex srcref KeyVal omext
% LocalWords:  beginItemize getProperty introdcue afterOpen numberIt Tokenize
% LocalWords:  OptionalSemiverbatim omdocmod PushValue assocarg getStomach prs
% LocalWords:  begingroup beginMode endMode endgroup insertElement resymdef sym
% LocalWords:  updir nargkey PresFormatters mixfixaii formatters argname expr
% LocalWords:  getSymmdefProperties XMath mcdcr exprlist recurse texttt scsys
% LocalWords:  textbackslash newcommand providecommand sc sc mathml openmath nx
% LocalWords:  latexml cmathml activemath twintoo atwin atwintoo mathcal Deyan
% LocalWords:  mathcal fileversion Ginev maketitle  newpage infty ulsmf08 exfig
% LocalWords:  omsemmac lstset basicstyle scriptsize aboveskip belowskip hline
% LocalWords:  morekeywords lstlisting csymbol showviews showviews foo exf cseq
% LocalWords:  qualifiedimports qualifiedimports termdef textbf filepath RabKoh
% LocalWords:  symname varSmoothfunctionsOn ednote abbrdef Sumfromto semmodule
% LocalWords:  vspace hrule vspace arith arbitraryn xbool oplus xdisjunction tw
% LocalWords:  emph captitalize ldots termref termref symref symref ctancite nc
% LocalWords:  smms hyperref RahObe hmlmh10 widehat texmf.cnf requiremodules cs
% LocalWords:  sinput sinputref sinputref defpath defpath defpath cname csname
% LocalWords:  OPhats usepackage importqualified Crossreferencing jobname ltxml
% LocalWords:  jobname printbibliography textsf langle textsf langle textlangle
% LocalWords:  textrangle textlangle newif ifmod qualifiedfalse qualifiedtrue
% LocalWords:  sref xspace expandafter noexpand endcsname namedef setkeys ifx
% LocalWords:  newenvironment parentmod usemodule ifundefined coolurion cooluri
% LocalWords:  coolurioff cwd ouri ifdefinable testopt ifnextchar xargdef bvars
% LocalWords:  argdef yargdef somefunction symdeflocaltrue bvar xpath assoc qr
% LocalWords:  symdeflocalfalse localpres isbound symdefs COMPLEXTOKEN localp
% LocalWords:  findnodes localname carg renewcommand bbb
% LocalWords:  refundefinedtrue subsubsection blaaa makeatletter makeatother rm
% LocalWords:  ifmodules gdef xdef xdef modulestrue modulesfalse pathpostfix
% LocalWords:  updatedsms newreg xref texorpdfstring srefaddidkey newsavebox
% LocalWords:  viewbox newcounter thesection theview theproblem hfill lrbox
% LocalWords:  stepcounter textwidth hbox noindent smallskip fbox vbox usebox
% LocalWords:  smallskip newxcomment vassign ensuremath mapsto doctex tocdepth
% LocalWords:  setcounter tableofcontents mathbb
