%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Copyright © 2022 Maximilian Keßler
% 
% Permission is hereby granted, free of charge, to any person obtaining a copy
% of this software and associated documentation files (the “Software”), to deal
% in the Software without restriction, including without limitation the rights
% to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
% copies of the Software, and to permit persons to whom the Software is
% furnished to do so, subject to the following conditions:
% The above copyright notice and this permission notice shall be included in all
% copies or substantial portions of the Software.
% 
% THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
% IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
% FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
% AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
% LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
% OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
% SOFTWARE.
% 
% This package has been generated by PyTeX, available at
%    https://github.com/kesslermaximilian/PyTeX
% and built from source file 'refproof.pysty'.
% It is STRONGLY DISCOURAGED to edit this source file directly, since local
% changes will not be versioned by Git and overwritten by the next build. Always
% edit the source file and build the package again.
% 
% Build details:
%   PyTeX version: v1.2.0-3-g5e077e7 (commit 5e077e7)
%   Source code version: v2.4.4-4-geb06eb8 (commit eb06eb8)
% 
% This LaTeX package is free software and distributed under the MIT License. You
% may use it freely for your purposes. The latest version of the package can be
% obtained via GitHub under
%    https://github.com/kesslermaximilian/LatexPackages
% For further information see the url above.
% Reportings of bugs, suggestions and improvements are welcome, see the README
% at the Git repository for further information.
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%

\NeedsTeXFormat{LaTeX2e}
\ProvidesPackage{mkessler-refproof}[2022/01/09 - Automatic references to theorems in proofs. Claim counters within proofs]



\RequirePackage{xkeyval}

\newif\ifmkessler@refproof@english\mkessler@refproof@englishtrue
\DeclareOptionX{german}{\mkessler@refproof@englishfalse}
\DeclareOptionX{ngerman}{\mkessler@refproof@englishfalse}
\DeclareOptionX{english}{\mkessler@refproof@englishtrue}

\DeclareOptionX*{\PackageWarning{mkessler-refproof}{Unknown '\CurrentOption'}}
\ProcessOptionsX*\relax


\RequirePackage{amssymb}
\RequirePackage{amsthm}
\RequirePackage{etoolbox}
\RequirePackage{xparse}
\RequirePackage{refcount}
\RequirePackage{translator}
\RequirePackage{fifo-stack}

\usedictionary{translator-proof-dictionary}

%%Give claim an own counter and let it reset at each proof
%See also at:
%https://tex.stackexchange.com/questions/283502/reset-counter-at-beginning-of-proof
\newtheorem{claim}{\translate{Claim}}
\newtheorem*{claim*}{\translate{Claim}}
\AtBeginDocument{\def\claimautorefname{\translate{Claim}}}

\AtBeginDocument{
    \@ifpackageloaded{hyperref}{
        \let\mkessler@refproof@autoref\autoref
    }{
        \let\mkessler@refproof@autoref\ref
    }
}

\newcounter{mkessler@refproof@proofdepth}
\setcounter{mkessler@refproof@proofdepth}{0}

\let\mkessler@refproof@saved@proof\proof
\let\mkessler@refproof@saved@endproof\endproof

\FSCreate{mkessler@refproof@save@claim}{-1}

%%subproof environment - essentially copied proof environment from amsthm and modified its name + symbol
\DeclareRobustCommand{\blackqed}{%
  \ifmmode \mathqed
  \else
    \leavevmode\unskip\penalty9999 \hbox{}\nobreak\hfill
    \quad\hbox{$\blacksquare$}%
  \fi
}

\newenvironment{mkessler@refproof@saved@subproof}[1][\translate{Subproof}]{\par
  \pushQED{\blackqed}%
  \normalfont \topsep6\p@\@plus6\p@\relax
  \trivlist
  \item[\hskip\labelsep
        \itshape
    #1\@addpunct{.}]\ignorespaces
}{%
  \popQED\endtrivlist\@endpefalse
}

%%%Now, we internally got a proof and a subproof environment
%%%Make them available as 'old' variants, with their defautl behaviour
\NewDocumentEnvironment{oldproof}{}
{
    \mkessler@refproof@saved@proof
}
{
    \mkessler@refproof@saved@endproof
}
\NewDocumentEnvironment{oldsubproof}{}
{
    \mkessler@refproof@saved@subproof
}
    \endmkessler@refproof@saved@subproof
{

\NewDocumentEnvironment{refproof}{s m !o}
{
    \stepcounter{mkessler@refproof@proofdepth}
    %Save the current claim counter
    \protected@edef\mkessler@refproof@dummy@expand{\arabic{claim}}
    \FSPush{mkessler@refproof@save@claim}{\mkessler@refproof@dummy@expand}
    % Restore correct counter for claims in this refproof
    \ifcsdef{themkessler@refproof@#2@save@claim}{
        \setcounter{claim}{\value{mkessler@refproof@#2@save@claim}}
        \def\mkessler@refproof@proofprefix{
            \IfBooleanTF{#1}{%
                \translate{Continuation of proof* of}%
            }{%
                \translate{Continuation of proof of}%
            }
        }
    }{
        \newcounter{mkessler@refproof@#2@save@claim}
        \setcounter{claim}{0}
        \def\mkessler@refproof@proofprefix{%
            \IfBooleanTF{#1}{%
                \translate{Proof* of}%
            }{%
                \translate{Proof of}%
            }
        }
    }
    % Set up counter number printing as subindexed by numbering of the reference
    \let\mkessler@refproof@saved@theclaim\theclaim
    \def\theclaim{\getrefnumber{#2}.\arabic{claim}}
    % Now, start the actual proof
    \mkessler@refproof@saved@proof[%
        \mkessler@refproof@proofprefix\space\mkessler@refproof@autoref{#2}%
        \IfValueT{#3}{\space(#3)}%
    ]
}
{
    \mkessler@refproof@saved@endproof % End proof
    % Save current claim counter for later restoration
    \setcounter{mkessler@refproof@#2@save@claim}{\value{claim}}
    %Restore previous claim counter
    \setcounter{claim}{\FSTop{mkessler@refproof@save@claim}}
    \FSPop{mkessler@refproof@save@claim}
    \addtocounter{mkessler@refproof@proofdepth}{-1}
   \let\theclaim\mkessler@refproof@saved@theclaim
}

%%% A 'smart' proof environment
\AtBeginDocument{
    \RenewDocumentEnvironment{proof}{!s !o}
    {
        \stepcounter{mkessler@refproof@proofdepth}
        %Save the current claim counter
        \protected@edef\mkessler@refproof@dummy@expand{\arabic{claim}}
        \FSPush{mkessler@refproof@save@claim}{\mkessler@refproof@dummy@expand}
        \setcounter{claim}{0}
        \def\theclaim{\arabic{claim}}
        \ifnum\value{mkessler@refproof@proofdepth}>1%
            \mkessler@refproof@saved@subproof[%
                \IfBooleanTF{#1}{%
                    \translate{Subproof*}%
                }{%
                    \translate{Subproof}%
                }%
                \IfValueT{#2}{\space(#2)}%
            ]
        \else%
            \mkessler@refproof@saved@proof[%
                \IfBooleanTF{#1}{%
                    \translate{Proof*}%
                }{%
                    \translate{Proof}%
                }%
                \IfValueT{#2}{\space(#2)}%
            ]
        \fi
    }
    {
        \mkessler@refproof@saved@endproof
        %Restore previous claim counter
        \setcounter{claim}{\FSTop{mkessler@refproof@save@claim}}
        \FSPop{mkessler@refproof@save@claim}
    }
}

\NewDocumentEnvironment{subproof}{!s !o}
{
    \stepcounter{mkessler@refproof@proofdepth}
    %Save the current claim counter
    \protected@edef\mkessler@refproof@dummy@expand{\arabic{claim}}
    \FSPush{mkessler@refproof@save@claim}{\mkessler@refproof@dummy@expand}
    \setcounter{claim}{0}
    \def\theclaim{\arabic{claim}}
    \mkessler@refproof@saved@subproof[%
        \IfBooleanTF{#1}{%
            \translate{Subproof*}%
        }{%
            \translate{Subproof}%
        }%
        \IfValueT{#2}{\space(#2)}%
    ]
}
{
    \mkessler@refproof@saved@endproof
    %Restore previous claim counter
    \setcounter{claim}{\FSTop{mkessler@refproof@save@claim}}
    \FSPop{mkessler@refproof@save@claim}
    \addtocounter{mkessler@refproof@proofdepth}{-1}
}

\newcommand\proofdepth{\arabic{mkessler@refproof@proofdepth}}