summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/tex/latex/stex/sproof/sproof.sty
blob: 35d2470cd02dcf6749f50d7b6bfe38033fd5f96e (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
%%
%% 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}[2012/01/28 v1.0 Semantic Markup for Proofs]
\DeclareOption{showmeta}{\PassOptionsToPackage{\CurrentOption}{metakeys}}
\ProcessOptions
\RequirePackage{sref}
\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}
\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}}
\def\pst@make@label@long#1#2{\@for\@I:=#1\do{\@I.}#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}
\newcommand{\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}}
\newenvironment{spf@proof}[2][]{\metasetkeys{spf}{#1}\sref@target
\count10=10
\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}{P}}
{\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}}
\newcommand{\spfidea}[2][]{\metasetkeys{spf}{#1}%
\stDMemph{\ifx\spf@type\@empty{Proof Idea}\else\spf@type\fi:} #2\sproofend}
\newenvironment{spfstep}[1][]{\metasetkeys{spf}{#1}
\ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi
\ifx\spf@title\@empty\else{(\stDMemph{\spf@title})}\fi}
{\next@pst@label}
\newenvironment{sproofcomment}[1][]{\metasetkeys{spf}{#1}
\ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi}
{\next@pst@label}
\newenvironment{spfcases}[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{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}:}\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}
\newenvironment{subproof}[1][]%
{\begin{pst@with@label}{\pst@label,\number\count\count10}}
{\ifx\spf@display\spf@flow\else\sproofend\fi\end{pst@with@label}}
\srefaddidkey{just}
\addmetakey{just}{method}
\addmetakey{just}{premises}
\addmetakey{just}{args}
\newenvironment{justification}[1][]{}{}
\newcommand{\premise}[2][]{#2}
\newcommand{\justarg}[2][]{#2}
\endinput
%%
%% End of file `sproof.sty'.