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.dtx1376
1 files changed, 0 insertions, 1376 deletions
diff --git a/Master/texmf-dist/source/latex/stex/statements/statements.dtx b/Master/texmf-dist/source/latex/stex/statements/statements.dtx
deleted file mode 100644
index 062ee52c0a9..00000000000
--- a/Master/texmf-dist/source/latex/stex/statements/statements.dtx
+++ /dev/null
@@ -1,1376 +0,0 @@
-% \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 1671 2010-11-06 07:05:15Z 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
-%
-% \iffalse\CheckSum{433}\fi
-%
-% \changes{v0.9}{2005/06/14}{First Version with Documentation}
-% \changes{v0.9a}{2005/07/01}{Completed Documentation}
-% \changes{v0.9b}{2005/08/06}{Complete functionality and Updated Documentation}
-% \changes{v0.9c}{2006/01/13}{more packaging}
-% \changes{v0.9d}{2007/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}}}
-%
-% \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{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}\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}|\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}
-%
-% Note that the |\definiendum|, |\defin|, |\twindef|, and |\atwindef| 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
-% \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 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
-% |\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}
-%
-% \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>
-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'))')()>"
- . "?&KeyVal(#1,'title')(<dc:title>&KeyVal(#1,'title')</dc:title>)()"
- . "<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}
-\addmetakey{symboldec}{functions}
-\addmetakey{symboldec}{role}
-\addmetakey*{symboldec}{title}
-\addmetakey{symboldec}{name}
-\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')'>"
- . "<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][]{\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;
- }}
- 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}%
-\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\defin,
-\protect\twindef, \protect\atwindef\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\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}
-%</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}{\inlineex}
-% \begin{macrocode}
-%<*package>
-\newcommand{\inlineex}[2][]{\metasetkeys{omtext}{#1}\sref@target\sref@label@id{here}#2}
-%</package>
-%<*ltxml>
-DefConstructor('\inlineex OptionalKeyVals:omtext {}',
- "<omdoc:phrase type='example'>#2</omdoc:phrase>");
-%</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{'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>
-\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 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 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