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