%%
%% This is file `sproof.sty',
%% generated with the docstrip utility.
%%
%% The original source files were:
%%
%% sproof.dtx  (with options: `package')
%% 
\NeedsTeXFormat{LaTeX2e}[1999/12/01]
\ProvidesPackage{sproof}[2016/04/06 v1.1 Semantic Markup for Proofs]
\DeclareOption*{\PassOptionsToPackage{\CurrentOption}{sref}}
\ProcessOptions
\RequirePackage{sref}
\RequirePackage{etoolbox}
\RequirePackage[base]{babel}
\srefaddidkey{spf}
\addmetakey*{spf}{display}
\addmetakey{spf}{for}
\addmetakey{spf}{from}
\addmetakey*[\sproof@box]{spf}{proofend}
\addmetakey{spf}{type}
\addmetakey*{spf}{title}
\addmetakey{spf}{continues}
\addmetakey{spf}{functions}
\addmetakey{spf}{method}
\def\spf@flow{flow}
\newenvironment{pst@with@label}[1]{%
  \edef\pst@label{#1}%
  \advance\count10 by 1%
  \count\count10=1%
}{%
  \advance\count10 by -1%
}%
\def\the@pst@label{%
  \pst@make@label\pst@label{\number\count\count10}\pstlabel@postfix%
}%
\addmetakey[P]{pstlabel}{prefix}[]
\addmetakey[.]{pstlabel}{delimiter}[]
\addmetakey[]{pstlabel}{postfix}[]
\metasetkeys{pstlabel}{}% initialization
\newrobustcmd\setpstlabelstyle[1]{%
  \metasetkeys{pstlabel}{#1}%
}%
\newrobustcmd\setpstlabelstyledefault{%
  \metasetkeys{pstlabel}{prefix=P,delimiter=.,postfix=}%
}%
\def\pst@make@label@long#1#2{\@for\@I:=#1\do{\expandafter\@I\pstlabel@delimiter}#2}
\def\pst@make@label@angles#1#2{\ensuremath{\@for\@I:=#1\do{\rangle}}#2}
\def\pst@make@label@short#1#2{#2}
\def\pst@make@label@empty#1#2{}
\def\pstlabelstyle#1{%
  \def\pst@make@label{\@nameuse{pst@make@label@#1}}%
}%
\pstlabelstyle{long}%
\def\next@pst@label{%
  \global\advance\count\count10 by 1%
}%
\def\sproof@box{%
  \hbox{\vrule\vbox{\hrule width 6 pt\vskip 6pt\hrule}\vrule}%
}%
\def\spf@proofend{\sproof@box}%
\def\sproofend{%
  \ifx\spf@proofend\@empty%
  \else%
    \hfil\null\nobreak\hfill\spf@proofend\par\smallskip%
  \fi%
}%
\def\sProofEndSymbol#1{\def\sproof@box{#1}}%
\def\spf@proofsketch@kw{Proof Sketch}
\def\spf@proof@kw{Proof}
\def\spf@step@kw{Step}
\AfterBabelLanguage{ngerman}{\input{sproof-ngerman.ldf}}
\newrobustcmd\spfsketch[2][]{%
  \metasetkeys{spf}{#1}%
  \sref@target%
  \ifx\spf@display\spf@flow%
  \else%
  {\stDMemph{\ifx\spf@type\@empty\spf@proofsketch@kw\else\spf@type\fi}:}
  \fi{ #2}%
  \sref@label@id{this \ifx\spf@type\@empty\spf@proofsketch@kw\else\spf@type\fi}\sproofend%
}%
\newenvironment{spfeq}[2][]{%
  \metasetkeys{spf}{#1}\sref@target%
  \ifx\spf@display\spf@flow%
  \else%
    {\stDMemph{\ifx\spf@type\@empty\spf@proof@kw\else\spf@type\fi}:} #2%
  \fi% display=flow
  \begin{displaymath}\begin{array}{rcll}%
}{%
  \end{array}\end{displaymath}%
}%
\newenvironment{spf@proof}[2][]{%
  \metasetkeys{spf}{#1}%
  \sref@target%
  \count10=10%
  \par\noindent%
  \ifx\spf@display\spf@flow%
  \else%
    \stDMemph{\ifx\spf@type\@empty\spf@proof@kw\else\spf@type\fi}:%
  \fi{ #2}%
  \sref@label@id{this \ifx\spf@type\@empty\spf@proof@kw\else\spf@type\fi}%
  \def\pst@label{}%
  \newcount\pst@count% initialize the labeling mechanism
  \begin{description}\begin{pst@with@label}{\pstlabel@prefix}%
}{%
  \end{pst@with@label}\end{description}%
}%
\newenvironment{sproof}[2][]{\begin{spf@proof}[#1]{#2}}{\sproofend\end{spf@proof}}%
\newenvironment{sProof}[2][]{\begin{spf@proof}[#1]{#2}}{\end{spf@proof}}%
\newrobustcmd\spfidea[2][]{%
  \metasetkeys{spf}{#1}%
  \stDMemph{\ifx\spf@type\@empty{Proof Idea}\else\spf@type\fi:} #2\sproofend%
}%
\newenvironment{spfstep}[1][]{%
  \metasetkeys{spf}{#1}%
  \@in@omtexttrue%
  \ifx\spf@display\spf@flow%
  \else%
    \item[\the@pst@label]%
  \fi%
  \ifx\spf@title\@empty\else{(\stDMemph{\spf@title})}\fi%
  \sref@label@id{\pst@label}\ignorespaces%
}{%
  \next@pst@label\@in@omtextfalse\ignorespaces%
}%
\newenvironment{sproofcomment}[1][]{%
  \metasetkeys{spf}{#1}%
  \ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi%
}{%
  \next@pst@label%
}%
\newenvironment{subproof}[2][]{%
  \metasetkeys{spf}{#1}%
  \def\@test{#2}%
  \ifx\@test\empty%
  \else%
    \ifx\spf@display\spf@flow {#2}%
    \else%
      \item[\the@pst@label]{#2} %
    \fi%
  \fi%
  \begin{pst@with@label}{\pst@label,\number\count\count10}%
}{%
  \end{pst@with@label}\next@pst@label%
}%
\newenvironment{spfcases}[2][]{%
  \def\@test{#1}%
  \ifx\@test\empty%
    \begin{subproof}[method=by-cases]{#2}%
  \else%
    \begin{subproof}[#1,method=by-cases]{#2}%
  \fi%
}{%
  \end{subproof}%
}%
\newenvironment{spfcase}[2][]{%
  \metasetkeys{spf}{#1}%
  \ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi%
  \def\@test{#2}%
  \ifx\@test\@empty%
  \else%
    {\stDMemph{#2}: }% need blank here
  \fi%
  \begin{pst@with@label}{\pst@label,\number\count\count10}
}{%
  \ifx\spf@display\spf@flow%
  \else%
    \sproofend%
  \fi%
  \end{pst@with@label}%
  \next@pst@label%
}%
\newrobustcmd\spfcasesketch[3][]{%
  \metasetkeys{spf}{#1}%
  \ifx\spf@display\spf@flow%
  \else%
    \item[\the@pst@label]%
  \fi%
  \def\@test{#2}%
  \ifx\@test\@empty%
  \else%
    {\stDMemph{#2}: }%
  \fi#3%
  \next@pst@label%
}%
\srefaddidkey{just}
\addmetakey{just}{method}
\addmetakey{just}{premises}
\addmetakey{just}{args}
\newenvironment{justification}[1][]{}{}
\newrobustcmd\premise[2][]{#2}
\newrobustcmd\justarg[2][]{#2}
\endinput
%%
%% End of file `sproof.sty'.
