blob: b2501b45948be1b8a39086c6ded3abc0a8933096 (
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
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
|
%%
%% 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}[2006/01/13 v0.9a Semantic Markup for Proofs]
\RequirePackage{omdoc}[2007/09/09]
\newif\ifjust@method\just@methodfalse
\DeclareOption{method}{\just@methodtrue}
\newif\ifspf@env\spf@envfalse
\newif\ifspf@id\spf@idfalse
\newif\ifspf@display\spf@displayfalse
\DeclareOption{id}{\spf@idtrue\spf@envtrue}
\DeclareOption{env}{\spf@envtrue}
\DeclareOption{display}{\spf@displaytrue\spf@envtrue}
\newif\ifspf@for\spf@forfalse
\newif\ifspf@from\spf@forfalse
\newif\ifspf@type\spf@typefalse
\newif\ifspf@title\spf@titlefalse
\newif\ifspf@proofend\spf@proofendtrue
\newif\ifspf@continues\spf@continuesfalse
\DeclareOption{for}{\spf@fortrue\spf@envtrue}
\DeclareOption{from}{\spf@fromtrue\spf@envtrue}
\DeclareOption{type}{\spf@typetrue\spf@envtrue}
\DeclareOption{title}{\spf@titletrue\spf@envtrue}
\DeclareOption{continues}{\spf@continuepfrue\spf@envtrue}
\DeclareOption{noproofend}{\spf@proofendfalse\spf@envtrue}
\def\spftrue{\spf@fortrue\spf@fromtrue\spf@typetrue\spf@continuepfrue}
\DeclareOption{draft}{\spf@envtrue\just@methodtrue}
\DeclareOption{all}{\spf@envtrue\just@medhodtrue}
\ProcessOptions
\define@key{spf}{id}{\def\spf@id{#1}}
\define@key{spf}{display}{\def\spf@display{#1}}
\define@key{spf}{for}{\def\spf@for{#1}}
\define@key{spf}{from}{\def\spf@from{#1}}
\define@key{spf}{sproofend}{\spf@proofendtrue\def\sproof@box{#1}}
\define@key{spf}{noproofend}[imeanit]{\spf@proofendfalse}
\define@key{spf}{type}{\def\spf@type{#1}}
\define@key{spf}{title}{\def\spf@title{#1}}
\define@key{spf}{continues}{\def\spf@continues{#1}}
\def\show@st@keys@aux{%
\@ifundefined{spf@id}{}{\ifspf@id{id=\spf@id},\fi}%
\@ifundefined{spf@display}{}{\ifspf@display{display=\spf@display}\fi}}
\def\clear@pf@keys{\let\spf@id=\relax\let\spf@display=\relax}
\def\show@pf@keys@aux{%
\@ifundefined{spf@for}{}{\ifspf@for{for=\spf@for},\fi}%
\@ifundefined{spf@from}{}{\ifspf@from{from=\spf@from},\fi}%
\@ifundefined{spf@prefix}{}{\ifspf@prefix{prefix=\spf@prefix},\fi}%
\@ifundefined{spf@type}{}{\ifspf@type{type=\spf@type},\fi}%
\@ifundefined{spf@title}{}{\ifspf@title{title=\spf@title},\fi}%
\@ifundefined{spf@continues}{}{\ifspf@continues{continues=\spf@continues}\fi}}
\def\show@pf@keys#1{\footnote{#1[\show@pf@keys@aux\show@pf@keys@aux]}%
\clear@pf@keys\clear@pf@keys}
\def\clear@pf@keys{\let\spf@for=\relax\let\spf@from=\relax\let\spf@prefix=\relax%
\let\spf@type=\relax\let\spf@title=\relax\let\spf@continues=\relax}
\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@label.\number\count\count10}
\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\sproofend{\ifspf@proofend\hfil\null\nobreak\hfill\sproof@box\par\smallskip\fi}
\def\sProofEndSymbol#1{\def\sproof@box{#1}}
\newenvironment{@proof}[2][]{\setkeys{spf}{#1}
\count10=10\ifx\spf@display\spf@flow\else{\stDMemph{Proof}:}\fi%
\ifspf@env\show@pf@keys{sproof}\fi{ #2}%
\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{@proof}[#1]{#2}}{\sproofend\end{@proof}}
\newcommand{\sproofidea}[2][]{{\stDMemph{Proof Idea}:} #2\sproofend}
\newenvironment{spfstep}[1][]{\setkeys{spf}{#1}
\ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi
\@ifundefined{spf@title}{}{(\stDMemph{\spf@title})}%
\ifspf@env\show@pf@keys{spfstep}\fi}
{\next@pst@label}
\newenvironment{sproofcomment}[1][]{\setkeys{spf}{#1}
\ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi
\ifspf@env\show@pf@keys{sproofcomment}\fi}
{\next@pst@label}
\newenvironment{spfcases}[2][]{\setkeys{spf}{#1}
\def\@test{#2}\ifx\@test\empty\else
\ifx\spf@display\spf@flow {#2}\else\item[\the@pst@label]{#2} \fi\fi
\ifspf@env\show@pf@keys{spfcases}\fi
\begin{pst@with@label}{\pst@label.\number\count\count10}}
{\end{pst@with@label}\next@pst@label}
\newenvironment{spfcase}[2][]{\setkeys{spf}{#1}
\ifx\spf@display\spf@flow\else\item[\the@pst@label]\fi
\def\@test{#2}\ifx\@test\empty\else{\stDMemph{#2}:}\fi
\ifspf@env\show@pf@keys{spfcase}\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}{\begin{pst@with@label}{\pst@label.\number\count\count10}}
{\ifx\spf@display\spf@flow\else\sproofend\fi\end{pst@with@label}}
\define@key{just}{id}{\def\just@id{#1}}
\define@key{just}{method}{\def\just@method{#1}}
\def\show@just@keys#1{\footnote{#1[\show@pf@keys@aux\show@just@keys@aux]}}%
\def\show@just@keys@aux{%
\@ifundefined{just@method}{\relax}{\ifjust@method{method=\just@method},\fi}%
\clear@pf@keys\clear@just@keys}
\def\clear@just@keys{\let\just@method=\relax}
\newenvironment{justification}[1][]{\ifspf@env\setkeys{just}{#1}
\show@just@keys{justification}\fi}{}
\newcommand{\premise}[2][]{#2}
\newcommand{\justarg}[2][]{#2}
\endinput
%%
%% End of file `sproof.sty'.
|
