start latex3 implementation of refproof

src/wip/refproof3.pysty3

@@ -0,0 +1,191 @@
+__HEADER__(Automatic references to theorems in proofs. Claim counters within proofs)
+
+\RequirePackage{xkeyval}
+
+__LANGUAGE_OPTIONS_X__
+
+__END_OPTIONS_X__
+
+\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__PACKAGE_MACRO__(autoref)\autoref
+    }{
+        \let__PACKAGE_MACRO__(autoref)\ref
+    }
+}
+
+\newcounter{__PACKAGE_PREFIX__proofdepth}
+\setcounter{__PACKAGE_PREFIX__proofdepth}{0}
+
+\let__PACKAGE_MACRO__(saved@proof)\proof
+\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
+\DeclareRobustCommand{\blackqed}{%
+  \ifmmode \mathqed
+  \else
+    \leavevmode\unskip\penalty9999 \hbox{}\nobreak\hfill
+    \quad\hbox{$\blacksquare$}%
+  \fi
+}
+
+\newenvironment{__PACKAGE_PREFIX__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}{}
+{
+    __PACKAGE_MACRO__(saved@proof)
+}
+{
+    __PACKAGE_MACRO__(saved@endproof)
+}
+\NewDocumentEnvironment{oldsubproof}{}
+{
+    \__PACKAGE_PREFIX__saved@subproof
+}
+    \end__PACKAGE_PREFIX__saved@subproof
+{
+
+\NewDocumentEnvironment{refproof}{s m !o}
+{
+    \stepcounter{__PACKAGE_PREFIX__proofdepth}
+    %Save the current claim counter
+    \protected@edef__PACKAGE_MACRO__(dummy@expand){\arabic{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}{
+        \setcounter{claim}{\value{__PACKAGE_PREFIX__#2@save@claim}}
+        \def__PACKAGE_MACRO__(proofprefix){
+            \IfBooleanTF{#1}{%
+                \translate{Continuation of proof* of}%
+            }{%
+                \translate{Continuation of proof of}%
+            }
+        }
+    }{
+        \newcounter{__PACKAGE_PREFIX__#2@save@claim}
+        \setcounter{claim}{0}
+        \def__PACKAGE_MACRO__(proofprefix){%
+            \IfBooleanTF{#1}{%
+                \translate{Proof* of}%
+            }{%
+                \translate{Proof of}%
+            }
+        }
+    }
+    % Set up counter number printing as subindexed by numbering of the reference
+    \let__PACKAGE_MACRO__(saved@theclaim)\theclaim
+    \def\theclaim{\getrefnumber{#2}.\arabic{claim}}
+    % Now, start the actual proof
+    __PACKAGE_MACRO__(saved@proof)[%
+        __PACKAGE_MACRO__(proofprefix)\space__PACKAGE_MACRO__(autoref){#2}%
+        \IfValueT{#3}{\space(#3)}%
+    ]
+}
+{
+    __PACKAGE_MACRO__(saved@endproof) % End proof
+    % Save current claim counter for later restoration
+    \setcounter{__PACKAGE_PREFIX__#2@save@claim}{\value{claim}}
+    %Restore previous claim counter
+    \setcounter{claim}{\FSTop{__PACKAGE_PREFIX__save@claim}}
+    \FSPop{__PACKAGE_PREFIX__save@claim}
+    \addtocounter{__PACKAGE_PREFIX__proofdepth}{-1}
+    \let\theclaim__PACKAGE_MACRO__(saved@theclaim)
+}
+
+%%% A 'smart' proof environment
+\AtBeginDocument{
+    \RenewDocumentEnvironment{proof}{!s !o}
+    {
+        \stepcounter{__PACKAGE_PREFIX__proofdepth}
+        %Save the current claim counter
+        \protected@edef__PACKAGE_MACRO__(dummy@expand){\arabic{claim}}
+        \FSPush{__PACKAGE_PREFIX__save@claim}{__PACKAGE_MACRO__(dummy@expand)}
+        \setcounter{claim}{0}
+        \let__PACKAGE_MACRO__(saved@theclaim)\theclaim
+        \def\theclaim{\arabic{claim}}
+        \ifnum\value{__PACKAGE_PREFIX__proofdepth}>1%
+            __PACKAGE_MACRO__(saved@subproof)[%
+                \IfBooleanTF{#1}{%
+                    \translate{Subproof*}%
+                }{%
+                    \translate{Subproof}%
+                }%
+                \IfValueT{#2}{\space(#2)}%
+            ]
+        \else%
+            __PACKAGE_MACRO__(saved@proof)[%
+                \IfBooleanTF{#1}{%
+                    \translate{Proof*}%
+                }{%
+                    \translate{Proof}%
+                }%
+                \IfValueT{#2}{\space(#2)}%
+            ]
+        \fi
+    }
+    {
+        __PACKAGE_MACRO__(saved@endproof)
+        %Restore previous claim counter
+        \setcounter{claim}{\FSTop{__PACKAGE_PREFIX__save@claim}}
+        \FSPop{__PACKAGE_PREFIX__save@claim}
+        \addtocounter{__PACKAGE_PREFIX__proofdepth}{-1}
+        \let\theclaim__PACKAGE_MACRO__(saved@theclaim)
+    }
+}
+
+\NewDocumentEnvironment{subproof}{!s !o}
+{
+    \stepcounter{__PACKAGE_PREFIX__proofdepth}
+    %Save the current claim counter
+    \protected@edef__PACKAGE_MACRO__(dummy@expand){\arabic{claim}}
+    \FSPush{__PACKAGE_PREFIX__save@claim}{__PACKAGE_MACRO__(dummy@expand)}
+    \setcounter{claim}{0}
+    \def\theclaim{\arabic{claim}}
+    __PACKAGE_MACRO__(saved@subproof)[%
+        \IfBooleanTF{#1}{%
+            \translate{Subproof*}%
+        }{%
+            \translate{Subproof}%
+        }%
+        \IfValueT{#2}{\space(#2)}%
+    ]
+}
+{
+    __PACKAGE_MACRO__(saved@endproof)
+    %Restore previous claim counter
+    \setcounter{claim}{\FSTop{__PACKAGE_PREFIX__save@claim}}
+    \FSPop{__PACKAGE_PREFIX__save@claim}
+    \addtocounter{__PACKAGE_PREFIX__proofdepth}{-1}
+}
+
+\newcommand\proofdepth{\arabic{__PACKAGE_PREFIX__proofdepth}}

tests/wip/refproof/Makefile

@@ -0,0 +1 @@
+../../COMPILE_MAKEFILE

tests/wip/refproof/test.tex

@@ -0,0 +1,128 @@
+\documentclass[ngerman]{article}
+
+\usepackage{babel}
+\usepackage{mkessler-refproof3}
+\usepackage{mkessler-fancythm}
+\usepackage{mkessler-hypersetup}
+\usepackage{parskip}
+
+\begin{document}
+\section{test}
+
+
+\begin{subproof}
+    test
+\end{subproof}
+
+\begin{subproof}*[hi]
+    test
+\end{subproof}
+
+\begin{proof}
+    Beginn des Beweises:
+    \begin{proof}*
+        Ein unterbeweis
+    \end{proof}
+    Jetzt sind wir fertig.
+\end{proof}
+
+\begin{theorem}\label{thm:krass}
+    Man sollte nach Würzburg fahren.
+\end{theorem}
+
+\begin{claim}
+    test
+\end{claim}
+
+\begin{proof}
+    \begin{claim}
+        hi
+    \end{claim}
+    \begin{proof}
+    \end{proof}
+    \begin{claim}
+        
+    \end{claim}
+\end{proof}
+
+\begin{claim}
+    test
+\end{claim}
+
+\begin{refproof}*{thm:krass}[hi]
+    \begin{claim}\label{cl:qed}
+       Der QED ist toll.
+   \end{claim}
+   Um \autoref{cl:qed} zu beweisen, brauchen wir zunächst ein Lemma. 
+   \begin{proof}
+       \begin{claim}
+           test
+       \end{claim}
+       hi
+       \proofdepth
+   \end{proof}
+   \begin{claim}
+       hi
+   \end{claim}
+\end{refproof}
+
+\begin{claim}
+    next
+\end{claim}
+
+\begin{lemma}\label{lm:krass}
+    Mathevereine sind krass.
+\end{lemma}
+
+\begin{refproof}{lm:krass}[quasi ein Fakt]
+    \begin{claim}
+        Mathe ist cool.
+    \end{claim}
+    \begin{oldsubproof}
+        trivial.
+    \end{oldsubproof}
+    Damit folgt nun das Lemma.
+\end{refproof}
+
+Nun kommen wir wieder zurück zum eigentlichen Beweis:
+
+\begin{refproof}{thm:krass}[hi]
+    \begin{claim}\label{cl:würzburg}
+        Der QED macht ein Seminar in Würzburg
+    \end{claim}
+    \begin{oldsubproof}
+        Zu prüfen in der DB. Fakt!
+    \end{oldsubproof}
+Aus \autoref{cl:qed}   und \autoref{cl:würzburg} folgt nun die Aussage. 
+\end{refproof}
+
+\begin{proof}[anm]
+    second
+\end{proof}
+\begin{proof}
+    first
+\end{proof}
+\begin{proof}*
+    third
+\end{proof}
+\begin{proof}*[anm]
+    fourth
+\end{proof}
+
+\begin{oldproof}
+    test
+\end{oldproof}
+
+\def\four{4}
+
+\def\foo{1}
+{\def\foo{2}\foo}
+{\let\foo\four\foo}
+\foo
+
+\begin{proof}
+    \def\foo{5}\foo
+\end{proof}
+\foo
+
+\end{document}