summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/stex/statements/statements.dtx
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/source/latex/stex/statements/statements.dtx')
-rw-r--r--Master/texmf-dist/source/latex/stex/statements/statements.dtx1312
1 files changed, 1312 insertions, 0 deletions
diff --git a/Master/texmf-dist/source/latex/stex/statements/statements.dtx b/Master/texmf-dist/source/latex/stex/statements/statements.dtx
new file mode 100644
index 00000000000..6619bc73714
--- /dev/null
+++ b/Master/texmf-dist/source/latex/stex/statements/statements.dtx
@@ -0,0 +1,1312 @@
+% \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}[2010/06/25 v1.0 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 1502 2010-07-20 08:17:00Z kohlhase $
+\svnKeyword $HeadURL: https://svn.kwarc.info/repos/stex/trunk/sty/statements/statements.dtx $
+\makeindex
+\floatstyle{boxed}
+\newfloat{exfig}{thp}{lop}
+\floatname{exfig}{Example}
+\begin{document}\DocInput{statements.dtx}\end{document}
+%</driver>
+% \fi
+%
+% \CheckSum{433}
+%
+% \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}}}
+%
+% \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:statements}
+%
+% 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{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=Constants]
+% 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}\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 takes two arguments. The first one is the system name
+% of the symbol defined (for reference via |\term|), the second one is the text that is to
+% be emphasized in the presentation. Note that the |\definiendum| macro can only be used
+% inside the |definition| environment. 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}.
+%
+%\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}|\defin{|\meta{word}|}| macro combines the functionality of the
+% |\definiendum| macro with index markup from the |omdoc|
+% package~\ctancite{Kohlhase:smomdl}: use |\defin[|\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{\twindef}|\twindef| and \DescribeMacro{\atwindef}|\atwindef| for
+% (adjectivized) two-word compounds. Finally, the varaiants
+% \DescribeMacro{\twindefalt}|\twindefalt| and \DescribeMacro{\atwindefalt}|\atwindefalt|
+% 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}
+%
+% \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.
+%
+% \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.
+%
+% \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
+% \meta{text} with (if the |hyperref| package is loaded) a hyperlink to the definition in
+% module \meta{cd} that defines the concept \meta{name}, i.e. that contains
+% |\definiendum[|\meta{name}|]{|\meta{something}|}|.
+%
+% Just as the |\definiendum| macro has the variants |\twindef| and |\atwindef| for
+% composita, the |\termref| has variants |\twinref| and |\atwinref| that take two and
+% three arguments for the parts of the compositum. Generally, concepts that are marked up
+% by |\definiendum{|\meta{name}|}| or |\defin|{|\meta{name}|} in the definition are
+% referenced by |\termref|{|\meta{name}|}, concepts defined via
+% |\twindef{|\meta{first}|}{|\meta{second}|}| with
+% |\twinref{|\meta{first}|}{|\meta{second}|}| and analogously for |\atwindef| and
+% |\atwinref|.
+%
+% 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}\label{sec:user:rest}
+%
+% \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
+% |\termin|, 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}
+%
+% \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.
+%
+% 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*{\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 {
+ my @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{
+ my @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>
+\def\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][]{\omdsetkeys{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][]{\omdsetkeys{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>
+DefCMPEnvironment('{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><omdoc:p>#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>
+DefCMPEnvironment('{example} OptionalKeyVals:omtext',
+ "<omdoc:example "
+ . "?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')() "
+ . "?&KeyVal(#1,'for')(for='&hash_wrapper(&KeyVal(#1,'for'))')()>"
+ . "<omdoc:CMP><omdoc:p>#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>
+DefCMPEnvironment('{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><omdoc:p>#body"
+ . "</omdoc:axiom>\n");
+%</ltxml>
+% \end{macrocode}
+% \end{environment}
+%
+% \begin{environment}{symboldec}
+% \begin{macrocode}
+%<*package>
+\srefaddidkey{symboldec}
+\omdaddkey{symboldec}{functions}
+\omdaddkey{symboldec}{role}
+\omdaddkey{symboldec}{title}
+\omdaddkey{symboldec}{name}
+\omdaddkey{symboldec}{display}
+\def\symboldec@type{Symbol}
+\newenvironment{symboldec}[1][]{\omdsetkeys{symboldec}{#1}\sref@target
+\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')'>"
+ . "<dc:description>#body</dc:description>"
+ ."</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'>#2</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][]{\omdsetkeys{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;
+ }}
+ 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;
+ $doc->openElement('omdoc:definition', %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->openElement('omdoc:p');
+ $doc->absorb($props{body}) if $props{body};
+ $doc->maybeCloseElement('omdoc:p');
+ $doc->maybeCloseElement('omdoc:CMP');
+ $doc->closeElement('omdoc:definition');
+ return; }
+DefCMPEnvironment('{definition} OptionalKeyVals:omtext', sub{definitionBody(@_)},
+ afterDigestBegin=>sub {
+ my ($stomach, $whatsit) = @_;
+ my @symbols = ();
+ $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>
+DefCMPEnvironment('{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><omdoc:p>#body"
+ . "</omdoc:definition>\n");
+DefConstructor('\notatiendum OptionalKeyVals:notation {}',
+ "<omdoc:phrase type='notation'>#2</omdoc:phrase>");
+%</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|, |\defin|, |\twindef|, and |\atwindef|
+% 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}%
+\@ifundefined{mod@id}%
+{\PackageError{statements}{definiendum in unidentified module}%
+{\protect\definiendum, \protect\defin,
+\protect\twindef, \protect\atwindef\MessageBreak
+may only be called in a module with id key}}%
+{\ifst@indef\else\PackageWarning{statements}
+ {definiendum outside definition context\MessageBreak
+\protect\definiendum, \protect\defin,
+\protect\twindef, \protect\atwindef\MessageBreak
+do not make sense semantically outside a definition.\MessageBreak
+Consider wrapping the defining phrase in a \protect\inlinedef}\fi
+\ifx\@test\@empty%
+\expandafter\sref@target@ifh{sref@#2@\mod@id @target}{}\else%
+\expandafter\sref@target@ifh{sref@#1@\mod@id @target}{}\fi}}
+%</package>
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\definiendum}
+% The |\definiendum| and |\notatiendum| macros are very simple, but instead of defining
+% them directly, we guard in the |\st@definition@initialize| macro so that they are
+% local to the |definition| environment.
+% \begin{macrocode}
+%<*package>
+\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 |\defin|, |\twindef| and |\atwindef| into two
+% instances one will be used for the definition and the other for indexing.
+%
+% \begin{macro}{\defin}
+% \begin{macrocode}
+%<*package>
+\newcommand{\defin}[2][]{\definiendum[#1]{#2}\omdoc@index[#1]{#2}}
+%</package>
+%<*ltxml>
+DefConstructor('\defin[]{}',
+ "<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=>'\defin');
+%</ltxml>
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\definalt}
+% \begin{macrocode}
+%<*package>
+\newcommand{\definalt}[3][]{\definiendum[#1]{#2}\omdoc@index[#1]{#3}}
+%</package>
+%<*ltxml>
+DefConstructor('\definalt[]{}{}',
+ "<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=>'\definalt');
+%</ltxml>
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\twindef}
+% \begin{macrocode}
+%<*package>
+\newcommand{\twindef}[3][]{\st@def@target{#1}{#2-#3}\defemph{#2 #3}\@twin[#1]{#2}{#3}}
+%</package>
+%<*ltxml>
+DefConstructor('\twindef[]{}{}',
+ "<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=>'\twindef');#$
+%</ltxml>
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\twindefalt}
+% \begin{macrocode}
+%<*package>
+\newcommand{\twindefalt}[4][]{\definiendum[#1]{#2}\@twin[#1]{#3}{#4}}
+%</package>
+%<*ltxml>
+DefConstructor('\twindefalt[]{}{}{}',
+ "<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=>'\twindef');#$
+%</ltxml>
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\atwindef}
+% \begin{macrocode}
+%<*package>
+\newcommand{\atwindef}[4][]{\st@def@target{#1}{#2-#3-#4}\defemph{#2 #3 #4}\@atwin[#1]{#2}{#3}{#4}}
+%</package>
+%<*ltxml>
+DefConstructor('\atwindef[]{}{}{}',
+ "<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=>'\atwindef');
+%</ltxml>
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\atwindefalt}
+% \begin{macrocode}
+%<*package>
+\newcommand{\atwindefalt}[5][]{\definiendum[#1]{#2}\@atwin[#1]{#3}{#4}{#5}}
+%</package>
+%<*ltxml>
+DefConstructor('\atwindefalt[]{}{}{}{}',
+ "<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=>'\atwindef');
+%</ltxml>
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\inlinedef}
+% \begin{macrocode}
+%<*package>
+\newcommand{\inlinedef}[2][]{\omdsetkeys{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{'type'} = 'inlinedef';
+ $document->openElement('omdoc:phrase',%attrs);
+ $document->absorb($body);
+ $document->closeElement('omdoc:phrase'); },
+ #Prepare 'defs' hooks for \defin 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>
+\omdaddkey[\mod@id]{termref}{cd}
+\omdaddkey{termref}{cdbase}
+\omdaddkey{termref}{name}
+\omdaddkey{termref}{role}
+\def\termref@set#1#2{\def\termref@name{#2}\omdsetkeys{termref}{#1}}
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\termref}
+% \begin{macrocode}
+\newcommand{\termref}[2][]{\omdsetkeys{termref}{#1}\st@termref{#2}}
+%</package>
+%<*ltxml>
+DefConstructor('\termref OptionalKeyVals:termref {}',
+ "<omdoc:term cd='&KeyVal(#1,'cd')' name='&KeyVal(#1,'name')'>"
+ . "#2"
+ ."</omdoc:term>");
+%</ltxml>
+% \end{macrocode}
+% \end{macro}
+% The next macro is where the actual work is done.
+% \begin{macro}{\st@termref}
+% We determine whether the macro \meta{module}|@cd@file@base| is defined. If it is, we
+% make the prefix of a URI reference in the local macro |\@uri|, which we compose to the
+% hyper-reference.
+% \begin{macrocode}
+%<*package>
+\def\st@termref#1{\ifx\termref@name\@empty\def\termref@name{#1}\fi%
+\mod@termref\termref@cd\termref@name{#1}}
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\twinref}
+% \begin{macrocode}
+\newcommand{\twinref}[3][]{\termref@set{#1}{#2-#3}\st@termref{#2 #3}}
+%</package>
+%<*ltxml>
+DefConstructor('\twinref OptionalKeyVals:termref {}{}',
+ "<omdoc:term cd='&KeyVal(#1,'cd')' name='&KeyVal(#1,'name')'>"
+ . "#2"
+ ."</omdoc:term>");
+%</ltxml>
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\atwinref}
+% \begin{macrocode}
+%<*package>
+\newcommand{\atwinref}[4][]{\termref@set{#1}{#2-#3-#4}\st@termref{#2 #3 #4}}
+%</package>
+%<*ltxml>
+DefConstructor('\atwinref OptionalKeyVals:termref {}{}{}',
+ "<omdoc:term cd='&KeyVal(#1,'cd')' name='&KeyVal(#1,'name')'>"
+ . "#2"
+ ."</omdoc:term>");
+%</ltxml>
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{macro}{\termin}
+% The |termin| macro is very simple, it just adds an index.
+% \begin{macrocode}
+%<*package>
+\newcommand{\termin}[2][]{\termref[#1]{#2}\index{#2}}
+%</package>
+%<*ltxml>
+DefConstructor('\termin OptionalKeyVals:term {}',
+ "<omdoc:idx>"
+ . "<omdoc:idt>"
+ . "<omdoc:term cd='&KeyVal(#1,'cd')' name='&KeyVal(#1,'name')'>#2</omdoc:term>"
+ . "</omdoc:idt>"
+ . "<omdoc:ide index='default'><omdoc:idp>#2</omdoc:idp></omdoc:ide>"
+ . "</omdoc:idx>");
+%</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{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 DefCMPEnvironment 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 omdsetkeys ifx csname endcsname
+% LocalWords: currentlabel theorembodyfont itshape theoremheaderfont bfseries
+% LocalWords: normalfont newtheorem upshape srefaddidkey omdaddkey symtype
+% 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