\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{ND}[14/04/2010 ND environment for typesetting Lemmon-style natural deduction proofs by Alex Steinberg]
\RequirePackage{xargs,calc}



%%%%%counters, lengths etc.
\newcounter{@NDnumber}
\newcounter{@NDlw}
\newcounter{@NDrw}
\newcounter{@NDtit}
\newlength\@NDitemsep
\setlength\@NDitemsep{2em}
\newlength\@NDboxwidth
\newcounter{@NDlines}
\newlength\@NDrulewidth
\newlength\@NDitemindent
\newlength\@NDlwin
\newlength\@NDrwin
\newlength\@NDlwf
\newlength\@NDlwtmp
\newlength\@NDrwf
\newlength\@NDrwtmp
\newlength\@NDsep
\newlength\@NDsepe
\newlength\@NDoriglw
\newlength\@NDlident
\newlength\@NDol
\newlength\@NDtempz
\let\@NDoldlabel\label\let\@NDoldref\ref
%%%from pbox:
\newcommand{\widthofpbox}[1]{%
  \widthof{\begin{tabular}{@{}l@{}}#1\end{tabular}}}
  
%%%%%Definition of auxilliary commands for the ND environment
\newcommand\@NDwriteout[2]{\immediate\write\@auxout{\noexpand\expandafter\gdef\noexpand\csname @ND#1w\@NDident\endcsname{#2}}}

\def\@NDinsertbreakingcomma{%
  \ifnum \@tempcnta = 0 \else,\linebreak[0] \fi
  \advance\@tempcnta\@ne
  }
\newcommand\NDalist[1]{\ensuremath{\@tempcnta = 0\@for\@ii:=#1\do{\@NDinsertbreakingcomma\@ii}}}

\newcommand\@NDlabel[1]{\refstepcounter{@NDlines}\begin{minipage}[t]{\csname @NDlw\@NDident\endcsname}%
\NDalist{#1}\hfill\end{minipage}\makebox[2\@NDitemsep][c]{\ensuremath{\ensuremath{\left(\the@NDlines\right)}}}}

\newcommand\@NDrules[1]{\hspace{\@NDitemsep}\begin{minipage}[t]{\@NDrulewidth}#1\end{minipage}}

%%%%%Definition of the ND environment and ndl command
\newenvironmentx{ND}[5][1,2,3,4,5]%
{\refstepcounter{@NDnumber}\setcounter{@NDlines}{0}%
\newcommand{\ndl}[3]{\settowidth\@NDlwtmp{\NDalist{##1}}\ifdim\@NDlwtmp > \@NDlwf \setlength\@NDlwf{\@NDlwtmp}\fi%
\settowidth\@NDrwtmp{\widthofpbox{##3}}\ifdim\@NDrwtmp > \@NDrwf \setlength\@NDrwf{\@NDrwtmp}\fi%
\par\@NDlabel{##1}\begin{minipage}[t]{\@NDboxwidth}##2\end{minipage}\@NDrules{##3}\par\addvspace{\parsep}}%
\def\@NDtempa{#3}\def\@NDtempb{}\ifx\@NDtempa\@NDtempb\setcounter{@NDlw}{0}\setlength\@NDlwin{2em}\else\setcounter{@NDlw}{1}\setlength\@NDlwin{#3}\fi%
\def\@NDtempa{#4}\ifx\@NDtempa\@NDtempb\setcounter{@NDrw}{0}\setlength\@NDrwin{2cm}\else\setcounter{@NDrw}{1}\setlength\@NDrwin{#4}\fi%
\def\@NDtempa{#1}\ifx\@NDtempa\@NDtempb\setcounter{@NDtit}{0}\else\setcounter{@NDtit}{1}\fi%
\def\@NDtempa{#5}\ifx\@NDtempa\@NDtempb\setlength\@NDol{\linewidth}\else\ifdim #5 > \linewidth\setlength\@NDol{\linewidth}\else\setlength\@NDol{#5}\fi\fi%
\def\@NDtempa{#2}\ifx\@NDtempa\@NDtempb\def\@NDident{\the@NDnumber}\else\def\@NDident{#2}\fi%
%
\def\label##1{\@NDoldlabel{@ND\@NDident:line##1}}\def\ref##1{\@NDoldref{@ND\@NDident:line##1}}
%
\expandafter\ifx\csname @NDlw\@NDident\endcsname\relax%
\expandafter\gdef\csname @NDlw\@NDident\endcsname{\the\@NDlwin}\fi%
\expandafter\ifx\csname @NDrw\@NDident\endcsname\relax%
\expandafter\gdef\csname @NDrw\@NDident\endcsname{\the\@NDrwin}\fi%
\setlength\@NDrulewidth{\csname @NDrw\@NDident\endcsname}%
\def\@NDtempc{\csname @NDlw\@NDident\endcsname}%
\setlength\@NDsep{\topsep+2\partopsep}\setlength\@NDsepe{\topsep+2\partopsep}%
\setlength\@NDlident{\linewidth - \@NDol}
\begin{list}{}{\setlength\parindent{0pt}\setlength\@NDtempz{\baselinestretch\baselineskip}\setlength\parsep{.3\@NDtempz}\setlength\leftmargin{.5\@NDlident}\setlength\rightmargin{\leftmargin}}\item[]\ifnum\the@NDtit = 1\textbf{#1}\penalty10000\fi\setlength\@NDboxwidth{\@NDol-\@NDrulewidth-\@NDtempc-3\@NDitemsep}\ignorespaces}%
{\unskip\ifnum\the@NDlw = 1 \@NDwriteout{l}{\the\@NDlwin}\else\@NDwriteout{l}{\the\@NDlwf}\fi%
\ifnum\the@NDrw = 1 \@NDwriteout{r}{\the\@NDrwin}\else\@NDwriteout{r}{\the\@NDrwf}\fi%\setlength\parsep{.5\topsep plus .25\topsep minus .125\topsep}
\end{list}}

%%%%%%user commands
\newcommand\awidth[1]{\@ifundefined{@NDlw#1}{0pt}{\csname @NDlw#1\endcsname}}
\newcommand\rwidth[1]{\@ifundefined{@NDrw#1}{0pt}{\csname @NDrw#1\endcsname}}
\newcommand\ndref[2]{\@NDoldref{@ND#1:line#2}}
\newcommand\linenumber[1]{\setcounter{@NDlines}{#1-2}\refstepcounter{@NDlines}}

