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