fix refproof bugs: correct restoring of counter values and claim style numberings in stacked proofs

This commit is contained in:
Maximilian Keßler 2022-01-09 21:45:25 +01:00
parent 47449c57cb
commit c0e4705c63

View file

@ -12,6 +12,7 @@ __END_OPTIONS_X__
\RequirePackage{xparse} \RequirePackage{xparse}
\RequirePackage{refcount} \RequirePackage{refcount}
\RequirePackage{translator} \RequirePackage{translator}
\RequirePackage{fifo-stack}
\usedictionary{translator-proof-dictionary} \usedictionary{translator-proof-dictionary}
@ -32,12 +33,12 @@ __END_OPTIONS_X__
\newcounter{__PACKAGE_PREFIX__proofdepth} \newcounter{__PACKAGE_PREFIX__proofdepth}
\setcounter{__PACKAGE_PREFIX__proofdepth}{0} \setcounter{__PACKAGE_PREFIX__proofdepth}{0}
\newcounter{__PACKAGE_PREFIX__save@claim}
\setcounter{__PACKAGE_PREFIX__save@claim}{0}
\let__PACKAGE_MACRO__(saved@proof)\proof \let__PACKAGE_MACRO__(saved@proof)\proof
\let__PACKAGE_MACRO__(saved@endproof)\endproof \let__PACKAGE_MACRO__(saved@endproof)\endproof
\FSCreate{__PACKAGE_PREFIX__save@claim}{-1}
%%subproof environment - essentially copied proof environment from amsthm and modified its name + symbol %%subproof environment - essentially copied proof environment from amsthm and modified its name + symbol
\DeclareRobustCommand{\blackqed}{% \DeclareRobustCommand{\blackqed}{%
\ifmmode \mathqed \ifmmode \mathqed
@ -78,8 +79,9 @@ __END_OPTIONS_X__
{ {
\stepcounter{__PACKAGE_PREFIX__proofdepth} \stepcounter{__PACKAGE_PREFIX__proofdepth}
%Save the current claim counter %Save the current claim counter
\setcounter{__PACKAGE_PREFIX__save@claim}{\value{claim}} \protected@edef__PACKAGE_MACRO__(dummy@expand){\arabic{claim}}
% Restore correct counter for claim \FSPush{__PACKAGE_PREFIX__save@claim}{__PACKAGE_MACRO__(dummy@expand)}
% Restore correct counter for claims in this refproof
\ifcsdef{the__PACKAGE_PREFIX__#2@save@claim}{ \ifcsdef{the__PACKAGE_PREFIX__#2@save@claim}{
\setcounter{claim}{\value{__PACKAGE_PREFIX__#2@save@claim}} \setcounter{claim}{\value{__PACKAGE_PREFIX__#2@save@claim}}
\def__PACKAGE_MACRO__(proofprefix){ \def__PACKAGE_MACRO__(proofprefix){
@ -101,6 +103,7 @@ __END_OPTIONS_X__
} }
} }
% Set up counter number printing as subindexed by numbering of the reference % Set up counter number printing as subindexed by numbering of the reference
\let__PACKAGE_MACRO__(saved@theclaim)\theclaim
\def\theclaim{\getrefnumber{#2}.\arabic{claim}} \def\theclaim{\getrefnumber{#2}.\arabic{claim}}
% Now, start the actual proof % Now, start the actual proof
__PACKAGE_MACRO__(saved@proof)[% __PACKAGE_MACRO__(saved@proof)[%
@ -113,8 +116,10 @@ __END_OPTIONS_X__
% Save current claim counter for later restoration % Save current claim counter for later restoration
\setcounter{__PACKAGE_PREFIX__#2@save@claim}{\value{claim}} \setcounter{__PACKAGE_PREFIX__#2@save@claim}{\value{claim}}
%Restore previous claim counter %Restore previous claim counter
\setcounter{claim}{\value{__PACKAGE_PREFIX__save@claim}} \setcounter{claim}{\FSTop{__PACKAGE_PREFIX__save@claim}}
\FSPop{__PACKAGE_PREFIX__save@claim}
\addtocounter{__PACKAGE_PREFIX__proofdepth}{-1} \addtocounter{__PACKAGE_PREFIX__proofdepth}{-1}
\let\theclaim__PACKAGE_MACRO__(saved@theclaim)
} }
\def\proofdepth{Depth:~\the__PACKAGE_PREFIX__proofdepth} \def\proofdepth{Depth:~\the__PACKAGE_PREFIX__proofdepth}
@ -125,7 +130,8 @@ __END_OPTIONS_X__
{ {
\stepcounter{__PACKAGE_PREFIX__proofdepth} \stepcounter{__PACKAGE_PREFIX__proofdepth}
%Save the current claim counter %Save the current claim counter
\setcounter{__PACKAGE_PREFIX__save@claim}{\value{claim}} \protected@edef__PACKAGE_MACRO__(dummy@expand){\arabic{claim}}
\FSPush{__PACKAGE_PREFIX__save@claim}{__PACKAGE_MACRO__(dummy@expand)}
\setcounter{claim}{0} \setcounter{claim}{0}
\def\theclaim{\arabic{claim}} \def\theclaim{\arabic{claim}}
\ifnum\value{__PACKAGE_PREFIX__proofdepth}>1% \ifnum\value{__PACKAGE_PREFIX__proofdepth}>1%
@ -151,8 +157,8 @@ __END_OPTIONS_X__
{ {
__PACKAGE_MACRO__(saved@endproof) __PACKAGE_MACRO__(saved@endproof)
%Restore previous claim counter %Restore previous claim counter
\setcounter{claim}{\value{__PACKAGE_PREFIX__save@claim}} \setcounter{claim}{\FSTop{__PACKAGE_PREFIX__save@claim}}
\addtocounter{__PACKAGE_PREFIX__proofdepth}{-1} \FSPop{__PACKAGE_PREFIX__save@claim}
} }
} }