% \iffalse meta-comment
% An Infrastructure for Mathematical Statements in sTeX
% Copyright (C) 2004-2008 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/statements/statements.dtx $
% \fi
%  
% \iffalse
%<package>\NeedsTeXFormat{LaTeX2e}[1999/12/01]
%<package>\ProvidesPackage{statements}[2012/01/28 v1.1 Semantic Markup for Statements]
%
%<*driver>
\documentclass{ltxdoc}
\usepackage{url,array,float,amsfonts}
\usepackage{statements,modules,presentation}
\usepackage{paralist}
\usepackage[show]{ed}
\usepackage[hyperref=auto,style=alphabetic]{biblatex}
\bibliography{kwarc}
\usepackage[eso-foot,today]{svninfo}
\usepackage{stex-logo}
\usepackage{../ctansvn}
\usepackage{hyperref}
\svnInfo $Id: statements.dtx 1999 2012-01-28 07:32:11Z kohlhase $
\svnKeyword $HeadURL: https://svn.kwarc.info/repos/stex/trunk/sty/statements/statements.dtx $
\makeindex
\floatstyle{boxed}
\newfloat{exfig}{thp}{lop}
\floatname{exfig}{Example}
\def\tracissue#1{\cite{sTeX:online}, \hyperlink{http://trac.kwarc.info/sTeX/ticket/#1}{issue #1}}
\begin{document}\DocInput{statements.dtx}\end{document}
%</driver>
% \fi
% 
% \CheckSum{597}
%
% \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/09/09}{moved omtext and friends to the omdoc package}
% \changes{v0.9d}{2007/09/09}{made dependence on the omdoc package explicit}
% \changes{v0.9d}{2007/09/09}{adding ids to many elements}
% \changes{v0.9e}{2008/05/27}{adding cross-references}
% \changes{v0.9e}{2008/09/29}{augmenting the index macros with optional values}
% \changes{v0.9f}{2008/12/04}{changed 'consymb' to 'symboldec' and documented it.}
% \changes{v0.9g}{2010/01/14}{the package is now based on {\texttt{ntheorem for presentation}}}
% \changes{v0.9g}{2010/01/19}{Added support for localization}
% \changes{v0.9g}{2010/02/23}{added {\texttt{\textbackslash symref}}}
% \changes{v1.0}{2010/06/18}{now based on  {\texttt{omtext}} package instead of {\texttt{omdoc}}}
% \changes{v1.0}{2010/07/13}{adding {\texttt{\textbackslash inlineex}}}
% \changes{v1.1}{2011/08/25}{renaming all convenience macros for {\texttt{\textbackslash
% definendum}} and {\texttt{\textbackslash termref}}}
% 
% \GetFileInfo{statements.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\activemath{\scsys{ActiveMath}}
% \title{Semantic Markup for Mathematical Statements\thanks{Version {\fileversion} (last revised
%        {\filedate})}}
%    \author{Michael Kohlhase\\
%            Jacobs University, Bremen\\
%            \url{http://kwarc.info/kohlhase}}
% \maketitle
%
% \begin{abstract}
%   The |statements| package is 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 provides semantic markup facilities for mathematical statements like
%   Theorems, Lemmata, Axioms, Definitions, etc. in {\stex} files. This structure can be
%   used by MKM systems for added-value services, either directly from the {\sTeX}
%   sources, or after translation.
% \end{abstract}
% 
% \setcounter{tocdepth}{2}\tableofcontents\newpage
%
% \section{Introduction}\label{sec:intro}
%
% The motivation for the |statements| package is very similar to that for semantic macros
% in the |modules| package: We want to annotate the structural semantic properties of
% statements in the source, but present them as usual in the formatted documents. In
% contrast to the case for mathematical objects, the repertoire of mathematical statements
% and their structure is more or less fixed.
%
% This structure can be used by MKM systems for added-value services, either directly from
% the {\sTeX} sources, or after translation. Even though it is part of the {\stex}
% collection, it can be used independently, like it's sister package |sproofs|.
%
% {\stex}~\cite{Kohlhase:ulsmf08,sTeX:online} is a version of {\TeX/\LaTeX} that allows
% to markup {\TeX/\LaTeX} documents semantically without leaving the document format,
% essentially turning {\TeX/\LaTeX} into a document format for mathematical knowledge
% management (MKM). Currently the {\omdoc} format~\cite{Kohlhase:omdoc1.2} is directly
% supported.
% 
% \section{The User Interface}\label{sec:user-interface}
% 
% The |statements| package supplies a semantically oriented infrastructure for marking up
% mathematical statements: fragments of natural language that state properties of
% mathematical objects, e.g. axioms, definitions, or theorems. The |statement| package
% provides an infrastructure for marking up the semantic relations between statements for
% the {\omdoc} transformation and uses the |ntheorem| package~\cite{MaySch:eltte09} for
% formatting (i.e. transformation to PDF).
%
% \subsection{Package Options}\label{sec:user:options}
% 
% The |statements| package takes a single option: \DescribeMacro{showmeta}|showmeta|. If
% this is set, then the metadata keys are shown (see~\cite{Kohlhase:metakeys:ctan} for details
% and customization options).
%
% \subsection{Statements}\label{sec:statements}
% 
% All the statements are marked up as environments, that take a |KeyVal| argument that
% allows to annotate semantic information. Generally, we distinguish two forms of
% statements:
% \begin{description}
% \item[{\twintoo{block}{statement}s}] have explicit discourse markers that delimit their
%   content in the surrounding text, e.g. the boldface word ``{\bf{Theorem}:}'' as a start
%   marker and a little line-end box as an end marker of a proof.
% \item[{\twintoo{flow}{statement}s}] do not have explicit markers, they are interspersed
%   with the surrounding text.
% \end{description}
% Since they have the same semantic status, they must both be marked up, but styled
% differently. We distinguis between these two presentational forms with the
% \DescribeMacro{display=}|display| key, which is allowed on all statement
% environments. If it has the value |block| (the default), then the statement will be
% presented in a paragraph of its own, have explicit discourse markers for its begin and
% end, possibly numbering, etc. If it has the value |flow|, then no extra presentation
% will be added the semantic information is invisible to the reader. Another key that is
% present on all statement environments in the \DescribeMacro{id=}|id| key it allows to
% identify the statement with a name and to reference it with the semantic referencing
% infrastructure provided by the |sref| package~\ctancite{Kohlhase:sref}.
%
% \subsubsection{Axioms and Assertions}\label{sec:user:axiomassertion}
% 
% The \DescribeEnv{assertion}|assertion| environment is used for marking up statements
% that can be justified from previously existing knowledge (usually marked with the
% monikers ``Theorem'', ``Lemma'', ``Proposition'', etc. in mathematical vernacular). The
% environment |assertion| is used for all of them, and the particular subtype of
% assertion is given in the \DescribeMacro{type=}|type| key. So instead of
% |\begin{Lemma}|\iffalse\end{Lemma}\fi we have to write
% |\begin{assertion}[type=lemma]|\iffalse\end{assertion}\fi (see
% Example~\ref{fig:assertion} for an example).
% \begin{exfig}
% \begin{verbatim}
% \begin{assertion}[id=sum-over-odds,type=lemma]
%   $\sum_{i=1}^n{2i-1}=n^2$
% \end{assertion}
% \end{verbatim}
% \vspace{-1em}will lead to the result\vspace{-2em}\par\noindent
% \begin{assertion}[id=sum-over-odds,type=lemma]
%   $\sum_{i=1}^n{2i-1}=n^2$
% \end{assertion}
% \caption{Semantic Markup for a Lemma in a {\texttt{module}} context}\label{fig:assertion}
% \end{exfig}
%
% Whether we will see the keyword ``Lemma'' will depend on the value of the optional
% |display| key.  In all of the |assertion| environments, the presentation expectation is
% that the text will be presented in italic font. The presentation (keywords, spacing, and
% numbering) of the |assertion| environment is delegated to a theorem styles from the
% |ntheorem| environment. For an assertion of type \meta{type} the |assertion| environment
% calls the |ST|\meta{type}|AssEnv| environment provided by the |statements| package; see
% Figure~\ref{fig:assertion-types} for a list of provided assertion types. Their
% formatting can be customized by redefining the |ST|\meta{type}|AssEnv| environment via
% the |\renewtheorem| command from the |ntheorem| package; see~\cite{MaySch:eltte09} for
% details.
%
% \begin{exfig}
%   \begin{tabular}{|l|l|}\hline
%     Value & Explanation \\\hline\hline
%     \textbf{theorem}, \textbf{proposition} 
%     & an important assertion with a proof\\\hline 
%     \multicolumn{2}{|p{12cm}|}{\footnotesize Note that the meaning of \textbf{theorem}
%       (in this case the existence of a proof) is not
%       enforced by {\omdoc} applications. It can be appropriate to give an assertion
%       the \textbf{theorem}, if the
%       author knows of a proof (e.g. in the literature), but has not formalized it in
%       {\omdoc} yet.}\\\hline\hline
%     \textbf{lemma} & a less important assertion with a proof\\\hline
%     \multicolumn{2}{|p{12cm}|}{\footnotesize The difference of importance specified
%     here is even softer than the other ones, since e.g. reusing
%     a mathematical paper as a chapter in a larger monograph, may make it necessary to
%     downgrade a theorem (e.g.  the main theorem of the paper) and give it the status of
%     a lemma in the overall work.}\\\hline\hline
%     \textbf{corollary} & a simple consequence\\\hline
%     \multicolumn{2}{|p{12cm}|}{\footnotesize An assertion is
%       sometimes marked as a corollary to some other statement, if the proof is
%       considered simple. This is often the case for important theorems that are simple
%       to get from technical lemmata.}\\\hline\hline
%     \textbf{postulate}, \textbf{conjecture}
%     & an assertion without proof or counter-exam\-ple\\\hline
%     \multicolumn{2}{|p{12cm}|}{\footnotesize Conjectures are assertions, whose
%       semantic value is not yet decided, but which the author considers likely to be
%       true. In particular, there is no proof or counter-example.}\\\hline\hline
%     \textbf{false-conjecture} 
%     & an assertion with a counter-example\\\hline
%     \multicolumn{2}{|p{12cm}|}{\footnotesize A conjecture that has proven to be false,
%       i.e. it has a counter-example. Such assertions are often kept for illustration and
%       historical purposes.}\\\hline\hline
%     \textbf{obligation}, \textbf{assumption} 
%     & an assertion on which a proof of another depends\\\hline
%     \multicolumn{2}{|p{12cm}|}{\footnotesize These kinds of assertions
%       are convenient during the exploration of a mathematical theory. They can be used
%       and proven later (or assumed as an axiom).}\\\hline\hline
%     \textbf{observation} & if everything else fails\\\hline
%     \multicolumn{2}{|p{12cm}|}{\footnotesize This type is the catch-all if none of the others
%       applies.}\\\hline 
%   \end{tabular}
% \caption{Types of Mathematical Assertions}\label{fig:assertion-types}
% \end{exfig}
%
% \DescribeEnv{axiom} The |axiom| environment is similar to |assertion|, but the content
% has a different ontological status: axioms are assumed without (formal) justification,
% whereas assertions are expected to be justified from other assertions, axioms or
% definitions. This environment relegates the formatting to the |STaxiomEnv| environment,
% which can be redefined for configuration.
% 
% \subsubsection{Symbols}\label{sec:user:symbol}
%
% \DescribeEnv{symboldec} The |symboldec| environment can be used for declaring concepts
% and symbols. Note the the |symdef| forms from the |modules| package will not do this
% automatically (but the |definition| environment and the |\inlinedef| macro will for all
% the definienda; see below). The |symboldec| environment takes an optional keywords
% argument with the keys |id|, |role|, |title| and |name|. The first is for general
% identification, the |role| specifies the {\openmath}/{\omdoc} role, which is one of
% |object|, |type|, |sort|, |binder|, |attribution|, |application|, |constant|,
% |semantic-attribution|, and |error| (see the {\omdoc} specification for details). The
% |name| key specifies the {\openmath} name of the symbol, it should coincide with the
% control sequence introduced by the corresponding |\symdef| (if one is present). The
% |title| key is for presenting the title of this symbol as in other statements. Usually,
% |axiom| and |symboldec| environments are used together as in Figure~\ref{fig:axioms}.
%
%\begin{exfig}
% \begin{verbatim}
% \symdef{zero}{0}
% \begin{symboldec}[name=zero,title=The number zero,type=constant]
%   The number zero, it is used as the base case of the inductive definition
%   of natural numbers via the Peano Axioms.
% \end{symboldec}
% 
% \symdef{succ}[1]{\prefix{s}{#1}}
% \begin{symboldec}[name=succ,title=The Successor Function,type=application]
%   The successor function, it is used for the step case of the inductive
%   definition of natural numbers via the Peano Axioms.
% \end{symboldec}
%
% \symdef{NaturalNumbers}{\mathbb{N}}
% \begin{symboldec}[name=succ,title=The Natural Numbers,type=constant]
%   The natural numbers inductively defined via the Peano Axioms.
% \end{symboldec}
% 
% \begin{axiom}[id=peano.P1,title=P1]
%   $\zero$ is a natural number.
% \end{axiom}
% ...
% \begin{axiom}[id=peano.P5,title=P5]
%   Any property $P$ such $P(\zero)$ and $P(\succ{k})$ whenever $P(k)$ 
%   holds for all $n$ in $\NaturalNumbers$
% \end{axiom}
% \end{verbatim}
% \vspace{-1em}will lead to the result\medskip\par\noindent
% \begin{module}[id=peano]
% \symdef{zero}{0}
% \begin{symboldec}[name=zero,title=The number zero,role=constant]
%   The number zero, it is used as the base case of the inductive definition
%   of natural numbers via the Peano Axioms.
% \end{symboldec}
% 
% \symdef{succ}[1]{\prefix{s}{#1}}
% \begin{symboldec}[name=succ,title=The Successor Function,role=application]
%   The successor function, it is used for the step case of the inductive
%   definition of natural numbers via the Peano Axioms.
% \end{symboldec}
%
% \symdef{NaturalNumbers}{\mathbb{N}}
% \begin{symboldec}[name=succ,title=The Natural Numbers,role=constant]
%   The natural numbers inductively defined via the Peano Axioms.
% \end{symboldec}
% 
% \begin{axiom}[id=peano.P1,title=P1]
%   $\zero$ is a natural number.
% \end{axiom}
% \ldots \stepcounter{STtheoremAssEnv}\stepcounter{STtheoremAssEnv}\stepcounter{STtheoremAssEnv}
% \begin{axiom}[id=peano.P5,title=P5]
%   Any property $P$ such $P(\zero)$ and $P(\succ{k})$ whenever $P(k)$ 
%   holds for all $n$ in $\NaturalNumbers$
% \end{axiom}
% \end{module}
% \caption{Semantic Markup for the Peano Axioms}\label{fig:axioms}
% \end{exfig}
%
% \subsubsection{Definitions, and Definienda}\label{sec:definition}
% 
% \DescribeEnv{definition} The |definition| environment is used for marking up
% mathematical definitions. Its peculiarity is that it defines (i.e. gives a meaning to)
% new mathematical concepts or objects. These\DescribeMacro{\definiendum} are identified
% by the |\definiendum| macro, which is used as
% |\definiendum[|\meta{sysname}|]{|\meta{text}|}|. Here, \meta{text} is the text that is
% to be emphasized in the presentation and the optional \meta{sysname} is a system name of
% the symbol defined (for reference via |\term|, see Section~\ref{sec:user:crossref}). If
% \meta{sysname} is not given, then \meta{text} is used as a system name instead, which is
% usually sufficient for most situations.
% 
%\begin{exfig}
% \begin{verbatim}
% \symdef{one}{1}
% \begin{definition}[id=one.def,for=one]
%   $\notatiendum[one]{\one}$ is the successor of $\zero$
%   (formally: $\one\colon=\succ\zero$)
% \end{definition}
% \end{verbatim}
% \vspace{-1em}will lead to the result\medskip\par\noindent
% \begin{module}
% \importmodule{peano}
% \symdef{one}{1}
% \begin{definition}[id=one.def,for=one]
%   $\notatiendum[one]{\one}$ is the successor of $\zero$
%   (formally: $\one\colon=\succ\zero$)
% \end{definition}
% \end{module}
% \caption{A Definition based on Figure {\ref{fig:axioms}}}\label{fig:definition}
% \end{exfig}
% The \DescribeMacro{defin}|\defi{|\meta{word}|}| macro combines the functionality of the
% |\definiendum| macro with index markup from the |omdoc|
% package~\ctancite{Kohlhase:smomdl}: use |\defi[|\meta{name}|]{|\meta{word}|}| to markup
% a definiendum \meta{word} with system name \meta{name} that appear in the index --- in
% other words in almost all definitions of single-word concepts. We also have the variants
% \DescribeMacro{\defii}|\defii| and \DescribeMacro{\defiii}|\defiii| for (adjectivized)
% two-word compounds. Finally, the varaiants \DescribeMacro{\adefi}|\adefi|,
% \DescribeMacro{\adefii}|\adefii|,and \DescribeMacro{\adefiii}|\adefiii| have an
% additional first argument that allows to specify an alternative text; see
% Figure~\ref{fig:defin}
% 
% \begin{exfig}
% \begin{tabular}{l|l|l}
%   \multicolumn{3}{l}{source}\\
%   system name & result & index \\\hline
%   \multicolumn{3}{l}{\texttt{\textbackslash defin\{concept\}}}\\
%   |concept| & concept& concept\\\hline
%   \multicolumn{3}{l}{\texttt{\textbackslash defin[csymbol]\{concept\}}}\\
%   |csymbol| & concept & concept\\\hline
%   \multicolumn{3}{l}{\texttt{\textbackslash definalt[csymbol]\{concepts\}\{concept\}}}\\
%   |csymbol| & concepts & concept\\\hline
%   \multicolumn{3}{l}{\texttt{\textbackslash twindef\{concept\}\{group\}}}\\
%   |concept-group| & concept group & concept group,  \\
%   && group - , concept\\\hline
%   \multicolumn{3}{l}{\texttt{\textbackslash atwindef\{small\}\{concept\}\{group\}}}\\
%   |small-concept-group| & small concept group &  small concept group,  \\
%   && concept group - , small\\
% \end{tabular}
% \caption{Some definienda with Index}\label{fig:defin}
% \end{exfig}
% 
% Note that the |\definiendum|, |\defi|, |\defii|, and |\defiii| macros can only be
% used inside the definitional situation, i.e. in a |definition| or |symboldec|
% environment or a |\inlinedef| macro. If you find yourself in a situation where you want
% to use it outside, you will most likely want to wrap the appropriate text fragment in a
% |\begin{definition}[display=flow]| ... and |\end{definition}|. For instance, we could
% continue the example in Figure~\ref{fig:axioms} with the |definition| environment in
% Figure~\ref{fig:definition}.
% 
% \DescribeMacro{\inlinedef} Sometimes we define mathematical concepts in passing, e.g. in
% a phrase like ``\ldots $s(o)$ which we call {\textbf{one}}.''. For this we cannot use
% the |definition| environment, which presupposes that its content gives all that is
% needed to understand the definition. But we do want to make use of the infrastructure
% introduced for the |definition| environment. In this situation, we just wrap the phrase
% in an |\inlinedef| macro that makes them available. The |\inlinedef| macro accepts the
% same |id| and |for| keys in its optional argument, and additionally the |verbalizes| key
% which can be used to point to a full definition of the concept somewhere else.
%
% Note that definienda can only be referenced via a |\term| element, if they are only
% allowed inside a named module, i.e. a |module| environment with a name given by the
% |id=| key or the |theory=| key on is specified on the definitional environment.
%
% \subsubsection{Examples}\label{sec:user:example}
% 
% \DescribeEnv{example} The |example| environment is a generic statement environment,
% except that the |for| key should be given to specify the identifier what this is an
% example for. The |example| environment also expects a |type| key to be specified, so
% that we know whether this is an example or a counterexample.
% 
% \DescribeMacro{\inlineex} The |\inlineex| is analogous to |\inlinedef|, only that it is
% used for inline examples, e.g. ``\ldots mammals, e.g. goats''. Note that we have used an
% inline example for an inline example.
%
% \subsection{Cross-Referencing Symbols and Concepts}\label{sec:user:crossref}
%
% If we have defined a concept with the |\definiendum| macro, then we can mark up other
% occurrences of the term as referring to this concept. Note that this process cannot be
% fully automatized yet, since that would need advanced language technology to get around
% problems of disambiguation, inflection, and non-contiguous phrases\footnote{We do have a
%   program that helps annotate larger text collections spotting the easy cases; see
%   {\url{http://kwarc.info/projects/stex}} and look for the program
%   |termin|.}. Therefore, the \DescribeMacro{\termref}|\termref| can be used to make this
% information explicit. It takes the keys
% \begin{compactdesc}
% \item[\texttt{cdbase}] to specify a URI (a path actually, since {\LaTeX} cannot load
%   from URIs) where the module can be found.
% \item[\texttt{cd}] to specify the module in which the term is defined. If the |cd| key
%   is not given, then the current module is assumed. If no |cdbase| is specified (this is
%   the usual case), then the CD has to be imported via a |\importmodule| from the
%   |modules| package~\ctancite{KohAmb:smmssl}.
% \item[\texttt{name}] to specify the name of the definiendum (which is given in the body
%   of the |\definiendum| or the optional argument). If the |name| key is not specified,
%   then argument of the |\termref| macro is used.
% \item[\texttt{role}] is currently unused.
% \end{compactdesc}
% |\termref[cd=|\meta{cd}|,name=|\meta{name}|]{|\meta{text}|}| will just typeset the link
% text \meta{text} with (if the |hyperref| package is loaded) a hyperlink to the
% definition in module \meta{cd} that defines the concept \meta{name}, e.g. that contains
% |\defi[|\meta{name}|]{|\meta{text}|}|.
%
% Just as the |\definiendum| macro has the convenience variants |\defi|, |\defii| and
% |\defiii|, the |\termref| has variants |\trefi|, |\trefii|, and |\trefiii| that take two
% and three arguments for the parts of the compositum. In the same module, concepts that
% are marked up by |\defi{|\meta{name}|}| in the definition can be referenced by
% \DescribeMacro{\trefi}|\trefi{|\meta{name}|}|. Here the link text is just
% \meta{name}. Concepts defined via |\defii{|\meta{first}|}{|\meta{second}|}| can be
% referenced by \DescribeMacro{\trefii}|\trefii{|\meta{first}|}{|\meta{second}|}| (with
% link text ``\meta{first} \meta{second}'') and analogously for |\defiii| and
% \DescribeMacro{\trefiii}|\trefiii|. Finally, we have variants
% \DescribeMacro{\atref*}|\atrefi|, |\atrefii|, and |\atrefiii| with alternative link
% text. For instance |\atrefii{|\meta{text}|{|\meta{first}|}{|\meta{second}|}| references
% a concept introduced by |\defii{|\meta{first}|}{|\meta{second}|}| but with link text
% \meta{text}.  Of course, if the system identifier is given explicitly in the optional
% argument of the definition form, as in
% |\defii[|\meta{name}|]{|\meta{first}|}{|\meta{second}|}|, then the terms are referenced
% by |\trefi{|\meta{name}|}|.
%
% For referencing terms outside the current module, the module name can be specified in
% the first optional argument of the |\*tref*| macros. To specify the |cdbase|, we have to
% resort to the |\termref| macro with the keyval arguments.
%
% Note that the |\termref| treatment above is natural for ``concepts'' declared by the
% |\termdef| macro from the |modules| package~\ctancite{KohAmb:smmssl}. Concepts are
% natural language names for mathematical objects. For ``symbols'', i.e. symbolic
% identifiers for mathematical objects used in mathematical formulae, we use the |\symdef|
% macro from the |modules| package. Sometimes, symbols also have an associated natural
% language concept, and we want to use the symbol name to reference it (instead of
% specifying |cd| and |name| which is more inconvenient). For this the |statements|
% package supplies the \DescribeMacro{\symref}|\symref| macro. Like |\termref|, and
% invocation of |\symref{|\meta{cseq}|}{|\meta{text}|}| will just typeset \meta{text} with
% a hyperlink to the relevant definition (i.e. the one that has the declaration
% |for=|\meta{cseq} in the metadata argument.)
% 
% \section{Configuration of the Presentation}\label{sec:conf}
% 
% \DescribeMacro{\defemph} The |\defemph| macro is a configuration hook that allows to
% specify the style of presentation of the {\index*{definiendum}}. By default, it is set to
% |\bf| as a fallback, since we can be sure that this is always available. It can be
% customized by  redefinition: For instance |\renewcommand{\defemph}[1]{\emph{#1}}|,
% changes the default behavior to italics.
%
% \DescribeMacro{\termemph} The |\termenph| macro does the same for the style for
% |\termref|, it is empty by default. Note the term might carry an implicit hyper-reference
% to the defining occurrence and that the presentation engine might mark this up, changing
% this behavior.
%
% \DescribeMacro{\stDMemph} The |\stDMemph| macro does the same for the style for the
% markup of the discourse markers like ``Theorem''. If it is not defined, it is set to
% |\bf|; that allows to preset this in the class file. \ednote{function declarations}
% 
% Some authors like to lowercase the semantic references, i.e. use ``axiom 2.6'' instead
% of the default ``\sref{peano.P5}'' to refer to the last axiom in
% Figure~\ref{fig:axioms}. This can be achieved by redefining the
% \DescribeMacro{\STpresent}|\STpresent| macro, which is applied to the keyword of the
% |ST*Env| theorem environments.\ednote{this does not quite work as yet, since
%   \textbf{STpresent} is applied when the label is written. But we would really like to
%   have it applied when the reference is constructed. But for that we need to split the
%   label into keyword and number in package |sref|.}
% 
% Finally, we provide configuration hooks in Figure~\ref{fig:hooks} for the statement
% types provided by the |statement| package. These are mainly intended for package authors
% building on |statements|, e.g. for multi-language support.\ednote{we might want to
%   develop an extension \texttt{statements-babel} in the future.}.
%\begin{exfig}
% \begin{tabular}{lll}
% Environment & configuration macro & value\\\hline\hline
% \texttt{STtheoremAssEnv} & \texttt{\textbackslash st@theorem@kw} & \makeatletter\st@theorem@kw\\\hline
% \texttt{STlemmaAssEnv}  & \texttt{\textbackslash st@lemma@kw}  & \makeatletter\st@lemma@kw \\\hline
% \texttt{STpropositionAssEnv} & \texttt{\textbackslash st@proposition@kw} &  \makeatletter\st@proposition@kw \\\hline
% \texttt{STcorollaryAssEnv} & \texttt{\textbackslash st@corollary@kw} & \makeatletter\st@corollary@kw\\\hline
% \texttt{STconjectureAssEnv} & \texttt{\textbackslash st@conjecture@kw} & \makeatletter\st@conjecture@kw\\\hline
% \texttt{STfalseconjectureAssEnv} & \texttt{\textbackslash st@falseconjecture@kw} & \makeatletter\st@falseconjecture@kw\\\hline
% \texttt{STpostulateAssEnv} & \texttt{\textbackslash st@postulate@kw} & \makeatletter\st@postulate@kw\\\hline
% \texttt{STobligationAssEnv} & \texttt{\textbackslash st@obligation@kw} & \makeatletter\st@obligation@kw\\\hline
% \texttt{STassumptionAssEnv} & \texttt{\textbackslash st@assumption@kw} & \makeatletter\st@assumption@kw\\\hline
% \texttt{STobservationAssEnv} & \texttt{\textbackslash st@observation@kw} & \makeatletter\st@observation@kw\\\hline
% \texttt{STexampleEnv} & \texttt{\textbackslash st@example@kw} & \makeatletter\st@example@kw\\\hline
% \texttt{STaxiomEnv} & \texttt{\textbackslash st@axiom@kw} & \makeatletter\st@axiom@kw\\\hline
% \texttt{STdefinitionEnv} & \texttt{\textbackslash st@definition@kw} & \makeatletter\st@definition@kw\\\hline
% \texttt{STnotationEnv} & \texttt{\textbackslash st@notation@kw} & \makeatletter\st@notation@kw
% \end{tabular}
% \caption{Configuration Hooks for statement types}\label{fig:hooks}
% \end{exfig}
%
% \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\printbibliography}
% 
% \section{The Implementation}\label{sec:impl} 
% 
% The |statements| package generates two files: the {\LaTeX} package (all the code between
% {\textsf{$\langle$*package$\rangle$}} and {\textsf{$\langle$/package$\rangle$}}) and the
% {\latexml} bindings (between {\textsf{$\langle$*ltxml$\rangle$ and
%     $\langle$/ltxml$\rangle$}}). We keep the corresponding code fragments together,
% since the documentation applies to both of them and to prevent them from getting out of
% sync.
%
% \subsection{Package Options}\label{sec:impl:options}
%
% We declare some switches which will modify the behavior according to the package
% options. Generally, an option |xxx| will just set the appropriate switches to true
% (otherwise they stay false). First we have the general options
%    \begin{macrocode}
%<*package>
\DeclareOption{showmeta}{\PassOptionsToPackage{\CurrentOption}{metakeys}}
\DeclareOption*{\PassOptionsToPackage{\CurrentOption}{omdoc}}
%    \end{macrocode}
%    Finally, we need to declare the end of the option declaration section to {\LaTeX}.
%    \begin{macrocode}
\ProcessOptions
%</package>
%    \end{macrocode}
% 
% The next measure is to ensure that some {\sTeX} packages are loaded: |omdoc| for the
% statement keys, |modules| since we need module identifiers for referencing. Furthermore,
% we need the |ntheorem| package for presenting statements. For {\latexml}, we also
% initialize the package inclusions, there we do not need |ntheorem|, since the XML does
% not do the presentation.
%    \begin{macrocode}
%<*package>
\RequirePackage{omtext}
\RequirePackage{modules}
\RequirePackage[hyperref]{ntheorem}
\theoremstyle{plain}
%</package>
%<*ltxml>
# -*- CPERL -*-
package LaTeXML::Package::Pool;
use strict;
use LaTeXML::Package;
RequirePackage('omtext');
RequirePackage('modules');
%</ltxml>
%    \end{macrocode}
% Now, we define an auxiliary function that lowercases strings
%    \begin{macrocode}
%<*ltxml>
sub lowcase {my ($string) = @_; $string ? return lc(ToString($string)) : return('')}#$
sub dashed { join('-',map($_->toString,@_));}#$
%</ltxml>
%    \end{macrocode}
% Sometimes it is necessary to fallback to symbol names in order to generate xml:id attributes. For this purpose,
% we define an auxiliary function which ensures the name receives a unique NCName equivalent.\ednote{Hard to be unique here, 
% e.g. the names "foo\_bar" and "foo bar" would receive the same xml:id attributes... of course we can devise a more complex scheme
% for the symbol replacement.}
%    \begin{macrocode}
%<*ltxml>
sub makeNCName {
  my ($name) = @_;
  my $ncname=$name;
  $ncname=~s/\s/_/g;  #Spaces to underscores
  $ncname="_$ncname" if $ncname!~/^(\w|_)/;  #Ensure start with letter or underscore
  ##More to come...
  $ncname;
}
%</ltxml>
%    \end{macrocode}
% The following functions are strictly utility functions that makes our life easier later on
%    \begin{macrocode}
%<*ltxml>
sub simple_wrapper {
  #Deref if array reference
  my @input;
  foreach (@_) {
  if (ref $_ && $_ =~ /ARRAY/ && $_ !~ /LaTeXML/) {
      @input=(@input,@$_);
    } else
      { push (@input,$_); }
  }
  return '' if (!@input);
  @input = map(split(/\s*,\s*/,ToString($_)),@input);
  my $output=join(" ",@input);
  $output=~s/(^ )|[{}]//g; #remove leading space and list separator brackets
  $output||'';
}
sub hash_wrapper{
  #Deref if array reference
  my @input;
  foreach (@_) {
  if (ref $_ && $_ =~ /ARRAY/ && $_ !~ /LaTeXML/) {
      @input=(@input,@$_);
    } else
      { push (@input,$_); }
  }
  return '' if (!@input);
  @input = map(split(/\s*,\s*/,ToString($_)),@input);
  my $output=join(".sym #",@input);
  $output=~s/(^\.sym )|[{}]//g; #remove leading space and list separator brackets
  "#$output"||'';
}
%</ltxml>
%    \end{macrocode}
% 
% \subsection{Statements}\label{sec:impl:statements}
%
% \begin{macro}{\STpresent}
%    \begin{macrocode}
%<*package>
\providecommand\STpresent[1]{#1}
%</package> 
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\define@statement@env}
%    We define a meta-macro that allows us to define several variants of statements. Upon
%    beginning this environment, we first set the |KeyVal| attributes, then we decide
%    whether to print the discourse marker based on the value of the |display| key, then
%    (given the right Options were set), we show the semantic annotations, and finally
%    initialize the environment using the appropriate macro. Upon ending the environment,
%    we just run the respective termination macro.
%    \begin{macrocode}
%<*package>
\def\define@statement@env#1{%
\newenvironment{#1}[1][]{\metasetkeys{omtext}{##1}\sref@target%
\ifx\omtext@display\st@flow\else%
\ifx\omtext@title\@empty\begin{ST#1Env}\else\begin{ST#1Env}[\omtext@title]\fi%
\ifx\sref@id\@empty\else\label{#1.\sref@id}\fi
\csname st@#1@initialize\endcsname\fi
\ifx\sref@id\@empty\sref@label@id{here}\else%
\sref@label@id{\STpresent{\csname ST#1EnvKeyword\endcsname}~\@currentlabel}\fi}
{\csname st@#1@terminate\endcsname\ifx\omtext@display\st@flow\else\end{ST#1Env}\fi}}
%</package>
%    \end{macrocode}
% \end{macro}
%
% \begin{environment}{assertion}
%    \begin{macrocode}
%<*package>
\newenvironment{assertion}[1][]{\metasetkeys{omtext}{#1}\sref@target%
\ifx\omtext@display\st@flow\else%
\ifx\omtext@title\@empty\begin{ST\omtext@type AssEnv}%
\else\begin{ST\omtext@type AssEnv}[\omtext@title]\fi\fi%
\ifx\omtext@type\@empty\sref@label@id{here}\else%
\sref@label@id{\STpresent{\csname ST\omtext@type AssEnvKeyword\endcsname}~\@currentlabel}\fi}
{\ifx\omtext@display\st@flow\else\end{ST\omtext@type AssEnv}\fi}
%</package>
%<*ltxml>
DefEnvironment('{assertion} OptionalKeyVals:omtext',
  "<omdoc:assertion "
  .   "?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')() "
  .   "?&KeyVal(#1,'theory')(theory='&KeyVal(#1,'theory')')() "
  .   "type='&lowcase(&KeyVal(#1,'type'))'>"
  .   "?&KeyVal(#1,'title')(<dc:title>&KeyVal(#1,'title')</dc:title>)()"
 .  "<omdoc:CMP>#body"
  ."</omdoc:assertion>\n");
%</ltxml>
%    \end{macrocode}
% \end{environment}
%
% \begin{macro}{\st@*@kw}
%   We configure the default keywords for the various theorem environments. 
%    \begin{macrocode}
%<*package>
\def\st@theorem@kw{Theorem}
\def\st@lemma@kw{Lemma}
\def\st@proposition@kw{Proposition}
\def\st@corollary@kw{Corollary}
\def\st@conjecture@kw{Conjecture}
\def\st@falseconjecture@kw{Conjecture (false)}
\def\st@postulate@kw{Postulate}
\def\st@obligation@kw{Obligation}
\def\st@assumption@kw{Assumption}
\def\st@observation@kw{Observation}
%    \end{macrocode}
% \end{macro}
% Then we configure the presentation of the theorem environments
%    \begin{macrocode}
\theorembodyfont{\itshape}
\theoremheaderfont{\normalfont\bfseries}
%    \end{macrocode}
% and then we finally define the theorem environments in terms of the statement keywords
% defined above. They are all numbered together with the section counter.
% \begin{environment}{ST*AssEnv}
%    \begin{macrocode}
\newtheorem{STtheoremAssEnv}{\st@theorem@kw}
\newtheorem{STlemmaAssEnv}[STtheoremAssEnv]{\st@lemma@kw}
\newtheorem{STpropositionAssEnv}[STtheoremAssEnv]{\st@proposition@kw}
\newtheorem{STcorollaryAssEnv}[STtheoremAssEnv]{\st@corollary@kw}
\newtheorem{STconjectureAssEnv}[STtheoremAssEnv]{\st@conjecture@kw}
\newtheorem{STfalseconjectureAssEnv}[STtheoremAssEnv]{\st@falseconjecture@kw}
\newtheorem{STpostulateAssEnv}[STtheoremAssEnv]{\st@postulate@kw}
\newtheorem{STobligationAssEnv}[STtheoremAssEnv]{\st@obligation@kw}
\newtheorem{STassumptionAssEnv}[STtheoremAssEnv]{\st@assumption@kw}
\newtheorem{STobservationAssEnv}[STtheoremAssEnv]{\st@observation@kw}
%</package>
%    \end{macrocode}
% \end{environment}
%
% \begin{environment}{example}
%    \begin{macrocode}
%<*package>
\def\st@example@initialize{}\def\st@example@terminate{}
\define@statement@env{example}
\def\st@example@kw{Example}
\theorembodyfont{\upshape}
\newtheorem{STexampleEnv}[STtheoremAssEnv]{\st@example@kw}
%</package>
%<*ltxml>
DefEnvironment('{example} OptionalKeyVals:omtext',
       "<omdoc:example "
       . "?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')() "
       . "?&KeyVal(#1,'for')(for='&hash_wrapper(&KeyVal(#1,'for'))')()>"
       . "?&KeyVal(#1,'title')(<dc:title>&KeyVal(#1,'title')</dc:title>)()"
      . "<omdoc:CMP>#body"
     . "</omdoc:example>\n");
%</ltxml>
%    \end{macrocode}
% \end{environment}
%
% \begin{environment}{axiom}
%    \begin{macrocode}
%<*package>
\def\st@axiom@initialize{}\def\st@axiom@terminate{}
\define@statement@env{axiom}
\def\st@axiom@kw{Axiom}
\theorembodyfont{\upshape}
\newtheorem{STaxiomEnv}[STtheoremAssEnv]{\st@axiom@kw}
%</package>
%<*ltxml>
DefEnvironment('{axiom} OptionalKeyVals:omtext',
  "<omdoc:axiom "
  .   "?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')()>"
  .   "?&KeyVal(#1,'title')(<dc:title>&KeyVal(#1,'title')</dc:title>)()"
 . "<omdoc:CMP>#body"
  . "</omdoc:axiom>\n");
%</ltxml>
%    \end{macrocode}
% \end{environment}
%
% \begin{environment}{symboldec}
%    \begin{macrocode}
%<*package>
\srefaddidkey{symboldec}
\addmetakey{symboldec}{functions}
\addmetakey{symboldec}{role}
\addmetakey*{symboldec}{title}
\addmetakey{symboldec}{name}
\addmetakey{symboldec}{subject}
\addmetakey*{symboldec}{display}
\def\symboldec@type{Symbol}
\newenvironment{symboldec}[1][]{\metasetkeys{symboldec}{#1}\sref@target\st@indeftrue%
\ifx\symboldec@display\st@flow\else{\stDMemph{\symboldec@type} \symboldec@name:}\fi%
\ifx\symboldec@title\@empty~\else~(\stDMemph{\symboldec@title})\par\fi}{}
%</package>
%<*ltxml>
DefEnvironment('{symboldec} OptionalKeyVals:symboldec',
       "<omdoc:symbol "
      .  "?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')"
      .                   "(xml:id='&makeNCName(&KeyVal(#1,'name')).def.sym')"
      .               "name='&KeyVal(#1,'name')'>"
      .  "?&KeyVal(#1,'title')(<dc:title>&KeyVal(#1,'title')</dc:title>)()"
      .  "<dc:description>#body"
      ."</omdoc:symbol>\n");
%</ltxml>
%    \end{macrocode}
% \end{environment}
% 
% \begin{macro}{\symtype}
%    \begin{macrocode} 
%<*package>
\newcommand{\symtype}[2]{Type (#1): $#2$}
%</package>
%<*ltxml>
DefConstructor('\symtype{}{}',
  "<omdoc:type system='#1'><ltx:Math><ltx:XMath>#2</ltx:XMath></ltx:Math></omdoc:type>");
%</ltxml>
%    \end{macrocode}
% \end{macro}
%
% \begin{environment}{definition}
%   The |definition| environment itself is quite similar to the other's but we need to set
%   the |\st@indef| switch to suppress warnings from |\st@def@target|.
%    \begin{macrocode}
%<*package>
\newif\ifst@indef\st@indeffalse
\newenvironment{definition}[1][]{\metasetkeys{omtext}{#1}\sref@target\st@indeftrue%
\ifx\omtext@display\st@flow\else%
\ifx\omtext@title\@empty\begin{STdefinitionEnv}\else\begin{STdefinitionEnv}[\omtext@title]\fi\fi%
\ifx\sref@id\@empty\sref@label@id{here}\else%
\sref@label@id{\STpresent{\csname STdefinitionEnvKeyword\endcsname}~\@currentlabel}\fi}
{\ifx\omtext@display\st@flow\else\end{STdefinitionEnv}\fi}
\def\st@definition@kw{Definition}
\theorembodyfont{\upshape}
\newtheorem{STdefinitionEnv}[STtheoremAssEnv]{\st@definition@kw}
%</package>
%<*ltxml>
sub definitionBody {
    my ($doc, $keyvals, %props) = @_;
    my $for = $keyvals->getValue('for') if $keyvals;
    my $type = $keyvals->getValue('type') if $keyvals;
   my %for_attr=();
    if (ToString($for)) {
      $for = ToString($for);
      $for =~ s/^{(.+)}$/$1/eg;
      foreach (split(/,\s*/,$for)) {
        $for_attr{$_}=1;
     }}
   if ($props{theory}) {
    my @symbols = @{$props{defs} || []};
    foreach my $symb(@symbols) {
      next if $for_attr{$symb};
      $for_attr{$symb}=1;
      $doc->insertElement('omdoc:symbol', undef, (name=>$symb, "xml:id"=>makeNCName("$symb.def.sym")));
    }
   }
    my %attrs = ();
    $for = join(" ",(keys %for_attr));
    $attrs{'for'} = $for if $for;
    my $id = $keyvals->getValue('id') if $keyvals;
    $attrs{'xml:id'} = $id if $id;
    $attrs{'type'} = $type if $type;
    if ($props{theory}) {
      $doc->openElement('omdoc:definition', %attrs);
    } else {
      $attrs{'type'}='definition';
      $doc->openElement('omdoc:omtext', %attrs);
    }
    my $title = $keyvals->getValue('title') if $keyvals;
    if ($title) {
      $doc->openElement('omdoc:metadata');
      $doc->openElement('dc:title');
      $doc->absorb($title);
      $doc->closeElement('dc:title');}
    $doc->openElement('omdoc:CMP');
   $doc->absorb($props{body}) if $props{body};
   $doc->maybeCloseElement('omdoc:CMP');
    if ($props{theory}) {
      $doc->closeElement('omdoc:definition');
    } else {
      $doc->closeElement('omdoc:omtext');
    }
    return; }
DefEnvironment('{definition} OptionalKeyVals:omtext', sub{definitionBody(@_)},
  afterDigestBegin=>sub {
    my ($stomach, $whatsit) = @_;
    my @symbols = ();
    $whatsit->setProperty(theory=>LookupValue('current_module'));
    $whatsit->setProperty(defs=>\@symbols);
    AssignValue('defs', \@symbols);  return; },
  afterDigest => sub { AssignValue('defs', undef); return; });#$
%</ltxml>
%    \end{macrocode}
% \end{environment}
%
% \begin{environment}{notation}
%   We initialize the |\def\st@notation@initialize{}| here, and extend it with
%   functionality below. 
%    \begin{macrocode}
%<*package>
\def\notemph#1{{\bf{#1}}}
\def\st@notation@terminate{}
\def\st@notation@initialize{}
\define@statement@env{notation}
\def\st@notation@kw{Notation}
\theorembodyfont{\upshape}
\newtheorem{STnotationEnv}[STtheoremAssEnv]{\st@notation@kw}
%</package>
%<*ltxml>
DefEnvironment('{notation} OptionalKeyVals:omtext',
  "<omdoc:definition " 
 .   "?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id').not')()"
 .   "?&KeyVal(#1,'for')(for='&simple_wrapper(&KeyVal(#1,'for'))')()>"
 . "?&KeyVal(#1,'title')(<dc:title>&KeyVal(#1,'title')</dc:title>)()"
 . "<omdoc:CMP>#body"
  . "</omdoc:definition>\n");
DefConstructor('\notatiendum OptionalKeyVals:notation {}',
              "<ltx:text class='notatiendum'>#2</ltx:text>");
%</ltxml>
%    \end{macrocode}
% \end{environment}
%
% \begin{macro}{\st@def@target}
%   the next macro is a variant of the |\sref@target| macro provided by the |sref| package
%   specialized for the use in the |\definiendum|, |\defi|, |\defii|, and |\defiii|
%   macros. |\st@def@target{|\meta{opt}|}{|\meta{name}|}| makes a target with label
%   |sref@|\meta{opt}|@|\meta{modulename}|@target|, if \meta{opt} is non-empty, else with
%   the label |sref@|\meta{name}|@|\meta{modulename}|@target|. Also it generates the
%   necessary warnings for a definiendum-like macro.
%    \begin{macrocode}
%<*package>
\def\st@def@target#1#2{\def\@test{#1}%
\ifst@indef% if we are in a definition or such
\ifx\omtext@theory\@empty% if there is no theory attribute
\@ifundefined{mod@id}% if we are not in a module
{\PackageWarning{statements}{definiendum in unidentified module\MessageBreak
\protect\definiendum, \protect\defi,
\protect\defii, \protect\defiii\MessageBreak
can only be referenced when called in a module with id key}}%
{\ifx\@test\@empty%
\expandafter\sref@target@ifh{sref@#2@\mod@id @target}{}\else%
\expandafter\sref@target@ifh{sref@#1@\mod@id @target}{}\fi}%
\else\expandafter\sref@target@ifh{sref@#1@\omtext@theory @target}{}\fi%
\else\PackageError{statements}%
{definiendum outside definition context\MessageBreak
\protect\definiendum, \protect\defi, 
\protect\defii, \protect\defiii\MessageBreak
do not make sense semantically outside a definition.\MessageBreak
Consider wrapping the defining phrase in a \protect\inlinedef}%
\fi}
%</package>
%    \end{macrocode}
% \end{macro}
%
%   The |\definiendum| and |\notatiendum| macros are very simple.
%
% \begin{macro}{\@termdef}
%   This macro is experimental, it is supposed to be invoked in |\definiendum| to define a
%   macro with the definiendum text, so that can be re-used later in term assignments (see
%   the |modules| package). But in the current context, where we rely on {\TeX} groupings
%   for visibility, this does not work, since the invocations of |\definiendum| are in
%   |definition| environments and thus one group level too low. Keeping this for future
%   reference.
%    \begin{macrocode}
%<*package>
\newcommand\@termdef[2][]{\def\@test{#1}%
\@ifundefined{mod@id}{}{\ifx\@test\@empty\def\@@name{#2}\else\def\@@name{#1}\fi%
\termdef{\mod@id @\@@name}{#2}}}
%</package>
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\definiendum}
%    \begin{macrocode}
%<*package>
%\newcommand\definiendum[2][]{\st@def@target{#1}{#2}\@termdef[#1]{#2}\defemph{#2}}
\newcommand\definiendum[2][]{\st@def@target{#1}{#2}\defemph{#2}}
%</package>
%<*ltxml>
DefConstructor('\definiendum [] {}',
       "<omdoc:term role='definiendum' name='#name' cd='#theory'>#2</omdoc:term>",
       afterDigest => sub {
 my ($stomach, $whatsit) = @_;
 my $addr = LookupValue('defs');
 my $name = $whatsit->getArg(1);
 $name = $whatsit->getArg(2) unless $name;
 $whatsit->setProperty(name=>$name->toString);
 push(@$addr, $name->toString) if ($addr and $name);
 $whatsit->setProperty(theory=>LookupValue('current_module'));
 return; });#$
%</ltxml>
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\notatiendum}
%   the |notatiendum| macro also needs to be visible in the |notation| and |definition|
%   environments
%    \begin{macrocode}
%<*package>
\newcommand{\notatiendum}[2][]{\notemph{#2}}
%</package>
%    \end{macrocode}
% \end{macro}
%
% We expand the {\latexml} bindings for |\defi|, |\defii| and |\defiii| into two
% instances one will be used for the definition and the other for indexing.
%
% \begin{macro}{\defi}
%    \begin{macrocode}
%<*package>
\newcommand{\defi}[2][]{\definiendum[#1]{#2}\omdoc@index[#1]{#2}}
%</package>
%<*ltxml>
DefConstructor('\defi[]{}',
       "<omdoc:idx>"
      .  "<omdoc:idt>"
      .     "<omdoc:term role='definiendum' name='?#1(#1)(#2)' cd='#theory'>#2</omdoc:term>"
      .  "</omdoc:idt>"
      .  "<omdoc:ide index='default'><omdoc:idp>#2</omdoc:idp></omdoc:ide>"
      ."</omdoc:idx>",
       afterDigest => sub {
 my ($stomach, $whatsit) = @_;
 my $addr = LookupValue('defs');
 my $name = $whatsit->getArg(1);
 $name = $whatsit->getArg(2) unless $name;
 push(@$addr, $name->toString) if ($addr and $name);
 $whatsit->setProperty(theory=>LookupValue('current_module'));#$
 return; },
       alias=>'\defi');
%</ltxml>
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\adefi}
%    \begin{macrocode}
%<*package>
\newcommand{\adefi}[3][]{\def\@test{#1}%
\ifx\@test\@empty\definiendum[#3]{#2}%
\else\definiendum[#1]{#2}\omdoc@index[#1]{#3}\fi}
%</package>
%<*ltxml>
DefConstructor('\adefi[]{}{}',
       "<omdoc:idx>"
      .  "<omdoc:idt>"
      .     "<omdoc:term role='definiendum' name='?#1(#1)(#3)' cd='#theory'>#2</omdoc:term>"
      .  "</omdoc:idt>"
      .  "<omdoc:ide index='default'><omdoc:idp>#3</omdoc:idp></omdoc:ide>"
      ."</omdoc:idx>",
       afterDigest => sub {
 my ($stomach, $whatsit) = @_;
 my $addr = LookupValue('defs');
 my $name = $whatsit->getArg(1);
 $name = $whatsit->getArg(3) unless $name;
 push(@$addr, $name->toString) if ($addr and $name);
 $whatsit->setProperty(theory=>LookupValue('current_module'));#$
 return; },
      alias=>'\adefi');
%</ltxml>
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\defii}
%    \begin{macrocode}
%<*package>
\newcommand{\defii}[3][]{\st@def@target{#1}{#2-#3}\defemph{#2 #3}\@twin[#1]{#2}{#3}}
%</package>
%<*ltxml>
DefConstructor('\defii[]{}{}',
       "<omdoc:idx>"
      .  "<omdoc:idt>"
      .    "<omdoc:term role='definiendum' name='?#1(#1)(&dashed(#2,#3))' cd='#theory'>"
      .      "#2 #3"
      .    "</omdoc:term>"
      .  "</omdoc:idt>"
      .  "<omdoc:ide index='default'>"
      .    "<omdoc:idp>#2</omdoc:idp>"
      .    "<omdoc:idp>#3</omdoc:idp>"
      .  "</omdoc:ide>"
      ."</omdoc:idx>",
       afterDigest => sub {
 my ($stomach, $whatsit) = @_;
my $addr = LookupValue('defs');
 my $name = $whatsit->getArg(1);
 $name = $name->toString if $name;
 $name = $whatsit->getArg(2)->toString.'-'.$whatsit->getArg(3)->toString unless $name;
 push(@$addr, $name) if ($addr and $name);
 $whatsit->setProperty(theory=>LookupValue('current_module'));
 return; },
       alias=>'\defii');#$
%</ltxml>
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\adefii}
%    \begin{macrocode}
%<*package>
\newcommand{\adefii}[4][]{\def\@test{#1}%
\ifx\@test\@empty\definiendum[#3-#4]{#2}%
\else\definiendum[#1]{#2}\@twin[#1]{#3}{#4}\fi}
%</package>
%<*ltxml>
DefConstructor('\adefii[]{}{}{}',
       "<omdoc:idx>"
      .  "<omdoc:idt>"
      .    "<omdoc:term role='definiendum' name='?#1(#1)(&dashed(#3,#4))' cd='#theory'>"
      .       "#2"
      .    "</omdoc:term>"
      .  "</omdoc:idt>"
      .  "<omdoc:ide index='default'>"
      .    "<omdoc:idp>#3</omdoc:idp>"
      .    "<omdoc:idp>#4</omdoc:idp>"
      .  "</omdoc:ide>"
      ."</omdoc:idx>",
       afterDigest => sub {
 my ($stomach, $whatsit) = @_;
 my $addr = LookupValue('defs');
 my $name = $whatsit->getArg(1);
 $name = $name->toString if $name;
 $name = $whatsit->getArg(3)->toString.'-'.$whatsit->getArg(4)->toString unless $name;
 push(@$addr, $name) if ($addr and $name);
 $whatsit->setProperty(theory=>LookupValue('current_module'));
 return; },
       alias=>'\defii');#$
%</ltxml>
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\defiii}
%    \begin{macrocode}
%<*package>
\newcommand{\defiii}[4][]{\st@def@target{#1}{#2-#3-#4}\defemph{#2 #3 #4}\@atwin[#1]{#2}{#3}{#4}}
%</package>
%<*ltxml>
DefConstructor('\defiii[]{}{}{}',
       "<omdoc:idx>"
       . "<omdoc:idt>"
         . "<omdoc:term role='definiendum' cd='#theory' name='?#1(#1)(&dashed(#2,#3,#4))'>#2 #3 #4</omdoc:term>"
       . "</omdoc:idt>"
       . "<omdoc:ide index='default'>"
         . "<omdoc:idp>#2</omdoc:idp>"
         . "<omdoc:idp>#3</omdoc:idp>"
         . "<omdoc:idp>#4</omdoc:idp>"
       . "</omdoc:ide>"
     . "</omdoc:idx>",
       afterDigest => sub {
 my ($stomach, $whatsit) = @_;
 my $addr = LookupValue('defs');
 my $name = $whatsit->getArg(1);
 $name = $name->toString if $name;
 $name = $whatsit->getArg(2)->toString.'-'.$whatsit->getArg(3)->toString.'-'.$whatsit->getArg(4)->toString unless $name;
 push(@$addr, $name) if ($addr and $name);
 $whatsit->setProperty(theory=>LookupValue('current_module'));
 return; },
       alias=>'\defiii');
%</ltxml>
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\adefiii}
%    \begin{macrocode}
%<*package>
\newcommand{\adefiii}[5][]{\def\@test{#1}%
\ifx\@test\@empty\definiendum[#3-#4-#5]{#2}%
\else\definiendum[#1]{#2}\@atwin[#1]{#3}{#4}{#5}\fi}
%</package>
%<*ltxml>
DefConstructor('\adefiii[]{}{}{}{}',
       "<omdoc:idx>"
       . "<omdoc:idt>"
       . "<omdoc:term role='definiendum' cd='#theory' name='?#1(#1)(&dashed(#3,#4,#5))'>#2</omdoc:term>"
       . "</omdoc:idt>"
       . "<omdoc:ide index='default'>"
         . "<omdoc:idp>#3</omdoc:idp>"
         . "<omdoc:idp>#4</omdoc:idp>"
         . "<omdoc:idp>#5</omdoc:idp>"
       . "</omdoc:ide>"
     . "</omdoc:idx>",
       afterDigest => sub {
 my ($stomach, $whatsit) = @_;
 my $addr = LookupValue('defs');
 my $name = $whatsit->getArg(1);
 $name = $name->toString if $name;
 $name = $whatsit->getArg(3)->toString.'-'.$whatsit->getArg(4)->toString.'-'.$whatsit->getArg(5)->toString unless $name;
 push(@$addr, $name) if ($addr and $name);
 $whatsit->setProperty(theory=>LookupValue('current_module'));
 return; },
       alias=>'\defiii');
%</ltxml>
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\inlineex}
%    \begin{macrocode}
%<*package>
\newcommand{\inlineex}[2][]{\metasetkeys{omtext}{#1}\sref@target\sref@label@id{here}#2}
%</package>
%<*ltxml>
DefConstructor('\inlineex OptionalKeyVals:omtext {}',
              "<ltx:text class='example'>#2</ltx:text>");
%</ltxml>
%    \end{macrocode}
% \end{macro}
% \begin{macro}{\inlinedef}
%    \begin{macrocode}
%<*package>
\newcommand{\inlinedef}[2][]{\metasetkeys{omtext}{#1}\sref@target\sref@label@id{here}\st@indeftrue #2}
%</package>
%<*ltxml>
DefConstructor('\inlinedef OptionalKeyVals:omtext {}', sub {
 my ($document, $keyvals, $body, %props) = @_;
 my $for = $keyvals->getValue('for') if $keyvals;
 my %for_attr=();
 if (ToString($for)) {
   $for = ToString($for);
   $for =~ s/^{(.+)}$/$1/eg;
   foreach (split(/,\s*/,$for)) {
     $for_attr{$_}=1;
   }}
 my @symbols = @{$props{defs} || []};
 #Prepare for symbol insertion -insert before the parent of the closest ancestor CMP element
  my $original_node = $document->getNode;
 my $xc = XML::LibXML::XPathContext->new( $original_node );
 $xc->registerNs('omdoc', 'http://omdoc.org/ns');
 my ($statement_ancestor) = $xc->findnodes('./ancestor::omdoc:CMP/..');
 foreach my $symb(@symbols) {
   next if $for_attr{$symb};
   $for_attr{$symb}=1;
   my $symbolnode = XML::LibXML::Element->new('symbol');
   $symbolnode->setAttribute(name=>$symb);
   $symbolnode->setAttribute("xml:id"=>makeNCName("$symb.def.sym"));
   $statement_ancestor->parentNode->insertBefore($symbolnode,$statement_ancestor);
 }
 #Restore the insertion point
 $document->setNode($original_node);
 my %attrs = ();
 $for = join(" ",(keys %for_attr));
 $attrs{'for'} = $for if $for;
 my $id = $keyvals->getValue('id') if $keyvals;
 $attrs{'xml:id'} = $id if $id;
$attrs{'class'} = 'inlinedef';
 $document->openElement('ltx:text',%attrs);
 $document->absorb($body);
$document->closeElement('ltx:text'); },
 #Prepare 'defs' hooks for \defi and \definiendum symbol names
  beforeDigest=>sub {
    my @symbols = ();
    AssignValue('defs', \@symbols); return; },
 #Adopt collected names as 'defs' property, remove hooks
  afterDigest=>sub {
    my ($stomach, $whatsit) = @_;
    my $defsref = LookupValue('defs');
    my @defs = @$defsref;
    $whatsit->setProperty('defs',\@defs);
    AssignValue('defs',undef);
 return; });
%</ltxml>
%    \end{macrocode}
% \end{macro}
% 
% \subsection{Cross-Referencing Symbols and Concepts}\label{sec:impl:crossref}
%
% \begin{macro}{\termref@set}
%   The |term| macro uses the |cd| and |name| keys for hyperlinking to create hyper-refs,
%   if the |hyperref| package is loaded: We first see if the |cd| key was given, if not we
%   define it as the local module identifier.
%    \begin{macrocode}
%<*package>
\addmetakey[\mod@id]{termref}{cd}
\addmetakey{termref}{cdbase}
\addmetakey{termref}{name}
\addmetakey{termref}{role}
\def\termref@set#1#2{\def\termref@name{#2}\metasetkeys{termref}{#1}}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\termref}
%    \begin{macrocode}
\newcommand{\termref}[2][]{\metasetkeys{termref}{#1}\st@termref{#2}}
%</package>
%<*ltxml>
DefConstructor('\termref OptionalKeyVals:termref {}',
               "<omdoc:term "
              .  "?&KeyVal(#1,'cdbase')(cdbase='&KeyVal(#1,'cdbase')')() "
             .  "cd='?&KeyVal(#1,'cd')(&KeyVal(#1,'cd'))(#module)' "
              .  "name='&KeyVal(#1,'name')'>"
              .  "#2"
              ."</omdoc:term>",
	      afterDigest=>sub{$_[1]->setProperty(module=>LookupValue('current_module'))});
%</ltxml>%$
%    \end{macrocode}
% \end{macro}
% The next macro is where the actual work is done. 
% \begin{macro}{\st@termref}
%   If the |cdbase| is given, then we make a hyper-reference, otherwise we punt to
%   |\mod@termref|, which can deal with the case where the cdbase is given by the imported
%   cd.
%    \begin{macrocode}
%<*package>
\def\st@termref#1{\ifx\termref@name\@empty\def\termref@name{#1}\fi%
\ifx\termref@cdbase\@empty\mod@termref\termref@cd\termref@name{#1}%
\else\sref@href@ifh\termref@cdbase{#1}\fi}
%</package>
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\tref*}
%    \begin{macrocode}
%<ltxml>RawTeX('
%<*package|ltxml>
\newcommand\atrefi[3][]{\def\@test{#1}\ifx\@test\@empty\termref[name=#3]{#2}\else\termref[cd=#1,name=#3]{#2}\fi}
\newcommand\atrefii[4][]{\atrefi[#1]{#2}{#3-#4}}
\newcommand\atrefiii[5][]{\atrefi[#1]{#2}{#3-#4-#5}}
%    \end{macrocode}
% \end{macro}
%
% \begin{macro}{\tref*}
%    \begin{macrocode}
\newcommand{\trefi}[2][]{\atrefi[#1]{#2}{#2}}
\newcommand{\trefii}[3][]{\atrefi[#1]{#2 #3}{#2-#3}}
\newcommand{\trefiii}[4][]{\atrefi[#1]{#2 #3 #4}{#2-#3-#4}}
%</package|ltxml>
%<ltxml>');
%    \end{macrocode}
% \end{macro}
%
% Now we care about the configuration switches, they are set to sensible values, if they
% are not defined already. These are just configuration parameters, which should not
% appear in documents, therefore we do not provide {\latexml} bindings for them.
% \begin{macro}{\*emph}
%    \begin{macrocode}
%<*package>
\providecommand{\termemph}[1]{#1}
\providecommand{\defemph}[1]{{\textbf{#1}}}
\providecommand{\stDMemph}[1]{{\textbf{#1}}}
%</package>
%    \end{macrocode}
% \end{macro}
% 
% \begin{macro}{\symref}
%   The |\symref| macros is quite simple, since we have done all the heavy lifting in the
%   |modules| package: we simply apply |\mod@symref@|\meta{arg1} to
%   \meta{arg2}.
%    \begin{macrocode}
%<*package>
\newcommand{\symref}[2]{\@nameuse{mod@symref@#1}{#2}}
%</package>
%<*ltxml>
DefConstructor('\symref{}{}',
               "<omdoc:term cd='&LookupValue('symdef.#1.cd')' name='&LookupValue('symdef.#1.name')'>"
              .  "#2"
              ."</omdoc:term>");
%</ltxml>
%    \end{macrocode}
% \end{macro}
%
% \subsection{Providing IDs for {\omdoc} Elements}\label{sec:impl:ids}
%
% To provide default identifiers, we tag all {\omdoc}
% elements that allow |xml:id| attributes by executing the |numberIt| procedure from |omdoc.sty.ltxml|.
% 
%    \begin{macrocode}
%<*ltxml>
Tag('omdoc:assertion',afterOpen=>\&numberIt,afterClose=>\&locateIt);
Tag('omdoc:definition',afterOpen=>\&numberIt,afterClose=>\&locateIt);
Tag('omdoc:example',afterOpen=>\&numberIt,afterClose=>\&locateIt);
Tag('omdoc:requation',afterOpen=>\&numberIt,afterClose=>\&locateIt);
Tag('omdoc:axiom',afterOpen=>\&numberIt,afterClose=>\&locateIt);
Tag('omdoc:symbol',afterOpen=>\&numberIt,afterClose=>\&locateIt);
Tag('omdoc:type',afterOpen=>\&numberIt,afterClose=>\&locateIt);
Tag('omdoc:term',afterOpen=>\&numberIt,afterClose=>\&locateIt);
%</ltxml>
%    \end{macrocode}
%
% \subsection{Deprecated Functionality}\label{sec:deprecated}
%
% In this section we centralize old interfaces that are only partially supported any
% more. 
% \begin{macro}{\*def*}
%    \begin{macrocode}
%<ltxml>RawTeX('
%<*package|ltxml>
\newcommand\defin[2][]{\defi[#1]{#2}%
\PackageWarning{statements}{\protect\defin\space is deprecated, use \protect\defi\space instead}}
\newcommand\twindef[3][]{\defii[#1]{#2}{#3}%
\PackageWarning{statements}{\protect\twindef\space is deprecated, use \protect\defii\space instead}}
\newcommand\atwindef[4][]{\defiii[#1]{#2}{#3}{#4}%
\PackageWarning{statements}{\protect\atwindef\space is deprecated, use \protect\defiii\space instead}}
\newcommand\definalt[3][]{\adefi[#1]{#2}{#3}%
\PackageWarning{statements}{\protect\definalt\space is deprecated, use \protect\adefi\space instead}}
\newcommand\twindefalt[4][]{\adefii[#1]{#2}{#3}{#4}%
\PackageWarning{statements}{\protect\twindefalt\space is deprecated, use \protect\adefii\space instead}}
\newcommand\atwindefalt[5][]{\adefiii[#1]{#2}{#3}{#4}{#5}%
\PackageWarning{statements}{\protect\atwindefalt\space is deprecated, use \protect\adefiii\space instead}}
%    \end{macrocode}
% \end{macro}
% 
% \begin{macro}{\*def*}
%    \begin{macrocode}
\newcommand\twinref[3][]{\trefii[#1]{#2}{#3}%
\PackageWarning{statements}{\protect\twinref\space is deprecated, use \protect\trefii\space instead}}
\newcommand\atwinref[4][]{\atrefiii[#1]{#2}{#3}{#4}%
\PackageWarning{statements}{\protect\atwindef\space is deprecated, use \protect\trefiii\space instead}}
%</package|ltxml>
%<ltxml>');
%    \end{macrocode}
% \end{macro}
% 
% \subsection{Finale}
%
% Finally, we need to terminate the file with a success mark for perl.
%    \begin{macrocode}
%<ltxml>1;
%    \end{macrocode}
%
% \Finale
%
\endinput
% \iffalse
% LocalWords:  GPL structuresharing STR dtx keyval env envfalse idfalse idtrue
% LocalWords:  displayfalse envtrue displaytrue forfalse typefalse titlefalse
% LocalWords:   continuesfalse fortrue fromtrue typetrue titletrue CPERL omdoc
% LocalWords:   continuestrue symboldec omtext RequirePackage lowcase lc ToString
% LocalWords:  foreach hyperref href hlink DefEnvironment OptionalKeyVals ne
% LocalWords:  KeyVal xml CMP simpleDef PatternDef DefEnvironment PatternRule
% LocalWords:  requation PatternCMP RecDef DefConstructor keyvals defs psymbols
% LocalWords:  openElement symb closeElement ffor getValue attrs metadata undef
% LocalWords:  afterDigestBegin setProperty AssignValue afterDigest definiendum
% LocalWords:  cd addr LookupValue getArg toString idx idt definiendum ide idp
% LocalWords:  DefMacro args unlist inlinedef uri pdf afterOpen numberIt texttt
% LocalWords:  iffalse consymb ntheorem textbackslash symref def scsys sc sc kw
% LocalWords:  mathml openmath latexml activemath fileversion maketitle stex
% LocalWords:  setcounter tocdepth tableofcontents newpage sproofs ulsmf08 sref
% LocalWords:  MaySch eltte09 twintoo sref subsubsection exfig vspace vspace
% LocalWords:  noindent renewtheorem hline textbf textbf footnotesize ple peano
% LocalWords:  STaxiomEnv symdef medskip succ mathbb ldots stepcounter ednote
% LocalWords:  STtheoremAssEnv stepcounter STtheoremAssEnv stepcounter defin
% LocalWords:  STtheoremAssEnv notatiendum defin smomdl biblatex twindef cdbase
% LocalWords:  twindef atwindef atwindef adjectivized varaiants twindefalt cseq
% LocalWords:  twindefalt atwindefalt atwindefalt csymbol definalt termref emph
% LocalWords:  termref compactdesc KohAmb smmssl twinref atwinref newpart impl
% LocalWords:  termdef defemph defemph renewcommand termemph termenph stDMemph
% LocalWords:  stDMemph STpresent STpresent makeatletter STlemmaAssEnv textsf
% LocalWords:  STpropositionAssEnv STcorollaryAssEnv STconjectureAssEnv langle
% LocalWords:  STfalseconjectureAssEnv STpostulateAssEnv STobligationAssEnv foo
% LocalWords:  STassumptionAssEnv STobservationAssEnv STexampleEnv textsf ltxml
% LocalWords:  STdefinitionEnv STnotationEnv printbibliography langle ncname
% LocalWords:  theoremstyle sym newenvironment ifx csname endcsname
% LocalWords:  currentlabel theorembodyfont itshape theoremheaderfont bfseries
% LocalWords:  normalfont newtheorem upshape srefaddidkey 
% LocalWords:  newcommand indef newif ifst indeffalse indeftrue attr whatsit
% LocalWords:  STdefinitionEnvKeyword notemph modulename ifundefined atwin
% LocalWords:  expandafter providecommand nameuse doctex ctancite funval

%%% Local Variables: 
%%% mode: doctex
%%% TeX-master: t
%%% End: 
% \fi
% LocalWords:  funsymbs findnodes symbolnode defsref