%%
%% This is file `statements.sty',
%% generated with the docstrip utility.
%%
%% The original source files were:
%%
%% statements.dtx  (with options: `package')
%% 
\NeedsTeXFormat{LaTeX2e}[1999/12/01]
\ProvidesPackage{statements}[2016/04/06 v1.2 Semantic Markup for Statements]
\newif\ifdef@index\def@indexfalse
\DeclareOption{defindex}{\def@indextrue}
\DeclareOption*{\PassOptionsToPackage{\CurrentOption}{omtext}}
\ProcessOptions
\RequirePackage{omtext}
\RequirePackage[base]{babel}
\RequirePackage[hyperref]{ntheorem}
\theoremstyle{plain}
\AfterBabelLanguage{ngerman}{\input{statements-ngerman.ldf}}
\providecommand\STpresent[1]{#1}
\def\define@statement@env#1{%
\newenvironment{#1}[1][]{\metasetkeys{omtext}{##1}\sref@target%
\@in@omtexttrue%
\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% display
\ifx\sref@id\@empty\sref@label@id{here}\else%
\sref@label@id{\STpresent{\csname ST#1EnvKeyword\endcsname}~\@currentlabel}\fi%
\ignorespaces}
{\csname st@#1@terminate\endcsname\ifx\omtext@display\st@flow\else\end{ST#1Env}\fi%
\omtext@post@skip\@in@omtextfalse}}
\newenvironment{assertion}[1][]{\metasetkeys{omtext}{#1}\sref@target%
\@in@omtexttrue%
\ifx\omtext@display\st@flow\itshape\noindent\ignorespaces%
\else% display!=flow
\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}%display=flow
{\ifx\omtext@display\st@flow\else\end{ST\omtext@type AssEnv}\@in@omtextfalse\fi}
\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@rule@kw{Rule}
\def\st@observation@kw{Observation}
\def\st@remark@kw{Remark}
\theorembodyfont{\itshape}
\theoremheaderfont{\normalfont\bfseries}
\newtheorem{STtheoremAssEnv}{\st@theorem@kw}[section]
\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}
\theorembodyfont{\rm}
\newtheorem{STremarkAssEnv}[STtheoremAssEnv]{\st@remark@kw}
\newtheorem{STruleAssEnv}[STtheoremAssEnv]{\st@rule@kw}
\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}
\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}
\srefaddidkey{symboldec}
\addmetakey{symboldec}{functions}
\addmetakey{symboldec}{role}
\addmetakey*{symboldec}{title}
\addmetakey*{symboldec}{name}
\addmetakey{symboldec}{subject}
\addmetakey*{symboldec}{display}
\newenvironment{symboldec}[1][]{\metasetkeys{symboldec}{#1}\sref@target\st@indeftrue%
\ifx\symboldec@display\st@flow\else{\noindent\stDMemph{\symdef@type} \symboldec@name:}\fi%
\ifx\symboldec@title\@empty~\else~(\stDMemph{\symboldec@title})\par\fi}{}
\srefaddidkey{symtype}
\addmetakey*{symtype}{system}
\addmetakey*{symtype}{for}
\newcommand\type@type{Type}
\newcommand\symtype[3][]{\metasetkeys{symtype}{#1}\sref@target%
\noindent\type@type \ifx\symtype@\@empty\else (\symtype@system)\fi #2: $#3$}
\newcommand\inlinetypedec[3][]{\metasetkeys{symtype}{#1}\sref@target{\def\thedectype{#2}#3}}
\def\st@typedec@kw{Type Declaration}
\theorembodyfont{\upshape}
\newtheorem{STtypedecEnv}[STtheoremAssEnv]{\st@typedec@kw}
\newenvironment{typedec}[2][]{\metasetkeys{omtext}{#1}\sref@target%
\def\thedectype{#2}%
\ifx\omtext@display\st@flow\else%
\ifx\omtext@title\@empty\begin{STtypedecEnv}\else\begin{STtypedecEnv}[\omtext@title]\fi%
\ifx\sref@id\@empty\else\label{typedec.\sref@id}\fi
\ifx\sref@id\@empty\sref@label@id{here}\else%
\sref@label@id{\STpresent{\csname STtypedecEnvKeyword\endcsname}~\@currentlabel}\fi%
\ignorespaces}
{\ifx\omtext@display\st@flow\else\end{STtypedecEnv}\fi\omtext@post@skip}
\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%
\ignorespaces}
{\ifx\omtext@display\st@flow\else\end{STdefinitionEnv}\fi}
\def\st@definition@kw{Definition}
\theorembodyfont{\upshape}
\newtheorem{STdefinitionEnv}[STtheoremAssEnv]{\st@definition@kw}
\def\notemph#1{#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}
\newcommand\st@def@target[3]{\def\@symname{#1}\def\@verbname{#2}%
\ifst@indef% if we are in a definition or such
\@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}}%
{% now we are in a module
\edef\@@cd{\ifx\omtext@theory\@empty\mod@id\else\omtext@theory\fi}%
\edef\@@name{\ifx\@symname\@empty\@verbname\else\@symname\fi}%
\defemph{\@ifundefined{sref@\@@name @\@@cd @defined}%
{\expandafter\sref@target@ifh{sref@\@@name @\@@cd @target}{#3}}%
{#3}}%
\expandafter\gdef\csname sref@\@@name @\@@cd @defined\endcsname{yes}%
\ifmetakeys@showmeta\metakeys@show@keys{\@@cd}{name:\@@name}\fi}%
\else% st@indef
\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}% st@indef
\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}}}
\newcommand\definiendum[2][]{\st@def@target{#1}{#2}{#2}}
\newcommand\notatiendum[2][]{\notemph{#2}}
\newcommand\defi[2][]{\st@def@target{#1}{#2}{#2}\def\@phrase{#2}\@defi}
\newcommand\@defi[1][]{\ifdef@index\omdoc@indexi[#1]{\@phrase}\fi\xspace}
\newcommand\defis[2][]{\st@def@target{#1}{#2}{#2s}\def\@phrase{#2}\@defi}
\newcommand\adefi[3][]{\def\@name{#1}\def\@verb{#3}%
\st@def@target{#1}{#3}{#2}\@adefi}
\newcommand\@adefi[1][]{%
\ifdef@index%
\ifx\@name\@empty\omdoc@indexi[#1]{\@verb}%
\else\omdoc@indexi[at=\@name,#1]{\@verb}\fi%
\fi\xspace}
\newcommand\@defii[1][]{\ifdef@index\@twin[#1]{\@pone}{\@ptwo}\fi\xspace}
\newcommand\defii[3][]{\def\@pone{#2}\def\@ptwo{#3}%
\st@def@target{#1}{#2-#3}{#2 #3}\@defii}
\newcommand\defiis[3][]{\def\@pone{#2}\def\@ptwo{#3}%
\st@def@target{#1}{#2-#3}{#2 #3s}\@defii}
\newcommand\adefii[4][]{\def\@name{#1}\def\@pone{#3}\def\@ptwo{#4}%
\st@def@target{#1}{#3-#4}{#2}\@adefii}
\newcommand\@adefii[1][]{%
\ifdef@index%
\ifx\@name\@empty\@twin[#1]{\@pone}{\@ptwo}%
\else\@twin[at=\@name,#1]{\@pone}{\@ptwo}\fi%
\fi\xspace}
\newcommand\defiii[4][]{\def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}%
\st@def@target{#1}{#2-#3-#4}{#2 #3 #4}\@defiii}
\newcommand\@defiii[1][]{\ifdef@index\@atwin[#1]{\@pone}{\@ptwo}{\@pthree}\fi\xspace}
\newcommand\defiiis[4][]{\def\@pone{#2}\def\@ptwo{#3}\def\@pthree{#4}%
\st@def@target{#1}{#2-#3-#4}{#2 #3 #4s}\@defiii}
\newcommand\adefiii[5][]{\def\@name{#1}\def\@pone{#3}\def\@ptwo{#4}\def\@pthree{#3}%
\st@def@target{#1}{#3-#4-#5}{#2}\@adefiii}
\newcommand\@adefiii[1][]{%
\ifdef@index%
\ifx\@name\@empty\@atwin[#1]{\@pone}{\@ptwo}{\@pthree}%
\else\@atwin[at=\@name,#1]{\@pone}{\@ptwo}{\@pthree}\fi%
\fi\xspace}
\newcommand\inlineex[2][]{\metasetkeys{omtext}{#1}%
\sref@target\sref@label@id{here}#2}
\newcommand\inlineass[2][]{\metasetkeys{omtext}{#1}%
\sref@target\sref@label@id{here}#2}
\newcommand\inlinedef[2][]{\metasetkeys{omtext}{#1}%
\if@in@omtext\else% we are not in an omtext or statement
\PackageError{modules}{\protect\inlinedef\space outside a statement!}%
{Try wrapping the paragraph in a\MessageBreak
\protect\begin{omtext}, \protect\begin{assertion}, \protect\begin{axiom}, ... \MessageBreak
whatever is suitable semantically}\fi%
\sref@target\sref@label@id{here}\st@indeftrue #2}
\addmetakey*{termref}{cd}
\addmetakey*{termref}{cdbase}
\addmetakey*{termref}{name}
\addmetakey*{termref}{role}
\newcommand\termref[2][]{\metasetkeys{termref}{#1}%
  \ifx\termref@cd\@empty\def\termref@cd{\mod@id}\fi%
  \ifx\termref@name\@empty\def\termref@name{#2}\fi%
  \@ifundefined{sref@\termref@name @\termref@cd @defined}
  {\ifx\termref@cdbase\@empty% external reference
    \mod@termref\termref@cd\termref@name{#2}%
    \else\sref@href@ifh\termref@cdbase{#2}%
    \fi}%
  {\sref@hlink@ifh{sref@\termref@name @\termref@cd @target}{#2}}%
}
\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}}
\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}}
\newcommand\trefis[2][]{\atrefi[#1]{#2s}{#2}}
\newcommand\trefiis[3][]{\atrefi[#1]{#2 #3s}{#2-#3}}
\newcommand\trefiiis[4][]{\atrefi[#1]{#2 #3 #4s}{#2-#3-#4}}
\providecommand{\termemph}[1]{#1}
\providecommand{\defemph}[1]{{\textbf{#1}}}
\providecommand{\stDMemph}[1]{{\textbf{#1}}}
\newcommand\term[2][]{\def\@test{#1}%
\ifx\@test\@empty\else
\@ifundefined{module@defs@#1}{\PackageWarning{statements}%
{{\protect\term} specifies module #1 which is not in
  scope\MessageBreak import it via e.g. via \protect\importmhmodule}}{}
\fi%
\PackageWarning{statements}%
{Dangling link (\protect\term) for "#2" still needs to be specified}%
\textcolor{blue}{\underline{#2}}}
\newcommand\symref[2]{\@nameuse{mod@symref@#1}{#2}}
\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}}
\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}}
\endinput
%%
%% End of file `statements.sty'.