summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/source/latex/stex/statements.dtx
diff options
context:
space:
mode:
Diffstat (limited to 'Master/texmf-dist/source/latex/stex/statements.dtx')
-rw-r--r--Master/texmf-dist/source/latex/stex/statements.dtx595
1 files changed, 595 insertions, 0 deletions
diff --git a/Master/texmf-dist/source/latex/stex/statements.dtx b/Master/texmf-dist/source/latex/stex/statements.dtx
new file mode 100644
index 00000000000..a1ca69e5614
--- /dev/null
+++ b/Master/texmf-dist/source/latex/stex/statements.dtx
@@ -0,0 +1,595 @@
+% \iffalse meta-comment
+% An Infrastructure for Mathematical Statements in sTeX
+% Copyright (C) 2004-2006 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
+% https://svn.kwarc.info/repos/kwarc/projects/stex/sty/statements.dtx
+% \fi
+%
+% \iffalse
+%<package>\NeedsTeXFormat{LaTeX2e}[1999/12/01]
+%<package>\ProvidesPackage{statements}[2007/09/09 v0.9d Semantic Markup for Statements]
+%
+%<*driver>
+\documentclass{ltxdoc}
+\usepackage{url,array,stex,float}
+\usepackage[show]{ed}
+\usepackage{hyperref}
+\makeindex
+\floatstyle{boxed}
+\newfloat{exfig}{thp}{lop}
+\floatname{exfig}{Example}
+\begin{document}\DocInput{statements.dtx}\end{document}
+%</driver>
+% \fi
+%
+% \CheckSum{266}
+%
+% \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}
+%
+% \GetFileInfo{statements.sty}
+%
+% \MakeShortVerb{\|}
+%\def\scsys#1{{{\sc #1}}\index{#1@{\sc #1}}}
+% \def\stex{{\raisebox{-.5ex}S\kern-.5ex\TeX}}
+% \def\sTeX{\stex}
+% \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}}
+% \def\twin#1#2{\index{#1!#2}\index{#2!#1}}
+% \def\twintoo#1#2{{#1 #2}\twin{#1}{#2}}
+% \def\atwin#1#2#3{\index{#1!#2!#3}\index{#3!#2 (#1)}}
+% \def\atwintoo#1#2#3{{#1 #2 #3}\atwin{#1}{#2}{#3}}
+% \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| packge 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}
+%\newpage
+%\section{Introduction}\label{sec:statements}
+%
+% The motivation for the |statemets| 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} 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).
+%
+% \section{The User Interface}
+%
+% All the statements are marked up as envioronments, that take a |KeyVal| argument that
+% allows to annotate semantic information. \DescribeEnv{assertion} For instance, instead
+% of providing environments for ``Theorem'', ``Lemma'', ``Proposition'',... we have a
+% single |assertion| environment that generalizes all of these, and takes a |type| key
+% that allows to specify the ``type''. 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).\ednote{talk about package options here!
+% Draft mode,...}
+%\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\medskip\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 {\tt{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. 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 |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\ednote{in the flow case, the text
+% should not be made italic; implement this! } the semantic information is invisible to
+% the reader.
+%
+% Another key that is present on all statement environments in the |id| key it allows to
+% identify the statement with a name.
+%
+% \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 expeceted to be justified from other assertions, axioms or
+% definitions.
+%
+% \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 |\termin| ), 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 apporpriate text fragment in a
+% |\begin{definition}[display=flow]| ... and |\end{definition}|.\ednote{need to leave
+% hypertargets on the definiendum, so that we can crosslink}
+%
+% \DescribeMacro{\termin} 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 lanauge
+% 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 |\termin| can be used to make this
+% information explicit.
+%
+% \DescribeEnv{simpleDef} The |simpleDef| environment is a statement environment for
+% simple definitions, which introduce a new symbol that abbreviates another concept. The
+% envioronment takes an argument for the new concept
+%
+% \DescribeEnv{example} The |example| environment is a generic statement envionment,
+% except that the |for| key should be given to specify the identifier what this is an
+% example for. The |example| environment also expcets a |type| key to be specified, so
+% that we know whether this is an example or a counterexample\ednote{think about this some
+% more}
+%
+% \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 hyperreference
+% to the defining occurrance 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.
+%
+% \StopEventually{\ednotemessage}
+%
+% \section{The Implementation}\label{sec:impl}
+%
+% 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>
+\newif\ifst@env\st@envfalse
+\newif\ifst@id\st@idfalse
+\newif\ifst@display\st@displayfalse
+\DeclareOption{id}{\st@idtrue\st@envtrue}
+\DeclareOption{env}{\st@envtrue}
+\DeclareOption{display}{\st@displaytrue\st@envtrue}
+% \end{macrocode}
+% And then the options that are specific to the |statements| package.
+% \begin{macrocode}
+\newif\ifstat@for\stat@forfalse
+\newif\ifstat@from\stat@forfalse
+\newif\ifstat@type\stat@typefalse
+\newif\ifstat@title\stat@titlefalse
+\newif\ifstat@continues\stat@continuesfalse
+\DeclareOption{for}{\stat@fortrue\st@envtrue}
+\DeclareOption{from}{\stat@fromtrue\st@envtrue}
+\DeclareOption{type}{\stat@typetrue\st@envtrue}
+\DeclareOption{title}{\stat@titletrue\st@envtrue}
+\DeclareOption{continues}{\stat@continuestrue\st@envtrue}
+% \end{macrocode}
+% \begin{macro}{\stattrue}
+% For convenience, we collect the switches into one.
+% \begin{macrocode}
+\def\stattrue{\stat@fortrue\stat@fromtrue\stat@typetrue\stat@continuestrue}
+% \end{macrocode}
+% \end{macro}
+% Now, we define two collective options, which are equivalent to turning on all the other
+% options.
+% \begin{macrocode}
+\DeclareOption{draft}{\st@envtrue\st@idtrue\stat@fortrue\stat@fromtrue\typetrue\justtrue}
+\DeclareOption{all}{\st@envtrue\stattrue\justtrue}
+% \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 the |omdoc| package is loaded (in the right
+% version). For {\latexml}, we also initialize the package inclusions.
+% \begin{macrocode}
+%<package>\RequirePackage{omdoc}[2007/09/09]
+%<*ltxml>
+# -*- CPERL -*-
+package LaTeXML::Package::Pool;
+use strict;
+use LaTeXML::Package;
+RequirePackage('omdoc');
+RequirePackage('myindex');
+%</ltxml>
+% \end{macrocode}
+%
+% \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 respcective termination macro.
+% \begin{macrocode}
+%<*package>
+\def\define@statement@env#1#2{
+\newenvironment{#1}[1][]{\setkeys{stat}{##1}
+\ifx\st@display\st@flow\else\stDMemph{#2}:\fi%
+\@ifundefined{stat@title}{}%
+{\space\ifx\st@display\st@flow\else(\fi\stDMemph{\stat@title}\ifx\st@display\st@flow:\else)\par\fi}\space%
+\ifst@env\show@stat@keys{#1}\fi\csname st@#1@initialize\endcsname}
+{\csname st@#1@terminate\endcsname}}
+%</package>
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{environment}{assertion}
+% \begin{macrocode}
+%<*package>
+\newenvironment{assertion}[1][]{\setkeys{stat}{#1}
+\ifx\st@display\st@flow\else{\stDMemph{\stat@type}:}\fi%
+\@ifundefined{stat@title}{~}{~(\stDMemph{\stat@title})\par}%
+\ifst@env\show@stat@keys{#1}\fi\em}{}
+%</package>
+%<*ltxml>
+DefCMPEnvironment('{assertion} OptionalKeyVals:stat',
+ "<omdoc:assertion ?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')() type='&KeyVal(#1,'type')'>"
+ . "?&KeyVal(#1,'title')(<omdoc:metadata><dc:title>&KeyVal(#1,'title')</dc:title></omdoc:metadata>)()"
+ . "<omdoc:CMP><omdoc:p>#body</omdoc:p></omdoc:CMP>"
+ ."</omdoc:assertion>\n");
+%</ltxml>
+% \end{macrocode}
+% \end{environment}
+%
+% \begin{environment}{simpleDef}
+% \begin{macrocode}
+%<*package>
+\newenvironment{simpleDef}[1][]{\setkeys{stat}{#1}
+\ifx\st@display\st@flow\else{\stDMemph{Definition}:}\fi%
+\@ifundefined{stat@title}{~}{~(\stDMemph{\stat@title})\par}%
+\ifst@env\show@stat@keys{#1}\fi}{}
+%</package>
+%<*ltxml>
+DefCMPEnvironment('{simpleDef} OptionalKeyVals:stat',
+ "?&KeyVal(#1,'for')(<omdoc:symbol name='&KeyVal(#1,'for')'/>)()"
+ . "<omdoc:definition type='simple' "
+ . "?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id').def')()"
+ . "?&KeyVal(#1,'for')(for='&KeyVal(#1,'for')')()>"
+ . "?&KeyVal(#1,'title')(<omdoc:metadata><dc:title>&KeyVal(#1,'title')</dc:title></omdoc:metadata>)()"
+ . "<omdoc:CMP><omdoc:p>#body</omdoc:p></omdoc:CMP>"
+ . "</omdoc:definition>\n");
+%</ltxml>
+% \end{macrocode}
+% \end{environment}
+%
+% \begin{environment}{PatternDef}
+% \begin{macrocode}
+%<*package>
+\newenvironment{PatternDef}[1][]{\setkeys{stat}{#1}
+\ifx\st@display\st@flow\else{\stDMemph{Definition}:}\fi%
+\@ifundefined{stat@title}{~}{~(\stDMemph{\stat@title})\par}%
+\ifst@env\show@stat@keys{#1}\fi}{}
+\newenvironment{PatternRule}[1]{#1$\colon=$}{}
+\newenvironment{PatternCMP}{}{}
+%</package>
+%<*ltxml>
+DefCMPEnvironment('{PatternDef} OptionalKeyVals:stat',
+ "?&KeyVal(#1,'for')(<omdoc:symbol name='&KeyVal(#1,'for')'/>)()"
+ . "<omdoc:definition type='pattern' "
+ . "?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id').def')()"
+ . "?&KeyVal(#1,'for')(for='&KeyVal(#1,'for')')()>"
+ . "?&KeyVal(#1,'title')(<omdoc:metadata><dc:title>&KeyVal(#1,'title')</dc:title></omdoc:metadata>)()"
+ . "#body"
+ . "</omdoc:definition>\n");
+DefEnvironment('{PatternRule}{}',
+ "<omdoc:requation>#1 #body</omdoc:requation>");
+DefEnvironment('{PatternCMP}{}',
+ "<omdoc:CMP>#body</omdoc:CMP>");
+%</ltxml>
+% \end{macrocode}
+% \end{environment}
+%
+% \begin{environment}{RecDef}
+% \begin{macrocode}
+%<*package>
+\newenvironment{RecDef}[1][]{\setkeys{stat}{#1}
+\ifx\st@display\st@flow\else{\stDMemph{Definition}:}\fi%
+\@ifundefined{stat@title}{~}{~(\stDMemph{\stat@title})\par}%
+\ifst@env\show@stat@keys{#1}\fi}{}
+%</package>
+%<*ltxml>
+DefEnvironment('{RecDef} OptionalKeyVals:stat',
+ "?&KeyVal(#1,'for')(<omdoc:symbol name='&KeyVal(#1,'for')'/>)()"
+ . "<omdoc:definition type='inductive' "
+ . "?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id').def')()"
+ . "?&KeyVal(#1,'for')(for='&KeyVal(#1,'for')')()>"
+ . "?&KeyVal(#1,'title')(<omdoc:metadata><dc:title>&KeyVal(#1,'title')</dc:title></omdoc:metadata>)()"
+ . "<omdoc:CMP><omdoc:p>#body</omdoc:p></omdoc:CMP>"
+ . "</omdoc:definition>\n");
+%</ltxml>
+% \end{macrocode}
+% \end{environment}
+%
+% \begin{environment}{example}
+% \begin{macrocode}
+%<*package>
+\def\st@example@initialize{}\def\st@example@terminate{}
+\define@statement@env{example}{Example}
+%</package>
+%<*ltxml>
+DefCMPEnvironment('{example} OptionalKeyVals:stat',
+ "<omdoc:example "
+ . "?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')() "
+ . "for='&KeyVal(#1,'for')'>"
+ . "<omdoc:CMP><omdoc:p>#body</omdoc:p></omdoc:CMP>"
+ . "</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}{Axiom}
+%</package>
+%<*ltxml>
+DefCMPEnvironment('{axiom} OptionalKeyVals:stat',
+ "<omdoc:axiom ?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')()>"
+ . "?&KeyVal(#1,'title')(<omdoc:metadata><dc:title>&KeyVal(#1,'title')</dc:title></omdoc:metadata>)()"
+ . "<omdoc:CMP><omdoc:p>#body</omdoc:p></omdoc:CMP>"
+ . "</omdoc:axiom>\n");
+%</ltxml>
+% \end{macrocode}
+% \end{environment}
+%
+% \begin{environment}{consymb}
+% \begin{macrocode}
+%<*package>
+\define@key{consymb}{type}{\def\consymb@type{#1}}
+\define@key{consymb}{title}{\def\consymb@title{#1}}
+\define@key{consymb}{name}{\def\consymb@name{#1}}
+\def\consymb@type{Symbol}
+\newenvironment{consymb}[1][]{\setkeys{consymb}{#1}
+\ifx\st@display\st@flow\else{\stDMemph{\consymb@type} \consymb@name:}\fi%
+\@ifundefined{consymb@title}{~}{~(\stDMemph{\consymb@title})\par}}{}
+%</package>
+%<*ltxml>
+DefEnvironment('{consymb} OptionalKeyVals:stat',
+ "<omdoc:symbol ?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id')')()"
+ . "name='&KeyVal(#1,'name')'>"
+ . "<omdoc:metadata>"
+ . "<dc:description>"
+ . "#body"
+ . "</dc:description>"
+ . "</omdoc:metadata>"
+ . "</omdoc:symbol>\n");
+%</ltxml>
+% \end{macrocode}
+% \end{environment}
+%
+% \begin{macro}{\symtype}
+% \begin{macrocode}
+%<package>\newcommand{\symtype}[2]{Type (#1): #2}
+%<ltxml>DefConstructor('\symtype{}{}',"<omdoc:type system='#1'>#2</omdoc:type>");
+% \end{macrocode}
+% \end{macro}
+%
+% \begin{environment}{definition}
+% The |definition| environment itself is quite simple. The only interesting thing is
+% that it locally defines the |definiendum| macro, which we do in the initialization
+% macro.
+% \begin{macro}{\definiendum}
+% The |\definiendum| macro is very simple: at the moment we do not do anything with the
+% keyword arguments.
+% \end{macro}
+% \begin{macrocode}
+%<*package>
+\def\st@definition@initialize{%
+\newcommand{\notatiendum}[2][]{\notemph{##2}}
+\newcommand{\definiendum}[2][]{\defemph{##2}}}
+\def\st@definition@terminate{}
+\define@statement@env{definition}{Definition}
+%</package>
+%<*ltxml>
+DefCMPEnvironment('{definition} OptionalKeyVals:stat', sub {
+ my ($doc, $keyvals, %props) = @_;
+ my @symbols = @{$props{defs} || []};
+ foreach my $symb(@symbols) {
+ $doc->openElement('omdoc:symbol', name=>$symb);
+ $doc->closeElement('omdoc:symbol'); }
+ my %attrs = ();
+ my $id = $keyvals->getValue('id') if $keyvals;
+ $attrs{'xml:id'} = $id if $id;
+ my $ffor = $keyvals->getValue('for') if $keyvals;
+ my $for = $ffor . join(' ',@symbols) if $ffor;
+ $attrs{for} = $for if $for;
+ $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->closeElement('omdoc:metadata'); }
+ $doc->openElement('omdoc:CMP');
+ $doc->openElement('omdoc:p');
+ $doc->absorb($props{body}) if $props{body};
+ $doc->closeElement('omdoc:p');
+ $doc->closeElement('omdoc:CMP');
+ $doc->closeElement('omdoc:definition');
+ return; },
+ afterDigestBegin=>sub {
+ my ($stomach, $whatsit) = @_;
+ my @symbols = ();
+ $whatsit->setProperty(defs=>\@symbols);
+ AssignValue('defs', \@symbols, 'global');
+ return; },
+ afterDigest => sub {
+ AssignValue('defs', undef, 'global');
+ return; });
+
+DefConstructor('\definiendum[]{}',
+ "<omdoc:term role='definiendum' name='#1' cd='#theory'>#2</omdoc:term>",
+ afterDigest => sub {
+ my ($stomach, $whatsit) = @_;
+ my $addr = LookupValue('defs');
+ push(@$addr, $whatsit->getArg(1)->toString) if $addr;
+ $whatsit->setProperty(theory=>LookupValue('current_module'));
+ return; });
+%</ltxml>
+% \end{macrocode}
+% \end{environment}
+%
+% 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{macrocode}
+%<*ltxml>
+DefMacro('\defin{}', sub {
+ my @args = (T_BEGIN, $_[1]->unlist, T_END);
+ (T_CS('\definiendum'), T_OTHER('['), $_[1]->unlist, T_OTHER(']'), @args, T_CS('\defin@index'), @args); });
+DefMacro('\twindef{}{}', sub {
+ my @args = (T_BEGIN, $_[1]->unlist, T_END, T_BEGIN, $_[2]->unlist, T_END);
+ (T_CS('\twindef@def'), @args, T_CS('\twindef@index'), @args); });
+DefMacro('\atwindef{}{}{}', sub {
+ my @args = (T_BEGIN, $_[1]->unlist, T_END, T_BEGIN, $_[2]->unlist, T_END,
+ T_BEGIN, $_[3]->unlist, T_END);
+ (T_CS('\atwindef@def'), @args, T_CS('\atwindef@index'), @args); });
+DefConstructor('\twindef@def{}{}',
+ "<omdoc:term role='definiendum' name='#1-#2' cd='#theory'>#1 #2</omdoc:term>",
+ afterDigest => sub {
+ my ($stomach, $whatsit) = @_;
+ my $addr = LookupValue('defs');
+ push(@$addr, $whatsit->getArg(1)->toString.'-'.$whatsit->getArg(2)->toString) if $addr;
+ $whatsit->setProperty(theory=>LookupValue('current_module'));
+ return; },
+ alias => '');
+DefConstructor('\atwindef@def{}{}{}',
+ "<omdoc:term role='definiendum' name='#1-#2-#3' cd='#theory'>#1 #2 #3</omdoc:term>",
+ afterDigest => sub {
+ my ($stomach, $whatsit) = @_;
+ my $addr = LookupValue('defs');
+ push(@$addr, $whatsit->getArg(1)->toString.'-'.$whatsit->getArg(2)->toString
+ .'-'.$whatsit->getArg(3)->toString) if $addr;
+ $whatsit->setProperty(theory=>LookupValue('current_module'));
+ return; },
+ alias => '');
+%</ltxml>
+% \end{macrocode}
+%
+% \begin{environment}{notation}
+% \begin{macrocode}
+%<*package>
+\def\notemph#1{{\bf{#1}}}
+\def\st@notation@initialize{\newcommand{\notatiendum}[2][]{\notemph{##2}}}
+\def\st@notation@terminate{}
+\define@statement@env{notation}{Notation}
+%</package>
+%<*ltxml>
+DefCMPEnvironment('{notation} OptionalKeyVals:stat',
+ "<omdoc:omtext type='notation' ?&KeyVal(#1,'id')(xml:id='&KeyVal(#1,'id').not')()>"
+ . "?&KeyVal(#1,'title')(<omdoc:metadata><dc:title>&KeyVal(#1,'title')</dc:title></omdoc:metadata>)()"
+ . "<omdoc:CMP><omdoc:p>#body</omdoc:p></omdoc:CMP>"
+ . "</omdoc:omtext>\n");
+DefConstructor('\notatiendum OptionalKeyVals:notation {}',
+ "<omdoc:phrase type='notation'>#1</omdoc:phrase>");
+%</ltxml>
+% \end{macrocode}
+% \end{environment}
+%
+% \begin{macro}{\termin}
+% The |termin| macro is very simple, it forgets the semantic annotations\ednote{use
+% those for hyperlinking in the future} and puts the
+% \begin{macrocode}
+%<*package>
+\def\termin{\@ifnextchar[{\@termin}{\@termin[]}}
+\def\@termin[#1]#2{{\termemph{\index*{#2}}}}
+%</package>
+% \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{macrocode}
+%<*package>
+\providecommand{\termemph}[1]{#1}
+\providecommand{\defemph}[1]{{\bf{#1}}}
+\providecommand{\stDMemph}[1]{{\bf{#1}}}
+%</package>
+% \end{macrocode}
+%
+% \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 excuting the |numberIt| procedure from |omdoc.sty.ltxml|.
+%
+% \begin{macrocode}
+%<*ltxml.sty>
+Tag('omdoc:assertion',afterOpen=>\&numberIt);
+Tag('omdoc:definition',afterOpen=>\&numberIt);
+%</ltxml.sty>
+% \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
+% LocalWords: continuestrue consymb omtext
+%%% Local Variables:
+%%% mode: doctex
+%%% TeX-master: t
+%%% End:
+% \fi