summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/tex/latex/stex/stex.sty
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2022-09-14 19:58:16 +0000
committerKarl Berry <karl@freefriends.org>2022-09-14 19:58:16 +0000
commit17b3bbda651c5296c1e222bb44b6a1d348a737bd (patch)
treee895b9d34f6ca6723d2b106d94fd0b334d31a9a4 /Master/texmf-dist/tex/latex/stex/stex.sty
parent732ae3fbb7543a76e6ed337dcc853e4dec34efbb (diff)
stex (14sep22)
git-svn-id: svn://tug.org/texlive/trunk@64383 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/tex/latex/stex/stex.sty')
-rw-r--r--Master/texmf-dist/tex/latex/stex/stex.sty1460
1 files changed, 920 insertions, 540 deletions
diff --git a/Master/texmf-dist/tex/latex/stex/stex.sty b/Master/texmf-dist/tex/latex/stex/stex.sty
index c4af84bc87b..3f23bb2557e 100644
--- a/Master/texmf-dist/tex/latex/stex/stex.sty
+++ b/Master/texmf-dist/tex/latex/stex/stex.sty
@@ -21,14 +21,14 @@
%%%%%%%%%%%%% basics.dtx %%%%%%%%%%%%%
\RequirePackage{expl3,l3keys2e,ltxcmds}
-\ProvidesExplPackage{stex}{2022/05/24}{3.1.0}{sTeX package}
+\ProvidesExplPackage{stex}{2022/09/14}{3.2.0}{sTeX package}
\bool_if_exist:NF \c_stex_document_class_bool {
\bool_set_false:N \c_stex_document_class_bool
\RequirePackage{standalone}
}
-\message{^^J*~This~is~sTeX~version~3.1.0~*^^J}
+\message{^^J*~This~is~sTeX~version~3.2.0~*^^J}
\keys_define:nn { stex } {
@@ -71,7 +71,7 @@
\msg_redirect_module:nnn{ stex }{ none }{ term }
}{
\clist_map_inline:Nn \c_stex_debug_clist {
- \msg_redirect_name:nnn{ stex }{ debug / ##1 }{ term }
+ \msg_redirect_name:nnn{ stex }{ debug / #1 }{ term }
}
}
@@ -100,14 +100,26 @@
}
}
}
+\ifcsname if@rustex\endcsname\else
+ \expandafter\newif\csname if@rustex\endcsname
+ \@rustexfalse
+\fi
+\ifcsname if@latexml\endcsname\else
+ \expandafter\newif\csname if@latexml\endcsname
+ \@latexmlfalse
+\fi
\tl_if_exist:NF\stex@backend{
- \ifcsname if@rustex\endcsname
+ \if@rustex
\def\stex@backend{rustex}
\else
- \ifcsname if@latexml\endcsname
+ \if@latexml
\def\stex@backend{latexml}
\else
- \def\stex@backend{pdflatex}
+ \cs_if_exist:NTF\HCode{
+ \def\stex@backend{tex4ht}
+ }{
+ \def\stex@backend{pdflatex}
+ }
\fi
\fi
}
@@ -192,6 +204,7 @@
}
}
}
+
\bool_if:NTF \c_stex_persist_mode_bool {
\def \stex_persist:n #1 {}
\def \stex_persist:x #1 {}
@@ -360,6 +373,7 @@
\detokenize{#1}~found~two~candidates~for~#2
}
\cs_new_protected:Nn \stex_path_from_string:Nn {
+ \stex_debug:nn{files}{#2}
\str_set:Nx \l_tmpa_str { #2 }
\str_if_empty:NTF \l_tmpa_str {
\seq_clear:N #1
@@ -375,6 +389,7 @@
}
\stex_path_canonicalize:N #1
}
+ \stex_debug:nn{files}{Yields: \stex_path_to_string:N#1}
}
\cs_new_protected:Nn \stex_path_to_string:NN {
@@ -476,6 +491,7 @@
}
\seq_gset_eq:NN\g_stex_currentfile_seq\g_stex_currentfile_seq
\exp_args:NNo\seq_gpush:Nn\g__stex_files_stack\g_stex_currentfile_seq
+ \stex_get_document_uri:
}
\cs_new_protected:Nn \stex_filestack_pop: {
\seq_if_empty:NF\g__stex_files_stack{
@@ -487,9 +503,14 @@
\seq_get:NN\g__stex_files_stack\l_tmpa_seq
\seq_gset_eq:NN\g_stex_currentfile_seq\l_tmpa_seq
}
+ \stex_get_document_uri:
}
\AddToHook{file/before}{
- \stex_filestack_push:n{\CurrentFilePath/\CurrentFile}
+ \tl_if_empty:NTF\CurrentFilePath{
+ \stex_filestack_push:n{\CurrentFile}
+ }{
+ \stex_filestack_push:n{\CurrentFilePath/\CurrentFile}
+ }
}
\AddToHook{file/after}{
\stex_filestack_pop:
@@ -499,6 +520,7 @@
\begingroup\escapechar=-1\catcode`\\=12
\exp_args:Nx\stex_kpsewhich:n{-expand-var~\c_percent_str MATHHUB\c_percent_str}
\exp_args:NNx\str_replace_all:Nnn\l_stex_kpsewhich_return_str{\c_backslash_str}/
+ \exp_args:NNx\str_if_eq:onT\l_stex_kpsewhich_return_str{\c_percent_str MATHHUB\c_percent_str}{\str_clear:N\l_stex_kpsewhich_return_str}
\exp_args:Nnx\use:nn{\endgroup}{\str_set:Nn\exp_not:N\l_stex_kpsewhich_return_str{\l_stex_kpsewhich_return_str}}
}{
\stex_kpsewhich:n{-var-value~MATHHUB}
@@ -514,15 +536,15 @@
}{
\stex_kpsewhich:n{-var-value~HOME}
}
- \ior_open:NnT \l_tmpa_ior{\l_stex_kpsewhich_return_str / .stex / mathhub.path}{
+ \ior_open:NnT \g_tmpa_ior{\l_stex_kpsewhich_return_str / .stex / mathhub.path}{
\begingroup\escapechar=-1\catcode`\\=12
- \ior_str_get:NN \l_tmpa_ior \l_tmpa_str
+ \ior_str_get:NN \g_tmpa_ior \l_tmpa_str
\sys_if_platform_windows:T{
\exp_args:NNx\str_replace_all:Nnn\l_tmpa_str{\c_backslash_str}/
}
\str_gset_eq:NN \c_stex_mathhub_str\l_tmpa_str
\endgroup
- \ior_close:N \l_tmpa_ior
+ \ior_close:N \g_tmpa_ior
}
}
\str_if_empty:NTF\c_stex_mathhub_str{
@@ -871,17 +893,23 @@
}
-%%%%%%%%%%%%% references.dtx %%%%%%%%%%%%%
-
+%%%%%%%%%%%%% stex-references.dtx %%%%%%%%%%%%%
+\msg_new:nnn{stex}{error/extrefmissing}{
+ Missing~in~or~cite~value~for~\detokenize{\extref}!
+}
+\msg_new:nnn{stex}{warning/smsmissing}{
+ .sref~file~#1~doesn't~exist!
+}
+\msg_new:nnn{stex}{warning/smslabelmissing}{
+ No~label~#2~in~.sref~file~#1!
+}
+\iow_new:N \c__stex_refs_refs_iow
\AtBeginDocument{
+ \iow_open:Nn \c__stex_refs_refs_iow {\jobname.sref}
}
\AtEndDocument{
-}
-\str_set:Nn \g__stex_refs_title_tl {Unnamed~Document}
-
-\NewDocumentCommand \STEXreftitle { m } {
- \tl_gset:Nx \g__stex_refs_title_tl { #1 }
+ \iow_close:N \c__stex_refs_refs_iow
}
\str_new:N \l_stex_current_docns_str
\cs_new_protected:Nn \stex_get_document_uri: {
@@ -916,13 +944,14 @@
}
\seq_if_empty:NTF \l_tmpa_seq {
- \str_set_eq:NN \l_stex_current_docns_str \l_tmpa_str
+ \str_gset_eq:NN \l_stex_current_docns_str \l_tmpa_str
}{
- \str_set:Nx \l_stex_current_docns_str {
+ \str_gset:Nx \l_stex_current_docns_str {
\l_tmpa_str/\stex_path_to_string:N \l_tmpa_seq
}
}
}
+ %\stex_get_document_url:
}
\str_new:N \l_stex_current_docurl_str
\cs_new_protected:Nn \stex_get_document_url: {
@@ -971,190 +1000,361 @@
\str_const:Nn \c__stex_refs_ref_str{REF}
\str_new:N \l__stex_refs_curr_label_str
\int_new:N \l__stex_refs_unnamed_counter_int
+\cs_new_protected:Npn \STEXInternalSrefRestoreTarget #1#2#3#4#5 {}
+\seq_new:N \g_stex_ref_files_seq
+
\cs_new_protected:Nn \stex_ref_new_doc_target:n {
- \stex_get_document_uri:
+ %\stex_get_document_uri:
\str_clear:N \l__stex_refs_curr_label_str
\str_set:Nx \l_tmpa_str { #1 }
\str_if_empty:NT \l_tmpa_str {
- \int_incr:N \l__stex_refs_unnamed_counter_int
+ \int_gincr:N \l__stex_refs_unnamed_counter_int
\str_set:Nx \l_tmpa_str {REF\int_use:N \l__stex_refs_unnamed_counter_int}
}
\str_set:Nx \l__stex_refs_curr_label_str {
\l_stex_current_docns_str?\l_tmpa_str
}
- \seq_if_exist:cF{g__stex_refs_labels_\l_tmpa_str _seq}{
- \seq_new:c {g__stex_refs_labels_\l_tmpa_str _seq}
- }
- \seq_if_in:coF{g__stex_refs_labels_\l_tmpa_str _seq}\l__stex_refs_curr_label_str {
- \seq_gput_right:co{g__stex_refs_labels_\l_tmpa_str _seq}\l__stex_refs_curr_label_str
- }
+
+ \exp_args:Noo \STEXInternalAuxAddDocRef\l_stex_current_docns_str\l_tmpa_str
+
+ %\seq_if_exist:cF{g__stex_refs_labels_\l_tmpa_str _seq}{
+ % \seq_new:c {g__stex_refs_labels_\l_tmpa_str _seq}
+ %}
+ %\seq_if_in:coF{g__stex_refs_labels_\l_tmpa_str _seq}\l__stex_refs_curr_label_str {
+ % \seq_gput_right:co{g__stex_refs_labels_\l_tmpa_str _seq}\l__stex_refs_curr_label_str
+ %}
+
\stex_if_smsmode:TF {
- \stex_get_document_url:
- \str_gset_eq:cN {sref_url_\l__stex_refs_curr_label_str _str}\l_stex_current_docurl_str
- \str_gset_eq:cN {sref_\l__stex_refs_curr_label_str _type}\c__stex_refs_url_str
+ %\stex_get_document_url:
+ %\str_gset_eq:cN {sref_url_\l__stex_refs_curr_label_str _str}\l_stex_current_docurl_str
+ %\str_gset_eq:cN {sref_\l__stex_refs_curr_label_str _type}\c__stex_refs_url_str
}{
- %\iow_now:Nx \c__stex_refs_refs_iow { \l_tmpa_str~=~\expandafter\unexpanded\expandafter{\@currentlabel}~in~\exp_args:No\unexpanded\g__stex_refs_title_tl,}
+ \iow_now:Nx \c__stex_refs_refs_iow {
+ \STEXInternalSrefRestoreTarget
+ {\l_stex_current_docns_str}
+ {\l_tmpa_str}
+ {\@currentcounter}
+ {\@currentlabel}
+ {\tl_if_exist:NT\@currentlabelname{\exp_args:No\unexpanded\@currentlabelname}}
+ }
+ %\iow_now:Nx \c__stex_refs_refs_iow {
+ % {\l_stex_current_docns_str?\l_tmpa_str}~=~{{\use:c{\@currentcounter autorefname}~\@currentlabel}~(\@currentlabelname)~in~\exp_args:No\unexpanded\g__stex_refs_title_tl},}
+ \stex_debug:nn{sref}{New~label~\l__stex_refs_curr_label_str~at~\use:c{\use:c{@currentcounter}autorefname}}
\exp_args:Nx\label{sref_\l__stex_refs_curr_label_str}
- \immediate\write\@auxout{\stexauxadddocref{\l_stex_current_docns_str}{\l_tmpa_str}}
- \str_gset:cx {sref_\l__stex_refs_curr_label_str _type}\c__stex_refs_ref_str
+ \immediate\write\@auxout{\STEXInternalAuxAddDocRef{\l_stex_current_docns_str}{\l_tmpa_str}}
+ %\str_gset:cx {sref_\l__stex_refs_curr_label_str _type}\c__stex_refs_ref_str
}
}
-\cs_new_protected:Npn \stexauxadddocref #1 #2 {
- \str_set:Nn \l_tmpa_str {#1?#2}
- \str_gset_eq:cN{sref_#1?#2_type}\c__stex_refs_ref_str
- \seq_if_exist:cF{g__stex_refs_labels_#2_seq}{
- \seq_new:c {g__stex_refs_labels_#2_seq}
- }
- \seq_if_in:coF{g__stex_refs_labels_#2_seq}\l_tmpa_str {
- \seq_gput_right:co{g__stex_refs_labels_#2_seq}\l_tmpa_str
- }
+\NewDocumentCommand \slabel {m} {\stex_ref_new_doc_target:n {#1}}
+\cs_new_protected:Npn \STEXInternalAuxAddDocRef #1 #2 {
+ \exp_args:NNx \seq_if_in:NnTF \g_stex_ref_files_seq {\detokenize{#1}} {
+ \exp_args:Nnx \seq_if_in:cnF{g_stex_ref_ #1 _seq}{\detokenize{#2}}{
+ \exp_args:Nnx \seq_gput_left:cn{g_stex_ref_ #1 _seq}{\detokenize{#2}}
+ }
+ }{
+ \exp_args:NNx \seq_gput_right:Nn \g_stex_ref_files_seq {\detokenize{#1}}
+ %\seq_if_exist:cF{g_stex_ref_ #1 _seq}{
+ \seq_new:c{g_stex_ref_ #1 _seq} % <- seq_new throws errors??
+ %}
+ \exp_args:Nnx \seq_gput_left:cn{g_stex_ref_ #1 _seq}{\detokenize{#2}}
+ }
+
+ %\str_set:Nn \l_tmpa_str {#1?#2}
+ %\str_gset_eq:cN{sref_#1?#2_type}\c__stex_refs_ref_str
+ %\seq_if_exist:cF{g__stex_refs_labels_#2_seq}{
+ % \seq_new:c {g__stex_refs_labels_#2_seq}
+ %}
+ %\seq_if_in:coF{g__stex_refs_labels_#2_seq}\l_tmpa_str {
+ % \seq_gput_right:co{g__stex_refs_labels_#2_seq}\l_tmpa_str
+ %}
}
\AtEndDocument{
- \def\stexauxadddocref#1 #2 {}{}
+ \def\STEXInternalAuxAddDocRef#1 #2 {}{}
}
\cs_new_protected:Nn \stex_ref_new_sym_target:n {
- \stex_if_smsmode:TF {
- \str_if_exist:cF{sref_sym_#1_type}{
- \stex_get_document_url:
- \str_gset_eq:cN {sref_sym_url_#1_str}\l_stex_current_docurl_str
- \str_gset_eq:cN {sref_sym_#1_type}\c__stex_refs_url_str
- }
- }{
- \str_if_empty:NF \l__stex_refs_curr_label_str {
- \str_gset_eq:cN {sref_sym_#1_label_str}\l__stex_refs_curr_label_str
- \immediate\write\@auxout{
- \exp_not:N\expandafter\def\exp_not:N\csname \exp_not:N\detokenize{sref_sym_#1_label_str}\exp_not:N\endcsname{
- \l__stex_refs_curr_label_str
- }
- }
- }
- }
+
}
-\str_new:N \l__stex_refs_indocument_str
-\keys_define:nn { stex / sref } {
- linktext .tl_set:N = \l__stex_refs_linktext_tl ,
- fallback .tl_set:N = \l__stex_refs_fallback_tl ,
- pre .tl_set:N = \l__stex_refs_pre_tl ,
- post .tl_set:N = \l__stex_refs_post_tl ,
+\keys_define:nn { stex / sref / 1 } {
+ archive .str_set_x:N = \l__stex_refs_repo_str,
+ file .str_set_x:N = \l__stex_refs_file_str,
+ % TODO get rid of this
+ fallback .code:n = {},
+ pre .code:n = {},
+ post .code:n = {}
}
-\cs_new_protected:Nn \__stex_refs_args:n {
- \tl_clear:N \l__stex_refs_linktext_tl
- \tl_clear:N \l__stex_refs_fallback_tl
- \tl_clear:N \l__stex_refs_pre_tl
- \tl_clear:N \l__stex_refs_post_tl
+\cs_new_protected:Nn \__stex_refs_args_i:n {
\str_clear:N \l__stex_refs_repo_str
- \keys_set:nn { stex / sref } { #1 }
-}
-\NewDocumentCommand \sref { O{} m}{
- \__stex_refs_args:n { #1 }
- \str_if_empty:NTF \l__stex_refs_indocument_str {
- \str_set:Nx \l_tmpa_str { #2 }
- \exp_args:NNno \seq_set_split:Nnn \l_tmpa_seq ? \l_tmpa_str
- \int_compare:nNnTF {\seq_count:N \l_tmpa_seq} = 1 {
- \seq_if_exist:cTF{g__stex_refs_labels_\l_tmpa_str _seq}{
- \seq_get_left:cNF {g__stex_refs_labels_\l_tmpa_str _seq} \l_tmpa_str {
- \str_clear:N \l_tmpa_str
+ \str_clear:N \l__stex_refs_file_str
+ \keys_set:nn { stex / sref / 1 } { #1 }
+}
+\keys_define:nn { stex / sref / 2 } {
+ in .str_set_x:N = \l__stex_refs_in_str,
+ archive .str_set_x:N = \l__stex_refs_repob_str,
+ title .tl_set:N = \l__stex_refs_title_tl
+}
+\cs_new_protected:Nn \__stex_refs_args_ii:n {
+ \str_clear:N \l__stex_refs_in_str
+ \tl_clear:N \l__stex_refs_title_tl
+ \str_clear:N \l__stex_refs_repob_str
+ \keys_set:nn { stex / sref / 2 } { #1 }
+}
+\NewDocumentCommand \sref { O{} m O{}}{
+ \__stex_refs_args_i:n{#1}
+ \__stex_refs_args_ii:n{#3}
+ \str_clear:N \l__stex_refs_uri_str
+ \__stex_refs_find_uri:n{#2}
+ \__stex_refs_do_sref:n{#2}
+}
+\NewDocumentCommand \extref { O{} m m}{
+ \__stex_refs_args_i:n{#1}
+ \__stex_refs_args_ii:n{#3}
+ \str_if_empty:NT \l__stex_refs_in_str {
+ \msg_error:nn{stex}{error/extrefmissing}
+ }
+ \str_clear:N \l__stex_refs_uri_str
+ \__stex_refs_find_uri:n{#2}
+ \__stex_refs_do_sref_in:n{#2}
+}
+
+\cs_new_protected:Nn \__stex_refs_find_uri:n {
+ \stex_debug:nn{sref}{File:~\l__stex_refs_file_str^^JRepo:\l__stex_refs_repo_str}
+ \str_if_empty:NTF \l__stex_refs_file_str {
+ \stex_debug:nn{sref}{Empty.~Checking~current~file~for~#1}
+ \seq_if_exist:cT{g_stex_ref_\l_stex_current_docns_str _seq}{
+ \seq_map_inline:cn{g_stex_ref_\l_stex_current_docns_str _seq}{
+ \str_if_eq:nnT{#1}{##1}{
+ \str_set_eq:NN \l__stex_refs_uri_str \l_stex_current_docns_str
+ \stex_debug:nn{sref}{Found.}
+ \seq_map_break:
}
- }{
- \str_clear:N \l_tmpa_str
}
- }{
- \seq_pop_left:NN \l_tmpa_seq \l_tmpb_str
- \seq_pop_right:NN \l_tmpa_seq \l_tmpa_str
- \int_set:Nn \l_tmpa_int { \exp_args:Ne \str_count:n {\l_tmpb_str?\l_tmpa_str} }
- \seq_if_exist:cTF{g__stex_refs_labels_\l_tmpa_str _seq}{
- \str_set_eq:NN \l_tmpc_str \l_tmpa_str
- \str_clear:N \l_tmpa_str
- \seq_map_inline:cn {g__stex_refs_labels_\l_tmpc_str _seq} {
- \str_if_eq:eeT { \l_tmpb_str?\l_tmpc_str }{
- \str_range:nnn { ##1 }{ -\l_tmpa_int}{ -1 }
- }{
- \seq_map_break:n {
- \str_set:Nn \l_tmpa_str { ##1 }
- }
+ }
+ \str_if_empty:NT \l__stex_refs_uri_str {
+ \stex_debug:nn{sref}{Checking~other~files}
+ \seq_map_inline:Nn \g_stex_ref_files_seq {
+ \stex_debug:nn{sref}{##1...}
+ \seq_map_inline:cn{g_stex_ref_##1_seq}{
+ \str_if_eq:nnT{#1}{####1}{
+ \stex_debug:nn{sref}{Found~##1}
+ \str_set:Nn \l__stex_refs_uri_str {##1}
+ \seq_map_break:n{\seq_map_break:}
}
}
+ }
+ }
+ }{
+ \str_if_empty:NTF \l__stex_refs_repo_str {
+ \prop_if_exist:NTF \l_stex_current_repository_prop {
+ \prop_get:NnN \l_stex_current_repository_prop { ns } \l__stex_refs_uri_str
+ \str_set:Nx \l__stex_refs_uri_str {\l__stex_refs_uri_str / \l__stex_refs_file_str}
+ \stex_path_from_string:Nn \l_tmpb_seq \l__stex_refs_uri_str
+ \str_set:Nx \l__stex_refs_uri_str {\stex_path_to_string:N \l_tmpb_seq}
}{
- \str_clear:N \l_tmpa_str
+ \stex_path_from_string:Nn \l_tmpb_seq {
+ \stex_path_to_string:N \g_stex_currentfile_seq/ .. / \l__stex_refs_file_str
+ }
+ \str_set:Nx \l__stex_refs_uri_str {file:/\stex_path_to_string:N \l_tmpb_seq}
}
+ }{
+ \stex_require_repository:n \l__stex_refs_repo_str
+ \prop_get:cnN { c_stex_mathhub_\l__stex_refs_repo_str _manifest_prop } { ns } \l__stex_refs_uri_str
+ \str_set:Nx \l__stex_refs_uri_str {\l__stex_refs_uri_str / \l__stex_refs_file_str}
+ \stex_path_from_string:Nn \l_tmpb_seq \l__stex_refs_uri_str
+ \str_set:Nx \l__stex_refs_uri_str {\stex_path_to_string:N \l_tmpb_seq}
}
- \str_if_empty:NTF \l_tmpa_str {
- \tl_if_empty:NTF \l__stex_refs_linktext_tl \l__stex_refs_fallback_tl \l__stex_refs_linktext_tl
+ }
+}
+
+\cs_new_protected:Nn \__stex_refs_do_autoref:n{
+ \cs_if_exist:cTF{autoref}{
+ \exp_args:Nx\autoref{sref_#1}
+ }{
+ \exp_args:Nx\ref{sref_#1}
+ }
+}
+
+\cs_new_protected:Nn \__stex_refs_do_sref:n {
+ \str_if_empty:NTF \l__stex_refs_uri_str {
+ \str_if_empty:NTF \l__stex_refs_in_str {
+ \stex_debug:nn{sref}{autoref~on~#1}
+ \__stex_refs_do_autoref:n{#1}
}{
- \str_if_eq:cNTF {sref_\l_tmpa_str _type} \c__stex_refs_ref_str {
- \tl_if_empty:NTF \l__stex_refs_linktext_tl {
- \cs_if_exist:cTF{autoref}{
- \l__stex_refs_pre_tl\exp_args:Nx\autoref{sref_\l_tmpa_str}\l__stex_refs_post_tl
- }{
- \l__stex_refs_pre_tl\exp_args:Nx\ref{sref_\l_tmpa_str}\l__stex_refs_post_tl
- }
- }{
- \ltx@ifpackageloaded{hyperref}{
- \hyperref[sref_\l_tmpa_str]\l__stex_refs_linktext_tl
- }{
- \l__stex_refs_linktext_tl
- }
- }
+ \stex_debug:nn{sref}{srefin~on~#1}
+ \__stex_refs_do_sref_in:n{#1}
+ }
+ }{
+ \exp_args:NNo \seq_if_in:NnTF \g_stex_ref_files_seq \l__stex_refs_uri_str {
+ \exp_args:Nnx \seq_if_in:cnTF{g_stex_ref_\l__stex_refs_uri_str _seq}{\detokenize{#1}}{
+ \stex_debug:nn{sref}{Reference~found~in~ref~files;~autoref~on~#1}
+ \__stex_refs_do_autoref:n{\l__stex_refs_uri_str?#1}
}{
- \ltx@ifpackageloaded{hyperref}{
- \href{\use:c{sref_url_\l_tmpa_str _str}}{\tl_if_empty:NTF \l__stex_refs_linktext_tl \l__stex_refs_fallback_tl \l__stex_refs_linktext_tl}
+ \str_if_empty:NTF \l__stex_refs_in_str {
+ \stex_debug:nn{sref}{in~empty;~autoref~on~#1}
+ \__stex_refs_do_autoref:n{#1}
}{
- \tl_if_empty:NTF \l__stex_refs_linktext_tl \l__stex_refs_fallback_tl \l__stex_refs_linktext_tl
+ \stex_debug:nn{sref}{in~non-empty;~srefin~on~#1}
+ \__stex_refs_do_sref_in:n{#1}
}
}
+ }{
+ \str_if_empty:NTF \l__stex_refs_in_str {
+ \stex_debug:nn{sref}{in~empty;~autoref~on~#1}
+ \__stex_refs_do_autoref:n{#1}
+ }{
+ \stex_debug:nn{sref}{in~non-empty;~srefin~on~#1}
+ \__stex_refs_do_sref_in:n{#1}
+ }
}
- }{
- % TODO
}
}
-\NewDocumentCommand \srefsym { O{} m}{
- \stex_get_symbol:n { #2 }
- \__stex_refs_sym_aux:nn{#1}{\l_stex_get_symbol_uri_str}
-}
-\cs_new_protected:Nn \__stex_refs_sym_aux:nn {
- \str_if_exist:cTF {sref_sym_#2 _label_str }{
- \sref[#1]{\use:c{sref_sym_#2 _label_str}}
+\cs_new_protected:Nn \__stex_refs_restore_target:nnnnn {
+ \str_if_empty:NTF \l__stex_refs_uri_str {
+ \exp_args:No \str_if_eq:nnT \l__stex_refs_id_str {#2}{
+ \tl_set:Nn \l__stex_refs_return_tl {
+ \use:c{#3autorefname}~#4\tl_if_empty:nF{#5}{~(#5)}~in~
+ \tl_if_empty:nTF\l__stex_refs_title_tl{
+ ???
+ }\l__stex_refs_title_tl
+ }
+ }
}{
- \__stex_refs_args:n { #1 }
- \str_if_empty:NTF \l__stex_refs_indocument_str {
- \tl_if_exist:cTF{sref_sym_#2 _type}{
- % doc uri in \l_tmpb_str
- \str_set:Nx \l_tmpa_str {\use:c{sref_sym_#2 _type}}
- \str_if_eq:NNTF \l_tmpa_str \c__stex_refs_ref_str {
- % reference
- \tl_if_empty:NTF \l__stex_refs_linktext_tl {
- \cs_if_exist:cTF{autoref}{
- \l__stex_refs_pre_tl\autoref{sref_sym_#2}\l__stex_refs_post_tl
- }{
- \l__stex_refs_pre_tl\ref{sref_sym_#2}\l__stex_refs_post_tl
- }
- }{
- \ltx@ifpackageloaded{hyperref}{
- \hyperref[sref_sym_#2]\l__stex_refs_linktext_tl
- }{
- \l__stex_refs_linktext_tl
- }
- }
- }{
- % URL
- \ltx@ifpackageloaded{hyperref}{
- \href{\use:c{sref_sym_url_#2 _str}}{\tl_if_empty:NTF \l__stex_refs_linktext_tl \l__stex_refs_fallback_tl \l__stex_refs_linktext_tl}
- }{
- \tl_if_empty:NTF \l__stex_refs_linktext_tl \l__stex_refs_fallback_tl \l__stex_refs_linktext_tl
- }
+ \stex_debug:nn{sref}{\l__stex_refs_uri_str{}~ == ~ #1 ~ ?}
+ \exp_args:No \str_if_eq:nnT \l__stex_refs_uri_str {#1}{
+ \stex_debug:nn{sref}{\l__stex_refs_id_str~ == ~ #2 ~ ?}
+ \exp_args:No \str_if_eq:nnT \l__stex_refs_id_str {#2}{
+ \stex_debug:nn{sref}{success!}
+ \tl_set:Nn \l__stex_refs_return_tl {
+ \use:c{#3autorefname}~#4\tl_if_empty:nF{#5}{~(#5)}~in~
+ \tl_if_empty:nTF\l__stex_refs_title_tl{
+ ???
+ }\l__stex_refs_title_tl
+ }
+ \endinput
+ }
+ }
+ }
+}
+
+\cs_new_protected:Nn \__stex_refs_do_sref_in:n {
+ \stex_debug:nn{sref}{In: \l__stex_refs_in_str^^JRepo:\l__stex_refs_repo_str}
+ \stex_debug:nn{sref}{URI: \l__stex_refs_uri_str?#1}
+ %\msg_warning:nnn{stex}{warning/smsmissing}{<filename>}
+ \begingroup\catcode13=9\relax\catcode10=9\relax
+ \str_if_empty:NTF \l__stex_refs_repob_str {
+ \prop_if_exist:NTF \l_stex_current_repository_prop {
+ \str_set:Nx \l_tmpa_str {
+ \c_stex_mathhub_str /
+ \prop_item:Nn \l_stex_current_repository_prop { id }
+ / source / \l__stex_refs_in_str .sref
}
}{
- \tl_if_empty:NTF \l__stex_refs_linktext_tl \l__stex_refs_fallback_tl \l__stex_refs_linktext_tl
+ \str_set:Nx \l_tmpa_str {
+ \stex_path_to_string:N \g_stex_currentfile_seq/ .. / \l__stex_refs_in_str . sref
+ }
}
}{
- % TODO
+ \str_set:Nx \l_tmpa_str {
+ \c_stex_mathhub_str / \l__stex_refs_repob_str
+ / source / \l__stex_refs_in_str . sref
+ }
+ }
+ \stex_path_from_string:Nn \l_tmpb_seq \l_tmpa_str
+ \stex_path_to_string:NN \l_tmpb_seq \l_tmpa_str
+ \stex_debug:nn{sref}{File: \l_tmpa_str}
+ \exp_args:No \IfFileExists \l_tmpa_str {
+ \tl_clear:N \l__stex_refs_return_tl
+ \str_set:Nn \l__stex_refs_id_str {#1}
+ \let\STEXInternalSrefRestoreTarget\__stex_refs_restore_target:nnnnn
+ \use:c{@ @ input}{\l_tmpa_str}
+ \exp_args:No \tl_if_empty:nTF \l__stex_refs_return_tl {
+ \exp_args:Nnno \msg_warning:nnnn{stex}{warning/smslabelmissing}\l_tmpa_str{#1}
+ \__stex_refs_do_autoref:n{
+ \str_if_empty:NF\l__stex_refs_uri_str{\l__stex_refs_uri_str?}#1
+ }
+ }{
+ \l__stex_refs_return_tl
+ }
+ }{
+ \exp_args:Nnno \msg_warning:nnn{stex}{warning/smsmissing}\l_tmpa_str
+ \__stex_refs_do_autoref:n{
+ \str_if_empty:NF\l__stex_refs_uri_str{\l__stex_refs_uri_str?}#1
+ }
}
- }
+ \endgroup
}
-\cs_new_protected:Npn \srefsymuri #1 #2 {
- \__stex_refs_sym_aux:nn{linktext={#2}}{#1}
+
+ % \__stex_refs_args:n { #1 }
+ % \str_if_empty:NTF \l__stex_refs_indocument_str {
+ % \str_set:Nx \l_tmpa_str { #2 }
+ % \exp_args:NNno \seq_set_split:Nnn \l_tmpa_seq ? \l_tmpa_str
+ % \int_compare:nNnTF {\seq_count:N \l_tmpa_seq} = 1 {
+ % \seq_if_exist:cTF{g__stex_refs_labels_\l_tmpa_str _seq}{
+ % \seq_get_left:cNF {g__stex_refs_labels_\l_tmpa_str _seq} \l_tmpa_str {
+ % \str_clear:N \l_tmpa_str
+ % }
+ % }{
+ % \str_clear:N \l_tmpa_str
+ % }
+ % }{
+ % \seq_pop_left:NN \l_tmpa_seq \l_tmpb_str
+ % \seq_pop_right:NN \l_tmpa_seq \l_tmpa_str
+ % \int_set:Nn \l_tmpa_int { \exp_args:Ne \str_count:n {\l_tmpb_str?\l_tmpa_str} }
+ % \seq_if_exist:cTF{g__stex_refs_labels_\l_tmpa_str _seq}{
+ % \str_set_eq:NN \l_tmpc_str \l_tmpa_str
+ % \str_clear:N \l_tmpa_str
+ % \seq_map_inline:cn {g__stex_refs_labels_\l_tmpc_str _seq} {
+ % \str_if_eq:eeT { \l_tmpb_str?\l_tmpc_str }{
+ % \str_range:nnn { ##1 }{ -\l_tmpa_int}{ -1 }
+ % }{
+ % \seq_map_break:n {
+ % \str_set:Nn \l_tmpa_str { ##1 }
+ % }
+ % }
+ % }
+ % }{
+ % \str_clear:N \l_tmpa_str
+ % }
+ % }
+ % \str_if_empty:NTF \l_tmpa_str {
+ % \tl_if_empty:NTF \l__stex_refs_linktext_tl \l__stex_refs_fallback_tl \l__stex_refs_linktext_tl
+ % }{
+ % \str_if_eq:cNTF {sref_\l_tmpa_str _type} \c__stex_refs_ref_str {
+ % \tl_if_empty:NTF \l__stex_refs_linktext_tl {
+ % \cs_if_exist:cTF{autoref}{
+ % \l__stex_refs_pre_tl\exp_args:Nx\autoref{sref_\l_tmpa_str}\l__stex_refs_post_tl
+ % }{
+ % \l__stex_refs_pre_tl\exp_args:Nx\ref{sref_\l_tmpa_str}\l__stex_refs_post_tl
+ % }
+ % }{
+ % \ltx@ifpackageloaded{hyperref}{
+ % \hyperref[sref_\l_tmpa_str]\l__stex_refs_linktext_tl
+ % }{
+ % \l__stex_refs_linktext_tl
+ % }
+ % }
+ % }{
+ % \ltx@ifpackageloaded{hyperref}{
+ % \href{\use:c{sref_url_\l_tmpa_str _str}}{\tl_if_empty:NTF \l__stex_refs_linktext_tl \l__stex_refs_fallback_tl \l__stex_refs_linktext_tl}
+ % }{
+ % \tl_if_empty:NTF \l__stex_refs_linktext_tl \l__stex_refs_fallback_tl \l__stex_refs_linktext_tl
+ % }
+ % }
+ % }
+ % }{
+ % TODO
+ % }
+\NewDocumentCommand \srefsym { O{} m}{
+ \stex_get_symbol:n { #2 }
+ \__stex_refs_sym_aux:nn{#1}{\l_stex_get_symbol_uri_str}
+}
+
+\cs_new_protected:Nn \__stex_refs_sym_aux:nn {
+
+}
+\cs_new_protected:Npn \srefsymuri #1 #2 { % TODO
+ #2%\__stex_refs_sym_aux:nn{linktext={#2}}{#1}
}
%%%%%%%%%%%%% modules.dtx %%%%%%%%%%%%%
@@ -1641,6 +1841,15 @@
\use:c{ c_stex_module_#1_code }
}
}
+\NewDocumentEnvironment { mmtinterface } { O{} m m } {
+ \begin{smodule}[#1]{#3}
+ \str_set:Nx \l_stex_module_mmtfor_str {#2}
+ \MMTinclude{#2}
+ \stex_reactivate_macro:N \mmtdecl
+ \stex_reactivate_macro:N \mmtdef
+}{
+ \end{smodule}
+}
%%%%%%%%%%%%% inheritance.dtx %%%%%%%%%%%%%
@@ -1685,7 +1894,9 @@
sexample,
sassertion,
sparagraph,
- mathstructure
+ mathstructure,
+ extstructure,
+ extstructure*
}
}
\bool_new:N \g__stex_smsmode_bool
@@ -2036,14 +2247,11 @@
\stex_debug:nn{modules}{Importing~module:~
\l_stex_import_ns_str ? \l_stex_import_name_str
}
- \stex_import_require_module:nnnn
- { \l_stex_import_ns_str } { \l_stex_import_archive_str }
- { \l_stex_import_path_str } { \l_stex_import_name_str }
\stex_if_smsmode:F {
\stex_annotate_invisible:nnn
{import} {\l_stex_import_ns_str ? \l_stex_import_name_str} {}
}
- \exp_args:Nx \stex_add_to_current_module:n {
+ \stex_execute_in_module:x {
\stex_import_require_module:nnnn
{ \l_stex_import_ns_str } { \l_stex_import_archive_str }
{ \l_stex_import_path_str } { \l_stex_import_name_str }
@@ -2112,15 +2320,14 @@
}
\keys_define:nn { stex / symdecl } {
name .str_set_x:N = \l_stex_symdecl_name_str ,
- local .bool_set:N = \l_stex_symdecl_local_bool ,
args .str_set_x:N = \l_stex_symdecl_args_str ,
type .tl_set:N = \l_stex_symdecl_type_tl ,
deprecate .str_set_x:N = \l_stex_symdecl_deprecate_str ,
align .str_set:N = \l_stex_symdecl_align_str , % TODO(?)
gfc .str_set:N = \l_stex_symdecl_gfc_str , % TODO(?)
- specializes .str_set:N = \l_stex_symdecl_specializes_str , % TODO(?)
def .tl_set:N = \l_stex_symdecl_definiens_tl ,
reorder .str_set_x:N = \l_stex_symdecl_reorder_str ,
+ argnames .clist_set:N = \l_stex_symdecl_argnames_clist ,
assoc .choices:nn =
{bin,binl,binr,pre,conj,pwconj}
{\str_set:Nx \l_stex_symdecl_assoctype_str {\l_keys_choice_tl}}
@@ -2137,6 +2344,7 @@
\bool_set_false:N \l_stex_symdecl_local_bool
\tl_clear:N \l_stex_symdecl_type_tl
\tl_clear:N \l_stex_symdecl_definiens_tl
+ \clist_clear:N \l_stex_symdecl_argnames_clist
\keys_set:nn { stex / symdecl } { #1 }
}
@@ -2217,6 +2425,7 @@
}{##1}
}
}
+
\bool_if:NTF \l_tmpa_bool {
% possibly numeric
\str_if_empty:NTF \l_stex_symdecl_args_str {
@@ -2244,6 +2453,19 @@
\prop_put:Nnx \l_tmpa_prop { defined }{ true }
}
+ % argnames
+
+ \clist_clear:N \l_tmpa_clist
+ \int_step_inline:nn {\prop_item:Nn \l_tmpa_prop {arity}} {
+ \clist_if_empty:NTF \l_stex_symdecl_argnames_clist {
+ \clist_put_right:Nn \l_tmpa_clist {##1}
+ }{
+ \clist_pop:NN \l_stex_symdecl_argnames_clist \l_tmpa_tl
+ \exp_args:NNx \clist_put_right:Nn \l_tmpa_clist {\c_dollar_str\l_tmpa_tl}
+ }
+ }
+ \prop_put:Nnx \l_tmpa_prop {argnames} {\clist_use:Nn \l_tmpa_clist ,}
+
% semantic macro
\bool_if:NT \l_stex_symdecl_make_macro_bool {
@@ -2289,7 +2511,7 @@
_prop
} {
\bool_if:NTF \l_stex_symdecl_local_bool \stex_do_up_to_module:x \stex_execute_in_module:x {
- \__stex_symdecl_restore_symbol:nnnnnnn
+ \__stex_symdecl_restore_symbol:nnnnnnnn
{\l_stex_symdecl_name_str}
{ \prop_item:Nn \l_tmpa_prop {args} }
{ \prop_item:Nn \l_tmpa_prop {arity} }
@@ -2297,10 +2519,11 @@
{ \prop_item:Nn \l_tmpa_prop {defined} }
{\bool_if:NT \l_stex_symdecl_make_macro_bool {#1} }
{\l_stex_current_module_str}
+ { \prop_item:Nn \l_tmpa_prop {argnames} }
}
}
}
-\cs_new_protected:Nn \__stex_symdecl_restore_symbol:nnnnnnn {
+\cs_new_protected:Nn \__stex_symdecl_restore_symbol:nnnnnnnn {
\prop_clear:N \l_tmpa_prop
\prop_put:Nnn \l_tmpa_prop { module } { #7 }
\prop_put:Nnn \l_tmpa_prop { name } { #1}
@@ -2308,6 +2531,7 @@
\prop_put:Nnn \l_tmpa_prop { arity } { #3 }
\prop_put:Nnn \l_tmpa_prop { assocs } { #4 }
\prop_put:Nnn \l_tmpa_prop { defined } { #5 }
+ \prop_put:Nnn \l_tmpa_prop { argnames } { #8 }
\tl_if_empty:nF{#6}{
\tl_set:cx{#6}{\stex_invoke_symbol:n{\detokenize{#7 ? #1}}}
}
@@ -2323,6 +2547,7 @@
\cs_new_protected:Nn \_stex_textsymdecl_args:n {
\str_clear:N \l__stex_symdecl_name_str
\tl_clear:N \l__stex_symdecl_type_tl
+ \clist_clear:N \l_stex_symdecl_argnames_clist
\keys_set:nn { stex / textsymdecl } { #1 }
}
@@ -2338,12 +2563,12 @@
\stex_execute_in_module:n{
\cs_set_nopar:cpn{#1name}{
\ifvmode\hbox_unpack:N\c_empty_box\fi
- \hbox{#3}\xspace
+ \ifmmode\hbox{#3}\else#3\fi\xspace
}
\cs_set_nopar:cpn{#1}{
\ifmmode\csname#1-sym\expandafter\endcsname\else
\ifvmode\hbox_unpack:N\c_empty_box\fi
- \symref{#1-sym}{\hbox{#3}}\expandafter\xspace
+ \symref{#1-sym}{#3}\expandafter\xspace
\fi
}
}
@@ -2464,18 +2689,20 @@
}
}
\keys_define:nn { stex / notation } {
- variant .tl_set_x:N = \l__stex_notation_variant_str ,
- prec .str_set_x:N = \l__stex_notation_prec_str ,
- op .tl_set:N = \l__stex_notation_op_tl ,
- primary .bool_set:N = \l__stex_notation_primary_bool ,
- primary .default:n = {true} ,
- unknown .code:n = \str_set:Nx
+ variant .tl_set_x:N = \l__stex_notation_variant_str ,
+ prec .str_set_x:N = \l__stex_notation_prec_str ,
+ op .tl_set:N = \l__stex_notation_op_tl ,
+ primary .bool_set:N = \l__stex_notation_primary_bool ,
+ primary .default:n = {true} ,
+ hints .str_set_x:N = \l__stex_notation_hints_str,
+ unknown .code:n = \str_set:Nx
\l__stex_notation_variant_str \l_keys_key_str
}
\cs_new_protected:Nn \_stex_notation_args:n {
\str_clear:N \l__stex_notation_variant_str
\str_clear:N \l__stex_notation_prec_str
+ \str_clear:N \l__stex_notation_hints_str
\tl_clear:N \l__stex_notation_op_tl
\bool_set_false:N \l__stex_notation_primary_bool
@@ -2535,7 +2762,7 @@
\exp_args:NNNo \exp_args:NNno \seq_set_split:Nnn
\l_tmpa_seq {\tl_to_str:n{x} } { \l_tmpa_str }
\seq_map_inline:Nn \l_tmpa_seq {
- \seq_put_right:Nn \l_tmpb_seq { ##1 }
+ \seq_put_right:Nn \l__stex_notation_precedences_seq { ##1 }
}
}
}{
@@ -2668,11 +2895,12 @@
\seq_pop_left:NN \l__stex_notation_remaining_precs_seq \l_tmpa_str
\tl_put_right:Nx \l_stex_notation_dummyargs_tl { {
- \STEXInternalTermMathAssocArgiiii
- { #1\int_use:N \l__stex_notation_currarg_int }
+ \STEXInternalTermMathAssocArgiiiii
+ { \int_use:N \l__stex_notation_currarg_int }
{ \l_tmpa_str }
{ ####\int_use:N \l__stex_notation_currarg_int }
{ \l_tmpa_cs {####1} {####2} }
+ {#1}
} }
\__stex_notation_arguments:
}
@@ -2861,7 +3089,6 @@
\keys_define:nn { stex / symdef } {
name .str_set_x:N = \l_stex_symdecl_name_str ,
- local .bool_set:N = \l_stex_symdecl_local_bool ,
args .str_set_x:N = \l_stex_symdecl_args_str ,
type .tl_set:N = \l_stex_symdecl_type_tl ,
def .tl_set:N = \l_stex_symdecl_definiens_tl ,
@@ -2870,6 +3097,7 @@
% lang .str_set_x:N = \l__stex_notation_lang_str ,
variant .str_set_x:N = \l__stex_notation_variant_str ,
prec .str_set_x:N = \l__stex_notation_prec_str ,
+ argnames .clist_set:N = \l_stex_symdecl_argnames_clist ,
assoc .choices:nn =
{bin,binl,binr,pre,conj,pwconj}
{\str_set:Nx \l_stex_symdecl_assoctype_str {\l_keys_choice_tl}},
@@ -2885,6 +3113,7 @@
\bool_set_false:N \l_stex_symdecl_local_bool
\tl_clear:N \l_stex_symdecl_type_tl
\tl_clear:N \l_stex_symdecl_definiens_tl
+ \clist_clear:N \l_stex_symdecl_argnames_clist
% \str_clear:N \l__stex_notation_lang_str
\str_clear:N \l__stex_notation_variant_str
\str_clear:N \l__stex_notation_prec_str
@@ -2912,6 +3141,70 @@
}
\stex_deactivate_macro:Nn \symdef {module~environments}
+\keys_define:nn { stex / mmtdef } {
+ name .str_set_x:N = \l_stex_symdecl_name_str ,
+ args .str_set_x:N = \l_stex_symdecl_args_str ,
+ reorder .str_set_x:N = \l_stex_symdecl_reorder_str ,
+ op .tl_set:N = \l__stex_notation_op_tl ,
+ % lang .str_set_x:N = \l__stex_notation_lang_str ,
+ variant .str_set_x:N = \l__stex_notation_variant_str ,
+ prec .str_set_x:N = \l__stex_notation_prec_str ,
+ argnames .clist_set:N = \l_stex_symdecl_argnames_clist ,
+ assoc .choices:nn =
+ {bin,binl,binr,pre,conj,pwconj}
+ {\str_set:Nx \l_stex_symdecl_assoctype_str {\l_keys_choice_tl}},
+ unknown .code:n = \str_set:Nx
+ \l__stex_notation_variant_str \l_keys_key_str
+}
+\cs_new_protected:Nn \_stex_mmtdef_args:n {
+ \str_clear:N \l_stex_symdecl_name_str
+ \str_clear:N \l_stex_symdecl_args_str
+ \str_clear:N \l_stex_symdecl_assoctype_str
+ \str_clear:N \l_stex_symdecl_reorder_str
+ \bool_set_false:N \l_stex_symdecl_local_bool
+ \clist_clear:N \l_stex_symdecl_argnames_clist
+ % \str_clear:N \l__stex_notation_lang_str
+ \str_clear:N \l__stex_notation_variant_str
+ \str_clear:N \l__stex_notation_prec_str
+ \tl_clear:N \l__stex_notation_op_tl
+
+ \keys_set:nn { stex / mmtdef } { #1 }
+}
+
+\NewDocumentCommand \mmtdef {m O{} }{
+ \_stex_mmtdef_args:n{ #2 }
+ \bool_set_true:N \l_stex_symdecl_make_macro_bool
+ \str_if_empty:NT \l_stex_symdecl_name_str {
+ \str_set:Nx \l_stex_symdecl_name_str { #1 }
+ }
+ %\tl_set:Nx \l_stex_symdecl_definiens_tl {
+ % \stex_annotate:nnn{ OMID }{
+ % \l_stex_module_mmtfor_str?\l_stex_symdecl_name_str
+ % }{}
+ %}
+ \stex_symdecl_do:n { #1 }
+ \MMTrule{rules.stex.mmt.kwarc.info?SubstitutionRule}{
+ \stex_annotate:nnn{ OMID }{
+ \l_stex_current_module_str ? \l_stex_symdecl_name_str
+ }{},
+ \stex_annotate:nnn{ OMID }{
+ \l_stex_module_mmtfor_str?\l_stex_symdecl_name_str
+ }{}
+ }
+ \tl_set:Nn \l_stex_notation_after_do_tl {
+ \__stex_notation_final:
+ \stex_smsmode_do:\ignorespacesandpars
+ }
+ \str_set:Nx \l_stex_get_symbol_uri_str {
+ \l_stex_current_module_str ? \l_stex_symdecl_name_str
+ }
+ \exp_args:Nx \stex_notation_do:nnnnn
+ { \prop_item:cn {l_stex_symdecl_\l_stex_get_symbol_uri_str _prop } { args } }
+ { \prop_item:cn { l_stex_symdecl_\l_stex_get_symbol_uri_str _prop } { arity } }
+ { \l__stex_notation_variant_str }
+ { \l__stex_notation_prec_str}
+}
+
\keys_define:nn { stex / vardef } {
name .str_set_x:N = \l__stex_variables_name_str ,
args .str_set_x:N = \l__stex_variables_args_str ,
@@ -2920,6 +3213,7 @@
op .tl_set:N = \l__stex_variables_op_tl ,
prec .str_set_x:N = \l__stex_variables_prec_str ,
reorder .str_set_x:N = \l__stex_variables_reorder_str ,
+ argnames .clist_set:N = \l__stex_variables_argnames_clist ,
assoc .choices:nn =
{bin,binl,binr,pre,conj,pwconj}
{\str_set:Nx \l__stex_variables_assoctype_str {\l_keys_choice_tl}},
@@ -2938,6 +3232,7 @@
\tl_clear:N \l__stex_variables_type_tl
\tl_clear:N \l__stex_variables_def_tl
\tl_clear:N \l__stex_variables_op_tl
+ \clist_clear:N \l__stex_variables_argnames_clist
\keys_set:nn { stex / vardef } { #1 }
}
@@ -2994,7 +3289,20 @@
\prop_put:Nnx \l_tmpa_prop { assocs } { \int_use:N \l_tmpb_int }
\tl_set:cx { #1 }{ \stex_invoke_variable:n { \l__stex_variables_name_str } }
- \prop_set_eq:cN { l_stex_variable_\l__stex_variables_name_str _prop} \l_tmpa_prop
+ % argnames
+
+ \clist_clear:N \l_tmpa_clist
+ \int_step_inline:nn {\prop_item:Nn \l_tmpa_prop {arity}} {
+ \clist_if_empty:NTF \l__stex_variables_argnames_clist {
+ \clist_put_right:Nn \l_tmpa_clist {##1}
+ }{
+ \clist_pop:NN \l__stex_variables_argnames_clist \l_tmpa_tl
+ \exp_args:NNx \clist_put_right:Nn \l_tmpa_clist {\c_dollar_str\l_tmpa_tl}
+ }
+ }
+ \prop_put:Nnx \l_tmpa_prop {argnames} {\clist_use:Nn \l_tmpa_clist ,}
+
+ \prop_set_eq:cN { l_stex_symdecl_var://\l__stex_variables_name_str _prop} \l_tmpa_prop
\tl_if_empty:NF \l__stex_variables_op_tl {
\cs_set:cpx {
@@ -3169,6 +3477,14 @@
\cs_generate_from_arg_count:cNnn {stex_varseq_\l__stex_variables_name_str _cs}
\cs_set:Npn {\int_use:N \l__stex_variables_args_int} { #5 }
+ % argnames
+
+ \clist_clear:N \l_tmpa_clist
+ \int_step_inline:nn {\l__stex_variables_args_int} {
+ \clist_put_right:Nn \l_tmpa_clist {##1}
+ }
+ \prop_put:Nnx \l_tmpa_prop {argnames} {\clist_use:Nn \l_tmpa_clist ,}
+
\exp_args:NNo \tl_set:No \l_tmpa_tl {\use:c{stex_varseq_\l__stex_variables_name_str _cs}}
\int_step_inline:nn \l__stex_variables_args_int {
\tl_put_right:Nx \l_tmpa_tl { {\seq_item:Nn \l_tmpa_seq {##1}} }
@@ -3214,6 +3530,8 @@
\expandafter\meaning\csname stex_varseq_\l__stex_variables_name_str _cs\endcsname\\~\\
\prop_to_keyval:N \l_tmpa_prop
}
+ \prop_set_eq:cN {l_stex_symdecl_varseq://\l__stex_variables_name_str _prop}\l_tmpa_prop
+
\stex_if_do_html:T{\stex_annotate_invisible:nnn{varseq}{\l__stex_variables_name_str}{
\tl_if_empty:NF \l__stex_variables_type_tl {
\stex_annotate:nnn {type}{}{$\l__stex_variables_type_tl$}
@@ -3243,10 +3561,62 @@
}}
- \prop_set_eq:cN {stex_varseq_\l__stex_variables_name_str _prop}\l_tmpa_prop
\ignorespacesandpars
}
+\keys_define:nn { stex / mmtdecl } {
+ name .str_set_x:N = \l_stex_symdecl_name_str ,
+ args .str_set_x:N = \l_stex_symdecl_args_str ,
+ deprecate .str_set_x:N = \l_stex_symdecl_deprecate_str ,
+ reorder .str_set_x:N = \l_stex_symdecl_reorder_str ,
+ argnames .clist_set:N = \l_stex_symdecl_argnames_clist ,
+ assoc .choices:nn =
+ {bin,binl,binr,pre,conj,pwconj}
+ {\str_set:Nx \l_stex_symdecl_assoctype_str {\l_keys_choice_tl}}
+}
+
+\cs_new_protected:Nn \_stex_mmtdecl_args:n {
+ \str_clear:N \l_stex_symdecl_name_str
+ \str_clear:N \l_stex_symdecl_args_str
+ \str_clear:N \l_stex_symdecl_deprecate_str
+ \str_clear:N \l_stex_symdecl_reorder_str
+ \str_clear:N \l_stex_symdecl_assoctype_str
+ \bool_set_false:N \l_stex_symdecl_local_bool
+ \clist_clear:N \l_stex_symdecl_argnames_clist
+
+ \keys_set:nn { stex / symdecl } { #1 }
+}
+
+\NewDocumentCommand \mmtdecl { s m O{}} {
+ \_stex_mmtdecl_args:n{#3}
+ \IfBooleanTF #1 {
+ \bool_set_false:N \l_stex_symdecl_make_macro_bool
+ } {
+ \bool_set_true:N \l_stex_symdecl_make_macro_bool
+ }
+ \str_if_empty:NT \l_stex_symdecl_name_str {
+ \str_set:Nx \l_stex_symdecl_name_str { #1 }
+ }
+ %\tl_set:Nx \l_stex_symdecl_definiens_tl {
+ % \stex_annotate:nnn{ OMID }{
+ % \l_stex_module_mmtfor_str?\l_stex_symdecl_name_str
+ % }{}
+ %}
+ \stex_symdecl_do:n{#2}
+ \MMTrule{rules.stex.mmt.kwarc.info?SubstitutionRule}{
+ \stex_annotate:nnn{ OMID }{
+ \l_stex_current_module_str ? \l_stex_symdecl_name_str
+ }{},
+ \stex_annotate:nnn{ OMID }{
+ \l_stex_module_mmtfor_str?\l_stex_symdecl_name_str
+ }{}
+ }
+ \stex_smsmode_do:
+}
+
+\stex_deactivate_macro:Nn \mmtdecl {mmtinterface~environments}
+\stex_deactivate_macro:Nn \mmtdef {mmtinterface~environments}
+
%%%%%%%%%%%%% terms.dtx %%%%%%%%%%%%%
@@ -3340,8 +3710,10 @@
\def\comp{\_comp}
\str_set:Nn \STEXInternalCurrentSymbolStr { #1 }
\bool_set_false:N \l_stex_allow_semantic_bool
- \_stex_term_oms:nnn {#1}{#1 \c_hash_str CUSTOM-}{
- \comp{ #2 }
+ \stex_mathml_intent:nn{#1}{
+ \_stex_term_oms:nnn {#1}{#1 \c_hash_str CUSTOM-}{
+ \comp{ #2 }
+ }
}
}{
\_stex_reset:N \comp
@@ -3454,6 +3826,8 @@
}
\prop_new:N \l__stex_terms_custom_args_prop
+\clist_new:N \l_stex_argnames_seq
+\seq_new:N \l__stex_terms_tmp_seq
\cs_new_protected:Nn\__stex_terms_custom_comp:n{\bool_set_false:N \l_stex_allow_semantic_bool\_comp{#1}\bool_set_true:N \l_stex_allow_semantic_bool}
@@ -3466,23 +3840,47 @@
\prop_get:cnN {
l_stex_symdecl_#1 _prop
}{ args } \l_tmpa_str
+ \exp_args:NNx \seq_set_from_clist:Nn \l_stex_argnames_seq {
+ \prop_item:cn {l_stex_symdecl_#1 _prop}{argnames}
+ }
\prop_put:Nno \l__stex_terms_custom_args_prop {args} \l_tmpa_str
\tl_set:Nn \arg { \__stex_terms_arg: }
\str_if_empty:NTF \l_tmpa_str {
- \_stex_term_oms:nnn {#1}{#1\c_hash_str CUSTOM-}{\ignorespaces#2}
+ \stex_mathml_intent:nn{#1}{
+ \_stex_term_oms:nnn {#1}{#1\c_hash_str CUSTOM-}{\ignorespaces#2}
+ }
}{
- \str_if_in:NnTF \l_tmpa_str b {
- \_stex_term_ombind:nnn {#1}{#1\c_hash_str CUSTOM-\l_tmpa_str}{\ignorespaces#2}
+ \seq_clear:N \l__stex_terms_tmp_seq
+ \exp_args:Nx\int_step_inline:nn{\prop_item:cn{l_stex_symdecl_#1 _prop}{arity}}{
+ \tl_set:Nx \l__stex_terms_tmp_tl {\seq_item:Nn \l_stex_argnames_seq {##1}}
+ \bool_lazy_or:nnT{
+ \str_if_eq_p:nn{a}{\str_item:Nn\l_tmpa_str{##1}}
+ }{
+ \str_if_eq_p:nn{B}{\str_item:Nn\l_tmpa_str{##1}}
+ }{
+ \tl_put_right:Nn \l__stex_terms_tmp_tl +
+ }
+ \seq_put_right:No \l__stex_terms_tmp_seq \l__stex_terms_tmp_tl
+ }
+ \stex_mathml_intent:nn{
+ #1[\prop_item:cn {l_stex_symdecl_#1 _prop}{ args }](
+ \seq_use:Nn \l__stex_terms_tmp_seq ,
+ )
}{
- \str_if_in:NnTF \l_tmpa_str B {
+ \str_if_in:NnTF \l_tmpa_str b {
\_stex_term_ombind:nnn {#1}{#1\c_hash_str CUSTOM-\l_tmpa_str}{\ignorespaces#2}
}{
- \_stex_term_oma:nnn {#1}{#1\c_hash_str CUSTOM-\l_tmpa_str}{\ignorespaces#2}
+ \str_if_in:NnTF \l_tmpa_str B {
+ \_stex_term_ombind:nnn {#1}{#1\c_hash_str CUSTOM-\l_tmpa_str}{\ignorespaces#2}
+ }{
+ \_stex_term_oma:nnn {#1}{#1\c_hash_str CUSTOM-\l_tmpa_str}{\ignorespaces#2}
+ }
}
}
}
% TODO check that all arguments exist
}{
+ \_stex_reset:N \l_stex_argnames_seq
\_stex_reset:N \STEXInternalCurrentSymbolStr
\_stex_reset:N \arg
\_stex_reset:N \comp
@@ -3524,15 +3922,21 @@
}
}
\exp_args:NNx \prop_put:Nnn \l__stex_terms_custom_args_prop {\int_use:N \l_tmpa_int} {\ignorespaces#3}
- \bool_set_true:N \l_stex_allow_semantic_bool
- \IfBooleanTF#1{
- \stex_annotate_invisible:n { %TODO
+ \bool_if:NTF \l_stex_allow_semantic_bool \use_i:nn {
+ \bool_set_true:N \l_stex_allow_semantic_bool
+ \use:nn
+ }
+ {
+ \stex_mathml_arg:nn{\seq_item:Nn \l_stex_argnames_seq \l_tmpa_int}{
+ \IfBooleanTF#1{
+ \stex_annotate_invisible:n { %TODO
+ \exp_args:No \_stex_term_arg:nn {\l_tmpa_str\int_use:N \l_tmpa_int}{\ignorespaces#3}
+ }
+ }{ %TODO
\exp_args:No \_stex_term_arg:nn {\l_tmpa_str\int_use:N \l_tmpa_int}{\ignorespaces#3}
}
- }{ %TODO
- \exp_args:No \_stex_term_arg:nn {\l_tmpa_str\int_use:N \l_tmpa_int}{\ignorespaces#3}
- }
- \bool_set_false:N \l_stex_allow_semantic_bool
+ }}
+ {\bool_set_false:N \l_stex_allow_semantic_bool}
}
\cs_new_protected:Nn \_stex_term_arg:nn {
@@ -3544,30 +3948,32 @@
\cs_new_protected:Npn \STEXInternalTermMathArgiii #1#2#3 {
\exp_args:Nnx \use:nn
{ \int_set:Nn \l__stex_terms_downprec { #2 }
+ \stex_mathml_arg:nn{\seq_item:Nn \l_stex_argnames_seq \l_tmpa_int}{
\_stex_term_arg:nn { #1 }{ #3 }
+ }
}
{ \int_set:Nn \exp_not:N \l__stex_terms_downprec { \int_use:N \l__stex_terms_downprec } }
}
-\cs_new_protected:Npn \STEXInternalTermMathAssocArgiiii #1#2#3#4 {
+\cs_new_protected:Npn \STEXInternalTermMathAssocArgiiiii #1#2#3#4#5 {
\cs_set:Npn \l_tmpa_cs ##1 ##2 { #4 }
- \tl_set:Nn \l_tmpb_tl {\STEXInternalTermMathArgiii{#1}{#2}}
+ \tl_set:Nn \l_tmpb_tl {\STEXInternalTermMathArgiii{#5#1}{#2}}
\tl_if_empty:nTF { #3 }{
- \STEXInternalTermMathArgiii{#1}{#2}{}
+ \STEXInternalTermMathArgiii{#5#1}{#2}{}
}{
\exp_args:Nx \tl_if_empty:nTF { \tl_tail:n{ #3 }}{
\expandafter\if\expandafter\relax\noexpand#3
- \tl_set:Nn \l_tmpa_tl {\__stex_terms_math_assoc_arg_maybe_sequence:Nn#3{#1}}
+ \tl_set:Nn \l_tmpa_tl {\__stex_terms_math_assoc_arg_maybe_sequence:Nnn#3{#1}{#5}}
\else
- \tl_set:Nn \l_tmpa_tl {\__stex_terms_math_assoc_arg_simple:nn{#1}{#3}}
+ \tl_set:Nn \l_tmpa_tl {\__stex_terms_math_assoc_arg_simple:nnn{#1}{#3}{#5}}
\fi
\l_tmpa_tl
}{
- \__stex_terms_math_assoc_arg_simple:nn{#1}{#3}
+ \__stex_terms_math_assoc_arg_simple:nnn{#1}{#3}{#5}
}
}
}
-\cs_new_protected:Nn \__stex_terms_math_assoc_arg_maybe_sequence:Nn {
+\cs_new_protected:Nn \__stex_terms_math_assoc_arg_maybe_sequence:Nnn {
\str_set:Nx \l_tmpa_str { \cs_argument_spec:N #1 }
\str_if_empty:NTF \l_tmpa_str {
\exp_args:Nx \cs_if_eq:NNTF {
@@ -3575,7 +3981,7 @@
} \stex_invoke_sequence:n {
\tl_set:Nx \l_tmpa_tl {\tl_tail:N #1}
\str_set:Nx \l_tmpa_str {\exp_after:wN \use:n \l_tmpa_tl}
- \tl_set:Nx \l_tmpa_tl {\prop_item:cn {stex_varseq_\l_tmpa_str _prop}{notation}}
+ \tl_set:Nx \l_tmpa_tl {\prop_item:cn {l_stex_symdecl_varseq://\l_tmpa_str _prop}{notation}}
\exp_args:NNo \seq_set_from_clist:Nn \l_tmpa_seq \l_tmpa_tl
\tl_set:Nx \l_tmpa_tl {{\exp_not:N \exp_not:n{
\exp_not:n{\exp_args:Nnx \use:nn} {
@@ -3591,7 +3997,7 @@
}
}
}}}
- \exp_args:Nno \use:nn {\seq_set_map:NNn \l_tmpa_seq \l_tmpa_seq} \l_tmpa_tl
+ \exp_args:Nno \use:n {\seq_set_map:NNn \l_tmpa_seq \l_tmpa_seq} \l_tmpa_tl
\seq_reverse:N \l_tmpa_seq
\seq_pop:NN \l_tmpa_seq \l_tmpa_tl
\seq_map_inline:Nn \l_tmpa_seq {
@@ -3607,28 +4013,38 @@
}
\exp_args:No\l_tmpb_tl\l_tmpa_tl
}{
- \__stex_terms_math_assoc_arg_simple:nn{#2} { #1 }
+ \__stex_terms_math_assoc_arg_simple:nnn{#2} { #1 }{#3}
}
} {
- \__stex_terms_math_assoc_arg_simple:nn{#2} { #1 }
+ \__stex_terms_math_assoc_arg_simple:nnn{#2} { #1 }{#3}
}
}
-\cs_new_protected:Nn \__stex_terms_math_assoc_arg_simple:nn {
+\cs_new_protected:Nn \__stex_terms_math_assoc_arg_simple:nnn {
\clist_set:Nn \l_tmpa_clist{ #2 }
\int_compare:nNnTF { \clist_count:N \l_tmpa_clist } < 2 {
- \tl_set:Nn \l_tmpa_tl { \_stex_term_arg:nn{A#1}{ #2 } }
+ \tl_set:Nn \l_tmpa_tl {
+ \stex_mathml_arg:nn{\seq_item:Nn \l_stex_argnames_seq #1}{
+ \_stex_term_arg:nn{A#3#1}{ #2 } }
+ }
}{
\clist_reverse:N \l_tmpa_clist
\clist_pop:NN \l_tmpa_clist \l_tmpa_tl
- \tl_set:Nx \l_tmpa_tl { \_stex_term_arg:nn{A#1}{
- \exp_args:No \exp_not:n \l_tmpa_tl
+ \tl_set:Nx \l_tmpa_tl {
+ \stex_mathml_arg:nn{\seq_item:Nn \l_stex_argnames_seq #1}{
+ \_stex_term_arg:nn{A#3#1}{
+ \exp_args:No \exp_not:n \l_tmpa_tl
+ }
}}
\clist_map_inline:Nn \l_tmpa_clist {
\exp_args:NNNo \exp_args:NNo \tl_set:No \l_tmpa_tl {
\exp_args:Nno
- \l_tmpa_cs { \_stex_term_arg:nn{A#1}{##1} } \l_tmpa_tl
+ \l_tmpa_cs {
+ \stex_mathml_arg:nn{\seq_item:Nn \l_stex_argnames_seq #1}{
+ \_stex_term_arg:nn{A#3#1}{##1}
+ }
+ } \l_tmpa_tl
}
}
}
@@ -3699,7 +4115,9 @@
\cs_new_protected:Npn \STEXInternalTermMathOMSiiii #1#2#3#4 {
\__stex_terms_maybe_brackets:nn { #3 }{
- \_stex_term_oms:nnn { #1 } { #1\c_hash_str#2 } { #4 }
+ \stex_mathml_intent:nn{#1} {
+ \_stex_term_oms:nnn { #1 } { #1\c_hash_str#2 } { #4 }
+ }
}
}
\cs_new_protected:Nn \_stex_term_omv:nn {
@@ -3714,8 +4132,35 @@
}
\cs_new_protected:Npn \STEXInternalTermMathOMAiiii #1#2#3#4 {
+ \exp_args:Nnx \use:nn {
+ \seq_clear:N \l__stex_terms_tmp_seq
+ \prop_if_exist:cT{l_stex_symdecl_#1 _prop}{
+ \exp_args:NNx \seq_set_from_clist:Nn \l_stex_argnames_seq {
+ \prop_item:cn {l_stex_symdecl_#1 _prop}{argnames}
+ }
+ \exp_args:Nx\int_step_inline:nn{\prop_item:cn{l_stex_symdecl_#1 _prop}{arity}}{
+ \tl_set:Nx \l__stex_terms_tmp_tl {\seq_item:Nn \l_stex_argnames_seq {##1}}
+ \bool_lazy_or:nnT{
+ \str_if_eq_p:nn{a}{\str_item:Nn\l_tmpa_str{##1}}
+ }{
+ \str_if_eq_p:nn{B}{\str_item:Nn\l_tmpa_str{##1}}
+ }{
+ \tl_put_right:Nn \l__stex_terms_tmp_tl +
+ }
+ \seq_put_right:No \l__stex_terms_tmp_seq \l__stex_terms_tmp_tl
+ }
+ }
\__stex_terms_maybe_brackets:nn { #3 }{
- \_stex_term_oma:nnn { #1 } { #1\c_hash_str#2 } { #4 }
+ \stex_mathml_intent:nn{
+ #1[\prop_item:cn {l_stex_symdecl_#1 _prop}{ args }](
+ \seq_use:Nn \l__stex_terms_tmp_seq ,
+ )
+ }{
+ \_stex_term_oma:nnn { #1 } { #1\c_hash_str#2 } { #4 }
+ }
+ }
+ }{
+ \_stex_reset:N \l_stex_argnames_seq
}
}
\cs_new_protected:Nn \_stex_term_ombind:nnn {
@@ -3725,8 +4170,35 @@
}
\cs_new_protected:Npn \STEXInternalTermMathOMBiiii #1#2#3#4 {
+ \exp_args:Nnx \use:nn {
+ \seq_clear:N \l__stex_terms_tmp_seq
+ \prop_if_exist:cT{l_stex_symdecl_#1 _prop}{
+ \exp_args:NNx \seq_set_from_clist:Nn \l_stex_argnames_seq {
+ \prop_item:cn {l_stex_symdecl_#1 _prop}{argnames}
+ }
+ \exp_args:Nx\int_step_inline:nn{\prop_item:cn{l_stex_symdecl_#1 _prop}{arity}}{
+ \tl_set:Nx \l__stex_terms_tmp_tl {\seq_item:Nn \l_stex_argnames_seq {##1}}
+ \bool_lazy_or:nnT{
+ \str_if_eq_p:nn{a}{\str_item:Nn\l_tmpa_str{##1}}
+ }{
+ \str_if_eq_p:nn{B}{\str_item:Nn\l_tmpa_str{##1}}
+ }{
+ \tl_put_right:Nn \l__stex_terms_tmp_tl +
+ }
+ \seq_put_right:No \l__stex_terms_tmp_seq \l__stex_terms_tmp_tl
+ }
+ }
\__stex_terms_maybe_brackets:nn { #3 }{
- \_stex_term_ombind:nnn { #1 } { #1\c_hash_str#2 } { #4 }
+ \stex_mathml_intent:nn{
+ #1[\prop_item:cn {l_stex_symdecl_#1 _prop}{ args }](
+ \seq_use:Nn \l__stex_terms_tmp_seq ,
+ )
+ }{
+ \_stex_term_ombind:nnn { #1 } { #1\c_hash_str#2 } { #4 }
+ }
+ }
+ }{
+ \_stex_reset:N \l_stex_argnames_seq
}
}
\cs_new:Nn \stex_capitalize:n { \uppercase{#1} }
@@ -3950,7 +4422,7 @@
\_stex_reset:N \STEXInternalCurrentSymbolStr
}
}{
- \int_compare:nNnTF {\prop_item:cn {l_stex_variable_#1_prop}{arity}} = 0{
+ \int_compare:nNnTF {\prop_item:cn {l_stex_symdecl_var://#1_prop}{arity}} = 0{
\__stex_variables_invoke_math_ii:n {#1}
}{
\msg_error:nnxx{stex}{error/noop}{variable~#1}{}
@@ -3984,7 +4456,7 @@
\prop_clear:N \l__stex_terms_custom_args_prop
\prop_put:Nnn \l__stex_terms_custom_args_prop {currnum} {1}
\prop_get:cnN {
- l_stex_variable_#1 _prop
+ l_stex_symdecl_var://#1 _prop
}{ args } \l_tmpa_str
\prop_put:Nno \l__stex_terms_custom_args_prop {args} \l_tmpa_str
\tl_set:Nn \arg { \__stex_terms_arg: }
@@ -4017,7 +4489,7 @@
\exp_args:Nnx \use:nn {
\def\comp{\_varcomp}
\str_set:Nn \STEXInternalCurrentSymbolStr {varseq://#1}
- \prop_item:cn{stex_varseq_#1_prop}{notation}
+ \prop_item:cn{l_stex_symdecl_varseq://#1_prop}{notation}
}{
\_stex_reset:N \comp
\_stex_reset:N \STEXInternalCurrentSymbolStr
@@ -4351,6 +4823,9 @@
{ \l_stex_import_ns_str } { \l_stex_import_archive_str }
{ \l_stex_import_path_str } { \l_stex_import_name_str }
}
+ \exp_args:Nx \stex_add_import_to_current_module:n{
+ \l_stex_import_ns_str ? \l_stex_import_name_str
+ }
\seq_map_inline:Nn \l__stex_copymodule_copymodule_modules_seq {
\seq_map_inline:cn {c_stex_module_##1_constants}{
@@ -4543,8 +5018,12 @@
\str_clear:N \l__stex_structures_name_str
\keys_set:nn { stex / features / structure } { #1 }
}
-
\NewDocumentEnvironment{mathstructure}{m O{}}{
+ \begin{mathstructure_inner}{#1}[#2]
+ \stex_smsmode_do:
+ \ignorespacesandpars
+ }{\end{mathstructure_inner}}
+\NewDocumentEnvironment{mathstructure_inner}{m O{}}{
\__stex_structures_structure_args:n { #2 }
\str_if_empty:NT \l__stex_structures_name_str {
\str_set:Nx \l__stex_structures_name_str { #1 }
@@ -4566,7 +5045,6 @@
\exp_args:Nnnx
\begin{structural_feature_module}{ structure }
{ \l__stex_structures_name_str }{}
- \stex_smsmode_do:
}{
\end{structural_feature_module}
\_stex_reset_up_to_module:n \l_stex_last_feature_str
@@ -4645,7 +5123,8 @@
\seq_map_inline:Nn \l_stex_all_modules_seq {
\prop_if_exist:cT {c_stex_module_##1_structures} {
\prop_map_inline:cn {c_stex_module_##1_structures} {
- \str_if_eq:eeT { \l_tmpa_str }{ \str_range:nnn {##1?####1}{-\l_tmpa_int}{-1}}{
+ \exp_args:No \str_if_eq:nnT \l_tmpa_str {####1}{
+ %\str_if_eq:eeT { \l_tmpa_str }{ \str_range:nnn {##1?####1}{-\l_tmpa_int}{-1}}{
\prop_map_break:n{\seq_map_break:n{
\tl_set:Nn \l_tmpa_tl {
\str_set:Nn \l_stex_get_structure_str {##1?####1}
@@ -4659,6 +5138,12 @@
\l_tmpa_tl
}
+\NewDocumentEnvironment{usestructure}{m}{
+ \stex_get_structure:n {#1}
+ \exp_args:Nnx \stex_debug:nn{features}{using~structure:~\l_stex_get_structure_module_str}
+ \exp_args:No \stex_activate_module:n \l_stex_get_structure_module_str
+}{}
+
\keys_define:nn { stex / instantiate } {
name .str_set_x:N = \l__stex_structures_name_str
}
@@ -4667,6 +5152,37 @@
\keys_set:nn { stex / instantiate } { #1 }
}
+\NewDocumentEnvironment{extstructure}{m m O{}}{
+ \begin{mathstructure_inner}{#1}[#3]
+ \seq_set_split:Nnn\__stex_structures_extstructure_imports_seq,{#2}
+ \seq_map_inline:Nn\__stex_structures_extstructure_imports_seq {
+ \stex_get_structure:n {##1}
+ \exp_args:Nnx \stex_debug:nn{features}{importing~structure:~\l_stex_get_structure_module_str{}~into~\l_stex_current_module_str}
+ \exp_args:No \stex_activate_module:n \l_stex_get_structure_module_str
+ \stex_if_smsmode:F {
+ \stex_annotate_invisible:nnn
+ {import} {\l_stex_get_structure_module_str} {}
+ }
+ \exp_args:Nx \stex_add_import_to_current_module:n {
+ \l_stex_get_structure_module_str
+ }
+ \exp_args:Nx \stex_add_to_current_module:n {
+ \exp_args:No \stex_activate_module:n \l_stex_get_structure_module_str
+ }
+ }
+ \stex_smsmode_do:
+ \ignorespacesandpars
+}{
+ \end{mathstructure_inner}
+}
+
+\NewDocumentEnvironment{extstructure*}{m m O{}}{
+ % TODO
+ \begin{extstructure}{#1}{#2}[#3]
+}{
+ \end{extstructure}
+}
+
\NewDocumentCommand \instantiate {m O{} m m O{}}{
\begingroup
\stex_get_structure:n {#3}
@@ -4718,7 +5234,8 @@
name = \l_tmpa_str ,
args = \prop_item:cn {l_stex_symdecl_##1_prop}{args} ,
arity = \prop_item:cn {l_stex_symdecl_##1_prop}{arity} ,
- assocs = \prop_item:cn {l_stex_symdecl_##1_prop}{assocs}
+ assocs = \prop_item:cn {l_stex_symdecl_##1_prop}{assocs} ,
+ argnames = {\prop_item:cn {l_stex_symdecl_##1_prop}{argnames}}
}
\seq_clear:c {l_stex_symdecl_\l_stex_current_module_str?\l_tmpa_str _notations}
}
@@ -4813,7 +5330,7 @@
}
\cs_new_protected:Nn \__stex_structures_symbolorvar_from_string:n {
- \prop_if_exist:cTF {l_stex_variable_#1 _prop}{
+ \prop_if_exist:cTF {l_stex_symdecl_var://#1 _prop}{
\bool_set_true:N \l_stex_symbol_or_var_bool
\str_set:Nn \l_stex_get_symbol_uri_str { #1 }
}{
@@ -4876,12 +5393,12 @@
\bool_if:NTF \l_stex_symbol_or_var_bool {
\exp_args:Nxx \str_if_eq:nnF
{\prop_item:cn{l_stex_symdecl_\l__stex_structures_dom_str _prop}{args}}
- {\prop_item:cn{l_stex_variable_\l_stex_get_symbol_uri_str _prop}{args}}{
+ {\prop_item:cn{l_stex_symdecl_var://\l_stex_get_symbol_uri_str _prop}{args}}{
\msg_error:nnxxxx{stex}{error/incompatible}
{\l__stex_structures_dom_str}
{\prop_item:cn{l_stex_symdecl_\l__stex_structures_dom_str _prop}{args}}
{\l_stex_get_symbol_uri_str}
- {\prop_item:cn{l_stex_variable_\l_stex_get_symbol_uri_str _prop}{args}}
+ {\prop_item:cn{l_stex_symdecl_var://\l_stex_get_symbol_uri_str _prop}{args}}
}
\prop_put:Nxx \l_tmpa_prop {\seq_item:Nn \l_tmpb_seq 1} {\stex_invoke_variable:n {\l_stex_get_symbol_uri_str}}
}{
@@ -4915,11 +5432,12 @@
}
\exp_args:NNx \tl_gput_right:Nn \g__stex_structures_aftergroup_tl {
- \prop_set_from_keyval:cn { l_stex_variable_ \l_tmpa_str _prop}{
+ \prop_set_from_keyval:cn { l_stex_symdecl_ var://\l_tmpa_str _prop}{
name = \l_tmpa_str ,
args = \prop_item:cn {l_stex_symdecl_##1_prop}{args} ,
arity = \prop_item:cn {l_stex_symdecl_##1_prop}{arity} ,
- assocs = \prop_item:cn {l_stex_symdecl_##1_prop}{assocs}
+ assocs = \prop_item:cn {l_stex_symdecl_##1_prop}{assocs} ,
+ argnames = {\prop_item:cn {l_stex_symdecl_##1_prop}{argnames}} ,
}
\cs_set_eq:cc {stex_var_notation_\l_tmpa_str _cs}
{g__stex_structures_tmpa_\l_tmpa_str _cs}
@@ -5287,6 +5805,7 @@
}
}
\clist_set_from_seq:NN \l__stex_statements_sdefinition_for_clist \l_tmpb_seq
+ \ifvmode\noindent\fi
\exp_args:Nnx
\stex_annotate:nnn{definition}{\seq_use:Nn \l_tmpb_seq {,}}{
\str_if_empty:NF \sdefinitiontype {
@@ -5445,6 +5964,7 @@
}
}
}
+ \ifvmode\noindent\fi
\exp_args:Nnx
\stex_annotate:nnn{assertion}{\seq_use:Nn \l_tmpb_seq {,}}{
\str_if_empty:NF \sassertiontype {
@@ -5590,6 +6110,7 @@
}
}
}
+ \ifvmode\noindent\fi
\exp_args:Nnx
\stex_annotate:nnn{example}{\seq_use:Nn \l_tmpb_seq {,}}{
\str_if_empty:NF \sexampletype {
@@ -5799,6 +6320,7 @@
}
}
}
+ \ifvmode\noindent\fi
\exp_args:Nnx
\stex_annotate:nnn{paragraph}{\seq_use:Nn \l_tmpb_seq {,}}{
\str_if_empty:NF \sparagraphtype {
@@ -5840,7 +6362,9 @@
title .tl_set:N = \spftitle,
continues .tl_set:N = \l__stex_sproof_spf_continues_tl,
functions .tl_set:N = \l__stex_sproof_spf_functions_tl,
- method .tl_set:N = \l__stex_sproof_spf_method_tl
+ term .tl_set:N = \l__stex_sproof_spf_term_tl,
+ method .tl_set:N = \l__stex_sproof_spf_method_tl,
+ hide .bool_set:N = \l__stex_sproof_spf_hide_bool
}
\cs_new_protected:Nn \__stex_sproof_spf_args:n {
\str_clear:N \spfid
@@ -5850,11 +6374,13 @@
\str_clear:N \spftype
\tl_clear:N \spftitle
\tl_clear:N \l__stex_sproof_spf_continues_tl
+\tl_clear:N \l__stex_sproof_spf_term_tl
\tl_clear:N \l__stex_sproof_spf_functions_tl
\tl_clear:N \l__stex_sproof_spf_method_tl
- \bool_set_false:N \l__stex_sproof_inc_counter_bool
+ \bool_set_false:N \l__stex_sproof_spf_hide_bool
\keys_set:nn { stex / spf }{ #1 }
}
+\bool_set_true:N \l__stex_sproof_inc_counter_bool
\str_set:Nn\c__stex_sproof_flow_str{inline}
\intarray_new:Nn\l__stex_sproof_counter_intarray{50}
\cs_new_protected:Npn \sproofnumber {
@@ -5987,155 +6513,130 @@
\stex_smsmode_do:
}
-\newenvironment{spfeq}[2][]{
- \__stex_sproof_spf_args:n{#1}
- \let \premise \stex_proof_premise:
- \stex_if_smsmode:TF {
- \str_if_empty:NF \spfid {
- \stex_ref_new_doc_target:n \spfid
- }
- }{
- \seq_clear:N \l_tmpa_seq
- \clist_map_inline:Nn \l__stex_sproof_spf_for_clist {
- \tl_if_empty:nF{ ##1 }{
- \stex_get_symbol:n { ##1 }
- \exp_args:NNo \seq_put_right:Nn \l_tmpa_seq {
- \l_stex_get_symbol_uri_str
- }
- }
- }
- \exp_args:Nnnx
- \begin{stex_annotate_env}{spfeq}{\seq_use:Nn \l_tmpa_seq {,}}
- \str_if_empty:NF \spftype {
- \stex_annotate_invisible:nnn{type}{\spftype}{}
- }
+\bool_set_false:N \l__stex_sproof_in_spfblock_bool
- \clist_set:No \l_tmpa_clist \spftype
- \tl_clear:N \l_tmpa_tl
- \clist_map_inline:Nn \l_tmpa_clist {
- \tl_if_exist:cT {__stex_sproof_spfeq_##1_start:}{
- \tl_set:Nn \l_tmpa_tl {\use:c{__stex_sproof_spfeq_##1_start:}}
- }
- \exp_args:No \str_if_eq:nnT \c__stex_sproof_flow_str {##1} {
- \tl_set:Nn \l_tmpa_tl {\use:n{}}
- }
- }
- \tl_if_empty:NTF \l_tmpa_tl {
- \__stex_sproof_spfeq_start:
- }{
- \l_tmpa_tl
- }{~#2}
- \str_if_empty:NF \spfid {
- \stex_ref_new_doc_target:n \spfid
- }
- \begin{displaymath}\begin{array}{rcll}
+\cs_new_protected:Nn \__stex_sproof_maybe_comment: {
+ \bool_if:NF \l__stex_sproof_in_spfblock_bool {
+ \par \setbox \l_tmpa_box \vbox \bgroup \everypar{\__stex_sproof_start_comment:}
}
- \stex_smsmode_do:
-}{
- \stex_if_smsmode:F {
- \end{array}\end{displaymath}
- \clist_set:No \l_tmpa_clist \spftype
- \tl_clear:N \l_tmpa_tl
- \clist_map_inline:Nn \l_tmpa_clist {
- \tl_if_exist:cT {__stex_sproof_spfeq_##1_end:}{
- \tl_set:Nn \l_tmpa_tl {\use:c{__stex_sproof_spfeq_##1_end:}}
+}
+\cs_new_protected:Nn \__stex_sproof_maybe_comment_end: {
+ \bool_if:NF \l__stex_sproof_in_spfblock_bool { \egroup }
+}
+\cs_new_protected:Nn \__stex_sproof_start_comment: {
+ \csname @ @ par\endcsname\egroup\item[]\bgroup\stexcommentfont
+}
+
+\cs_new_protected:Npn \stexcommentfont {
+ \small\itshape
+}
+\cs_new_protected:Nn \__stex_sproof_start_env:nnn {
+ \seq_clear:N \l_tmpa_seq
+ \clist_map_inline:Nn \l__stex_sproof_spf_for_clist {
+ \tl_if_empty:nF{ ##1 }{
+ \stex_get_symbol:n { ##1 }
+ \exp_args:NNo \seq_put_right:Nn \l_tmpa_seq {
+ \l_stex_get_symbol_uri_str
}
}
- \tl_if_empty:NTF \l_tmpa_tl {
- \__stex_sproof_spfeq_end:
- }{
- \l_tmpa_tl
- }
- \end{stex_annotate_env}
}
-}
+ \exp_args:Nnnx
+ \begin{stex_annotate_env}{#1}{\seq_use:Nn \l_tmpa_seq {,}}
+ \str_if_empty:NF \spftype {
+ \stex_annotate_invisible:nnn{type}{\spftype}{}
+ }
+ #3 {~\stex_annotate:nnn{spftitle}{}{#2}}
+ \str_if_empty:NF \spfid {
+ \stex_ref_new_doc_target:n \spfid
+ }
+ \begin{stex_annotate_env}{spfbody}{\bool_if:NTF \l__stex_sproof_spf_hide_bool {false}{true}}
+ \bool_if:NT \l__stex_sproof_spf_hide_bool{
+ \stex_html_backend:F{\setbox\l_tmpa_box\vbox\bgroup}
+ }
+ \begin{list}{}{
+ \setlength\topsep{0pt}
+ \setlength\parsep{0pt}
+ \setlength\rightmargin{0pt}
-\cs_new_protected:Nn \__stex_sproof_spfeq_start: {
- \titleemph{
- \tl_if_empty:NTF \spftitle {
- \spf@proof@kw
- }{
- \spftitle
- }
- }:
+ }\__stex_sproof_maybe_comment:
}
-\cs_new_protected:Nn \__stex_sproof_spfeq_end: {\sproofend}
-
-\newcommand\stexpatchspfeq[3][] {
- \str_set:Nx \l_tmpa_str{ #1 }
- \str_if_empty:NTF \l_tmpa_str {
- \tl_set:Nn \__stex_sproof_spfeq_start: { #2 }
- \tl_set:Nn \__stex_sproof_spfeq_end: { #3 }
- }{
- \exp_after:wN \tl_set:Nn \csname __stex_sproof_spfeq_#1_start:\endcsname{ #2 }
- \exp_after:wN \tl_set:Nn \csname __stex_sproof_spfeq_#1_end:\endcsname{ #3 }
+\cs_new_protected:Nn \__stex_sproof_end_env:n {
+ \stex_if_smsmode:F{
+ \__stex_sproof_maybe_comment_end:
+ \end{list}
+ \bool_if:NT \l__stex_sproof_spf_hide_bool{
+ \stex_html_backend:F{\egroup}
}
+ \clist_set:No \l_tmpa_clist \spftype
+ #1
+ \end{stex_annotate_env}
+ \end{stex_annotate_env}
+ }
}
-
-\newenvironment{sproof}[2][]{
- \let \premise \stex_proof_premise:
+\NewDocumentEnvironment{sproof}{s O{} m}{
\intarray_gzero:N \l__stex_sproof_counter_intarray
\intarray_gset:Nnn \l__stex_sproof_counter_intarray 1 1
- \__stex_sproof_spf_args:n{#1}
+ \stex_reactivate_macro:N \yield
+ \stex_reactivate_macro:N \eqstep
+ \stex_reactivate_macro:N \assumption
+ \stex_reactivate_macro:N \conclude
+ \stex_reactivate_macro:N \spfstep
+ \__stex_sproof_spf_args:n{#2}
\stex_if_smsmode:TF {
\str_if_empty:NF \spfid {
\stex_ref_new_doc_target:n \spfid
}
}{
- \seq_clear:N \l_tmpa_seq
- \clist_map_inline:Nn \l__stex_sproof_spf_for_clist {
- \tl_if_empty:nF{ ##1 }{
- \stex_get_symbol:n { ##1 }
- \exp_args:NNo \seq_put_right:Nn \l_tmpa_seq {
- \l_stex_get_symbol_uri_str
+ \__stex_sproof_start_env:nnn{sproof}{#3}{
+ \clist_set:No \l_tmpa_clist \spftype
+ \tl_clear:N \l_tmpa_tl
+ \clist_map_inline:Nn \l_tmpa_clist {
+ \tl_if_exist:cT {__stex_sproof_sproof_##1_start:}{
+ \tl_set:Nn \l_tmpa_tl {\use:c{__stex_sproof_sproof_##1_start:}}
+ }
+ \exp_args:No \str_if_eq:nnT \c__stex_sproof_flow_str {##1} {
+ \tl_set:Nn \l_tmpa_tl {\use:n{}}
}
}
- }
- \exp_args:Nnnx
- \begin{stex_annotate_env}{sproof}{\seq_use:Nn \l_tmpa_seq {,}}
- \str_if_empty:NF \spftype {
- \stex_annotate_invisible:nnn{type}{\spftype}{}
- }
-
- \clist_set:No \l_tmpa_clist \spftype
- \tl_clear:N \l_tmpa_tl
- \clist_map_inline:Nn \l_tmpa_clist {
- \tl_if_exist:cT {__stex_sproof_sproof_##1_start:}{
- \tl_set:Nn \l_tmpa_tl {\use:c{__stex_sproof_sproof_##1_start:}}
- }
- \exp_args:No \str_if_eq:nnT \c__stex_sproof_flow_str {##1} {
- \tl_set:Nn \l_tmpa_tl {\use:n{}}
+ \tl_if_empty:NTF \l_tmpa_tl {
+ \__stex_sproof_sproof_start:
+ }{
+ \l_tmpa_tl
}
}
- \tl_if_empty:NTF \l_tmpa_tl {
- \__stex_sproof_sproof_start:
- }{
- \l_tmpa_tl
- }{~#2}
+ }
+ \stex_smsmode_do:
+}{\__stex_sproof_end_env:n{
+ \tl_clear:N \l_tmpa_tl
+ \clist_map_inline:Nn \l_tmpa_clist {
+ \tl_if_exist:cT {__stex_sproof_sproof_##1_end:}{
+ \tl_set:Nn \l_tmpa_tl {\use:c{__stex_sproof_sproof_##1_end:}}
+ }
+ }
+ \tl_if_empty:NTF \l_tmpa_tl {
+ \__stex_sproof_sproof_end:
+ }{
+ \l_tmpa_tl
+ }
+}}
+\NewDocumentEnvironment{subproof}{s O{} m}{
+ \__stex_sproof_spf_args:n{#2}
+ \stex_if_smsmode:TF {
\str_if_empty:NF \spfid {
\stex_ref_new_doc_target:n \spfid
}
- \begin{description}
+ }{
+ \__stex_sproof_start_env:nnn{subproof}{\item[\sproofnumber]\ignorespacesandpars #3}{}
}
+ \__stex_sproof_add_counter:
\stex_smsmode_do:
-}{
- \stex_if_smsmode:F{
- \end{description}
- \clist_set:No \l_tmpa_clist \spftype
- \tl_clear:N \l_tmpa_tl
- \clist_map_inline:Nn \l_tmpa_clist {
- \tl_if_exist:cT {__stex_sproof_sproof_##1_end:}{
- \tl_set:Nn \l_tmpa_tl {\use:c{__stex_sproof_sproof_##1_end:}}
- }
- }
- \tl_if_empty:NTF \l_tmpa_tl {
- \__stex_sproof_sproof_end:
- }{
- \l_tmpa_tl
- }
- \end{stex_annotate_env}
+}{\__stex_sproof_remove_counter:\__stex_sproof_end_env:n{}
+ \bool_if:NT \l__stex_sproof_inc_counter_bool {
+ \__stex_sproof_inc_counter:
}
+ \aftergroup\__stex_sproof_maybe_comment:
}
+\AddToHook{env/subproof/before}{\__stex_sproof_maybe_comment_end:}
\cs_new_protected:Nn \__stex_sproof_sproof_start: {
\par\noindent\titleemph{
@@ -6158,211 +6659,88 @@
\exp_after:wN \tl_set:Nn \csname __stex_sproof_sproof_#1_end:\endcsname{ #3 }
}
}
-\newcommand\spfidea[2][]{
- \__stex_sproof_spf_args:n{#1}
- \titleemph{
- \tl_if_empty:NTF \spftype {Proof~Idea}{
- \spftype
- }:
- }~#2
- \sproofend
+
+\keys_define:nn { stex / spfsteps } {
+ id .str_set_x:N = \spfstepid,
+ for .clist_set:N = \l__stex_sproof_spf_for_clist ,
+ type .str_set_x:N = \spftype,
+ title .tl_set:N = \spftitle,
+ method .tl_set:N = \l__stex_sproof_spf_method_tl,
+ term .tl_set:N = \l__stex_sproof_spf_term_tl
}
-\newenvironment{spfstep}[1][]{
- \__stex_sproof_spf_args:n{#1}
- \stex_if_smsmode:TF {
- \str_if_empty:NF \spfid {
- \stex_ref_new_doc_target:n \spfid
- }
- }{
- \@in@omtexttrue
- \clist_set:No \l_tmpa_clist \spftype
- \tl_set:Nn \l_tmpa_tl {
- \item[\sproofnumber]
- \bool_set_true:N \l__stex_sproof_inc_counter_bool
- }
- \clist_map_inline:Nn \l_tmpa_clist {
- \exp_args:No \str_if_eq:nnT \c__stex_sproof_flow_str {##1} {
- \tl_clear:N \l_tmpa_tl
+\cs_new_protected:Nn \__stex_sproof_spfstep_args:n {
+\str_clear:N \spfstepid
+\clist_clear:N \l__stex_sproof_spf_for_clist
+\str_clear:N \spftype
+\tl_clear:N \l__stex_sproof_spf_method_tl
+\tl_clear:N \l__stex_sproof_spf_term_tl
+ %\bool_set_false:N \l__stex_sproof_inc_counter_bool
+\keys_set:nn { stex / spfsteps }{ #1 }
+}
+
+\cs_new_protected:Nn \__stex_sproof_make_step_macro:Nnnnn {
+ \NewDocumentCommand #1 {s O{} +m} {
+ \__stex_sproof_maybe_comment_end:
+
+ \__stex_sproof_spfstep_args:n{##2}
+ \stex_annotate:nnn{spfstep}{#2}{
+ \tl_if_empty:NF \l__stex_sproof_spf_term_tl {
+ \stex_annotate_invisible:nnn{spfyield}{}{$\l__stex_sproof_spf_term_tl$}
}
- }
- \l_tmpa_tl
- \seq_clear:N \l_tmpa_seq
- \clist_map_inline:Nn \l__stex_sproof_spf_for_clist {
- \tl_if_empty:nF{ ##1 }{
- \stex_get_symbol:n { ##1 }
- \exp_args:NNo \seq_put_right:Nn \l_tmpa_seq {
- \l_stex_get_symbol_uri_str
- }
+ \bool_if:NTF \l__stex_sproof_in_spfblock_bool {
+ #4
+ }{
+ \item[\IfBooleanTF ##1 {}{#3}]
}
+ \ignorespacesandpars ##3
}
- \exp_args:Nnnx
- \begin{stex_annotate_env}{spfstep}{\seq_use:Nn \l_tmpa_seq {,}}
- \str_if_empty:NF \spftype {
- \stex_annotate_invisible:nnn{type}{\spftype}{}
- }
- \tl_if_empty:NF \spftitle {
- {(\titleemph{\spftitle})\enspace}
- }
- \str_if_empty:NF \spfid {
- \stex_ref_new_doc_target:n \spfid
- }
- }
- \stex_smsmode_do:
- \ignorespacesandpars
-}{
- \bool_if:NT \l__stex_sproof_inc_counter_bool {
- \__stex_sproof_inc_counter:
- }
- \stex_if_smsmode:F {
- \end{stex_annotate_env}
+ \bool_if:NF \l__stex_sproof_in_spfblock_bool { \IfBooleanTF ##1 {}{ #5 } }
+ \__stex_sproof_maybe_comment:
}
+ \stex_deactivate_macro:Nn #1 {sproof~environments}
}
-\newenvironment{spfcomment}[1][]{
- \__stex_sproof_spf_args:n{#1}
- \clist_set:No \l_tmpa_clist \spftype
- \tl_set:Nn \l_tmpa_tl {
- \item[\sproofnumber]
- \bool_set_true:N \l__stex_sproof_inc_counter_bool
- }
- \clist_map_inline:Nn \l_tmpa_clist {
- \exp_args:No \str_if_eq:nnT \c__stex_sproof_flow_str {##1} {
- \tl_clear:N \l_tmpa_tl
- }
- }
- \l_tmpa_tl
-}{
- \bool_if:NT \l__stex_sproof_inc_counter_bool {
- \__stex_sproof_inc_counter:
+
+\__stex_sproof_make_step_macro:Nnnnn \assumption {assumption} \sproofnumber {} \__stex_sproof_inc_counter:
+\__stex_sproof_make_step_macro:Nnnnn \conclude {conclusion} {$\Rightarrow$} {} {}
+\__stex_sproof_make_step_macro:Nnnnn \spfstep {} \sproofnumber {} \__stex_sproof_inc_counter:
+
+\NewDocumentCommand \eqstep {s m}{
+ \__stex_sproof_maybe_comment_end:
+ \bool_if:NTF \l__stex_sproof_in_spfblock_bool {
+ $=$
+ }{
+ \item[$=$]
}
+ $\stex_annotate:nnn{spfstep}{eq}{ #2 }$
+ \__stex_sproof_maybe_comment:
}
-\newenvironment{subproof}[2][]{
- \__stex_sproof_spf_args:n{#1}
- \stex_if_smsmode:TF{
- \str_if_empty:NF \spfid {
- \stex_ref_new_doc_target:n \spfid
- }
- }{
- \seq_clear:N \l_tmpa_seq
- \clist_map_inline:Nn \l__stex_sproof_spf_for_clist {
- \tl_if_empty:nF{ ##1 }{
- \stex_get_symbol:n { ##1 }
- \exp_args:NNo \seq_put_right:Nn \l_tmpa_seq {
- \l_stex_get_symbol_uri_str
- }
- }
- }
- \exp_args:Nnnx
- \begin{stex_annotate_env}{subproof}{\seq_use:Nn \l_tmpa_seq {,}}
- \str_if_empty:NF \spftype {
- \stex_annotate_invisible:nnn{type}{\spftype}{}
- }
+\stex_deactivate_macro:Nn \eqstep {sproof~environments}
- \clist_set:No \l_tmpa_clist \spftype
- \tl_set:Nn \l_tmpa_tl {
- \item[\sproofnumber]
- \bool_set_true:N \l__stex_sproof_inc_counter_bool
- }
- \clist_map_inline:Nn \l_tmpa_clist {
- \exp_args:No \str_if_eq:nnT \c__stex_sproof_flow_str {##1} {
- \tl_clear:N \l_tmpa_tl
- }
- }
- \l_tmpa_tl
- \tl_if_empty:NF \spftitle {
- {(\titleemph{\spftitle})\enspace}
- }
- {~#2}
- \str_if_empty:NF \spfid {
- \stex_ref_new_doc_target:n \spfid
- }
- }
- \__stex_sproof_add_counter:
- \stex_smsmode_do:
-}{
- \__stex_sproof_remove_counter:
- \bool_if:NT \l__stex_sproof_inc_counter_bool {
- \__stex_sproof_inc_counter:
- }
- \stex_if_smsmode:F{
- \end{stex_annotate_env}
- }
+\NewDocumentCommand \yield {+m}{
+ \stex_annotate:nnn{spfyield}{}{ #1 }
}
-\newenvironment{spfcases}[2][]{
- \tl_if_empty:nTF{#1}{
- \begin{subproof}[method=by-cases]{#2}
- }{
- \begin{subproof}[#1,method=by-cases]{#2}
- }
+\stex_deactivate_macro:Nn \yield {sproof~environments}
+
+\NewDocumentEnvironment{spfblock}{}{
+ \item[]
+ \bool_set_true:N \l__stex_sproof_in_spfblock_bool
}{
- \end{subproof}
+ \aftergroup\__stex_sproof_maybe_comment:
}
-\newenvironment{spfcase}[2][]{
+\AddToHook{env/spfblock/before}{\__stex_sproof_maybe_comment_end:}
+
+\NewDocumentCommand\spfidea{O{} +m}{
\__stex_sproof_spf_args:n{#1}
- \stex_if_smsmode:TF {
- \str_if_empty:NF \spfid {
- \stex_ref_new_doc_target:n \spfid
- }
- }{
- \seq_clear:N \l_tmpa_seq
- \clist_map_inline:Nn \l__stex_sproof_spf_for_clist {
- \tl_if_empty:nF{ ##1 }{
- \stex_get_symbol:n { ##1 }
- \exp_args:NNo \seq_put_right:Nn \l_tmpa_seq {
- \l_stex_get_symbol_uri_str
- }
- }
- }
- \exp_args:Nnnx
- \begin{stex_annotate_env}{spfcase}{\seq_use:Nn \l_tmpa_seq {,}}
- \str_if_empty:NF \spftype {
- \stex_annotate_invisible:nnn{type}{\spftype}{}
- }
- \clist_set:No \l_tmpa_clist \spftype
- \tl_set:Nn \l_tmpa_tl {
- \item[\sproofnumber]
- \bool_set_true:N \l__stex_sproof_inc_counter_bool
- }
- \clist_map_inline:Nn \l_tmpa_clist {
- \exp_args:No \str_if_eq:nnT \c__stex_sproof_flow_str {##1} {
- \tl_clear:N \l_tmpa_tl
- }
- }
- \l_tmpa_tl
- \tl_if_empty:nF{#2}{
- \titleemph{#2}:~
- }
- }
- \__stex_sproof_add_counter:
- \stex_smsmode_do:
-}{
- \__stex_sproof_remove_counter:
- \bool_if:NT \l__stex_sproof_inc_counter_bool {
- \__stex_sproof_inc_counter:
- }
- \stex_if_smsmode:F{
- \clist_set:No \l_tmpa_clist \spftype
- \tl_set:Nn \l_tmpa_tl{\sproofend}
- \clist_map_inline:Nn \l_tmpa_clist {
- \exp_args:No \str_if_eq:nnT \c__stex_sproof_flow_str {##1} {
- \tl_clear:N \l_tmpa_tl
- }
- }
- \l_tmpa_tl
- \end{stex_annotate_env}
- }
-}
-\newcommand\spfcasesketch[3][]{
- \begin{spfcase}[#1]{#2}#3\end{spfcase}
+ \titleemph{
+ \tl_if_empty:NTF \spftype {Proof~Idea}{
+ \spftype
+ }:
+ }~#2
+ \sproofend
}
-\keys_define:nn { stex / just }{
- id .str_set_x:N = \l__stex_sproof_just_id_str,
- method .tl_set:N = \l__stex_sproof_just_method_tl,
- premises .tl_set:N = \l__stex_sproof_just_premises_tl,
- args .tl_set:N = \l__stex_sproof_just_args_tl
+\newcommand\spfjust[1]{
+ #1
}
-\newcommand\spfjust[1][]{}
-\newcommand\stex_proof_premise:[2][]{#2}
-\newcommand\justarg[2][]{#2}
%%%%%%%%%%%%% metatheory.dtx %%%%%%%%%%%%%
@@ -6516,6 +6894,8 @@
\exp_args:Nx \stex_set_current_repository:n { \l_tmpa_str }
}
}
+
+\stex_get_document_uri:
\endinput
%%
%% End of file `stex.sty'.