diff --git a/src/wip/refproofnew.pysty3 b/src/wip/refproofnew.pysty3 index 121a366..aacc999 100644 --- a/src/wip/refproofnew.pysty3 +++ b/src/wip/refproofnew.pysty3 @@ -1,38 +1,38 @@ __HEADER__(Automatic references to theorems in proofs. Claim counters within proofs) + \ExplSyntaxOn -\RequirePackage{xkeyval} \RequirePackage{amssymb} \RequirePackage{amsthm} -\RequirePackage{etoolbox} \RequirePackage{xparse} \RequirePackage{refcount} \RequirePackage{translator} +\RequirePackage{mkessler-subproof} % TODO: let PyTeX format the mkessler- prefix -\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}}} +%%%% Hook management -\cs_new:Npn__PACKAGE_MACRO__(autoref) +\cs_new:Npn__PACKAGE_MACRO__(autoref:n) { \ref } \AddToHook{package/hyperref/after} { - \cs_set:Npn__PACKAGE_MACRO__(autoref) + \cs_set:Npn__PACKAGE_MACRO__(autoref:n) { \autoref } } -\cs_new_eq:NN __PACKAGE_MACRO__(saved_proof) \proof -\cs_new_eq:NN __PACKAGE_MACRO__(saved_endproof) \endproof +%%% Saving old definitions + +\cs_new_eq:NN __PACKAGE_MACRO__(saved_proof:w) \proof +\cs_new_eq:NN __PACKAGE_MACRO__(saved_endproof:) \endproof +\cs_new_eq:NN __PACKAGE_MACRO__(saved_subproof:n) \rawsubproof +\cs_new_eq:NN __PACKAGE_MACRO__(saved_endsubproof:) \rawendsubproof + +%%% Internal variables \int_new:N __PACKAGE_MACRO__(proofdepth_int) \seq_new:N __PACKAGE_MACRO__(nested_claim_counter_values_seq) @@ -40,206 +40,204 @@ __HEADER__(Automatic references to theorems in proofs. Claim counters within pro \cs_generate_variant:Nn \seq_push:Nn { N x } -%%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 -} +%%% Language translations -\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 -} +\usedictionary{translator-proof-dictionary} %%%Now, we internally got a proof and a subproof environment %%%Make them available as 'old' variants, with their defautl behaviour -\NewDocumentEnvironment{oldproof}{} +\NewDocumentEnvironment{oldproof}{ o } { - __PACKAGE_MACRO__(saved_proof) + \IfValueTF { #1 } + { + __PACKAGE_MACRO__(saved_proof:w) { #1 } + } + { + __PACKAGE_MACRO__(saved_proof:w) + } } { - __PACKAGE_MACRO__(saved_endproof) + __PACKAGE_MACRO__(saved_endproof:) } -\NewDocumentEnvironment{oldsubproof}{} +\NewDocumentEnvironment{oldsubproof}{ o } { - \__PACKAGE_PREFIX__saved_subproof + \IfValueTF { #1 } + { + __PACKAGE_MACRO__(saved_subproof:n) { #1 } + } + { + __PACKAGE_MACRO__(saved_subproof:n) { \translate { Subproof } } + } } - \end__PACKAGE_PREFIX__saved_subproof { + __PACKAGE_MACRO__(saved_endsubproof:) +} +%%% Main implementation + +%Introduce claim environment +\newtheorem{claim}{\translate{Claim}} +\newtheorem*{claim*}{\translate{Claim}} +\AtBeginDocument{\def\claimautorefname{\translate{Claim}}} + + +\cs_new:Nn __PACKAGE_MACRO__(enter_proof:) + { + \int_gincr:N __PACKAGE_MACRO__(proofdepth_int) + \seq_gpush:Nx __PACKAGE_MACRO__(nested_claim_counter_values_seq) + { + \arabic { claim } + } + \group_begin: + } + +\cs_new:Nn __PACKAGE_MACRO__(leave_proof:) + { + \group_end: + \seq_gpop:NN __PACKAGE_MACRO__(nested_claim_counter_values_seq) \l_tmpa_tl + \setcounter { claim } { \tl_use:N \l_tmpa_tl } + \int_gdecr:N __PACKAGE_MACRO__(proofdepth_int) + } + + +% Usage: +% #1 = \BooleanTrue or \BooleanFalse indicating presence of star +% #2 = star version of translation +% #3 = nonstar version of translation +\cs_new:Nn __PACKAGE_MACRO__(set_proof_prefix:nnn) + { + \IfBooleanTF { #1 } + { + \cs_set:Nn __PACKAGE_MACRO__(proof_prefix:) + { + \translate { #2 } + } + } + { + \cs_set:Nn __PACKAGE_MACRO__(proof_prefix:) + { + \translate { #3 } + } + } + } + +\cs_new:Nn __PACKAGE_MACRO__(proof_comment:n) +{ + \IfValueT { #1 } + { + \c_space_tl ( #1 ) + } +} \NewDocumentEnvironment{refproof}{s m !o} -{ - \int_incr:N __PACKAGE_MACRO__(proofdepth_int) - %Save the current claim counter - \seq_push:Nx __PACKAGE_MACRO__(nested_claim_counter_values_seq) - { - \arabic{claim} - } - % Restore correct counter for claims in this refproof + { + __PACKAGE_MACRO__(enter_proof:) + \prop_get:NnN __PACKAGE_MACRO__(refproof_claim_counters_prop) { #2 } \l_tmpa_tl -% \tl_show:N \l_tmpa_tl -% \error + \quark_if_no_value:NTF \l_tmpa_tl { \setcounter { claim } { 0 } - \IfBooleanTF { #1 } - { - \cs_set:Nn __PACKAGE_MACRO__(proof_prefix:) - { - \translate { Proof*~of } - } - } - { - \cs_set:Nn __PACKAGE_MACRO__(proof_prefix:) - { - \translate { Proof~of } - } - } + __PACKAGE_MACRO__(set_proof_prefix:nnn) { #1 } + { Proof* ~ of } + { Proof ~ of } } { - \setcounter{claim} - { - \tl_use:N \l_tmpa_tl - } - \IfBooleanTF{#1} - { - \cs_set:Nn __PACKAGE_MACRO__(proof_prefix:) - { - \translate { Continuation~of~proof*~of } - } - } - { - \cs_set:Nn __PACKAGE_MACRO__(proof_prefix:) - { - \translate { Continuation~of~proof~of } - } - } + \setcounter { claim } { \tl_use:N \l_tmpa_tl } + __PACKAGE_MACRO__(set_proof_prefix:nnn) { #1 } + { Continuation ~ of ~ proof* ~ of } + { Continuation ~ of ~ proof ~ of } } % Set up counter number printing as subindexed by numbering of the reference - \group_begin: - \renewcommand\theclaim{\getrefnumber{#2}.\arabic{claim}} - % Now, start the actual proof - __PACKAGE_MACRO__(saved_proof) + \renewcommand \theclaim + { + \getrefnumber { #2 } . \arabic { claim } + } + __PACKAGE_MACRO__(saved_proof:w) [ __PACKAGE_MACRO__(proof_prefix:) - ~ - __PACKAGE_MACRO__(autoref) { #2 } - \IfValueT{#3} - { - \space(#3) - } + \c_space_tl + __PACKAGE_MACRO__(autoref:n) { #2 } + __PACKAGE_MACRO__(proof_comment:n) { #3 } ] -} + } { - __PACKAGE_MACRO__(saved_endproof) % End proof - \group_end: - % Save current claim counter for later restoration - \prop_put:Nnx __PACKAGE_MACRO__(refproof_claim_counters_prop) - {#2} + __PACKAGE_MACRO__(saved_endproof:) + \prop_gput:Nnx __PACKAGE_MACRO__(refproof_claim_counters_prop) + { #2 } { \value{claim} } - %Restore previous claim counter - \seq_pop:NN __PACKAGE_MACRO__(nested_claim_counter_values_seq) - \l_tmpa_tl - \setcounter{claim} - { - \tl_use:N \l_tmpa_tl - } - \int_decr:N __PACKAGE_MACRO__(proofdepth_int) + __PACKAGE_MACRO__(leave_proof:) } %%% A 'smart' proof environment \AtBeginDocument{ \RenewDocumentEnvironment{proof}{!s !o} { - \int_incr:N __PACKAGE_MACRO__(proofdepth_int) - %Save the current claim counter - \seq_push:Nx __PACKAGE_MACRO__(nested_claim_counter_values_seq) - { - \arabic{claim} - } + __PACKAGE_MACRO__(enter_proof:) + \setcounter{claim}{0} - \group_begin: - \renewcommand\theclaim{\arabic{claim}} + \renewcommand \theclaim + { + \arabic { claim } + } \int_compare:nNnTF __PACKAGE_MACRO__(proofdepth_int) > 1 { - __PACKAGE_MACRO__(saved_subproof)[% - \IfBooleanTF{#1}{% - \translate{Subproof*}% - }{% - \translate{Subproof}% - }% - \IfValueT{#2}{\space(#2)}% - ] + __PACKAGE_MACRO__(set_proof_prefix:nnn) { #1 } + { Subproof* } + { Subproof } + __PACKAGE_MACRO__(saved_subproof:n) + { + __PACKAGE_MACRO__(proof_prefix:) + __PACKAGE_MACRO__(proof_comment:n) { #2 } + } } { - __PACKAGE_MACRO__(saved_proof)[% - \IfBooleanTF{#1}{% - \translate{Proof*}% - }{% - \translate{Proof}% - }% - \IfValueT{#2}{\space(#2)}% + __PACKAGE_MACRO__(set_proof_prefix:nnn) { #1 } + { Proof* } + { Proof } + __PACKAGE_MACRO__(saved_proof:w) + [ + __PACKAGE_MACRO__(proof_prefix:) + __PACKAGE_MACRO__(proof_comment:n) { #2 } ] } } { - __PACKAGE_MACRO__(saved_endproof) - \group_end: - %Restore previous claim counter - \seq_pop:NN __PACKAGE_MACRO__(nested_claim_counter_values_seq) \l_tmpa_tl - \setcounter{claim}{\tl_use:N \l_tmpa_tl} - \int_decr:N __PACKAGE_MACRO__(proofdepth_int) + __PACKAGE_MACRO__(saved_endproof:) + __PACKAGE_MACRO__(leave_proof:) } } -\NewDocumentEnvironment{subproof}{!s !o} +\RenewDocumentEnvironment{subproof}{!s !o} { - \int_incr:N __PACKAGE_MACRO__(proofdepth_int) - %Save the current claim counter - \seq_push:Nx __PACKAGE_MACRO__(nested_claim_counter_values_seq) - { - \arabic{claim} - } - \setcounter{claim}{0} - \group_begin: - \renewcommand\theclaim{\arabic{claim}} - __PACKAGE_MACRO__(saved_subproof)[% - \IfBooleanTF{#1}{% - \translate{Subproof*}% - }{% - \translate{Subproof}% - }% - \IfValueT{#2}{\space(#2)}% - ] + __PACKAGE_MACRO__(enter_proof:) + + \setcounter { claim } { 0 } + \renewcommand \theclaim + { + \arabic { claim } + } + + __PACKAGE_MACRO__(set_proof_prefix:nnn) { #1 } + { Subproof* } + { Subproof } + __PACKAGE_MACRO__(saved_subproof:n) + { + __PACKAGE_MACRO__(proof_prefix:) + __PACKAGE_MACRO__(proof_comment:n) { #2 } + } } { - __PACKAGE_MACRO__(saved_endproof) - \group_end: - %Restore previous claim counter - \seq_pop:NN __PACKAGE_MACRO__(nested_claim_counter_values_seq) \l_tmpa_tl - \setcounter{claim}{\tl_use:N \l_tmpa_tl} - \int_decr:N __PACKAGE_MACRO__(proofdepth_int) + __PACKAGE_MACRO__(saved_endsubproof:) + __PACKAGE_MACRO__(leave_proof:) } \DeclareDocumentCommand { \proofdepth } { } diff --git a/src/wip/subproof.pysty b/src/wip/subproof.pysty index a474b12..3935204 100644 --- a/src/wip/subproof.pysty +++ b/src/wip/subproof.pysty @@ -16,25 +16,36 @@ __HEADER__(Subproof environment with black square at end of proof.) \fi } -\DeclareDocumentEnvironment{subproof}{ o } +\newcommand\rawsubproof[1] { - \IfValueTF{#1} - { - \def__PACKAGE_MACRO__(subproof@prefix){#1} - } - { - \def__PACKAGE_MACRO__(subproof@prefix){\translate{Subproof}} - } \pushQED { \blackqed - }% + }% \normalfont \topsep6\p@\@plus6\p@\relax \trivlist \item[\hskip\labelsep \itshape - __PACKAGE_MACRO__(subproof@prefix)\@addpunct{.}]\ignorespaces + #1\@addpunct{.}]\ignorespaces } + +\newcommand\rawendsubproof { \popQED\endtrivlist\@endpefalse } + + +%%subproof environment - essentially copied proof environment from amsthm and modified its name + symbol +\DeclareDocumentEnvironment{subproof}{ o } +{ + \IfValueTF{#1} + { + \rawsubproof{#1} + } + { + \rawsubproof{\translate{Subproof}} + } +} +{ + \rawendsubproof +} diff --git a/tests/wip/refproof/test.tex b/tests/wip/refproof/test.tex index 6e28be1..2c0263d 100644 --- a/tests/wip/refproof/test.tex +++ b/tests/wip/refproof/test.tex @@ -3,13 +3,17 @@ \usepackage{babel} \usepackage{mkessler-refproofnew} \usepackage{mkessler-fancythm} -\usepackage{mkessler-hypersetup} +%\usepackage{mkessler-hypersetup} \usepackage{parskip} \begin{document} \section{test} +\begin{oldsubproof}[hi] + test +\end{oldsubproof} + \begin{subproof} test \end{subproof} @@ -53,7 +57,7 @@ \begin{claim}\label{cl:qed} Der QED ist toll. \end{claim} - Um \autoref{cl:qed} zu beweisen, brauchen wir zunächst ein Lemma. + Um \ref{cl:qed} zu beweisen, brauchen wir zunächst ein Lemma. \begin{proof} \begin{claim} test @@ -93,7 +97,7 @@ Nun kommen wir wieder zurück zum eigentlichen Beweis: \begin{oldsubproof} Zu prüfen in der DB. Fakt! \end{oldsubproof} -Aus \autoref{cl:qed} und \autoref{cl:würzburg} folgt nun die Aussage. +Aus \ref{cl:qed} und \ref{cl:würzburg} folgt nun die Aussage. \end{refproof} \begin{proof}[anm]