diff options
Diffstat (limited to 'Master/texmf-dist/source/latex/stex/statements.dtx')
-rw-r--r-- | Master/texmf-dist/source/latex/stex/statements.dtx | 595 |
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 |