diff options
author | Karl Berry <karl@freefriends.org> | 2022-02-27 16:47:55 +0000 |
---|---|---|
committer | Karl Berry <karl@freefriends.org> | 2022-02-27 16:47:55 +0000 |
commit | 4b2d4c25ef033d6f3bd19e2f728691743a450685 (patch) | |
tree | c80d911cec744e2aa13b3fc24e4c3f9dcf6e7d70 /Master/texmf-dist/tex/latex/stex/stex.sty | |
parent | eceb75dcb8e604edf3fbf7542164c8974618a32c (diff) |
stex (26feb22)
git-svn-id: svn://tug.org/texlive/trunk@62230 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.sty | 5472 |
1 files changed, 5472 insertions, 0 deletions
diff --git a/Master/texmf-dist/tex/latex/stex/stex.sty b/Master/texmf-dist/tex/latex/stex/stex.sty new file mode 100644 index 00000000000..2c28b1ee36e --- /dev/null +++ b/Master/texmf-dist/tex/latex/stex/stex.sty @@ -0,0 +1,5472 @@ +%% +%% This is file `stex.sty', +%% generated with the docstrip utility. +%% +%% The original source files were: +%% +%% stex-basics.dtx (with options: `package') +%% stex-mathhub.dtx (with options: `package') +%% stex-references.dtx (with options: `package') +%% stex-modules.dtx (with options: `package') +%% stex-inheritance.dtx (with options: `package') +%% stex-symbols.dtx (with options: `package') +%% stex-terms.dtx (with options: `package') +%% stex-features.dtx (with options: `package') +%% stex-statements.dtx (with options: `package') +%% stex-proofs.dtx (with options: `package') +%% stex-others.dtx (with options: `package') +%% stex-metatheory.dtx (with options: `package') +%% + +%%%%%%%%%%%%% basics.dtx %%%%%%%%%%%%% + +\RequirePackage{expl3,l3keys2e,ltxcmds} +\ProvidesExplPackage{stex}{2022/02/26}{3.0.1}{sTeX package} + + +\keys_define:nn { stex } { + debug .clist_set:N = \c_stex_debug_clist , + lang .clist_set:N = \c_stex_languages_clist , + mathhub .tl_set_x:N = \mathhub , + sms .bool_set:N = \c_stex_persist_mode_bool , + image .bool_set:N = \c_tikzinput_image_bool, + unknown .code:n = {} +} +\ProcessKeysOptions { stex } +\protected\def\stex{% + \@ifundefined{texorpdfstring}% + {\let\texorpdfstring\@firstoftwo}% + {}% + \texorpdfstring{\raisebox{-.5ex}S\kern-.5ex\TeX}{sTeX}\xspace% +} +\def\sTeX{\stex} +\msg_new:nnn{stex}{error/unknownlanguage}{ + Unknown~language:~#1 +} +\msg_new:nnn{stex}{warning/nomathhub}{ + MATHHUB~system~variable~not~found~and~no~ + \detokenize{\mathhub}-value~set! +} +\msg_new:nnn{stex}{error/deactivated-macro}{ + The~\detokenize{#1}~command~is~only~allowed~in~#2! +} +\cs_new_protected:Nn \stex_debug:nn { + \clist_if_in:NnTF \c_stex_debug_clist { all } { + \exp_args:Nnnx\msg_set:nnn{stex}{debug / #1}{ + \\Debug~#1:~#2\\ + } + \msg_none:nn{stex}{debug / #1} + }{ + \clist_if_in:NnT \c_stex_debug_clist { #1 } { + \exp_args:Nnnx\msg_set:nnn{stex}{debug / #1}{ + \\Debug~#1:~#2\\ + } + \msg_none:nn{stex}{debug / #1} + } + } +} +\clist_if_in:NnTF \c_stex_debug_clist {all} { + \msg_redirect_module:nnn{ stex }{ none }{ term } +}{ + \clist_map_inline:Nn \c_stex_debug_clist { + \msg_redirect_name:nnn{ stex }{ debug / ##1 }{ term } + } +} + +\stex_debug:nn{log}{debug~mode~on} +\RequirePackage{rustex} +\rustex_add_Namespace:nn{stex}{http://kwarc.info/ns/sTeX} +\ifcsname if@latexml\endcsname\else + \expandafter\newif\csname if@latexml\endcsname\@latexmlfalse +\fi +\prg_new_conditional:Nnn \latexml_if: {p, T, F, TF} { + \if@latexml + \prg_return_true: + \else: + \prg_return_false: + \fi: +} +\tl_new:N \l__stex_annotate_arg_tl +\tl_const:Nx \c__stex_annotate_emptyarg_tl { + \rustex_if:TF { + \rustex_direct_HTML:n { \c_ampersand_str lrm; } + }{~} +} +\cs_new_protected:Nn \__stex_annotate_checkempty:n { + \tl_set:Nn \l__stex_annotate_arg_tl { #1 } + \tl_if_empty:NT \l__stex_annotate_arg_tl { + \tl_set_eq:NN \l__stex_annotate_arg_tl \c__stex_annotate_emptyarg_tl + } +} +\bool_new:N \_stex_html_do_output_bool +\bool_set_true:N \_stex_html_do_output_bool + +\prg_new_conditional:Nnn \stex_if_do_html: {p,T,F,TF} { + \bool_if:nTF \_stex_html_do_output_bool + \prg_return_true: \prg_return_false: +} +\cs_new_protected:Nn \stex_suppress_html:n { + \exp_args:Nne \use:nn { + \bool_set_false:N \_stex_html_do_output_bool + #1 + }{ + \stex_if_do_html:T { + \bool_set_true:N \_stex_html_do_output_bool + } + } +} +\rustex_if:TF{ + \cs_new_protected:Nn \stex_annotate:nnn { + \__stex_annotate_checkempty:n { #3 } + \rustex_annotate_HTML:nn { + property="stex:#1" ~ + resource="#2" + } { + \mode_if_vertical:TF{ + \tl_use:N \l__stex_annotate_arg_tl\par + }{ + \tl_use:N \l__stex_annotate_arg_tl + } + } + } + \cs_new_protected:Nn \stex_annotate_invisible:n { + \__stex_annotate_checkempty:n { #1 } + \rustex_annotate_HTML:nn { + stex:visible="false" ~ + style:display="none" + } { + \mode_if_vertical:TF{ + \tl_use:N \l__stex_annotate_arg_tl\par + }{ + \tl_use:N \l__stex_annotate_arg_tl + } + } + } + \cs_new_protected:Nn \stex_annotate_invisible:nnn { + \__stex_annotate_checkempty:n { #3 } + \rustex_annotate_HTML:nn { + property="stex:#1" ~ + resource="#2" ~ + stex:visible="false" ~ + style:display="none" + } { + \mode_if_vertical:TF{ + \tl_use:N \l__stex_annotate_arg_tl\par + }{ + \tl_use:N \l__stex_annotate_arg_tl + } + } + } + \NewDocumentEnvironment{stex_annotate_env} { m m } { + \par + \rustex_annotate_HTML_begin:n { + property="stex:#1" ~ + resource="#2" + } + }{ + \par\rustex_annotate_HTML_end: + } +}{ + \latexml_if:TF { + \cs_new_protected:Nn \stex_annotate:nnn { + \__stex_annotate_checkempty:n { #3 } + \mode_if_math:TF { + \cs:w latexml@annotate@math\cs_end:{#1}{#2}{ + \tl_use:N \l__stex_annotate_arg_tl + } + }{ + \cs:w latexml@annotate@text\cs_end:{#1}{#2}{ + \tl_use:N \l__stex_annotate_arg_tl + } + } + } + \cs_new_protected:Nn \stex_annotate_invisible:n { + \__stex_annotate_checkempty:n { #1 } + \mode_if_math:TF { + \cs:w latexml@invisible@math\cs_end:{ + \tl_use:N \l__stex_annotate_arg_tl + } + } { + \cs:w latexml@invisible@text\cs_end:{ + \tl_use:N \l__stex_annotate_arg_tl + } + } + } + \cs_new_protected:Nn \stex_annotate_invisible:nnn { + \__stex_annotate_checkempty:n { #3 } + \cs:w latexml@annotate@invisible\cs_end:{#1}{#2}{ + \tl_use:N \l__stex_annotate_arg_tl + } + } + \NewDocumentEnvironment{stex_annotate_env} { m m } { + \par\begin{latexml@annotateenv}{#1}{#2} + }{ + \par\end{latexml@annotateenv} + } + }{ + \cs_new_protected:Nn \stex_annotate:nnn {#3} + \cs_new_protected:Nn \stex_annotate_invisible:n {} + \cs_new_protected:Nn \stex_annotate_invisible:nnn {} + \NewDocumentEnvironment{stex_annotate_env} { m m } {}{} + } +} +\prop_const_from_keyval:Nn \c_stex_languages_prop { + en = english , + de = ngerman , + ar = arabic , + bg = bulgarian , + ru = russian , + fi = finnish , + ro = romanian , + tr = turkish , + fr = french +} + +\prop_const_from_keyval:Nn \c_stex_language_abbrevs_prop { + english = en , + ngerman = de , + arabic = ar , + bulgarian = bg , + russian = ru , + finnish = fi , + romanian = ro , + turkish = tr , + french = fr +} +\clist_if_empty:NF \c_stex_languages_clist { + \clist_clear:N \l_tmpa_clist + \clist_map_inline:Nn \c_stex_languages_clist { + \prop_get:NnNTF \c_stex_languages_prop { #1 } \l_tmpa_str { + \clist_put_right:No \l_tmpa_clist \l_tmpa_str + } { + \msg_error:nnx{stex}{error/unknownlanguage}{\l_tmpa_str} + } + } + \stex_debug:nn{lang} {Languages:~\clist_use:Nn \l_tmpa_clist {,~} } + \RequirePackage[\clist_use:Nn \l_tmpa_clist,]{babel} +} +\cs_new_protected:Nn \stex_deactivate_macro:Nn { + \exp_after:wN\let\csname \detokenize{#1} - orig\endcsname#1 + \def#1{ + \msg_error:nnnn{stex}{error/deactivated-macro}{#1}{#2} + } +} +\cs_new_protected:Nn \stex_reactivate_macro:N { + \exp_after:wN\let\exp_after:wN#1\csname \detokenize{#1} - orig\endcsname +} +\protected\def\ignorespacesandpars{ + \begingroup\catcode13=10\relax + \@ifnextchar\par{ + \endgroup\expandafter\ignorespacesandpars\@gobble + }{ + \endgroup + } +} + +%%%%%%%%%%%%% mathhub.dtx %%%%%%%%%%%%% + +\msg_new:nnn{stex}{error/norepository}{ + No~archive~#1~found~in~#2 +} +\msg_new:nnn{stex}{error/notinarchive}{ + Not~currently~in~an~archive,~but~\detokenize{#1}~ + needs~one! +} +\msg_new:nnn{stex}{error/nofile}{ + \detokenize{#1}~could~not~find~file~#2 +} +\msg_new:nnn{stex}{error/twofiles}{ + \detokenize{#1}~found~two~candidates~for~#2 +} +\cs_new_protected:Nn \stex_path_from_string:Nn { + \str_set:Nx \l_tmpa_str { #2 } + \str_if_empty:NTF \l_tmpa_str { + \seq_clear:N #1 + }{ + \exp_args:NNNo \seq_set_split:Nnn #1 / { \l_tmpa_str } + \sys_if_platform_windows:T{ + \seq_clear:N \l_tmpa_tl + \seq_map_inline:Nn #1 { + \seq_set_split:Nnn \l_tmpb_tl \c_backslash_str { ##1 } + \seq_concat:NNN \l_tmpa_tl \l_tmpa_tl \l_tmpb_tl + } + \seq_set_eq:NN #1 \l_tmpa_tl + } + \stex_path_canonicalize:N #1 + } +} + +\cs_new_protected:Nn \stex_path_to_string:NN { + \exp_args:NNe \str_set:Nn #2 { \seq_use:Nn #1 / } +} + +\cs_new:Nn \stex_path_to_string:N { + \seq_use:Nn #1 / +} +\str_const:Nn \c__stex_path_dot_str {.} +\str_const:Nn \c__stex_path_up_str {..} +\cs_new_protected:Nn \stex_path_canonicalize:N { + \seq_if_empty:NF #1 { + \seq_clear:N \l_tmpa_seq + \seq_get_left:NN #1 \l_tmpa_tl + \str_if_empty:NT \l_tmpa_tl { + \seq_put_right:Nn \l_tmpa_seq {} + } + \seq_map_inline:Nn #1 { + \str_set:Nn \l_tmpa_tl { ##1 } + \str_if_eq:NNF \l_tmpa_tl \c__stex_path_dot_str { + \str_if_eq:NNTF \l_tmpa_tl \c__stex_path_up_str { + \seq_if_empty:NTF \l_tmpa_seq { + \exp_args:NNo \seq_put_right:Nn \l_tmpa_seq { + \c__stex_path_up_str + } + }{ + \seq_get_right:NN \l_tmpa_seq \l_tmpa_tl + \str_if_eq:NNTF \l_tmpa_tl \c__stex_path_up_str { + \exp_args:NNo \seq_put_right:Nn \l_tmpa_seq { + \c__stex_path_up_str + } + }{ + \seq_pop_right:NN \l_tmpa_seq \l_tmpb_tl + } + } + }{ + \str_if_empty:NF \l_tmpa_tl { + \exp_args:NNo \seq_put_right:Nn \l_tmpa_seq { \l_tmpa_tl } + } + } + } + } + \seq_gset_eq:NN #1 \l_tmpa_seq + } +} +\prg_new_conditional:Nnn \stex_path_if_absolute:N {p, T, F, TF} { + \seq_if_empty:NTF #1 { + \prg_return_false: + }{ + \seq_get_left:NN #1 \l_tmpa_tl + \sys_if_platform_windows:TF{ + \str_if_in:NnTF \l_tmpa_tl {:}{ + \prg_return_true: + }{ + \prg_return_false: + } + }{ + \str_if_empty:NTF \l_tmpa_tl { + \prg_return_true: + }{ + \prg_return_false: + } + } + } +} +\str_new:N\l_stex_kpsewhich_return_str +\cs_new_protected:Nn \stex_kpsewhich:n { + \sys_get_shell:nnN { kpsewhich ~ #1 } { } \l_tmpa_tl + \exp_args:NNo\str_set:Nn\l_stex_kpsewhich_return_str{\l_tmpa_tl} + \tl_trim_spaces:N \l_stex_kpsewhich_return_str +} +\sys_if_platform_windows:TF{ + \begingroup\escapechar=-1\catcode`\\=12 + \exp_args:Nx\stex_kpsewhich:n{-expand-var~\c_percent_str CD\c_percent_str} + \exp_args:NNx\str_replace_all:Nnn\l_stex_kpsewhich_return_str{\c_backslash_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~PWD} +} + +\stex_path_from_string:Nn\c_stex_pwd_seq\l_stex_kpsewhich_return_str +\stex_path_to_string:NN\c_stex_pwd_seq\c_stex_pwd_str +\stex_debug:nn {mathhub} {PWD:~\str_use:N\c_stex_pwd_str} +\seq_gclear_new:N\g__stex_files_stack +\str_set:Nx \c_stex_mainfile_str {\c_stex_pwd_str/\jobname.tex} +\stex_path_from_string:Nn \c_stex_mainfile_seq + \c_stex_mainfile_str +\seq_gclear_new:N\g_stex_currentfile_seq +\cs_new_protected:Nn \stex_filestack_push:n { + \stex_path_from_string:Nn\g_stex_currentfile_seq{#1} + \stex_path_if_absolute:NF\g_stex_currentfile_seq{ + \stex_path_from_string:Nn\g_stex_currentfile_seq{ + \c_stex_pwd_str/#1 + } + } + \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 +} +\cs_new_protected:Nn \stex_filestack_pop: { + \seq_if_empty:NF\g__stex_files_stack{ + \seq_gpop:NN\g__stex_files_stack\l_tmpa_seq + } + \seq_if_empty:NTF\g__stex_files_stack{ + \seq_gset_eq:NN\g_stex_currentfile_seq\c_stex_mainfile_seq + }{ + \seq_get:NN\g__stex_files_stack\l_tmpa_seq + \seq_gset_eq:NN\g_stex_currentfile_seq\l_tmpa_seq + } +} +\AddToHook{file/before}{ + \stex_filestack_push:n{\CurrentFilePath/\CurrentFile} +} +\AddToHook{file/after}{ + \stex_filestack_pop: +} +\str_if_empty:NTF\mathhub{ + \sys_if_platform_windows:TF{ + \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\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} + } + \str_set_eq:NN\c_stex_mathhub_str\l_stex_kpsewhich_return_str + + \str_if_empty:NTF\c_stex_mathhub_str{ + \msg_warning:nn{stex}{warning/nomathhub} + }{ + \stex_debug:nn{mathhub}{MathHub:~\str_use:N\c_stex_mathhub_str} + \exp_args:NNo \stex_path_from_string:Nn\c_stex_mathhub_seq\c_stex_mathhub_str + } +}{ + \stex_path_from_string:Nn \c_stex_mathhub_seq \mathhub + \stex_path_if_absolute:NF \c_stex_mathhub_seq { + \exp_args:NNx \stex_path_from_string:Nn \c_stex_mathhub_seq { + \c_stex_pwd_str/\mathhub + } + } + \stex_path_to_string:NN\c_stex_mathhub_seq\c_stex_mathhub_str + \stex_debug:nn{mathhub} {MathHub:~\str_use:N\c_stex_mathhub_str} +} +\cs_new_protected:Nn \__stex_mathhub_do_manifest:n { + \prop_if_exist:cF {c_stex_mathhub_#1_manifest_prop} { + \str_set:Nx \l_tmpa_str { #1 } + \prop_new:c { c_stex_mathhub_#1_manifest_prop } + \seq_set_split:NnV \l_tmpa_seq / \l_tmpa_str + \seq_concat:NNN \l_tmpa_seq \c_stex_mathhub_seq \l_tmpa_seq + \__stex_mathhub_find_manifest:N \l_tmpa_seq + \seq_if_empty:NTF \l__stex_mathhub_manifest_file_seq { + \msg_error:nnxx{stex}{error/norepository}{#1}{ + \stex_path_to_string:N \c_stex_mathhub_str + } + } { + \exp_args:No \__stex_mathhub_parse_manifest:n { \l_tmpa_str } + } + } +} +\seq_new:N\l__stex_mathhub_manifest_file_seq +\cs_new_protected:Nn \__stex_mathhub_find_manifest:N { + \seq_set_eq:NN\l_tmpa_seq #1 + \bool_set_true:N\l_tmpa_bool + \bool_while_do:Nn \l_tmpa_bool { + \seq_if_empty:NTF \l_tmpa_seq { + \bool_set_false:N\l_tmpa_bool + }{ + \file_if_exist:nTF{ + \stex_path_to_string:N\l_tmpa_seq/MANIFEST.MF + }{ + \seq_put_right:Nn\l_tmpa_seq{MANIFEST.MF} + \bool_set_false:N\l_tmpa_bool + }{ + \file_if_exist:nTF{ + \stex_path_to_string:N\l_tmpa_seq/META-INF/MANIFEST.MF + }{ + \seq_put_right:Nn\l_tmpa_seq{META-INF} + \seq_put_right:Nn\l_tmpa_seq{MANIFEST.MF} + \bool_set_false:N\l_tmpa_bool + }{ + \file_if_exist:nTF{ + \stex_path_to_string:N\l_tmpa_seq/meta-inf/MANIFEST.MF + }{ + \seq_put_right:Nn\l_tmpa_seq{meta-inf} + \seq_put_right:Nn\l_tmpa_seq{MANIFEST.MF} + \bool_set_false:N\l_tmpa_bool + }{ + \seq_pop_right:NN\l_tmpa_seq\l_tmpa_tl + } + } + } + } + } + \seq_set_eq:NN\l__stex_mathhub_manifest_file_seq\l_tmpa_seq +} +\ior_new:N \c__stex_mathhub_manifest_ior +\cs_new_protected:Nn \__stex_mathhub_parse_manifest:n { + \seq_set_eq:NN \l_tmpa_seq \l__stex_mathhub_manifest_file_seq + \ior_open:Nn \c__stex_mathhub_manifest_ior {\stex_path_to_string:N \l_tmpa_seq} + \ior_map_inline:Nn \c__stex_mathhub_manifest_ior { + \str_set:Nn \l_tmpa_str {##1} + \exp_args:NNoo \seq_set_split:Nnn + \l_tmpb_seq \c_colon_str \l_tmpa_str + \seq_pop_left:NNTF \l_tmpb_seq \l_tmpa_tl { + \exp_args:NNe \str_set:Nn \l_tmpb_tl { + \exp_args:NNo \seq_use:Nn \l_tmpb_seq \c_colon_str + } + \exp_args:No \str_case:nnTF \l_tmpa_tl { + {id} { + \prop_gput:cno { c_stex_mathhub_#1_manifest_prop } + { id } \l_tmpb_tl + } + {narration-base} { + \prop_gput:cno { c_stex_mathhub_#1_manifest_prop } + { narr } \l_tmpb_tl + } + {url-base} { + \prop_gput:cno { c_stex_mathhub_#1_manifest_prop } + { docurl } \l_tmpb_tl + } + {source-base} { + \prop_gput:cno { c_stex_mathhub_#1_manifest_prop } + { ns } \l_tmpb_tl + } + {ns} { + \prop_gput:cno { c_stex_mathhub_#1_manifest_prop } + { ns } \l_tmpb_tl + } + {dependencies} { + \prop_gput:cno { c_stex_mathhub_#1_manifest_prop } + { deps } \l_tmpb_tl + } + }{}{} + }{} + } + \ior_close:N \c__stex_mathhub_manifest_ior +} +\cs_new_protected:Nn \stex_set_current_repository:n { + \stex_require_repository:n { #1 } + \prop_set_eq:Nc \l_stex_current_repository_prop { + c_stex_mathhub_#1_manifest_prop + } +} +\cs_new_protected:Nn \stex_require_repository:n { + \prop_if_exist:cF { c_stex_mathhub_#1_manifest_prop } { + \stex_debug:nn{mathhub}{Opening~archive:~#1} + \__stex_mathhub_do_manifest:n { #1 } + } +} + +\__stex_mathhub_find_manifest:N \c_stex_pwd_seq +\seq_if_empty:NTF \l__stex_mathhub_manifest_file_seq { + \stex_debug:nn{mathhub}{Not~currently~in~a~MathHub~repository} +} { + \__stex_mathhub_parse_manifest:n { main } + \prop_get:NnN \c_stex_mathhub_main_manifest_prop {id} + \l_tmpa_str + \prop_set_eq:cN { c_stex_mathhub_\l_tmpa_str _manifest_prop } + \c_stex_mathhub_main_manifest_prop + \exp_args:Nx \stex_set_current_repository:n { \l_tmpa_str } + \stex_debug:nn{mathhub}{Current~repository:~ + \prop_item:Nn \l_stex_current_repository_prop {id} + } +} +\cs_new_protected:Nn \stex_in_repository:nn { + \str_set:Nx \l_tmpa_str { #1 } + \cs_set:Npn \l_tmpa_cs ##1 { #2 } + \str_if_empty:NTF \l_tmpa_str { + \prop_if_exist:NTF \l_stex_current_repository_prop { + \stex_debug:nn{mathhub}{do~in~current~repository:~\prop_item:Nn \l_stex_current_repository_prop { id }} + \exp_args:Ne \l_tmpa_cs{ + \prop_item:Nn \l_stex_current_repository_prop { id } + } + }{ + \l_tmpa_cs{} + } + }{ + \stex_debug:nn{mathhub}{in~repository:~\l_tmpa_str} + \stex_require_repository:n \l_tmpa_str + \str_set:Nx \l_tmpa_str { #1 } + \exp_args:Nne \use:nn { + \stex_set_current_repository:n \l_tmpa_str + \exp_args:Nx \l_tmpa_cs{\l_tmpa_str} + }{ + \stex_debug:nn{mathhub}{switching~back~to:~ + \prop_if_exist:NTF \l_stex_current_repository_prop { + \prop_item:Nn \l_stex_current_repository_prop { id }:~ + \meaning\l_stex_current_repository_prop + }{ + no~repository + } + } + \prop_if_exist:NTF \l_stex_current_repository_prop { + \stex_set_current_repository:n { + \prop_item:Nn \l_stex_current_repository_prop { id } + } + }{ + \let\exp_not:N\l_stex_current_repository_prop\exp_not:N\undefined + } + } + } +} +\def \mhpath #1 #2 { + \exp_args:Ne \tl_if_empty:nTF{#1}{ + \c_stex_mathhub_str / + \prop_item:Nn \l_stex_current_repository_prop { id } + / source / #2 + }{ + \c_stex_mathhub_str / #1 / source / #2 + } +} +\newif \ifinputref \inputreffalse + +\cs_new_protected:Nn \__stex_mathhub_mhinput:nn { + \stex_in_repository:nn {#1} { + \ifinputref + \input{ \c_stex_mathhub_str / ##1 / source / #2 } + \else + \inputreftrue + \input{ \c_stex_mathhub_str / ##1 / source / #2 } + \inputreffalse + \fi + } +} +\NewDocumentCommand \mhinput { O{} m}{ + \stex_mhinput:nn{ #1 }{ #2 } +} + +\cs_new_protected:Nn \__stex_mathhub_inputref:nn { + \stex_in_repository:nn {#1} { + \bool_lazy_any:nTF { + {\rustex_if_p:} + {\latexml_if_p:} + } { + \str_clear:N \l_tmpa_str + \prop_get:NnNF \l_stex_current_repository_prop { narr } \l_tmpa_str { + \prop_get:NnNF \l_stex_current_repository_prop { ns } \l_tmpa_str {} + } + \stex_annotate_invisible:nnn{inputref}{ + \l_tmpa_str / #2 + }{} + }{ + \begingroup + \inputreftrue + \input{ \c_stex_mathhub_str / ##1 / source / #2 } + \endgroup + } + } +} +\NewDocumentCommand \inputref { O{} m}{ + \__stex_mathhub_inputref:nn{ #1 }{ #2 } +} +\cs_new_protected:Nn \__stex_mathhub_mhbibresource:nn { + \stex_in_repository:nn {#1} { + \addbibresource{ \c_stex_mathhub_str / ##1 / #2 } + } +} +\newcommand\addmhbibresource[2][]{ + \__stex_mathhub_mhbibresource:nn{ #1 }{ #2 } +} +\cs_new_protected:Npn \libinput #1 { + \prop_if_exist:NF \l_stex_current_repository_prop { + \msg_error:nnn{stex}{error/notinarchive}\libinput + } + \prop_get:NnNF \l_stex_current_repository_prop {id} \l_tmpa_str { + \msg_error:nnn{stex}{error/notinarchive}\libinput + } + \seq_clear:N \l__stex_mathhub_libinput_files_seq + \seq_set_eq:NN \l_tmpa_seq \c_stex_mathhub_seq + \seq_set_split:NnV \l_tmpb_seq / \l_tmpa_str + + \bool_while_do:nn { ! \seq_if_empty_p:N \l_tmpb_seq }{ + \str_set:Nx \l_tmpa_str {\stex_path_to_string:N \l_tmpa_seq / meta-inf / lib / #1.tex} + \IfFileExists{ \l_tmpa_str }{ + \seq_put_right:No \l__stex_mathhub_libinput_files_seq \l_tmpa_str + }{} + \seq_pop_left:NN \l_tmpb_seq \l_tmpa_str + \seq_put_right:No \l_tmpa_seq \l_tmpa_str + } + + \str_set:Nx \l_tmpa_str {\stex_path_to_string:N \l_tmpa_seq / lib / #1.tex} + \IfFileExists{ \l_tmpa_str }{ + \seq_put_right:No \l__stex_mathhub_libinput_files_seq \l_tmpa_str + }{} + + \seq_if_empty:NTF \l__stex_mathhub_libinput_files_seq { + \msg_error:nnxx{stex}{error/nofile}{\exp_not:N\libinput}{#1.tex} + }{ + \seq_map_inline:Nn \l__stex_mathhub_libinput_files_seq { + \input{ ##1 } + } + } +} +\NewDocumentCommand \libusepackage {O{} m} { + \prop_if_exist:NF \l_stex_current_repository_prop { + \msg_error:nnn{stex}{error/notinarchive}\libusepackage + } + \prop_get:NnNF \l_stex_current_repository_prop {id} \l_tmpa_str { + \msg_error:nnn{stex}{error/notinarchive}\libusepackage + } + \seq_clear:N \l__stex_mathhub_libinput_files_seq + \seq_set_eq:NN \l_tmpa_seq \c_stex_mathhub_seq + \seq_set_split:NnV \l_tmpb_seq / \l_tmpa_str + + \bool_while_do:nn { ! \seq_if_empty_p:N \l_tmpb_seq }{ + \str_set:Nx \l_tmpa_str {\stex_path_to_string:N \l_tmpa_seq / meta-inf / lib / #2} + \IfFileExists{ \l_tmpa_str.sty }{ + \seq_put_right:No \l__stex_mathhub_libinput_files_seq \l_tmpa_str + }{} + \seq_pop_left:NN \l_tmpb_seq \l_tmpa_str + \seq_put_right:No \l_tmpa_seq \l_tmpa_str + } + + \str_set:Nx \l_tmpa_str {\stex_path_to_string:N \l_tmpa_seq / lib / #2} + \IfFileExists{ \l_tmpa_str.sty }{ + \seq_put_right:No \l__stex_mathhub_libinput_files_seq \l_tmpa_str + }{} + + \seq_if_empty:NTF \l__stex_mathhub_libinput_files_seq { + \msg_error:nnxx{stex}{error/nofile}{\exp_not:N\libusepackage}{#2.sty} + }{ + \int_compare:nNnTF {\seq_count:N \l__stex_mathhub_libinput_files_seq} = 1 { + \seq_map_inline:Nn \l__stex_mathhub_libinput_files_seq { + \usepackage[#1]{ ##1 } + } + }{ + \msg_error:nnxx{stex}{error/twofiles}{\exp_not:N\libusepackage}{#2.sty} + } + } +} + +\AddToHook{begindocument}{ +\ltx@ifpackageloaded{graphicx}{ + \define@key{Gin}{mhrepos}{\def\Gin@mhrepos{#1}} + \newcommand\mhgraphics[2][]{% + \def\Gin@mhrepos{}\setkeys{Gin}{#1}% + \includegraphics[#1]{\mhpath\Gin@mhrepos{#2}}} + \newcommand\cmhgraphics[2][]{\begin{center}\mhgraphics[#1]{#2}\end{center}} + }{} +\ltx@ifpackageloaded{listings}{ + \define@key{lst}{mhrepos}{\def\lst@mhrepos{#1}} + \newcommand\lstinputmhlisting[2][]{% + \def\lst@mhrepos{}\setkeys{lst}{#1}% + \lstinputlisting[#1]{\mhpath\lst@mhrepos{#2}}} + \newcommand\clstinputmhlisting[2][]{\begin{center}\lstinputmhlisting[#1]{#2}\end{center}} + }{} +} + + +%%%%%%%%%%%%% references.dtx %%%%%%%%%%%%% + + +\AddToHook{begindocument}{ +} +\AddToHook{enddocument}{ +} +\str_set:Nn \g__stex_refs_title_tl {Unnamed~Document} + +\NewDocumentCommand \STEXreftitle { m } { + \tl_gset:Nx \g__stex_refs_title_tl { #1 } +} +\str_new:N \l_stex_current_docns_str +\cs_new_protected:Nn \stex_get_document_uri: { + \seq_set_eq:NN \l_tmpa_seq \g_stex_currentfile_seq + \seq_pop_right:NN \l_tmpa_seq \l_tmpb_str + \exp_args:NNno \seq_set_split:Nnn \l_tmpb_seq . \l_tmpb_str + \seq_get_left:NN \l_tmpb_seq \l_tmpb_str + \seq_put_right:No \l_tmpa_seq \l_tmpb_str + + \str_clear:N \l_tmpa_str + \prop_if_exist:NT \l_stex_current_repository_prop { + \prop_get:NnNF \l_stex_current_repository_prop { narr } \l_tmpa_str { + \prop_get:NnNF \l_stex_current_repository_prop { ns } \l_tmpa_str {} + } + } + + \str_if_empty:NTF \l_tmpa_str { + \str_set:Nx \l_stex_current_docns_str { + file:/\stex_path_to_string:N \l_tmpa_seq + } + }{ + \bool_set_true:N \l_tmpa_bool + \bool_while_do:Nn \l_tmpa_bool { + \seq_pop_left:NN \l_tmpa_seq \l_tmpb_str + \exp_args:No \str_case:nnTF { \l_tmpb_str } { + {source} { \bool_set_false:N \l_tmpa_bool } + }{}{ + \seq_if_empty:NT \l_tmpa_seq { + \bool_set_false:N \l_tmpa_bool + } + } + } + + \seq_if_empty:NTF \l_tmpa_seq { + \str_set_eq:NN \l_stex_current_docns_str \l_tmpa_str + }{ + \str_set:Nx \l_stex_current_docns_str { + \l_tmpa_str/\stex_path_to_string:N \l_tmpa_seq + } + } + } +} +\str_new:N \l_stex_current_docurl_str +\cs_new_protected:Nn \stex_get_document_url: { + \seq_set_eq:NN \l_tmpa_seq \g_stex_currentfile_seq + \seq_pop_right:NN \l_tmpa_seq \l_tmpb_str + \exp_args:NNno \seq_set_split:Nnn \l_tmpb_seq . \l_tmpb_str + \seq_get_left:NN \l_tmpb_seq \l_tmpb_str + \seq_put_right:No \l_tmpa_seq \l_tmpb_str + + \str_clear:N \l_tmpa_str + \prop_if_exist:NT \l_stex_current_repository_prop { + \prop_get:NnNF \l_stex_current_repository_prop { docurl } \l_tmpa_str { + \prop_get:NnNF \l_stex_current_repository_prop { narr } \l_tmpa_str { + \prop_get:NnNF \l_stex_current_repository_prop { ns } \l_tmpa_str {} + } + } + } + + \str_if_empty:NTF \l_tmpa_str { + \str_set:Nx \l_stex_current_docurl_str { + file:/\stex_path_to_string:N \l_tmpa_seq + } + }{ + \bool_set_true:N \l_tmpa_bool + \bool_while_do:Nn \l_tmpa_bool { + \seq_pop_left:NN \l_tmpa_seq \l_tmpb_str + \exp_args:No \str_case:nnTF { \l_tmpb_str } { + {source} { \bool_set_false:N \l_tmpa_bool } + }{}{ + \seq_if_empty:NT \l_tmpa_seq { + \bool_set_false:N \l_tmpa_bool + } + } + } + + \seq_if_empty:NTF \l_tmpa_seq { + \str_set_eq:NN \l_stex_current_docurl_str \l_tmpa_str + }{ + \str_set:Nx \l_stex_current_docurl_str { + \l_tmpa_str/\stex_path_to_string:N \l_tmpa_seq + } + } + } +} +\str_const:Nn \c__stex_refs_url_str{URL} +\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:Nn \stex_ref_new_doc_target:n { + \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 + \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 + } + \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 + }{ + %\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,} + \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 + } +} +\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 + } +} +\AtEndDocument{ + \def\stexauxadddocref#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 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 , +} +\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 + \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_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 { + \str_if_exist:cTF {sref_sym_#2 _label_str }{ + \sref[#1]{\use:c{sref_sym_#2 _label_str}} + }{ + \__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 + } + } + }{ + \tl_if_empty:NTF \l__stex_refs_linktext_tl \l__stex_refs_fallback_tl \l__stex_refs_linktext_tl + } + }{ + % TODO + } + } +} +\cs_new_protected:Npn \srefsymuri #1 #2 { + \__stex_refs_sym_aux:nn{linktext={#2}}{#1} +} + +%%%%%%%%%%%%% modules.dtx %%%%%%%%%%%%% + +\msg_new:nnn{stex}{error/unknownmodule}{ + No~module~#1~found +} +\msg_new:nnn{stex}{error/syntax}{ + Syntax~error:~#1 +} +\msg_new:nnn{stex}{error/siglanguage}{ + Module~#1~declares~signature~#2,~but~does~not~ + declare~its~language +} +\msg_new:nnn{stex}{warning/deprecated}{ + #1~is~deprecated;~please~use~#2~instead! +} + +\msg_new:nnn{stex}{error/conflictingmodules}{ + Conflicting~imports~for~module~#1 +} +\str_new:N \l_stex_current_module_str +\seq_new:N \l_stex_all_modules_seq +\prg_new_conditional:Nnn \stex_if_in_module: {p, T, F, TF} { + \str_if_empty:NTF \l_stex_current_module_str + \prg_return_false: \prg_return_true: +} +\prg_new_conditional:Nnn \stex_if_module_exists:n {p, T, F, TF} { + \prop_if_exist:cTF { c_stex_module_#1_prop } + \prg_return_true: \prg_return_false: +} +\cs_new_protected:Nn \stex_add_to_current_module:n { + \tl_gput_right:cn {c_stex_module_\l_stex_current_module_str _code} { #1 } +} +\cs_new_protected:Npn \STEXexport { + \begingroup + \newlinechar=-1\relax + \endlinechar=-1\relax + %\catcode`\ = 9\relax + \expandafter\endgroup\__stex_modules_export:n +} +\cs_new_protected:Nn \__stex_modules_export:n { + \ignorespaces #1 + \stex_add_to_current_module:n { \ignorespaces #1 } + \stex_smsmode_do: +} +\stex_deactivate_macro:Nn \STEXexport {module~environments} +\cs_new_protected:Nn \stex_add_constant_to_current_module:n { + \str_set:Nx \l_tmpa_str { #1 } + \seq_gput_right:co {c_stex_module_\l_stex_current_module_str _constants} { \l_tmpa_str } +} +\cs_new_protected:Nn \stex_add_import_to_current_module:n { + \str_set:Nx \l_tmpa_str { #1 } + \exp_args:Nno + \seq_if_in:cnF{c_stex_module_\l_stex_current_module_str _imports}\l_tmpa_str{ + \seq_gput_right:co{c_stex_module_\l_stex_current_module_str _imports}\l_tmpa_str + } +} +\cs_new_protected:Nn \stex_collect_imports:n { + \seq_clear:N \l_stex_collect_imports_seq + \__stex_modules_collect_imports:n {#1} +} +\cs_new_protected:Nn \__stex_modules_collect_imports:n { + \seq_map_inline:cn {c_stex_module_#1_imports} { + \seq_if_in:NnF \l_stex_collect_imports_seq { ##1 } { + \__stex_modules_collect_imports:n { ##1 } + } + } + \seq_if_in:NnF \l_stex_collect_imports_seq { #1 } { + \seq_put_right:Nx \l_stex_collect_imports_seq { #1 } + } +} +\int_new:N \l__stex_modules_group_depth_int +\tl_new:N \l__stex_modules_aftergroup_tl +\cs_new_protected:Nn \stex_do_up_to_module:n { + \int_compare:nNnTF \l__stex_modules_group_depth_int = \currentgrouplevel { + #1 + }{ + #1 + \expandafter \tl_gset:Nn \expandafter \l__stex_modules_aftergroup_tl \expandafter { \l__stex_modules_aftergroup_tl #1 } + \aftergroup\__stex_modules_aftergroup_do: + } +} +\cs_new_protected:Nn \__stex_modules_aftergroup_do: { + \int_compare:nNnTF \l__stex_modules_group_depth_int = \currentgrouplevel { + \l__stex_modules_aftergroup_tl + \tl_clear:N \l__stex_modules_aftergroup_tl + }{ + \l__stex_modules_aftergroup_tl + \aftergroup\__stex_modules_aftergroup_do: + } +} + +\str_new:N \l_stex_modules_ns_str +\str_new:N \l_stex_modules_subpath_str +\cs_new_protected:Nn \__stex_modules_compute_namespace:nN { + \str_set:Nx \l_tmpa_str { #1 } + \seq_set_eq:NN \l_tmpa_seq #2 + % split off file extension + \seq_pop_right:NN \l_tmpa_seq \l_tmpb_str + \exp_args:NNno \seq_set_split:Nnn \l_tmpb_seq . \l_tmpb_str + \seq_get_left:NN \l_tmpb_seq \l_tmpb_str + \seq_put_right:No \l_tmpa_seq \l_tmpb_str + + \bool_set_true:N \l_tmpa_bool + \bool_while_do:Nn \l_tmpa_bool { + \seq_pop_left:NN \l_tmpa_seq \l_tmpb_str + \exp_args:No \str_case:nnTF { \l_tmpb_str } { + {source} { \bool_set_false:N \l_tmpa_bool } + }{}{ + \seq_if_empty:NT \l_tmpa_seq { + \bool_set_false:N \l_tmpa_bool + } + } + } + + \stex_path_to_string:NN \l_tmpa_seq \l_stex_modules_subpath_str + \str_if_empty:NTF \l_stex_modules_subpath_str { + \str_set_eq:NN \l_stex_modules_ns_str \l_tmpa_str + }{ + \str_set:Nx \l_stex_modules_ns_str { + \l_tmpa_str/\l_stex_modules_subpath_str + } + } +} + +\cs_new_protected:Nn \stex_modules_current_namespace: { + \str_clear:N \l_stex_modules_subpath_str + \prop_if_exist:NTF \l_stex_current_repository_prop { + \prop_get:NnN \l_stex_current_repository_prop { ns } \l_tmpa_str + \__stex_modules_compute_namespace:nN \l_tmpa_str \g_stex_currentfile_seq + }{ + % split off file extension + \seq_set_eq:NN \l_tmpa_seq \g_stex_currentfile_seq + \seq_pop_right:NN \l_tmpa_seq \l_tmpb_str + \exp_args:NNno \seq_set_split:Nnn \l_tmpb_seq . \l_tmpb_str + \seq_get_left:NN \l_tmpb_seq \l_tmpb_str + \seq_put_right:No \l_tmpa_seq \l_tmpb_str + \str_set:Nx \l_stex_modules_ns_str { + file:/\stex_path_to_string:N \l_tmpa_seq + } + } +} +\keys_define:nn { stex / module } { + title .tl_set:N = \smoduletitle , + type .str_set_x:N = \smoduletype , + id .str_set_x:N = \smoduleid , + deprecate .str_set_x:N = \l_stex_module_deprecate_str , + ns .str_set_x:N = \l_stex_module_ns_str , + lang .str_set_x:N = \l_stex_module_lang_str , + sig .str_set_x:N = \l_stex_module_sig_str , + creators .str_set_x:N = \l_stex_module_creators_str , + contributors .str_set_x:N = \l_stex_module_contributors_str , + meta .str_set_x:N = \l_stex_module_meta_str , + srccite .str_set_x:N = \l_stex_module_srccite_str +} + +\cs_new_protected:Nn \__stex_modules_args:n { + \str_clear:N \smoduletitle + \str_clear:N \smoduletype + \str_clear:N \smoduleid + \str_clear:N \l_stex_module_ns_str + \str_clear:N \l_stex_module_deprecate_str + \str_clear:N \l_stex_module_lang_str + \str_clear:N \l_stex_module_sig_str + \str_clear:N \l_stex_module_creators_str + \str_clear:N \l_stex_module_contributors_str + \str_clear:N \l_stex_module_meta_str + \str_clear:N \l_stex_module_srccite_str + \keys_set:nn { stex / module } { #1 } +} + + +\cs_new_protected:Nn \stex_module_setup:nn { + \str_set:Nx \l_stex_module_name_str { #2 } + \__stex_modules_args:n { #1 } + \stex_if_in_module:TF { + % Nested module + \prop_get:cnN {c_stex_module_\l_stex_current_module_str _prop} + { ns } \l_stex_module_ns_str + \str_set:Nx \l_stex_module_name_str { + \prop_item:cn {c_stex_module_\l_stex_current_module_str _prop} + { name } / \l_stex_module_name_str + } + }{ + % not nested: + \str_if_empty:NT \l_stex_module_ns_str { + \stex_modules_current_namespace: + \str_set_eq:NN \l_stex_module_ns_str \l_stex_modules_ns_str + \exp_args:NNNo \seq_set_split:Nnn \l_tmpa_seq + / {\l_stex_module_ns_str} + \seq_pop_right:NN \l_tmpa_seq \l_tmpa_str + \str_if_eq:NNT \l_tmpa_str \l_stex_module_name_str { + \str_set:Nx \l_stex_module_ns_str { + \stex_path_to_string:N \l_tmpa_seq + } + } + } + } + \str_if_empty:NT \l_stex_module_lang_str { + \seq_get_right:NN \g_stex_currentfile_seq \l_tmpa_str + \seq_set_split:NnV \l_tmpa_seq . \l_tmpa_str + \seq_pop_right:NN \l_tmpa_seq \l_tmpa_str % .tex + \seq_pop_left:NN \l_tmpa_seq \l_tmpa_str % <filename> + \seq_if_empty:NF \l_tmpa_seq { %remaining element should be language + \stex_debug:nn{modules} {Language~\l_stex_module_lang_str~ + inferred~from~file~name} + \seq_pop_left:NN \l_tmpa_seq \l_stex_module_lang_str + } + } + + \stex_if_smsmode:F { \str_if_empty:NF \l_stex_module_lang_str { + \prop_get:NVNTF \c_stex_languages_prop \l_stex_module_lang_str + \l_tmpa_str { + \ltx@ifpackageloaded{babel}{ + \exp_args:Nx \selectlanguage { \l_tmpa_str } + }{} + } { + \msg_error:nnx{stex}{error/unknownlanguage}{\l_tmpa_str} + } + }} + \str_if_empty:NTF \l_stex_module_sig_str { + \exp_args:Nnx \prop_gset_from_keyval:cn { + c_stex_module_\l_stex_module_ns_str?\l_stex_module_name_str _prop + } { + name = \l_stex_module_name_str , + ns = \l_stex_module_ns_str , + file = \exp_not:o { \g_stex_currentfile_seq } , + lang = \l_stex_module_lang_str , + sig = \l_stex_module_sig_str , + deprecate = \l_stex_module_deprecate_str , + meta = \l_stex_module_meta_str + } + \seq_clear:c {c_stex_module_\l_stex_module_ns_str?\l_stex_module_name_str _imports} + \seq_clear:c {c_stex_module_\l_stex_module_ns_str?\l_stex_module_name_str _constants} + \tl_clear:c {c_stex_module_\l_stex_module_ns_str?\l_stex_module_name_str _code} + \str_set:Nx\l_stex_current_module_str{\l_stex_module_ns_str?\l_stex_module_name_str} + \str_if_empty:NT \l_stex_module_meta_str { + \str_set:Nx \l_stex_module_meta_str { + \c_stex_metatheory_ns_str ? Metatheory + } + } + \str_if_eq:VnF \l_stex_module_meta_str {NONE} { + \bool_set_true:N \l_stex_in_meta_bool + \exp_args:Nx \stex_add_to_current_module:n { + \bool_set_true:N \l_stex_in_meta_bool + \stex_activate_module:n {\l_stex_module_meta_str} + \bool_set_false:N \l_stex_in_meta_bool + } + \stex_activate_module:n {\l_stex_module_meta_str} + \bool_set_false:N \l_stex_in_meta_bool + } + }{ + \str_if_empty:NT \l_stex_module_lang_str { + \msg_error:nnxx{stex}{error/siglanguage}{ + \l_stex_module_ns_str?\l_stex_module_name_str + }{\l_stex_module_sig_str} + } + + \seq_set_eq:NN \l_tmpa_seq \g_stex_currentfile_seq + \seq_pop_right:NN \l_tmpa_seq \l_tmpa_str + \seq_set_split:NnV \l_tmpb_seq . \l_tmpa_str + \seq_pop_right:NN \l_tmpb_seq \l_tmpa_str % .tex + \seq_pop_left:NN \l_tmpb_seq \l_tmpa_str % <filename> + \str_set:Nx \l_tmpa_str { + \stex_path_to_string:N \l_tmpa_seq / + \l_tmpa_str . \l_stex_module_sig_str .tex + } + \IfFileExists \l_tmpa_str { + \exp_args:No \stex_file_in_smsmode:nn { \l_tmpa_str } { + \str_clear:N \l_stex_current_module_str + \seq_clear:N \l_stex_all_modules_seq + \stex_debug:nn{modules}{Loading~signature~\l_tmpa_str} + } + }{ + \msg_error:nnx{stex}{error/unknownmodule}{for~signature~\l_tmpa_str} + } + \stex_if_smsmode:F { + \stex_activate_module:n { + \l_stex_module_ns_str ? \l_stex_module_name_str + } + } + \str_set:Nx\l_stex_current_module_str{\l_stex_module_ns_str?\l_stex_module_name_str} + } + \str_if_empty:NF \l_stex_module_deprecate_str { + \msg_warning:nnxx{stex}{warning/deprecated}{ + Module~\l_stex_current_module_str + }{ + \l_stex_module_deprecate_str + } + } + \seq_put_right:Nx \l_stex_all_modules_seq { + \l_stex_module_ns_str ? \l_stex_module_name_str + } +} +\cs_new_protected:Nn \__stex_modules_begin_module: { + \stex_reactivate_macro:N \STEXexport + \stex_reactivate_macro:N \importmodule + \stex_reactivate_macro:N \symdecl + \stex_reactivate_macro:N \notation + \stex_reactivate_macro:N \symdef + + \stex_debug:nn{modules}{ + New~module:\\ + Namespace:~\l_stex_module_ns_str\\ + Name:~\l_stex_module_name_str\\ + Language:~\l_stex_module_lang_str\\ + Signature:~\l_stex_module_sig_str\\ + Metatheory:~\l_stex_module_meta_str\\ + File:~\stex_path_to_string:N \g_stex_currentfile_seq + } + + \stex_if_smsmode:F{ + \begin{stex_annotate_env} {theory} { + \l_stex_module_ns_str ? \l_stex_module_name_str + } + + \stex_annotate_invisible:nnn{header}{} { + \stex_annotate:nnn{language}{ \l_stex_module_lang_str }{} + \stex_annotate:nnn{signature}{ \l_stex_module_sig_str }{} + \str_if_eq:VnF \l_stex_module_meta_str {NONE} { + \stex_annotate:nnn{metatheory}{ \l_stex_module_meta_str }{} + } + \str_if_empty:NF \smoduletype { + \stex_annotate:nnn{type}{\smoduletype}{} + } + } + } + \int_set:Nn \l__stex_modules_group_depth_int {\currentgrouplevel} + % TODO: Inherit metatheory for nested modules? +} +\iffalse \end{stex_annotate_env} \fi %^^A make syntax highlighting work again +\cs_new_protected:Nn \__stex_modules_end_module: { + \stex_debug:nn{modules}{Closing~module~\prop_item:cn {c_stex_module_\l_stex_current_module_str _prop} { name }} +} +\iffalse \begin{stex_annotate_env} \fi %^^A make syntax highlighting work again +\NewDocumentEnvironment { smodule } { O{} m } { + \stex_module_setup:nn{#1}{#2} + \par + \stex_if_smsmode:F{ + \tl_clear:N \l_tmpa_tl + \clist_map_inline:Nn \smoduletype { + \tl_if_exist:cT {__stex_modules_smodule_##1_start:}{ + \tl_set:Nn \l_tmpa_tl {\use:c{__stex_modules_smodule_##1_start:}} + } + } + \tl_if_empty:NTF \l_tmpa_tl { + \__stex_modules_smodule_start: + }{ + \l_tmpa_tl + } + } + \__stex_modules_begin_module: + \str_if_empty:NF \smoduleid { + \stex_ref_new_doc_target:n \smoduleid + } + \stex_smsmode_do: +} { + \__stex_modules_end_module: + \stex_if_smsmode:F { + \end{stex_annotate_env} + \clist_set:No \l_tmpa_clist \smoduletype + \tl_clear:N \l_tmpa_tl + \clist_map_inline:Nn \l_tmpa_clist { + \tl_if_exist:cT {__stex_modules_smodule_##1_end:}{ + \tl_set:Nn \l_tmpa_tl {\use:c{__stex_modules_smodule_##1_end:}} + } + } + \tl_if_empty:NTF \l_tmpa_tl { + \__stex_modules_smodule_end: + }{ + \l_tmpa_tl + } + } +} +\cs_new_protected:Nn \__stex_modules_smodule_start: {} +\cs_new_protected:Nn \__stex_modules_smodule_end: {} + +\newcommand\stexpatchmodule[3][] { + \str_set:Nx \l_tmpa_str{ #1 } + \str_if_empty:NTF \l_tmpa_str { + \tl_set:Nn \__stex_modules_smodule_start: { #2 } + \tl_set:Nn \__stex_modules_smodule_end: { #3 } + }{ + \exp_after:wN \tl_set:Nn \csname __stex_modules_smodule_#1_start:\endcsname{ #2 } + \exp_after:wN \tl_set:Nn \csname __stex_modules_smodule_#1_end:\endcsname{ #3 } + } +} +\NewDocumentCommand \STEXModule { m } { + \exp_args:NNx \str_set:Nn \l_tmpa_str { #1 } + \int_set:Nn \l_tmpa_int { \str_count:N \l_tmpa_str } + \tl_set:Nn \l_tmpa_tl { + \msg_error:nnx{stex}{error/unknownmodule}{#1} + } + \seq_map_inline:Nn \l_stex_all_modules_seq { + \str_set:Nn \l_tmpb_str { ##1 } + \str_if_eq:eeT { \l_tmpa_str } { + \str_range:Nnn \l_tmpb_str { -\l_tmpa_int } { -1 } + } { + \seq_map_break:n { + \tl_set:Nn \l_tmpa_tl { + \stex_invoke_module:n { ##1 } + } + } + } + } + \l_tmpa_tl +} + +\cs_new_protected:Nn \stex_invoke_module:n { + \stex_debug:nn{modules}{Invoking~module~#1} + \peek_charcode_remove:NTF ! { + \__stex_modules_invoke_uri:nN { #1 } + } { + \peek_charcode_remove:NTF ? { + \__stex_modules_invoke_symbol:nn { #1 } + } { + \msg_error:nnx{stex}{error/syntax}{ + ?~or~!~expected~after~ + \c_backslash_str STEXModule{#1} + } + } + } +} + +\cs_new_protected:Nn \__stex_modules_invoke_uri:nN { + \str_set:Nn #2 { #1 } +} + +\cs_new_protected:Nn \__stex_modules_invoke_symbol:nn { + \stex_invoke_symbol:n{#1?#2} +} +\bool_new:N \l_stex_in_meta_bool +\bool_set_false:N \l_stex_in_meta_bool +\cs_new_protected:Nn \stex_activate_module:n { + \stex_debug:nn{modules}{Activating~module~#1} + \seq_if_in:NnT \l_stex_implicit_morphisms_seq { #1 }{ + \msg_error:nnn{stex}{error/conflictingmodules}{ #1 } + } + \exp_args:NNx \seq_if_in:NnF \l_stex_all_modules_seq { #1 } { + \seq_put_right:Nx \l_stex_all_modules_seq { #1 } + \use:c{ c_stex_module_#1_code } + } +} + +%%%%%%%%%%%%% inheritance.dtx %%%%%%%%%%%%% + +\tl_new:N \g_stex_smsmode_allowedmacros_tl +\tl_new:N \g_stex_smsmode_allowedmacros_escape_tl +\seq_new:N \g_stex_smsmode_allowedenvs_seq + +\tl_set:Nn \g_stex_smsmode_allowedmacros_tl { + \makeatletter + \makeatother + \ExplSyntaxOn + \ExplSyntaxOff + \rustexBREAK +} + +\tl_set:Nn \g_stex_smsmode_allowedmacros_escape_tl { + \symdef + \importmodule + \notation + \symdecl + \STEXexport + \inlineass + \inlinedef + \inlineex + \endinput + \setnotation + \copynotation +} + +\exp_args:NNx \seq_set_from_clist:Nn \g_stex_smsmode_allowedenvs_seq { + \tl_to_str:n { + smodule, + copymodule, + interpretmodule, + sdefinition, + sexample, + sassertion, + sparagraph + } +} +\bool_new:N \g__stex_smsmode_bool +\bool_set_false:N \g__stex_smsmode_bool +\prg_new_conditional:Nnn \stex_if_smsmode: { p, T, F, TF } { + \bool_if:NTF \g__stex_smsmode_bool \prg_return_true: \prg_return_false: +} +\cs_new_protected:Nn \__stex_smsmode_in_smsmode:nn { + \vbox_set:Nn \l_tmpa_box { + \bool_set_eq:cN { l__stex_smsmode_#1_bool } \g__stex_smsmode_bool + \bool_gset_true:N \g__stex_smsmode_bool + #2 + \bool_gset_eq:Nc \g__stex_smsmode_bool { l__stex_smsmode_#1_bool } + } + \box_clear:N \l_tmpa_box +} +\quark_new:N \q__stex_smsmode_break + +\cs_new_protected:Nn \stex_file_in_smsmode:nn { + \stex_filestack_push:n{#1} + \__stex_smsmode_in_smsmode:nn{#1} { + #2 + \everyeof{\q__stex_smsmode_break\noexpand} + \expandafter\expandafter\expandafter + \stex_smsmode_do: + \csname @ @ input\endcsname "#1"\relax + } + \stex_filestack_pop: +} +\cs_new_protected:Npn \stex_smsmode_do: { + \stex_if_smsmode:T { + \__stex_smsmode_do:w + } +} +\cs_new_protected:Npn \__stex_smsmode_do:w #1 { + \exp_args:Nx \tl_if_empty:nTF { \tl_tail:n{ #1 }}{ + \expandafter\if\expandafter\relax\noexpand#1 + \expandafter\__stex_smsmode_do_aux:N\expandafter#1 + \else\expandafter\__stex_smsmode_do:w\fi + }{ + \__stex_smsmode_do:w %#1 + } +} +\cs_new_protected:Nn \__stex_smsmode_do_aux:N { + \cs_if_eq:NNF #1 \q__stex_smsmode_break { + \tl_if_in:NnTF \g_stex_smsmode_allowedmacros_tl {#1} { + #1\__stex_smsmode_do:w + }{ + \tl_if_in:NnTF \g_stex_smsmode_allowedmacros_escape_tl {#1} { + #1 + }{ + \cs_if_eq:NNTF \begin #1 { + \__stex_smsmode_check_begin:n + }{ + \cs_if_eq:NNTF \end #1 { + \__stex_smsmode_check_end:n + }{ + \__stex_smsmode_do:w + } + } + } + } + } +} + +\cs_new_protected:Nn \__stex_smsmode_check_begin:n { + \seq_if_in:NxTF \g_stex_smsmode_allowedenvs_seq { \detokenize{#1} }{ + \begin{#1} + }{ + \__stex_smsmode_do:w + } +} +\cs_new_protected:Nn \__stex_smsmode_check_end:n { + \seq_if_in:NxTF \g_stex_smsmode_allowedenvs_seq { \detokenize{#1} }{ + \end{#1}\__stex_smsmode_do:w + }{ + \str_if_eq:nnTF{#1}{document}{\endinput}{\__stex_smsmode_do:w} + } +} + +\cs_new_protected:Nn \stex_import_module_uri:nn { + \str_set:Nx \l_stex_import_archive_str { #1 } + \str_set:Nn \l_stex_import_path_str { #2 } + + \exp_args:NNNo \seq_set_split:Nnn \l_tmpb_seq ? { \l_stex_import_path_str } + \seq_pop_right:NN \l_tmpb_seq \l_stex_import_name_str + \str_set:Nx \l_stex_import_path_str { \seq_use:Nn \l_tmpb_seq ? } + + \stex_modules_current_namespace: + \bool_lazy_all:nTF { + {\str_if_empty_p:N \l_stex_import_archive_str} + {\str_if_empty_p:N \l_stex_import_path_str} + {\stex_if_module_exists_p:n { \l_stex_module_ns_str ? \l_stex_import_name_str } } + }{ + \str_set_eq:NN \l_stex_import_path_str \l_stex_modules_subpath_str + \str_set_eq:NN \l_stex_import_ns_str \l_stex_module_ns_str + }{ + \str_if_empty:NT \l_stex_import_archive_str { + \prop_if_exist:NT \l_stex_current_repository_prop { + \prop_get:NnN \l_stex_current_repository_prop { id } \l_stex_import_archive_str + } + } + \str_if_empty:NTF \l_stex_import_archive_str { + \str_if_empty:NF \l_stex_import_path_str { + \str_set:Nx \l_stex_import_ns_str { + \l_stex_module_ns_str / \l_stex_import_path_str + } + } + }{ + \stex_require_repository:n \l_stex_import_archive_str + \prop_get:cnN { c_stex_mathhub_\l_stex_import_archive_str _manifest_prop } { ns } + \l_stex_import_ns_str + \str_if_empty:NF \l_stex_import_path_str { + \str_set:Nx \l_stex_import_ns_str { + \l_stex_import_ns_str / \l_stex_import_path_str + } + } + } + } +} +\str_new:N \l_stex_import_name_str +\str_new:N \l_stex_import_archive_str +\str_new:N \l_stex_import_path_str +\str_new:N \l_stex_import_ns_str +\cs_new_protected:Nn \stex_import_require_module:nnnn { + \exp_args:Nx \stex_if_module_exists:nF { #1 ? #4 } { + + % archive + \str_set:Nx \l_tmpa_str { #2 } + \str_if_empty:NTF \l_tmpa_str { + \seq_set_eq:NN \l_tmpa_seq \g_stex_currentfile_seq + } { + \stex_path_from_string:Nn \l_tmpb_seq { \l_tmpa_str } + \seq_concat:NNN \l_tmpa_seq \c_stex_mathhub_seq \l_tmpb_seq + \seq_put_right:Nn \l_tmpa_seq { source } + } + + % path + \str_set:Nx \l_tmpb_str { #3 } + \str_if_empty:NTF \l_tmpb_str { + \str_set:Nx \l_tmpa_str { \stex_path_to_string:N \l_tmpa_seq / #4 } + + \ltx@ifpackageloaded{babel} { + \exp_args:NNx \prop_get:NnNF \c_stex_language_abbrevs_prop + { \languagename } \l_tmpb_str { + \msg_error:nnx{stex}{error/unknownlanguage}{\languagename} + } + } { + \str_clear:N \l_tmpb_str + } + + \stex_debug:nn{modules}{Checking~\l_tmpa_str.\l_tmpb_str.tex} + \IfFileExists{ \l_tmpa_str.\l_tmpb_str.tex }{ + \str_gset:Nx \g__stex_importmodule_file_str { \l_tmpa_str.\l_tmpb_str.tex } + }{ + \stex_debug:nn{modules}{Checking~\l_tmpa_str.tex} + \IfFileExists{ \l_tmpa_str.tex }{ + \str_gset:Nx \g__stex_importmodule_file_str { \l_tmpa_str.tex } + }{ + % try english as default + \stex_debug:nn{modules}{Checking~\l_tmpa_str.en.tex} + \IfFileExists{ \l_tmpa_str.en.tex }{ + \str_gset:Nx \g__stex_importmodule_file_str { \l_tmpa_str.en.tex } + }{ + \msg_error:nnx{stex}{error/unknownmodule}{#1?#4} + } + } + } + + } { + \seq_set_split:NnV \l_tmpb_seq / \l_tmpb_str + \seq_concat:NNN \l_tmpa_seq \l_tmpa_seq \l_tmpb_seq + + \ltx@ifpackageloaded{babel} { + \exp_args:NNx \prop_get:NnNF \c_stex_language_abbrevs_prop + { \languagename } \l_tmpb_str { + \msg_error:nnx{stex}{error/unknownlanguage}{\languagename} + } + } { + \str_clear:N \l_tmpb_str + } + + \stex_path_to_string:NN \l_tmpa_seq \l_tmpa_str + + \stex_debug:nn{modules}{Checking~\l_tmpa_str/#4.\l_tmpb_str.tex} + \IfFileExists{ \l_tmpa_str/#4.\l_tmpb_str.tex }{ + \str_gset:Nx \g__stex_importmodule_file_str { \l_tmpa_str/#4.\l_tmpb_str.tex } + }{ + \stex_debug:nn{modules}{Checking~\l_tmpa_str/#4.tex} + \IfFileExists{ \l_tmpa_str/#4.tex }{ + \str_gset:Nx \g__stex_importmodule_file_str { \l_tmpa_str/#4.tex } + }{ + % try english as default + \stex_debug:nn{modules}{Checking~\l_tmpa_str/#4.en.tex} + \IfFileExists{ \l_tmpa_str/#4.en.tex }{ + \str_gset:Nx \g__stex_importmodule_file_str { \l_tmpa_str/#4.en.tex } + }{ + \stex_debug:nn{modules}{Checking~\l_tmpa_str.\l_tmpb_str.tex} + \IfFileExists{ \l_tmpa_str.\l_tmpb_str.tex }{ + \str_gset:Nx \g__stex_importmodule_file_str { \l_tmpa_str.\l_tmpb_str.tex } + }{ + \stex_debug:nn{modules}{Checking~\l_tmpa_str.tex} + \IfFileExists{ \l_tmpa_str.tex }{ + \str_gset:Nx \g__stex_importmodule_file_str { \l_tmpa_str.tex } + }{ + % try english as default + \stex_debug:nn{modules}{Checking~\l_tmpa_str.en.tex} + \IfFileExists{ \l_tmpa_str.en.tex }{ + \str_gset:Nx \g__stex_importmodule_file_str { \l_tmpa_str.en.tex } + }{ + \msg_error:nnx{stex}{error/unknownmodule}{#1?#4} + } + } + } + } + } + } + } + + \exp_args:No \stex_file_in_smsmode:nn { \g__stex_importmodule_file_str } { + \seq_clear:N \l_stex_all_modules_seq + \str_clear:N \l_stex_current_module_str + \str_set:Nx \l_tmpb_str { #2 } + \str_if_empty:NF \l_tmpb_str { + \stex_set_current_repository:n { #2 } + } + \stex_debug:nn{modules}{Loading~\g__stex_importmodule_file_str} + } + + \stex_if_module_exists:nF { #1 ? #4 } { + \msg_error:nnx{stex}{error/unknownmodule}{ + #1?#4~(in~file~\g__stex_importmodule_file_str) + } + } + } + \stex_activate_module:n { #1 ? #4 } +} +\NewDocumentCommand \importmodule { O{} m } { + \stex_import_module_uri:nn { #1 } { #2 } + \stex_debug:nn{modules}{Importing~module:~ + \l_stex_import_ns_str ? \l_stex_import_name_str + } + \stex_if_smsmode:F { + \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_annotate_invisible:nnn + {import} {\l_stex_import_ns_str ? \l_stex_import_name_str} {} + } + \exp_args:Nx \stex_add_to_current_module:n { + \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 } + } + \exp_args:Nx \stex_add_import_to_current_module:n { + \l_stex_import_ns_str ? \l_stex_import_name_str + } + \stex_smsmode_do: + \ignorespacesandpars +} +\stex_deactivate_macro:Nn \importmodule {module~environments} +\NewDocumentCommand \usemodule { O{} m } { + \stex_if_smsmode:F { + \stex_import_module_uri:nn { #1 } { #2 } + \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_annotate_invisible:nnn + {usemodule} {\l_stex_import_ns_str ? \l_stex_import_name_str} {} + } + \stex_smsmode_do: + \ignorespacesandpars +} + +%%%%%%%%%%%%% symbols.dtx %%%%%%%%%%%%% + +\msg_new:nnn{stex}{error/wrongargs}{ + args~value~in~symbol~declaration~for~#1~ + needs~to~be~i,~a,~b~or~B,~but~#2~given +} +\cs_new_protected:Nn \stex_all_symbols:n { + \def \__stex_symdecl_all_symbols_cs ##1 {#1} + \seq_map_inline:Nn \l_stex_all_modules_seq { + \seq_map_inline:cn{c_stex_module_##1_constants}{ + \__stex_symdecl_all_symbols_cs{##1?####1} + } + } +} +\NewDocumentCommand \STEXsymbol { m } { + \stex_get_symbol:n { #1 } + \exp_args:No + \stex_invoke_symbol:n { \l_stex_get_symbol_uri_str } +} +\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 , + assoc .choices:nn = + {bin,binl,binr,pre,conj,pwconj} + {\str_set:Nx \l_stex_symdecl_assoctype_str {\l_keys_choice_tl}} +} + +\bool_new:N \l_stex_symdecl_make_macro_bool + +\cs_new_protected:Nn \__stex_symdecl_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_assoctype_str + \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 + + \keys_set:nn { stex / symdecl } { #1 } +} + +\NewDocumentCommand \symdecl { s m O{}} { + \__stex_symdecl_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 + } + \stex_symdecl_do:n { #2 } + \stex_smsmode_do: +} + +\cs_new_protected:Nn \stex_symdecl_do:nn { + \__stex_symdecl_args:n{#1} + \bool_set_false:N \l_stex_symdecl_make_macro_bool + \stex_symdecl_do:n{#2} +} + +\stex_deactivate_macro:Nn \symdecl {module~environments} +\cs_new_protected:Nn \stex_symdecl_do:n { + \stex_if_in_module:F { + % TODO throw error? some default namespace? + } + + \str_if_empty:NT \l_stex_symdecl_name_str { + \str_set:Nx \l_stex_symdecl_name_str { #1 } + } + + \prop_if_exist:cT { l_stex_symdecl_ + \l_stex_current_module_str ? + \l_stex_symdecl_name_str + _prop + }{ + % TODO throw error (beware of circular dependencies) + } + + \prop_clear:N \l_tmpa_prop + \prop_put:Nnx \l_tmpa_prop { module } { \l_stex_current_module_str } + \seq_clear:N \l_tmpa_seq + \prop_put:Nno \l_tmpa_prop { name } \l_stex_symdecl_name_str + \prop_put:Nno \l_tmpa_prop { type } \l_stex_symdecl_type_tl + + \str_if_empty:NT \l_stex_symdecl_deprecate_str { + \str_if_empty:NF \l_stex_module_deprecate_str { + \str_set_eq:NN \l_stex_symdecl_deprecate_str \l_stex_module_deprecate_str + } + } + \prop_put:Nno \l_tmpa_prop { deprecate } \l_stex_symdecl_deprecate_str + + \exp_args:No \stex_add_constant_to_current_module:n { + \l_stex_symdecl_name_str + } + + % arity/args + \int_zero:N \l_tmpb_int + + \bool_set_true:N \l_tmpa_bool + \str_map_inline:Nn \l_stex_symdecl_args_str { + \token_case_meaning:NnF ##1 { + 0 {} 1 {} 2 {} 3 {} 4 {} 5 {} 6 {} 7 {} 8 {} 9 {} + {\tl_to_str:n i} { \bool_set_false:N \l_tmpa_bool } + {\tl_to_str:n b} { \bool_set_false:N \l_tmpa_bool } + {\tl_to_str:n a} { + \bool_set_false:N \l_tmpa_bool + \int_incr:N \l_tmpb_int + } + {\tl_to_str:n B} { + \bool_set_false:N \l_tmpa_bool + \int_incr:N \l_tmpb_int + } + }{ + \msg_error:nnxx{stex}{error/wrongargs}{ + \l_stex_current_module_str ? + \l_stex_symdecl_name_str + }{##1} + } + } + \bool_if:NTF \l_tmpa_bool { + % possibly numeric + \str_if_empty:NTF \l_stex_symdecl_args_str { + \prop_put:Nnn \l_tmpa_prop { args } {} + \prop_put:Nnn \l_tmpa_prop { arity } { 0 } + }{ + \int_set:Nn \l_tmpa_int { \l_stex_symdecl_args_str } + \prop_put:Nnx \l_tmpa_prop { arity } { \int_use:N \l_tmpa_int } + \str_clear:N \l_tmpa_str + \int_step_inline:nn \l_tmpa_int { + \str_put_right:Nn \l_tmpa_str i + } + \prop_put:Nnx \l_tmpa_prop { args } { \l_tmpa_str } + } + } { + \prop_put:Nnx \l_tmpa_prop { args } { \l_stex_symdecl_args_str } + \prop_put:Nnx \l_tmpa_prop { arity } + { \str_count:N \l_stex_symdecl_args_str } + } + \prop_put:Nnx \l_tmpa_prop { assocs } { \int_use:N \l_tmpb_int } + + % semantic macro + + \bool_if:NT \l_stex_symdecl_make_macro_bool { + \exp_args:Nx \stex_do_up_to_module:n { + \tl_set:cn { #1 } { \stex_invoke_symbol:n { + \l_stex_current_module_str ? \l_stex_symdecl_name_str + }} + } + + \bool_if:NF \l_stex_symdecl_local_bool { + \exp_args:Nx \stex_add_to_current_module:n { + \tl_set:cn { #1 } { \stex_invoke_symbol:n { + \l_stex_current_module_str ? \l_stex_symdecl_name_str + } } + } + } + } + + \stex_debug:nn{symbols}{New~symbol:~ + \l_stex_current_module_str ? \l_stex_symdecl_name_str^^J + Type:~\exp_not:o { \l_stex_symdecl_type_tl }^^J + Args:~\prop_item:Nn \l_tmpa_prop { args } + } + + % circular dependencies require this: + + \prop_if_exist:cF { + l_stex_symdecl_ + \l_stex_current_module_str ? \l_stex_symdecl_name_str + _prop + } { + \prop_set_eq:cN { + l_stex_symdecl_ + \l_stex_current_module_str ? \l_stex_symdecl_name_str + _prop + } \l_tmpa_prop + } + + \seq_clear:c { + l_stex_symdecl_ + \l_stex_current_module_str ? \l_stex_symdecl_name_str + _notations + } + + \bool_if:NF \l_stex_symdecl_local_bool { + \exp_args:Nx + \stex_add_to_current_module:n { + \seq_clear:c { + l_stex_symdecl_ + \l_stex_current_module_str ? \l_stex_symdecl_name_str + _notations + } + \prop_set_from_keyval:cn { + l_stex_symdecl_ + \l_stex_current_module_str ? \l_stex_symdecl_name_str + _prop + } { + name = \prop_item:Nn \l_tmpa_prop { name } , + module = \prop_item:Nn \l_tmpa_prop { module } , + type = \prop_item:Nn \l_tmpa_prop { type } , + args = \prop_item:Nn \l_tmpa_prop { args } , + arity = \prop_item:Nn \l_tmpa_prop { arity } , + assocs = \prop_item:Nn \l_tmpa_prop { assocs } + } + } + } + + \stex_if_smsmode:F { + \stex_if_do_html:T { + \stex_annotate_invisible:nnn {symdecl} { + \l_stex_current_module_str ? \l_stex_symdecl_name_str + } { + \tl_if_empty:NF \l_stex_symdecl_type_tl {\stex_annotate_invisible:nnn{type}{}{$\l_stex_symdecl_type_tl$}} + \stex_annotate_invisible:nnn{args}{}{ + \prop_item:Nn \l_tmpa_prop { args } + } + \stex_annotate_invisible:nnn{macroname}{#1}{} + \tl_if_empty:NF \l_stex_symdecl_definiens_tl { + \stex_annotate_invisible:nnn{definiens}{} + {$\l_stex_symdecl_definiens_tl$} + } + \str_if_empty:NF \l_stex_symdecl_assoctype_str { + \stex_annotate_invisible:nnn{assoctype}{\l_stex_symdecl_assoctype_str}{} + } + } + } + } +} +\str_new:N \l_stex_get_symbol_uri_str + +\cs_new_protected:Nn \stex_get_symbol:n { + \tl_if_head_eq_catcode:nNTF { #1 } \relax { + \__stex_symdecl_get_symbol_from_cs:n { #1 } + }{ + % argument is a string + % is it a command name? + \cs_if_exist:cTF { #1 }{ + \cs_set_eq:Nc \l_tmpa_tl { #1 } + \str_set:Nx \l_tmpa_str { \cs_argument_spec:N \l_tmpa_tl } + \str_if_empty:NTF \l_tmpa_str { + \exp_args:Nx \cs_if_eq:NNTF { + \tl_head:N \l_tmpa_tl + } \stex_invoke_symbol:n { + \exp_args:No \__stex_symdecl_get_symbol_from_cs:n { \use:c { #1 } } + }{ + \__stex_symdecl_get_symbol_from_string:n { #1 } + } + } { + \__stex_symdecl_get_symbol_from_string:n { #1 } + } + }{ + % argument is not a command name + \__stex_symdecl_get_symbol_from_string:n { #1 } + % \l_stex_all_symbols_seq + } + } + \str_if_eq:eeF { + \prop_item:cn { + l_stex_symdecl_\l_stex_get_symbol_uri_str _prop + }{ deprecate } + }{}{ + \msg_warning:nnxx{stex}{warning/deprecated}{ + Symbol~\l_stex_get_symbol_uri_str + }{ + \prop_item:cn {l_stex_symdecl_\l_stex_get_symbol_uri_str _prop}{ deprecate } + } + } +} + +\cs_new_protected:Nn \__stex_symdecl_get_symbol_from_string:n { + \tl_set:Nn \l_tmpa_tl { + \msg_set:nnn{stex}{error/unknownsymbol}{ + No~symbol~#1~found! + } + \msg_error:nn{stex}{error/unknownsymbol} + } + \str_set:Nn \l_tmpa_str { #1 } + \int_set:Nn \l_tmpa_int { \str_count:N \l_tmpa_str } + + \stex_all_symbols:n { + \str_if_eq:eeT { \l_tmpa_str }{ \str_range:nnn {##1}{-\l_tmpa_int}{-1}}{ + \seq_map_break:n{\seq_map_break:n{ + \tl_set:Nn \l_tmpa_tl { + \str_set:Nn \l_stex_get_symbol_uri_str { ##1 } + } + }} + } + } + + \l_tmpa_tl +} + +\cs_new_protected:Nn \__stex_symdecl_get_symbol_from_cs:n { + \exp_args:NNx \tl_set:Nn \l_tmpa_tl + { \tl_tail:N \l_tmpa_tl } + \tl_if_single:NTF \l_tmpa_tl { + \exp_args:No \tl_if_head_is_group:nTF \l_tmpa_tl { + \exp_after:wN \str_set:Nn \exp_after:wN + \l_stex_get_symbol_uri_str \l_tmpa_tl + }{ + % TODO + % tail is not a single group + } + }{ + % TODO + % tail is not a single group + } +} +\keys_define:nn { stex / notation } { + lang .tl_set_x:N = \l__stex_notation_lang_str , + 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 + \l__stex_notation_variant_str \l_keys_key_str +} + +\cs_new_protected:Nn \_stex_notation_args:n { + \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 + \bool_set_false:N \l__stex_notation_primary_bool + + \keys_set:nn { stex / notation } { #1 } +} +\NewDocumentCommand \notation { s m O{}} { + \_stex_notation_args:n { #3 } + \tl_clear:N \l_stex_symdecl_definiens_tl + \stex_get_symbol:n { #2 } + \tl_set:Nn \l_stex_notation_after_do_tl { + \__stex_notation_final: + \IfBooleanTF#1{ + \stex_setnotation:n {\l_stex_get_symbol_uri_str} + }{} + \stex_smsmode_do: + } + \stex_notation_do:nnnn + { \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 \c_hash_str \l__stex_notation_lang_str } +} +\stex_deactivate_macro:Nn \notation {module~environments} +\seq_new:N \l__stex_notation_precedences_seq +\tl_new:N \l__stex_notation_opprec_tl +\int_new:N \l__stex_notation_currarg_int +\tl_new:N \stex_symbol_after_invocation_tl + +\cs_new_protected:Nn \stex_notation_do:nnnn { + \let\l_stex_current_symbol_str\relax + \seq_clear:N \l__stex_notation_precedences_seq + \tl_clear:N \l__stex_notation_opprec_tl + \str_set:Nx \l__stex_notation_args_str { #1 } + \str_set:Nx \l__stex_notation_arity_str { #2 } + \str_set:Nx \__stex_notation_suffix_str { #3 } + + % precedences + \str_if_empty:NTF \l__stex_notation_prec_str { + \int_compare:nNnTF \l__stex_notation_arity_str = 0 { + \tl_set:No \l__stex_notation_opprec_tl { \neginfprec } + }{ + \tl_set:Nn \l__stex_notation_opprec_tl { 0 } + } + } { + \str_if_eq:onTF \l__stex_notation_prec_str {nobrackets}{ + \tl_set:No \l__stex_notation_opprec_tl { \neginfprec } + \int_step_inline:nn { \l__stex_notation_arity_str } { + \exp_args:NNo + \seq_put_right:Nn \l__stex_notation_precedences_seq { \infprec } + } + }{ + \seq_set_split:NnV \l_tmpa_seq ; \l__stex_notation_prec_str + \seq_pop_left:NNTF \l_tmpa_seq \l_tmpa_str { + \tl_set:No \l__stex_notation_opprec_tl { \l_tmpa_str } + \seq_pop_left:NNT \l_tmpa_seq \l_tmpa_str { + \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 } + } + } + }{ + \int_compare:nNnTF \l__stex_notation_arity_str = 0 { + \tl_set:No \l__stex_notation_opprec_tl { \infprec } + }{ + \tl_set:No \l__stex_notation_opprec_tl { 0 } + } + } + } + } + + \seq_set_eq:NN \l_tmpa_seq \l__stex_notation_precedences_seq + \int_step_inline:nn { \l__stex_notation_arity_str } { + \seq_pop_left:NNF \l_tmpa_seq \l_tmpb_str { + \exp_args:NNo + \seq_put_right:No \l__stex_notation_precedences_seq { + \l__stex_notation_opprec_tl + } + } + } + \tl_clear:N \l_stex_notation_dummyargs_tl + + \int_compare:nNnTF \l__stex_notation_arity_str = 0 { + \exp_args:NNe + \cs_set:Npn \l_stex_notation_macrocode_cs { + \_stex_term_math_oms:nnnn { \l_stex_current_symbol_str } + { \__stex_notation_suffix_str } + { \l__stex_notation_opprec_tl } + { \exp_not:n { #4 } } + } + \l_stex_notation_after_do_tl + }{ + \str_if_in:NnTF \l__stex_notation_args_str b { + \exp_args:Nne \use:nn + { + \cs_generate_from_arg_count:NNnn \l_stex_notation_macrocode_cs + \cs_set:Npn \l__stex_notation_arity_str } { { + \_stex_term_math_omb:nnnn { \l_stex_current_symbol_str } + { \__stex_notation_suffix_str } + { \l__stex_notation_opprec_tl } + { \exp_not:n { #4 } } + }} + }{ + \str_if_in:NnTF \l__stex_notation_args_str B { + \exp_args:Nne \use:nn + { + \cs_generate_from_arg_count:NNnn \l_stex_notation_macrocode_cs + \cs_set:Npn \l__stex_notation_arity_str } { { + \_stex_term_math_omb:nnnn { \l_stex_current_symbol_str } + { \__stex_notation_suffix_str } + { \l__stex_notation_opprec_tl } + { \exp_not:n { #4 } } + } } + }{ + \exp_args:Nne \use:nn + { + \cs_generate_from_arg_count:NNnn \l_stex_notation_macrocode_cs + \cs_set:Npn \l__stex_notation_arity_str } { { + \_stex_term_math_oma:nnnn { \l_stex_current_symbol_str } + { \__stex_notation_suffix_str } + { \l__stex_notation_opprec_tl } + { \exp_not:n { #4 } } + } } + } + } + + \str_set_eq:NN \l__stex_notation_remaining_args_str \l__stex_notation_args_str + \int_zero:N \l__stex_notation_currarg_int + \seq_set_eq:NN \l__stex_notation_remaining_precs_seq \l__stex_notation_precedences_seq + \__stex_notation_arguments: + } +} +\cs_new_protected:Nn \__stex_notation_arguments: { + \int_incr:N \l__stex_notation_currarg_int + \str_if_empty:NTF \l__stex_notation_remaining_args_str { + \l_stex_notation_after_do_tl + }{ + \str_set:Nx \l_tmpa_str { \str_head:N \l__stex_notation_remaining_args_str } + \str_set:Nx \l__stex_notation_remaining_args_str { \str_tail:N \l__stex_notation_remaining_args_str } + \str_if_eq:VnTF \l_tmpa_str a { + \__stex_notation_argument_assoc:n + }{ + \str_if_eq:VnTF \l_tmpa_str B { + \__stex_notation_argument_assoc:n + }{ + \seq_pop_left:NN \l__stex_notation_remaining_precs_seq \l_tmpa_str + \tl_put_right:Nx \l_stex_notation_dummyargs_tl { + { \_stex_term_math_arg:nnn + { \int_use:N \l__stex_notation_currarg_int } + { \l_tmpa_str } + { ####\int_use:N \l__stex_notation_currarg_int } + } + } + \__stex_notation_arguments: + } + } + } +} +\cs_new_protected:Nn \__stex_notation_argument_assoc:n { + + \cs_generate_from_arg_count:NNnn \l_tmpa_cs \cs_set:Npn + {\l__stex_notation_arity_str}{ + #1 + } + \int_zero:N \l_tmpa_int + \tl_clear:N \l_tmpa_tl + \str_map_inline:Nn \l__stex_notation_args_str { + \int_incr:N \l_tmpa_int + \tl_put_right:Nx \l_tmpa_tl { + \str_if_eq:nnTF {##1}{a}{ {} }{ + \str_if_eq:nnTF {##1}{B}{ {} }{ + {\_stex_term_arg:nn{\int_use:N \l_tmpa_int}{################ \int_use:N \l_tmpa_int}} + } + } + } + } + \exp_after:wN\exp_after:wN\exp_after:wN \def + \exp_after:wN\exp_after:wN\exp_after:wN \l_tmpa_cs + \exp_after:wN\exp_after:wN\exp_after:wN ## + \exp_after:wN\exp_after:wN\exp_after:wN 1 + \exp_after:wN\exp_after:wN\exp_after:wN ## + \exp_after:wN\exp_after:wN\exp_after:wN 2 + \exp_after:wN\exp_after:wN\exp_after:wN { + \exp_after:wN \exp_after:wN \exp_after:wN + \exp_not:n \exp_after:wN \exp_after:wN \exp_after:wN { + \exp_after:wN \l_tmpa_cs \l_tmpa_tl + } + } + + \seq_pop_left:NN \l__stex_notation_remaining_precs_seq \l_tmpa_str + \tl_put_right:Nx \l_stex_notation_dummyargs_tl { { + \_stex_term_math_assoc_arg:nnnn + { \int_use:N \l__stex_notation_currarg_int } + { \l_tmpa_str } + { ####\int_use:N \l__stex_notation_currarg_int } + { \l_tmpa_cs {####1} {####2} } + } } + \__stex_notation_arguments: +} +\cs_new_protected:Nn \__stex_notation_final: { + \exp_args:Nne \use:nn + { + \cs_generate_from_arg_count:cNnn { + stex_notation_ \l_stex_get_symbol_uri_str \c_hash_str + \__stex_notation_suffix_str + _cs + } + \cs_set:Npn \l__stex_notation_arity_str } { { + \exp_after:wN \exp_after:wN \exp_after:wN + \exp_not:n \exp_after:wN \exp_after:wN \exp_after:wN + { \exp_after:wN \l_stex_notation_macrocode_cs \l_stex_notation_dummyargs_tl \stex_symbol_after_invocation_tl} + } } + + \tl_if_empty:NF \l__stex_notation_op_tl { + \cs_set:cpx { + stex_op_notation_ \l_stex_get_symbol_uri_str \c_hash_str + \__stex_notation_suffix_str + _cs + } { + \_stex_term_oms:nnn { + \l_stex_get_symbol_uri_str \c_hash_str \__stex_notation_suffix_str + }{ + \l_stex_get_symbol_uri_str + }{ \comp{ \exp_args:No \exp_not:n { \l__stex_notation_op_tl } } } + } + } + + \exp_args:Ne + \stex_add_to_current_module:n { + \cs_generate_from_arg_count:cNnn { + stex_notation_ \l_stex_get_symbol_uri_str \c_hash_str + \__stex_notation_suffix_str + _cs + } \cs_set:Npn {\l__stex_notation_arity_str} { + \exp_after:wN \exp_after:wN \exp_after:wN + \exp_not:n \exp_after:wN \exp_after:wN \exp_after:wN + { \exp_after:wN \l_stex_notation_macrocode_cs \l_stex_notation_dummyargs_tl \stex_symbol_after_invocation_tl} + } + \tl_if_empty:NF \l__stex_notation_op_tl { + \cs_set:cpn { + stex_op_notation_\l_stex_get_symbol_uri_str \c_hash_str + \__stex_notation_suffix_str + _cs + } { + \_stex_term_oms:nnn { + \l_stex_get_symbol_uri_str\c_hash_str \__stex_notation_suffix_str + }{ + \l_stex_get_symbol_uri_str + }{ \comp{ \exp_args:No \exp_not:n { \l__stex_notation_op_tl } } } + } + } + } + %\exp_args:Nx + % \stex_do_up_to_module:n { + \seq_put_right:cx { + l_stex_symdecl_ \l_stex_get_symbol_uri_str + _notations + } { + \__stex_notation_suffix_str + } + % } + + \stex_debug:nn{symbols}{ + Notation~\__stex_notation_suffix_str + ~for~\l_stex_get_symbol_uri_str^^J + Operator~precedence:~\l__stex_notation_opprec_tl^^J + Argument~precedences:~ + \seq_use:Nn \l__stex_notation_precedences_seq {,~}^^J + Notation: \cs_meaning:c { + stex_notation_ \l_stex_get_symbol_uri_str \c_hash_str + \__stex_notation_suffix_str + _cs + } + } + + \exp_args:Ne + \stex_add_to_current_module:n { + \seq_put_right:cn { + l_stex_symdecl_\l_stex_get_symbol_uri_str + _notations + } { \__stex_notation_suffix_str } + } + + \stex_if_smsmode:F { + + % HTML annotations + \stex_if_do_html:T { + \stex_annotate_invisible:nnn { notation } + { \l_stex_get_symbol_uri_str } { + \stex_annotate_invisible:nnn { notationfragment } + { \__stex_notation_suffix_str }{} + \stex_annotate_invisible:nnn { precedence } + { \l__stex_notation_prec_str }{} + + \int_zero:N \l_tmpa_int + \str_set_eq:NN \l__stex_notation_remaining_args_str \l__stex_notation_args_str + \tl_clear:N \l_tmpa_tl + \int_step_inline:nn { \l__stex_notation_arity_str }{ + \int_incr:N \l_tmpa_int + \str_set:Nx \l_tmpb_str { \str_head:N \l__stex_notation_remaining_args_str } + \str_set:Nx \l__stex_notation_remaining_args_str { \str_tail:N \l__stex_notation_remaining_args_str } + \str_if_eq:VnTF \l_tmpb_str a { + \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { + \c_hash_str \c_hash_str \int_use:N \l_tmpa_int a , + \c_hash_str \c_hash_str \int_use:N \l_tmpa_int b + } } + }{ + \str_if_eq:VnTF \l_tmpb_str B { + \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { + \c_hash_str \c_hash_str \int_use:N \l_tmpa_int a , + \c_hash_str \c_hash_str \int_use:N \l_tmpa_int b + } } + }{ + \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { + \c_hash_str \c_hash_str \int_use:N \l_tmpa_int + } } + } + } + } + \stex_annotate_invisible:nnn { notationcomp }{}{ + \str_set:Nx \l_stex_current_symbol_str {\l_stex_get_symbol_uri_str } + $ \exp_args:Nno \use:nn { \use:c { + stex_notation_ \l_stex_current_symbol_str + \c_hash_str \__stex_notation_suffix_str _cs + } } { \l_tmpa_tl } $ + } + } + } + } +} +\keys_define:nn { stex / setnotation } { + lang .tl_set_x:N = \l__stex_notation_lang_str , + variant .tl_set_x:N = \l__stex_notation_variant_str , + unknown .code:n = \str_set:Nx + \l__stex_notation_variant_str \l_keys_key_str +} + +\cs_new_protected:Nn \_stex_setnotation_args:n { + \str_clear:N \l__stex_notation_lang_str + \str_clear:N \l__stex_notation_variant_str + \keys_set:nn { stex / setnotation } { #1 } +} + +\cs_new_protected:Nn \stex_setnotation:n { + \exp_args:Nnx \seq_if_in:cnTF { l_stex_symdecl_#1 _notations } + { \l__stex_notation_variant_str \c_hash_str \l__stex_notation_lang_str }{ + \exp_args:Nnx \seq_remove_all:cn { l_stex_symdecl_#1 _notations } + { \l__stex_notation_variant_str \c_hash_str \l__stex_notation_lang_str } + \exp_args:Nnx \seq_remove_all:cn { l_stex_symdecl_#1 _notations } + { \c_hash_str } + \exp_args:Nnx \seq_put_left:cn { l_stex_symdecl_#1 _notations } + { \l__stex_notation_variant_str \c_hash_str \l__stex_notation_lang_str } + \exp_args:Nx \stex_add_to_current_module:n { + \exp_args:Nnx \seq_remove_all:cn { l_stex_symdecl_#1 _notations } + { \l__stex_notation_variant_str \c_hash_str \l__stex_notation_lang_str } + \exp_args:Nnx \seq_put_left:cn { l_stex_symdecl_#1 _notations } + { \l__stex_notation_variant_str \c_hash_str \l__stex_notation_lang_str } + \exp_args:Nnx \seq_remove_all:cn { l_stex_symdecl_#1 _notations } + { \c_hash_str } + } + \stex_debug:nn {notations}{ + Setting~default~notation~ + {\l__stex_notation_variant_str \c_hash_str \l__stex_notation_lang_str}~for~ + #1 \\ + \expandafter\meaning\csname + l_stex_symdecl_#1 _notations\endcsname + } + }{ + % todo throw error + } +} + +\NewDocumentCommand \setnotation {m m} { + \stex_get_symbol:n { #1 } + \_stex_setnotation_args:n { #2 } + \stex_setnotation:n{\l_stex_get_symbol_uri_str} + \stex_smsmode_do: +} + +\cs_new_protected:Nn \stex_copy_notations:nn { + \stex_debug:nn {notations}{ + Copying~notations~from~#2~to~#1\\ + \seq_use:cn{l_stex_symdecl_#2_notations}{,~} + } + \tl_clear:N \l_tmpa_tl + \int_step_inline:nn { \prop_item:cn {l_stex_symdecl_#2_prop}{ arity } } { + \tl_put_right:Nn \l_tmpa_tl { {## ##1} } + } + \seq_map_inline:cn {l_stex_symdecl_#2_notations}{ + \cs_set_eq:Nc \l_tmpa_cs { stex_notation_ #2 \c_hash_str ##1 _cs } + \edef \l_tmpa_tl { + \exp_after:wN\exp_after:wN\exp_after:wN \exp_not:n + \exp_after:wN\exp_after:wN\exp_after:wN { + \exp_after:wN \l_tmpa_cs \l_tmpa_tl + } + } + \exp_args:Nx + \stex_do_up_to_module:n { + \seq_put_right:cn{l_stex_symdecl_#1_notations}{##1} + \cs_generate_from_arg_count:cNnn { + stex_notation_ #1 \c_hash_str ##1 _cs + } \cs_set:Npn { \prop_item:cn {l_stex_symdecl_#2_prop}{ arity } }{ + \exp_after:wN\exp_not:n\exp_after:wN{\l_tmpa_tl} + } + } + } +} + +\NewDocumentCommand \copynotation {m m} { + \stex_get_symbol:n { #1 } + \str_set_eq:NN \l_tmpa_str \l_stex_get_symbol_uri_str + \stex_get_symbol:n { #2 } + \exp_args:Noo + \stex_copy_notations:nn \l_tmpa_str \l_stex_get_symbol_uri_str + \exp_args:Nx \stex_add_import_to_current_module:n{ + \stex_copy_notations:nn {\l_tmpa_str} {\l_stex_get_symbol_uri_str} + } + \stex_smsmode_do: +} + +\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 , + 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 , + 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_notation_symdef_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 + \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 + \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 / symdef } { #1 } +} + +\NewDocumentCommand \symdef { m O{} } { + \__stex_notation_symdef_args:n { #2 } + \bool_set_true:N \l_stex_symdecl_make_macro_bool + \stex_symdecl_do:n { #1 } + \tl_set:Nn \l_stex_notation_after_do_tl { + \__stex_notation_final: + \stex_smsmode_do: + } + \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:nnnn + { \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 \c_hash_str \l__stex_notation_lang_str } +} +\stex_deactivate_macro:Nn \symdef {module~environments} + +\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 , + type .tl_set:N = \l__stex_variables_type_tl , + def .tl_set:N = \l__stex_variables_def_tl , + op .tl_set:N = \l__stex_variables_op_tl , + prec .str_set_x:N = \l__stex_variables_prec_str , + assoc .choices:nn = + {bin,binl,binr,pre,conj,pwconj} + {\str_set:Nx \l__stex_variables_assoctype_str {\l_keys_choice_tl}}, + bind .choices:nn = + {forall,exists} + {\str_set:Nx \l__stex_variables_bind_str {\l_keys_choice_tl}} +} + +\cs_new_protected:Nn \__stex_variables_args:n { + \str_clear:N \l__stex_variables_name_str + \str_clear:N \l__stex_variables_args_str + \str_clear:N \l__stex_variables_prec_str + \str_clear:N \l__stex_variables_assoctype_str + \str_clear:N \l__stex_variables_bind_str + \tl_clear:N \l__stex_variables_type_tl + \tl_clear:N \l__stex_variables_def_tl + \tl_clear:N \l__stex_variables_op_tl + + \keys_set:nn { stex / vardef } { #1 } +} + +\NewDocumentCommand \__stex_variables_do_simple:nnn { m O{}} { + \__stex_variables_args:n {#2} + \str_if_empty:NT \l__stex_variables_name_str { + \str_set:Nx \l__stex_variables_name_str { #1 } + } + \prop_clear:N \l_tmpa_prop + \prop_put:Nno \l_tmpa_prop { name } \l__stex_variables_name_str + + \int_zero:N \l_tmpb_int + \bool_set_true:N \l_tmpa_bool + \str_map_inline:Nn \l__stex_variables_args_str { + \token_case_meaning:NnF ##1 { + 0 {} 1 {} 2 {} 3 {} 4 {} 5 {} 6 {} 7 {} 8 {} 9 {} + {\tl_to_str:n i} { \bool_set_false:N \l_tmpa_bool } + {\tl_to_str:n b} { \bool_set_false:N \l_tmpa_bool } + {\tl_to_str:n a} { + \bool_set_false:N \l_tmpa_bool + \int_incr:N \l_tmpb_int + } + {\tl_to_str:n B} { + \bool_set_false:N \l_tmpa_bool + \int_incr:N \l_tmpb_int + } + }{ + \msg_error:nnxx{stex}{error/wrongargs}{ + variable~\l__stex_variables_name_str + }{##1} + } + } + \bool_if:NTF \l_tmpa_bool { + % possibly numeric + \str_if_empty:NTF \l__stex_variables_args_str { + \prop_put:Nnn \l_tmpa_prop { args } {} + \prop_put:Nnn \l_tmpa_prop { arity } { 0 } + }{ + \int_set:Nn \l_tmpa_int { \l__stex_variables_args_str } + \prop_put:Nnx \l_tmpa_prop { arity } { \int_use:N \l_tmpa_int } + \str_clear:N \l_tmpa_str + \int_step_inline:nn \l_tmpa_int { + \str_put_right:Nn \l_tmpa_str i + } + \str_set_eq:NN \l__stex_variables_args_str \l_tmpa_str + \prop_put:Nnx \l_tmpa_prop { args } { \l__stex_variables_args_str } + } + } { + \prop_put:Nnx \l_tmpa_prop { args } { \l__stex_variables_args_str } + \prop_put:Nnx \l_tmpa_prop { arity } + { \str_count:N \l__stex_variables_args_str } + } + \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 + + \tl_if_empty:NF \l__stex_variables_op_tl { + \cs_set:cpx { + stex_var_op_notation_ \l__stex_variables_name_str _cs + } { + \_stex_term_omv:nn { + var://\l__stex_variables_name_str + }{ \comp{ \exp_args:No \exp_not:n { \l__stex_variables_op_tl } } } + } + } + + \tl_set:Nn \l_stex_notation_after_do_tl { + \exp_args:Nne \use:nn { + \cs_generate_from_arg_count:cNnn { stex_var_notation_\l__stex_variables_name_str _cs } + \cs_set:Npn { \prop_item:Nn \l_tmpa_prop { arity } } + } {{ + \exp_after:wN \exp_after:wN \exp_after:wN + \exp_not:n \exp_after:wN \exp_after:wN \exp_after:wN + { \exp_after:wN \l_stex_notation_macrocode_cs \l_stex_notation_dummyargs_tl \stex_symbol_after_invocation_tl} + }} + \stex_if_do_html:T { + \stex_annotate_invisible:nnn {vardecl}{\l__stex_variables_name_str}{ + \stex_annotate_invisible:nnn { precedence } + { \l__stex_variables_prec_str }{} + \tl_if_empty:NF \l__stex_variables_type_tl {\stex_annotate_invisible:nnn{type}{}{$\l__stex_variables_type_tl$}} + \stex_annotate_invisible:nnn{args}{}{ \l__stex_variables_args_str } + \stex_annotate_invisible:nnn{macroname}{#1}{} + \tl_if_empty:NF \l__stex_variables_def_tl { + \stex_annotate_invisible:nnn{definiens}{} + {$\l__stex_variables_def_tl$} + } + \str_if_empty:NF \l__stex_variables_assoctype_str { + \stex_annotate_invisible:nnn{assoctype}{\l__stex_variables_assoctype_str}{} + } + \int_zero:N \l_tmpa_int + \str_set_eq:NN \l__stex_variables_remaining_args_str \l__stex_variables_args_str + \tl_clear:N \l_tmpa_tl + \int_step_inline:nn { \prop_item:Nn \l_tmpa_prop { arity } }{ + \int_incr:N \l_tmpa_int + \str_set:Nx \l_tmpb_str { \str_head:N \l__stex_variables_remaining_args_str } + \str_set:Nx \l__stex_variables_remaining_args_str { \str_tail:N \l__stex_variables_remaining_args_str } + \str_if_eq:VnTF \l_tmpb_str a { + \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { + \c_hash_str \c_hash_str \int_use:N \l_tmpa_int a , + \c_hash_str \c_hash_str \int_use:N \l_tmpa_int b + } } + }{ + \str_if_eq:VnTF \l_tmpb_str B { + \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { + \c_hash_str \c_hash_str \int_use:N \l_tmpa_int a , + \c_hash_str \c_hash_str \int_use:N \l_tmpa_int b + } } + }{ + \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { + \c_hash_str \c_hash_str \int_use:N \l_tmpa_int + } } + } + } + } + \stex_annotate_invisible:nnn { notationcomp }{}{ + \str_set:Nx \l_stex_current_symbol_str {var://\l__stex_variables_name_str } + $ \exp_args:Nno \use:nn { \use:c { + stex_var_notation_\l__stex_variables_name_str _cs + } } { \l_tmpa_tl } $ + } + } + } + } + + \stex_notation_do:nnnn { \l__stex_variables_args_str } { \prop_item:Nn \l_tmpa_prop { arity } } {} +} + +\cs_new:Nn \__stex_variables_reset:N { + \tl_if_exist:NTF #1 { + \def \exp_not:N #1 { \exp_args:No \exp_not:n #1 } + }{ + \let \exp_not:N #1 \exp_not:N \undefined + } +} + +\NewDocumentCommand \__stex_variables_do_complex:nn { m m }{ + \clist_set:Nx \l__stex_variables_names { \tl_to_str:n {#1} } + \exp_args:Nnx \use:nn { + % TODO + \stex_annotate_invisible:nnn {vardecls}{\clist_use:Nn\l__stex_variables_names,}{ + #2 + } + }{ + \__stex_variables_reset:N \varnot + \__stex_variables_reset:N \vartype + \__stex_variables_reset:N \vardefi + } +} + +\NewDocumentCommand \vardef { s } { + \IfBooleanTF#1 { + \__stex_variables_do_complex:nn + }{ + \__stex_variables_do_simple:nnn + } +} + +\NewDocumentCommand \svar { O{} m }{ + \tl_if_empty:nTF {#1}{ + \str_set:Nn \l_tmpa_str { #2 } + }{ + \str_set:Nn \l_tmpa_str { #1 } + } + \_stex_term_omv:nn { + var://\l_tmpa_str + }{ \comp{ #2 } } +} + + + +%%%%%%%%%%%%% terms.dtx %%%%%%%%%%%%% + +\msg_new:nnn{stex}{error/nonotation}{ + Symbol~#1~invoked,~but~has~no~notation#2! +} +\msg_new:nnn{stex}{error/notationarg}{ + Error~in~parsing~notation~#1 +} +\msg_new:nnn{stex}{error/noop}{ + Symbol~#1~has~no~operator~notation~for~notation~#2 +} +\msg_new:nnn{stex}{error/notallowed}{ + Symbol~invocation~#1~not~allowed~in~notation~component~of~#2 +} + +\keys_define:nn { stex / terms } { + lang .tl_set_x:N = \l__stex_terms_lang_str , + variant .tl_set_x:N = \l__stex_terms_variant_str , + unknown .code:n = \str_set:Nx + \l__stex_terms_variant_str \l_keys_key_str +} + +\cs_new_protected:Nn \__stex_terms_args:n { + \str_clear:N \l__stex_terms_lang_str + \str_clear:N \l__stex_terms_variant_str + + \keys_set:nn { stex / terms } { #1 } +} + +\cs_new:Nn \__stex_terms_reset:N { + \tl_if_exist:NTF #1 { + \def \exp_not:N #1 { \exp_args:No \exp_not:n #1 } + }{ + \let \exp_not:N #1 \exp_not:N \undefined + } +} + +\bool_new:N \l__stex_terms_allow_semantic_bool +\bool_set_true:N \l__stex_terms_allow_semantic_bool + +\cs_new_protected:Nn \stex_invoke_symbol:n { + \bool_if:NTF \l__stex_terms_allow_semantic_bool { + \str_if_eq:eeF { + \prop_item:cn { + l_stex_symdecl_#1_prop + }{ deprecate } + }{}{ + \msg_warning:nnxx{stex}{warning/deprecated}{ + Symbol~#1 + }{ + \prop_item:cn {l_stex_symdecl_#1_prop}{ deprecate } + } + } + \if_mode_math: + \exp_after:wN \__stex_terms_invoke_math:n + \else: + \exp_after:wN \__stex_terms_invoke_text:n + \fi: { #1 } + }{ + \msg_error:nnxx{stex}{error/notallowed}{#1}{\l_stex_current_symbol_str} + } +} + +\cs_new_protected:Nn \__stex_terms_invoke_text:n { + \peek_charcode_remove:NTF ! { + \__stex_terms_invoke_op_custom:nn {#1} + }{ + \__stex_terms_invoke_custom:nn {#1} + } +} + +\cs_new_protected:Nn \__stex_terms_invoke_math:n { + \peek_charcode_remove:NTF ! { + % operator + \peek_charcode_remove:NTF * { + % custom op + \__stex_terms_invoke_op_custom:nn {#1} + }{ + % op notation + \peek_charcode:NTF [ { + \__stex_terms_invoke_op_notation:nw {#1} + }{ + \__stex_terms_invoke_op_notation:nw {#1}[] + } + } + }{ + \peek_charcode_remove:NTF * { + \__stex_terms_invoke_custom:nn {#1} + % custom + }{ + % normal + \peek_charcode:NTF [ { + \__stex_terms_invoke_notation:nw {#1} + }{ + \__stex_terms_invoke_notation:nw {#1}[] + } + } + } +} + +\cs_new_protected:Nn \__stex_terms_invoke_op_custom:nn { + \exp_args:Nnx \use:nn { + \str_set:Nn \l_stex_current_symbol_str { #1 } + \bool_set_false:N \l__stex_terms_allow_semantic_bool + \_stex_term_oms:nnn {#1 \c_hash_str\c_hash_str}{#1}{ + \comp{ #2 } + } + }{ + \__stex_terms_reset:N \l_stex_current_symbol_str + \bool_set_true:N \l__stex_terms_allow_semantic_bool + } +} + +\cs_new_protected:Nn \__stex_terms_find_notation:nn { + \str_set:Nn \l_stex_current_symbol_str { #1 } + \__stex_terms_args:n { #2 } + \seq_if_empty:cTF { + l_stex_symdecl_ #1 _notations + } { + \msg_error:nnxx{stex}{error/nonotation}{#1}{s} + } { + \bool_lazy_all:nTF { + {\str_if_empty_p:N \l__stex_terms_variant_str} + {\str_if_empty_p:N \l__stex_terms_lang_str} + }{ + \seq_get_left:cN {l_stex_symdecl_#1_notations}\l__stex_terms_variant_str + }{ + \seq_if_in:cxTF {l_stex_symdecl_#1_notations}{ + \l__stex_terms_variant_str \c_hash_str \l__stex_terms_lang_str + }{ + \str_set:Nx \l__stex_terms_variant_str { \l__stex_terms_variant_str \c_hash_str \l__stex_terms_lang_str } + }{ + \msg_error:nnxx{stex}{error/nonotation}{#1}{ + ~\l__stex_terms_variant_str \c_hash_str \l__stex_terms_lang_str + } + } + } + } +} + +\cs_new_protected:Npn \__stex_terms_invoke_op_notation:nw #1 [#2] { + \__stex_terms_find_notation:nn { #1 }{ #2 } + \bool_set_false:N \l__stex_terms_allow_semantic_bool + \cs_if_exist:cTF { + stex_op_notation_ #1 \c_hash_str \l__stex_terms_variant_str _cs + }{ + \use:c{stex_op_notation_ #1 \c_hash_str \l__stex_terms_variant_str _cs} + }{ + \msg_error:nnxx{stex}{error/noop}{#1}{\l__stex_terms_variant_str} + } + \bool_set_true:N \l__stex_terms_allow_semantic_bool +} + +\cs_new_protected:Npn \__stex_terms_invoke_notation:nw #1 [#2] { + \__stex_terms_find_notation:nn { #1 }{ #2 } + \cs_if_exist:cTF { + stex_notation_ #1 \c_hash_str \l__stex_terms_variant_str _cs + }{ + \tl_set:Nx \stex_symbol_after_invocation_tl { + \__stex_terms_reset:N \stex_symbol_after_invocation_tl + \__stex_terms_reset:N \l_stex_current_symbol_str + \bool_set_true:N \l__stex_terms_allow_semantic_bool + } + \bool_set_false:N \l__stex_terms_allow_semantic_bool + \use:c{stex_notation_ #1 \c_hash_str \l__stex_terms_variant_str _cs} + }{ + \msg_error:nnxx{stex}{error/nonotation}{#1}{ + ~\l__stex_terms_variant_str + } + } +} + +\prop_new:N \l__stex_terms_custom_args_prop + +\cs_new_protected:Nn \__stex_terms_invoke_custom:nn { + \exp_args:Nnx \use:nn { + \bool_set_false:N \l__stex_terms_allow_semantic_bool + \str_set:Nn \l_stex_current_symbol_str { #1 } + \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_symdecl_#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: } + \str_if_empty:NTF \l_tmpa_str { + \_stex_term_oms:nnn {#1}{#1}{#2} + }{ + \str_if_in:NnTF \l_tmpa_str b { + \_stex_term_ombind:nnn {#1}{#1}{#2} + }{ + \str_if_in:NnTF \l_tmpa_str B { + \_stex_term_ombind:nnn {#1}{#1}{#2} + }{ + \_stex_term_oma:nnn {#1}{#1}{#2} + } + } + } + % TODO check that all arguments exist + }{ + \__stex_terms_reset:N \l_stex_current_symbol_str + \__stex_terms_reset:N \arg + \__stex_terms_reset:N \l__stex_terms_custom_args_prop + \bool_set_true:N \l__stex_terms_allow_semantic_bool + } +} + +\NewDocumentCommand \__stex_terms_arg: { s O{} m}{ + \tl_if_empty:nTF {#2}{ + \int_set:Nn \l_tmpa_int {\prop_item:Nn \l__stex_terms_custom_args_prop {currnum}} + \bool_set_true:N \l_tmpa_bool + \bool_do_while:Nn \l_tmpa_bool { + \exp_args:NNx \prop_if_in:NnTF \l__stex_terms_custom_args_prop {\int_use:N \l_tmpa_int} { + \int_incr:N \l_tmpa_int + }{ + \bool_set_false:N \l_tmpa_bool + } + } + }{ + \int_set:Nn \l_tmpa_int { #2 } + \exp_args:NNx \prop_if_in:NnT \l__stex_terms_custom_args_prop {\int_use:N \l_tmpa_int} { + % TODO throw error + } + } + \str_set:Nx \l_tmpa_str {\prop_item:Nn \l__stex_terms_custom_args_prop {args} } + \int_compare:nNnT \l_tmpa_int > {\str_count:N \l_tmpa_str} { + % TODO throw error + } + \IfBooleanTF#1{ + \stex_annotate_invisible:n { + \exp_args:No \_stex_term_arg:nn {\l_stex_current_symbol_str}{#3} + } + }{ + \exp_args:No \_stex_term_arg:nn {\l_stex_current_symbol_str}{#3} + } +} + +\cs_new_protected:Nn \_stex_term_arg:nn { + \exp_args:Nnx \use:nn { + \bool_set_true:N \l__stex_terms_allow_semantic_bool + \stex_annotate:nnn{ arg }{ #1 }{ #2 } + }{ + \bool_set_false:N \l__stex_terms_allow_semantic_bool + } +} + +\cs_new_protected:Nn \_stex_term_math_arg:nnn { + \exp_args:Nnx \use:nn + { \int_set:Nn \l__stex_terms_downprec { #2 } + \_stex_term_arg:nn { #1 }{ #3 } + } + { \int_set:Nn \exp_not:N \l__stex_terms_downprec { \int_use:N \l__stex_terms_downprec } } +} + +\tl_const:Nx \infprec {\int_use:N \c_max_int} +\tl_const:Nx \neginfprec {-\int_use:N \c_max_int} +\int_new:N \l__stex_terms_downprec +\int_set_eq:NN \l__stex_terms_downprec \infprec +\tl_set:Nn \l__stex_terms_left_bracket_str ( +\tl_set:Nn \l__stex_terms_right_bracket_str ) +\cs_new_protected:Nn \__stex_terms_maybe_brackets:nn { + \bool_if:NTF \l__stex_terms_brackets_done_bool { + \bool_set_false:N \l__stex_terms_brackets_done_bool + #2 + } { + \int_compare:nNnTF { #1 } > \l__stex_terms_downprec { + \bool_if:NTF \l_stex_inparray_bool { #2 }{ + \stex_debug:nn{dobrackets}{\number#1 > \number\l__stex_terms_downprec; \detokenize{#2}} + \dobrackets { #2 } + } + }{ #2 } + } +} +\bool_new:N \l__stex_terms_brackets_done_bool +\cs_new_protected:Npn \dobrackets #1 { + %\ThisStyle{\if D\m@switch + % \exp_args:Nnx \use:nn + % { \exp_after:wN \left\l__stex_terms_left_bracket_str #1 } + % { \exp_not:N\right\l__stex_terms_right_bracket_str } + % \else + \exp_args:Nnx \use:nn + { + \bool_set_true:N \l__stex_terms_brackets_done_bool + \int_set:Nn \l__stex_terms_downprec \infprec + \l__stex_terms_left_bracket_str + #1 + } + { + \bool_set_false:N \l__stex_terms_brackets_done_bool + \l__stex_terms_right_bracket_str + \int_set:Nn \l__stex_terms_downprec { \int_use:N \l__stex_terms_downprec } + } + %\fi} +} +\cs_new_protected:Npn \withbrackets #1 #2 #3 { + \exp_args:Nnx \use:nn + { + \tl_set:Nx \l__stex_terms_left_bracket_str { #1 } + \tl_set:Nx \l__stex_terms_right_bracket_str { #2 } + #3 + } + { + \tl_set:Nn \exp_not:N \l__stex_terms_left_bracket_str + {\l__stex_terms_left_bracket_str} + \tl_set:Nn \exp_not:N \l__stex_terms_right_bracket_str + {\l__stex_terms_right_bracket_str} + } +} +\cs_new_protected:Npn \STEXinvisible #1 { + \stex_annotate_invisible:n { #1 } +} +\cs_new_protected:Nn \_stex_term_oms:nnn { + \stex_annotate:nnn{ OMID }{ #2 }{ + \stex_highlight_term:nn { #1 } { #3 } + } +} + +\cs_new_protected:Nn \_stex_term_math_oms:nnnn { + \__stex_terms_maybe_brackets:nn { #3 }{ + \_stex_term_oms:nnn { #1 } { #1\c_hash_str#2 } { #4 } + } +} +\cs_new_protected:Nn \_stex_term_omv:nn { + \stex_annotate:nnn{ OMID }{ #1 }{ + \stex_highlight_term:nn { #1 } { #2 } + } +} +\cs_new_protected:Nn \_stex_term_oma:nnn { + \stex_annotate:nnn{ OMA }{ #2 }{ + \stex_highlight_term:nn { #1 } { #3 } + } +} + +\cs_new_protected:Nn \_stex_term_math_oma:nnnn { + \__stex_terms_maybe_brackets:nn { #3 }{ + \_stex_term_oma:nnn { #1 } { #1\c_hash_str#2 } { #4 } + } +} +\cs_new_protected:Nn \_stex_term_ombind:nnn { + \stex_annotate:nnn{ OMBIND }{ #2 }{ + \stex_highlight_term:nn { #1 } { #3 } + } +} + +\cs_new_protected:Nn \_stex_term_math_omb:nnnn { + \__stex_terms_maybe_brackets:nn { #3 }{ + \_stex_term_ombind:nnn { #1 } { #1\c_hash_str#2 } { #4 } + } +} +\cs_new_protected:Nn \_stex_term_math_assoc_arg:nnnn { + % TODO sequences + \clist_set:Nn \l_tmpa_clist{ #3 } + \int_compare:nNnTF { \clist_count:N \l_tmpa_clist } < 2 { + \tl_set:Nn \l_tmpa_tl { #3 } + }{ + \cs_set:Npn \l_tmpa_cs ##1 ##2 { #4 } + \clist_reverse:N \l_tmpa_clist + \clist_pop:NN \l_tmpa_clist \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 { ##1 } \l_tmpa_tl + } + } + } + \exp_args:Nnno + \_stex_term_math_arg:nnn{#1}{#2}\l_tmpa_tl +} +\cs_new_protected:Nn \stex_term_custom:nn { + \str_set:Nn \l__stex_terms_custom_uri { #1 } + \str_set:Nn \l_tmpa_str { #2 } + \tl_clear:N \l_tmpa_tl + \int_zero:N \l_tmpa_int + \int_set:Nn \l_tmpb_int { \str_count:N \l_tmpa_str } + \__stex_terms_custom_loop: +} +\cs_new_protected:Nn \__stex_terms_custom_loop: { + \bool_set_false:N \l_tmpa_bool + \bool_while_do:nn { + \str_if_eq_p:ee X { + \str_item:Nn \l_tmpa_str { \l_tmpa_int + 1 } + } + }{ + \int_incr:N \l_tmpa_int + } + + \peek_charcode:NTF [ { + % notation/text component + \__stex_terms_custom_component:w + } { + \int_compare:nNnTF \l_tmpa_int = \l_tmpb_int { + % all arguments read => finish + \__stex_terms_custom_final: + } { + % arguments missing + \peek_charcode_remove:NTF * { + % invisible, specific argument position or both + \peek_charcode:NTF [ { + % visible specific argument position + \__stex_terms_custom_arg:wn + } { + % invisible + \peek_charcode_remove:NTF * { + % invisible specific argument position + \__stex_terms_custom_arg_inv:wn + } { + % invisible next argument + \__stex_terms_custom_arg_inv:wn [ \l_tmpa_int + 1 ] + } + } + } { + % next normal argument + \__stex_terms_custom_arg:wn [ \l_tmpa_int + 1 ] + } + } + } +} +\cs_new_protected:Npn \__stex_terms_custom_arg_inv:wn [ #1 ] #2 { + \bool_set_true:N \l_tmpa_bool + \__stex_terms_custom_arg:wn [ #1 ] { #2 } +} +\cs_new_protected:Npn \__stex_terms_custom_arg:wn [ #1 ] #2 { + \str_set:Nx \l_tmpb_str { + \str_item:Nn \l_tmpa_str { #1 } + } + \str_case:VnTF \l_tmpb_str { + { X } { + \msg_error:nnx{stex}{error/notationarg}{\l__stex_terms_custom_uri} + } + { i } { \__stex_terms_custom_set_X:n { #1 } } + { b } { \__stex_terms_custom_set_X:n { #1 } } + { a } { \__stex_terms_custom_set_X:n { #1 } } % TODO ? + { B } { \__stex_terms_custom_set_X:n { #1 } } % TODO ? + }{}{ + \msg_error:nnx{stex}{error/notationarg}{\l__stex_terms_custom_uri} + } + + \bool_if:nTF \l_tmpa_bool { + \tl_put_right:Nx \l_tmpa_tl { + \stex_annotate_invisible:n { + \_stex_term_arg:nn { \int_eval:n { #1 } } + \exp_not:n { { #2 } } + } + } + } { + \tl_put_right:Nx \l_tmpa_tl { + \_stex_term_arg:nn { \int_eval:n { #1 } } + \exp_not:n { { #2 } } + } + } + + \__stex_terms_custom_loop: +} +\cs_new_protected:Nn \__stex_terms_custom_set_X:n { + \str_set:Nx \l_tmpa_str { + \str_range:Nnn \l_tmpa_str 1 { #1 - 1 } + X + \str_range:Nnn \l_tmpa_str { #1 + 1 } { -1 } + } +} +\cs_new_protected:Npn \__stex_terms_custom_component:w [ #1 ] { + \tl_put_right:Nn \l_tmpa_tl { \comp{ #1 } } + \__stex_terms_custom_loop: +} +\cs_new_protected:Nn \__stex_terms_custom_final: { + \int_compare:nNnTF \l_tmpb_int = 0 { + \exp_args:Nnno \_stex_term_oms:nnn + }{ + \str_if_in:NnTF \l_tmpa_str {b} { + \exp_args:Nnno \_stex_term_ombind:nnn + } { + \exp_args:Nnno \_stex_term_oma:nnn + } + } + { \l__stex_terms_custom_uri } { \l__stex_terms_custom_uri } { \l_tmpa_tl } +} +\cs_new:Nn \stex_capitalize:n { \uppercase{#1} } + +\keys_define:nn { stex / symname } { + pre .tl_set_x:N = \l__stex_terms_pre_tl , + post .tl_set_x:N = \l__stex_terms_post_tl , + root .tl_set_x:N = \l__stex_terms_root_tl +} + +\cs_new_protected:Nn \stex_symname_args:n { + \tl_clear:N \l__stex_terms_post_tl + \tl_clear:N \l__stex_terms_pre_tl + \tl_clear:N \l__stex_terms_root_str + \keys_set:nn { stex / symname } { #1 } +} + +\NewDocumentCommand \symref { m m }{ + \let\compemph_uri_prev:\compemph@uri + \let\compemph@uri\symrefemph@uri + \STEXsymbol{#1}!{ #2 } + \let\compemph@uri\compemph_uri_prev: +} + +\NewDocumentCommand \synonym { O{} m m}{ + \stex_symname_args:n { #1 } + \let\compemph_uri_prev:\compemph@uri + \let\compemph@uri\symrefemph@uri + % TODO + \STEXsymbol{#2}!{\l__stex_terms_pre_tl #3 \l__stex_terms_post_tl} + \let\compemph@uri\compemph_uri_prev: +} + +\NewDocumentCommand \symname { O{} m }{ + \stex_symname_args:n { #1 } + \stex_get_symbol:n { #2 } + \str_set:Nx \l_tmpa_str { + \prop_item:cn { l_stex_symdecl_ \l_stex_get_symbol_uri_str _prop } { name } + } + \exp_args:NNno \str_replace_all:Nnn \l_tmpa_str {-} {~} + + \let\compemph_uri_prev:\compemph@uri + \let\compemph@uri\symrefemph@uri + \exp_args:NNx \use:nn + \stex_invoke_symbol:n { { \l_stex_get_symbol_uri_str }!{ + \l__stex_terms_pre_tl \l_tmpa_str \l__stex_terms_post_tl + } } + \let\compemph@uri\compemph_uri_prev: +} + +\NewDocumentCommand \Symname { O{} m }{ + \stex_symname_args:n { #1 } + \stex_get_symbol:n { #2 } + \str_set:Nx \l_tmpa_str { + \prop_item:cn { l_stex_symdecl_ \l_stex_get_symbol_uri_str _prop } { name } + } + \exp_args:NNno \str_replace_all:Nnn \l_tmpa_str {-} {~} + \let\compemph_uri_prev:\compemph@uri + \let\compemph@uri\symrefemph@uri + \exp_args:NNx \use:nn + \stex_invoke_symbol:n { { \l_stex_get_symbol_uri_str }!{ + \exp_after:wN \stex_capitalize:n \l_tmpa_str + \l__stex_terms_post_tl + } } + \let\compemph@uri\compemph_uri_prev: +} + +\str_new:N \l_stex_current_symbol_str +\cs_new_protected:Nn \stex_highlight_term:nn { + \exp_args:Nnx + \use:nn { + \str_set:Nx \l_stex_current_symbol_str { #1 } + #2 + } { + \str_set:Nx \exp_not:N \l_stex_current_symbol_str + { \l_stex_current_symbol_str } + } +} + +\cs_new_protected:Nn \stex_unhighlight_term:n { + #1 %\iffalse{{\fi}} #1 {{\iffalse}}\fi +} +\cs_new_protected:Npn \comp #1 { + \str_if_empty:NF \l_stex_current_symbol_str { + \rustex_if:TF { + \stex_annotate:nnn { comp }{ \l_stex_current_symbol_str }{ #1 } + }{ + \exp_args:Nnx \compemph@uri { #1 } { \l_stex_current_symbol_str } + } + } +} + +\cs_new_protected:Npn \compemph@uri #1 #2 { + \compemph{ #1 } +} + +\cs_new_protected:Npn \compemph #1 { + #1 +} + +\cs_new_protected:Npn \defemph@uri #1 #2 { + \defemph{#1} +} + +\cs_new_protected:Npn \defemph #1 { + \textbf{#1} +} + +\cs_new_protected:Npn \symrefemph@uri #1 #2 { + \symrefemph{#1} +} + +\cs_new_protected:Npn \symrefemph #1 { + \textbf{#1} +} +\NewDocumentCommand \ellipses {} { \ldots } +\bool_new:N \l_stex_inparray_bool +\bool_set_false:N \l_stex_inparray_bool +\NewDocumentCommand \parray { m m } { + \begingroup + \bool_set_true:N \l_stex_inparray_bool + \begin{array}{#1} + #2 + \end{array} + \endgroup +} + +\NewDocumentCommand \prmatrix { m } { + \begingroup + \bool_set_true:N \l_stex_inparray_bool + \begin{matrix} + #1 + \end{matrix} + \endgroup +} + +\def \maybephline { + \bool_if:NT \l_stex_inparray_bool {\hline} +} + +\def \parrayline #1 #2 { + #1 #2 \bool_if:NT \l_stex_inparray_bool {\\} +} + +\def \pmrow #1 { \parrayline{}{ #1 } } + +\def \parraylineh #1 #2 { + #1 #2 \bool_if:NT \l_stex_inparray_bool {\\\hline} +} + +\def \parraycell #1 { + #1 \bool_if:NT \l_stex_inparray_bool {&} +} +\cs_new_protected:Nn \stex_invoke_variable:n { + \if_mode_math: + \exp_after:wN \__stex_variables_invoke_math:n + \else: + \exp_after:wN \__stex_variables_invoke_text:n + \fi: {#1} +} + +\cs_new_protected:Nn \__stex_variables_invoke_text:n { + %TODO +} + +\cs_new_protected:Nn \__stex_variables_invoke_math:n { + \peek_charcode_remove:NTF ! { + \peek_charcode_remove:NTF ! { + \peek_charcode:NTF [ { + \__stex_variables_invoke_op_custom:nw + }{ + % TODO throw error + } + }{ + \__stex_variables_invoke_op:n { #1 } + } + }{ + \peek_charcode_remove:NTF * { + \__stex_variables_invoke_text:n { #1 } + }{ + \__stex_variables_invoke_math_ii:n { #1 } + } + } +} + +\cs_new_protected:Nn \__stex_variables_invoke_op:n { + \cs_if_exist:cTF { + stex_var_op_notation_ #1 _cs + }{ + \use:c{stex_var_op_notation_ #1 _cs } + }{ + \msg_error:nnxx{stex}{error/noop}{variable~#1}{} + } +} + +\cs_new_protected:Npn \__stex_variables_invoke_math_ii:n #1 { + \cs_if_exist:cTF { + stex_var_notation_#1_cs + }{ + \str_set:Nn \l_stex_current_symbol_str { #1 } + \use:c{stex_var_notation_#1_cs} + }{ + \msg_error:nnxx{stex}{error/nonotation}{variable~#1}{s} + } +} + + +%%%%%%%%%%%%% features.dtx %%%%%%%%%%%%% + +\msg_new:nnn{stex}{error/copymodule/notallowed}{ + Symbol~#1~can~not~be~assigned~in~copymodule~#2 +} +\msg_new:nnn{stex}{error/interpretmodule/nodefiniens}{ + Symbol~#1~not~assigned~in~interpretmodule~#2 +} + +\cs_new_protected:Nn \stex_get_symbol_in_copymodule:n { + \tl_if_head_eq_catcode:nNTF { #1 } \relax { + \__stex_features_get_symbol_from_cs:n { #1 } + }{ + % argument is a string + % is it a command name? + \cs_if_exist:cTF { #1 }{ + \cs_set_eq:Nc \l_tmpa_tl { #1 } + \str_set:Nx \l_tmpa_str { \cs_argument_spec:N \l_tmpa_tl } + \str_if_empty:NTF \l_tmpa_str { + \exp_args:Nx \cs_if_eq:NNTF { + \tl_head:N \l_tmpa_tl + } \stex_invoke_symbol:n { + \exp_args:No \__stex_features_get_symbol_from_cs:n { \use:c { #1 } } + }{ + \__stex_features_get_symbol_from_string:n { #1 } + } + } { + \__stex_features_get_symbol_from_string:n { #1 } + } + }{ + % argument is not a command name + \__stex_features_get_symbol_from_string:n { #1 } + % \l_stex_all_symbols_seq + } + } +} + +\cs_new_protected:Nn \__stex_features_get_symbol_from_string:n { + \str_set:Nn \l_tmpa_str { #1 } + \bool_set_false:N \l_tmpa_bool + \bool_if:NF \l_tmpa_bool { + \tl_set:Nn \l_tmpa_tl { + \msg_set:nnn{stex}{error/unknownsymbol}{ + No~symbol~#1~found! + } + \msg_error:nn{stex}{error/unknownsymbol} + } + \str_set:Nn \l_tmpa_str { #1 } + \int_set:Nn \l_tmpa_int { \str_count:N \l_tmpa_str } + \seq_map_inline:Nn \l__stex_features_copymodule_fields_seq { + \str_set:Nn \l_tmpb_str { ##1 } + \str_if_eq:eeT { \l_tmpa_str } { + \str_range:Nnn \l_tmpb_str { -\l_tmpa_int } { -1 } + } { + \seq_map_break:n { + \tl_set:Nn \l_tmpa_tl { + \str_set:Nn \l_stex_get_symbol_uri_str { + ##1 + } + \__stex_features_get_symbol_check: + } + } + } + } + \l_tmpa_tl + } +} + +\cs_new_protected:Nn \__stex_features_get_symbol_from_cs:n { + \exp_args:NNx \tl_set:Nn \l_tmpa_tl + { \tl_tail:N \l_tmpa_tl } + \tl_if_single:NTF \l_tmpa_tl { + \exp_args:No \tl_if_head_is_group:nTF \l_tmpa_tl { + \exp_after:wN \str_set:Nn \exp_after:wN + \l_stex_get_symbol_uri_str \l_tmpa_tl + \__stex_features_get_symbol_check: + }{ + % TODO + % tail is not a single group + } + }{ + % TODO + % tail is not a single group + } +} + +\cs_new_protected:Nn \__stex_features_get_symbol_check: { + \exp_args:NNno \seq_set_split:Nnn \l_tmpa_seq {?} \l_stex_get_symbol_uri_str + \int_compare:nNnTF {\seq_count:N \l_tmpa_seq} = 3 { + \seq_pop_right:NN \l_tmpa_seq \l_tmpb_str + \str_set:Nx \l_tmpa_str {\seq_use:Nn \l_tmpa_seq ?} + \seq_if_in:NoF \l__stex_features_copymodule_modules_seq \l_tmpa_str { + \msg_error:nnxx{stex}{error/copymodule/notallowed}{\l_stex_get_symbol_uri_str}{ + \l_stex_current_copymodule_name_str\\Allowed:~\seq_use:Nn \l__stex_features_copymodule_modules_seq {,~} + } + } + }{ + \msg_error:nnxx{stex}{error/copymodule/notallowed}{\l_stex_get_symbol_uri_str}{ + \l_stex_current_copymodule_name_str~(inexplicably) + } + } +} + +\cs_new_protected:Nn \stex_copymodule_start:nnnn { + \stex_import_module_uri:nn { #1 } { #2 } + \str_set:Nx \l_stex_current_copymodule_name_str {#3} + \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_collect_imports:n {\l_stex_import_ns_str ?\l_stex_import_name_str } + \seq_set_eq:NN \l__stex_features_copymodule_modules_seq \l_stex_collect_imports_seq + \seq_clear:N \l__stex_features_copymodule_fields_seq + \seq_map_inline:Nn \l__stex_features_copymodule_modules_seq { + \seq_map_inline:cn {c_stex_module_##1_constants}{ + \exp_args:NNx \seq_put_right:Nn \l__stex_features_copymodule_fields_seq { + ##1 ? ####1 + } + } + } + \seq_clear:N \l_tmpa_seq + \exp_args:NNx \prop_set_from_keyval:Nn \l_stex_current_copymodule_prop { + name = \l_stex_current_copymodule_name_str , + module = \l_stex_current_module_str , + from = \l_stex_import_ns_str ?\l_stex_import_name_str , + includes = \l_tmpa_seq , + fields = \l_tmpa_seq + } + \stex_debug:nn{copymodule}{#4~for~module~{\l_stex_import_ns_str ?\l_stex_import_name_str} + as~\l_stex_current_module_str?\l_stex_current_copymodule_name_str} + \stex_debug:nn{copymodule}{modules:\seq_use:Nn \l__stex_features_copymodule_modules_seq {,~}} + \stex_debug:nn{copymodule}{fields:\seq_use:Nn \l__stex_features_copymodule_fields_seq {,~}} + \stex_if_smsmode:F { + \begin{stex_annotate_env} {#4} { + \l_stex_current_module_str?\l_stex_current_copymodule_name_str + } + \stex_annotate_invisible:nnn{from}{\l_stex_import_ns_str ?\l_stex_import_name_str}{} + } + \bool_set_eq:NN \l__stex_features_oldhtml_bool \_stex_html_do_output_bool + \bool_set_false:N \_stex_html_do_output_bool +} +\cs_new_protected:Nn \stex_copymodule_end:n { + \def \l_tmpa_cs ##1 ##2 {#1} + \bool_set_eq:NN \_stex_html_do_output_bool \l__stex_features_oldhtml_bool + \tl_clear:N \l_tmpa_tl + \tl_clear:N \l_tmpb_tl + \prop_get:NnN \l_stex_current_copymodule_prop {fields} \l_tmpa_seq + \seq_map_inline:Nn \l__stex_features_copymodule_modules_seq { + \seq_map_inline:cn {c_stex_module_##1_constants}{ + \tl_clear:N \l_tmpc_tl + \l_tmpa_cs{##1}{####1} + \str_if_exist:cTF {l__stex_features_copymodule_##1?####1_name_str} { + \tl_put_right:Nx \l_tmpa_tl { + \prop_set_from_keyval:cn { + l_stex_symdecl_\l_stex_current_module_str ? \use:c{l__stex_features_copymodule_##1?####1_name_str}_prop + }{ + \exp_after:wN \prop_to_keyval:N \csname + l_stex_symdecl_\l_stex_current_module_str ? \use:c{l__stex_features_copymodule_##1?####1_name_str}_prop + \endcsname + } + \seq_clear:c { + l_stex_symdecl_ + \l_stex_current_module_str ? \use:c{l__stex_features_copymodule_##1?####1_name_str} + _notations + } + } + \tl_put_right:Nx \l_tmpc_tl { + \stex_copy_notations:nn {\l_stex_current_module_str ? \use:c{l__stex_features_copymodule_##1?####1_name_str}}{##1?####1} + \stex_annotate_invisible:nnn{alias}{\use:c{l__stex_features_copymodule_##1?####1_name_str}}{} + } + \seq_put_right:Nx \l_tmpa_seq {\l_stex_current_module_str ? \use:c{l__stex_features_copymodule_##1?####1_name_str}} + \str_if_exist:cT {l__stex_features_copymodule_##1?####1_macroname_str} { + \tl_put_right:Nx \l_tmpc_tl { + \stex_annotate_invisible:nnn{macroname}{\use:c{l__stex_features_copymodule_##1?####1_macroname_str}}{} + } + \tl_put_right:Nx \l_tmpa_tl { + \tl_set:cx {\use:c{l__stex_features_copymodule_##1?####1_macroname_str}}{ + \stex_invoke_symbol:n { + \l_stex_current_module_str ? \use:c{l__stex_features_copymodule_##1?####1_name_str} + } + } + } + } + }{ + \tl_put_right:Nx \l_tmpc_tl { + \stex_copy_notations:nn {\l_stex_current_module_str ? \l_stex_current_copymodule_name_str / ####1 }{##1?####1} + } + \prop_set_eq:Nc \l_tmpa_prop {l_stex_symdecl_ ##1?####1 _prop} + \prop_put:Nnx \l_tmpa_prop { name }{ \l_stex_current_copymodule_name_str / ####1 } + \prop_put:Nnx \l_tmpa_prop { module }{ \l_stex_current_module_str } + \tl_put_right:Nx \l_tmpa_tl { + \prop_set_from_keyval:cn { + l_stex_symdecl_\l_stex_current_module_str ? \l_stex_current_copymodule_name_str / ####1_prop + }{ + \prop_to_keyval:N \l_tmpa_prop + } + \seq_clear:c { + l_stex_symdecl_ + \l_stex_current_module_str ? \l_stex_current_copymodule_name_str / ####1 + _notations + } + } + \seq_put_right:Nx \l_tmpa_seq {\l_stex_current_module_str ? \l_stex_current_copymodule_name_str / ####1 } + \str_if_exist:cT {l__stex_features_copymodule_##1?####1_macroname_str} { + \tl_put_right:Nx \l_tmpc_tl { + \stex_annotate_invisible:nnn{macroname}{\use:c{l__stex_features_copymodule_##1?####1_macroname_str}}{} + } + \tl_put_right:Nx \l_tmpa_tl { + \tl_set:cx {\use:c{l__stex_features_copymodule_##1?####1_macroname_str}}{ + \stex_invoke_symbol:n { + \l_stex_current_module_str ? \l_stex_current_copymodule_name_str / ####1 + } + } + } + } + } + \tl_if_exist:cT {l__stex_features_copymodule_##1?####1_def_tl}{ + \tl_put_right:Nx \l_tmpc_tl { + \stex_annotate_invisible:nnn{definiens}{}{$\use:c{l__stex_features_copymodule_##1?####1_def_tl}$} + } + } + \tl_put_right:Nx \l_tmpb_tl { + \stex_annotate:nnn{assignment} {##1?####1} { \l_tmpc_tl } + } + } + } + \prop_put:Nno \l_stex_current_copymodule_prop {fields} \l_tmpa_seq + \tl_put_left:Nx \l_tmpa_tl { + \prop_set_from_keyval:cn { + l_stex_copymodule_ \l_stex_current_module_str?\l_stex_current_copymodule_name_str _prop + }{ + \prop_to_keyval:N \l_stex_current_copymodule_prop + } + } + \exp_args:No \stex_add_to_current_module:n \l_tmpa_tl + \stex_debug:nn{copymodule}{result:\meaning \l_tmpa_tl} + \exp_args:Nx \stex_do_up_to_module:n { + \exp_args:No \exp_not:n \l_tmpa_tl + } + \l_tmpb_tl + \stex_if_smsmode:F { + \end{stex_annotate_env} + } +} + +\NewDocumentEnvironment {copymodule} { O{} m m}{ + \stex_copymodule_start:nnnn { #1 }{ #2 }{ #3 }{ structure } + \stex_deactivate_macro:Nn \symdecl {module~environments} + \stex_deactivate_macro:Nn \symdef {module~environments} + \stex_deactivate_macro:Nn \notation {module~environments} + \stex_reactivate_macro:N \assign + \stex_reactivate_macro:N \renamedecl + \stex_reactivate_macro:N \donotcopy + \stex_smsmode_do: +}{ + \stex_copymodule_end:n {} +} + +\NewDocumentEnvironment {interpretmodule} { O{} m m}{ + \stex_copymodule_start:nnnn { #1 }{ #2 }{ #3 }{ realization } + \stex_deactivate_macro:Nn \symdecl {module~environments} + \stex_deactivate_macro:Nn \symdef {module~environments} + \stex_deactivate_macro:Nn \notation {module~environments} + \stex_reactivate_macro:N \assign + \stex_reactivate_macro:N \renamedecl + \stex_reactivate_macro:N \donotcopy + \stex_smsmode_do: +}{ + \stex_copymodule_end:n { + \tl_if_exist:cF { + l__stex_features_copymodule_##1?##2_def_tl + }{ + \msg_error:nnxx{stex}{error/interpretmodule/nodefiniens}{ + ##1?##2 + }{\l_stex_current_copymodule_name_str} + } + } +} + +\NewDocumentCommand \donotcopy { O{} m}{ + \stex_import_module_uri:nn { #1 } { #2 } + \stex_collect_imports:n {\l_stex_import_ns_str ?\l_stex_import_name_str } + \seq_map_inline:Nn \l_stex_collect_imports_seq { + \seq_remove_all:Nn \l__stex_features_copymodule_modules_seq { ##1 } + \seq_map_inline:cn {c_stex_module_##1_constants}{ + \seq_remove_all:Nn \l__stex_features_copymodule_fields_seq { ##1 ? ####1 } + \bool_lazy_any_p:nT { + { \cs_if_exist_p:c {l__stex_features_copymodule_##1?####1_name_str}} + { \cs_if_exist_p:c {l__stex_features_copymodule_##1?####1_macroname_str}} + { \cs_if_exist_p:c {l__stex_features_copymodule_##1?####1_def_tl}} + }{ + % TODO throw error + } + } + } + + \prop_get:NnN \l_stex_current_copymodule_prop { includes } \l_tmpa_seq + \seq_put_right:Nx \l_tmpa_seq {\l_stex_import_ns_str ?\l_stex_import_name_str } + \prop_put:Nnx \l_stex_current_copymodule_prop {includes} \l_tmpa_seq +} + +\NewDocumentCommand \assign { m m }{ + \stex_get_symbol_in_copymodule:n {#1} + \stex_debug:nn{assign}{defining~{\l_stex_get_symbol_uri_str}~as~\detokenize{#2}} + \tl_set:cn {l__stex_features_copymodule_\l_stex_get_symbol_uri_str _def_tl}{#2} +} + +\keys_define:nn { stex / renamedecl } { + name .str_set_x:N = \l_stex_renamedecl_name_str +} +\cs_new_protected:Nn \__stex_features_renamedecl_args:n { + \str_clear:N \l_stex_renamedecl_name_str + + \keys_set:nn { stex / renamedecl } { #1 } +} + +\NewDocumentCommand \renamedecl { O{} m m}{ + \__stex_features_renamedecl_args:n { #1 } + \stex_get_symbol_in_copymodule:n {#2} + \stex_debug:nn{renamedecl}{renaming~{\l_stex_get_symbol_uri_str}~to~#3} + \str_set:cx {l__stex_features_copymodule_\l_stex_get_symbol_uri_str _macroname_str}{#3} + \str_if_empty:NTF \l_stex_renamedecl_name_str { + \tl_set:cx { #3 }{ \stex_invoke_symbol:n { + \l_stex_get_symbol_uri_str + } } + } { + \str_set:cx {l__stex_features_copymodule_\l_stex_get_symbol_uri_str _name_str}{\l_stex_renamedecl_name_str} + \stex_debug:nn{renamedecl}{@~\l_stex_current_module_str ? \l_stex_renamedecl_name_str} + \prop_set_eq:cc {l_stex_symdecl_ + \l_stex_current_module_str ? \l_stex_renamedecl_name_str + _prop + }{l_stex_symdecl_ \l_stex_get_symbol_uri_str _prop} + \seq_set_eq:cc {l_stex_symdecl_ + \l_stex_current_module_str ? \l_stex_renamedecl_name_str + _notations + }{l_stex_symdecl_ \l_stex_get_symbol_uri_str _notations} + \prop_put:cnx {l_stex_symdecl_ + \l_stex_current_module_str ? \l_stex_renamedecl_name_str + _prop + }{ name }{ \l_stex_renamedecl_name_str } + \prop_put:cnx {l_stex_symdecl_ + \l_stex_current_module_str ? \l_stex_renamedecl_name_str + _prop + }{ module }{ \l_stex_current_module_str } + \exp_args:NNx \seq_put_left:Nn \l__stex_features_copymodule_fields_seq { + \l_stex_current_module_str ? \l_stex_renamedecl_name_str + } + \tl_set:cx { #3 }{ \stex_invoke_symbol:n { + \l_stex_current_module_str ? \l_stex_renamedecl_name_str + } } + } +} + +\stex_deactivate_macro:Nn \assign {copymodules} +\stex_deactivate_macro:Nn \renamedecl {copymodules} +\stex_deactivate_macro:Nn \donotcopy {copymodules} + +\seq_new:N \l_stex_implicit_morphisms_seq +\NewDocumentCommand \implicitmorphism { O{} m m}{ + \stex_import_module_uri:nn { #1 } { #2 } + \stex_debug:nn{implicits}{ + Implicit~morphism:~ + \l_stex_module_ns_str ? \l__stex_features_name_str + } + \exp_args:NNx \seq_if_in:NnT \l_stex_all_modules_seq { + \l_stex_module_ns_str ? \l__stex_features_name_str + }{ + \msg_error:nnn{stex}{error/conflictingmodules}{ + \l_stex_module_ns_str ? \l__stex_features_name_str + } + } + + % TODO + + \seq_put_right:Nx \l_stex_implicit_morphisms_seq { + \l_stex_module_ns_str ? \l__stex_features_name_str + } +} + + +\NewDocumentEnvironment{structural@feature}{ m m m }{ + \stex_if_in_module:F { + \msg_set:nnn{stex}{error/nomodule}{ + Structural~Feature~has~to~occur~in~a~module:\\ + Feature~#2~of~type~#1\\ + In~File:~\stex_path_to_string:N \g_stex_currentfile_seq + } + \msg_error:nn{stex}{error/nomodule} + } + + \str_set:Nx \l_stex_module_name_str { + \prop_item:Nn \l_stex_current_module_prop + { name } / #2 - feature + } + + \str_set:Nx \l_stex_module_ns_str { + \prop_item:Nn \l_stex_current_module_prop + { ns } + } + + \str_clear:N \l_tmpa_str + \seq_clear:N \l_tmpa_seq + \tl_clear:N \l_tmpa_tl + \exp_args:NNx \prop_set_from_keyval:Nn \l_stex_current_module_prop { + origname = #2, + name = \l_stex_module_name_str , + ns = \l_stex_module_ns_str , + imports = \exp_not:o { \l_tmpa_seq } , + constants = \exp_not:o { \l_tmpa_seq } , + content = \exp_not:o { \l_tmpa_tl } , + file = \exp_not:o { \g_stex_currentfile_seq } , + lang = \l_stex_module_lang_str , + sig = \l_tmpa_str , + meta = \l_tmpa_str , + feature = #1 , + } + + \stex_if_smsmode:F { + \begin{stex_annotate_env}{ feature:#1 }{} + \stex_annotate_invisible:nnn{header}{}{ #3 } + } +}{ + \str_set:Nx \l_tmpa_str { + c_stex_feature_ + \prop_item:Nn \l_stex_current_module_prop { ns } ? + \prop_item:Nn \l_stex_current_module_prop { name } + _prop + } + \prop_gset_eq:cN { \l_tmpa_str } \l_stex_current_module_prop + \prop_gset_eq:NN \g_stex_last_feature_prop \l_stex_current_module_prop + \stex_if_smsmode:F { + \end{stex_annotate_env} + } +} + + +\prop_new:N \l_stex_all_structures_prop + +\keys_define:nn { stex / features / structure } { + name .str_set_x:N = \l__stex_features_structure_name_str , +} + +\cs_new_protected:Nn \__stex_features_structure_args:n { + \str_clear:N \l__stex_features_structure_name_str + \keys_set:nn { stex / features / structure } { #1 } +} + +\NewDocumentEnvironment{mathstructure}{ O{} m }{ + \__stex_features_structure_args:n { #1 } + \str_if_empty:NT \l__stex_features_structure_name_str { + \str_set:Nx \l__stex_features_structure_name_str { #2 } + } + \exp_args:Nnnx + \begin{structural@feature}{ structure } + { \l__stex_features_structure_name_str }{} + \seq_clear:N \l_tmpa_seq + \prop_put:Nno \l_stex_current_module_prop { fields } \l_tmpa_seq + \stex_smsmode_do: +}{ + \prop_get:NnN \l_stex_current_module_prop { constants } \l_tmpa_seq + \prop_get:NnN \l_stex_current_module_prop { fields } \l_tmpb_seq + \str_set:Nx \l_tmpa_str { + \prop_item:Nn \l_stex_current_module_prop { ns } ? + \prop_item:Nn \l_stex_current_module_prop { name } + } + \seq_map_inline:Nn \l_tmpa_seq { + \exp_args:NNx \seq_put_right:Nn \l_tmpb_seq { \l_tmpa_str ? ##1 } + } + \prop_put:Nno \l_stex_current_module_prop { fields } { \l_tmpb_seq } + \exp_args:Nnx + \AddToHookNext { env / mathstructure / after }{ + \symdecl{ #2 }[type = \exp_not:N\collection,def={\STEXsymbol{module-type}{ + \_stex_term_math_oms:nnnn { \l_tmpa_str }{}{0}{} + }}, name = \prop_item:Nn \l_stex_current_module_prop { origname }] + \STEXexport { + \prop_put:Nno \exp_not:N \l_stex_all_structures_prop + {\prop_item:Nn \l_stex_current_module_prop { origname }} + {\l_tmpa_str} + \prop_put:Nno \exp_not:N \l_stex_all_structures_prop + {#2}{\l_tmpa_str} + } + } + + \end{structural@feature} + % \g_stex_last_feature_prop +} +\seq_new:N \l__stex_features_structure_field_seq +\str_new:N \l__stex_features_structure_field_str +\str_new:N \l__stex_features_structure_def_tl +\prop_new:N \l__stex_features_structure_prop +\NewDocumentCommand \instantiate { m O{} m }{ + \prop_get:NnN \l_stex_all_structures_prop {#1} \l_tmpa_str + \prop_set_eq:Nc \l__stex_features_structure_prop { + c_stex_feature_\l_tmpa_str _prop + } + \seq_set_from_clist:Nn \l__stex_features_structure_field_seq { #2 } + \seq_map_inline:Nn \l__stex_features_structure_field_seq { + \seq_set_split:Nnn \l_tmpa_seq{=}{ ##1 } + \int_compare:nNnTF {\seq_count:N \l_tmpa_seq} > 1 { + \seq_get_left:NN \l_tmpa_seq \l_tmpa_tl + \exp_args:NNno \seq_set_split:Nnn \l_tmpb_seq + {!} \l_tmpa_tl + \int_compare:nNnTF {\seq_count:N \l_tmpb_seq} > 1 { + \str_set:Nx \l__stex_features_structure_field_str {\seq_item:Nn \l_tmpb_seq 1} + \seq_get_right:NN \l_tmpb_seq \l_tmpb_tl + \seq_get_right:NN \l_tmpa_seq \l_tmpa_tl + }{ + \str_set:Nx \l__stex_features_structure_field_str \l_tmpa_tl + \seq_get_right:NN \l_tmpa_seq \l_tmpa_tl + \exp_args:NNno \seq_set_split:Nnn \l_tmpb_seq{!} + \l_tmpa_tl + \int_compare:nNnTF {\seq_count:N \l_tmpb_seq} > 1 { + \seq_get_left:NN \l_tmpb_seq \l_tmpa_tl + \seq_get_right:NN \l_tmpb_seq \l_tmpb_tl + }{ + \tl_clear:N \l_tmpb_tl + } + } + }{ + \seq_set_split:Nnn \l_tmpa_seq{!}{ ##1 } + \int_compare:nNnTF {\seq_count:N \l_tmpa_seq} > 1 { + \str_set:Nx \l__stex_features_structure_field_str {\seq_item:Nn \l_tmpa_seq 1} + \seq_get_right:NN \l_tmpa_seq \l_tmpb_tl + \tl_clear:N \l_tmpa_tl + }{ + % TODO throw error + } + } + % \l_tmpa_str: name + % \l_tmpa_tl: definiens + % \l_tmpb_tl: notation + \tl_if_empty:NT \l__stex_features_structure_field_str { + % TODO throw error + } + \str_clear:N \l_tmpb_str + + \prop_get:NnN \l__stex_features_structure_prop { fields } \l_tmpa_seq + \seq_map_inline:Nn \l_tmpa_seq { + \seq_set_split:Nnn \l_tmpb_seq ? { ####1 } + \seq_get_right:NN \l_tmpb_seq \l_tmpb_str + \str_if_eq:NNT \l__stex_features_structure_field_str \l_tmpb_str { + \seq_map_break:n { + \str_set:Nn \l_tmpb_str { ####1 } + } + } + } + \prop_get:cnN { l_stex_symdecl_ \l_tmpb_str _prop } {args} + \l_tmpb_str + + \tl_if_empty:NTF \l_tmpb_tl { + \tl_if_empty:NF \l_tmpa_tl { + \exp_args:Nx \use:n { + \symdecl{#3/\l__stex_features_structure_field_str}[args=\l_tmpb_str,def={\exp_args:No\exp_not:n{\l_tmpa_tl}}] + } + } + }{ + \tl_if_empty:NTF \l_tmpa_tl { + \exp_args:Nx \use:n { + \symdef{#3/\l__stex_features_structure_field_str}[args=\l_tmpb_str]\exp_after:wN\exp_not:n\exp_after:wN{\l_tmpb_tl} + } + + }{ + \exp_args:Nx \use:n { + \symdef{#3/\l__stex_features_structure_field_str}[args=\l_tmpb_str,def={\exp_args:No\exp_not:n{\l_tmpa_tl}}] + \exp_after:wN\exp_not:n\exp_after:wN{\l_tmpb_tl} + } + } + } + } + + \tl_clear:N \l__stex_features_structure_def_tl + + \prop_get:NnN \l__stex_features_structure_prop { fields } \l_tmpa_seq + \seq_map_inline:Nn \l_tmpa_seq { + \seq_set_split:Nnn \l_tmpb_seq ? { ##1 } + \seq_get_right:NN \l_tmpb_seq \l_tmpa_str + \exp_args:Nx \use:n { + \tl_put_right:Nn \exp_not:N \l__stex_features_structure_def_tl { + + } + } + + \prop_if_exist:cF { + l_stex_symdecl_ + \prop_item:Nn \l_stex_current_module_prop {ns} ? + \prop_item:Nn \l_stex_current_module_prop {name} ? + #3/\l_tmpa_str + _prop + }{ + \prop_get:cnN { l_stex_symdecl_ ##1 _prop } {args} + \l_tmpb_str + \exp_args:Nx \use:n { + \symdecl{#3/\l_tmpa_str}[args=\l_tmpb_str] + } + } + } + + \symdecl*{#3}[type={\STEXsymbol{module-type}{ + \_stex_term_math_oms:nnnn { + \prop_item:Nn \l__stex_features_structure_prop {ns} ? + \prop_item:Nn \l__stex_features_structure_prop {name} + }{}{0}{} + }}] + + % TODO: -> sms file + + \tl_set:cx{ #3 }{ + \stex_invoke_structure:nnn { + \prop_item:Nn \l_stex_current_module_prop {ns} ? + \prop_item:Nn \l_stex_current_module_prop {name} ? #3 + } { + \prop_item:Nn \l__stex_features_structure_prop {ns} ? + \prop_item:Nn \l__stex_features_structure_prop {name} + } + } + \stex_smsmode_do: +} +\cs_new_protected:Nn \stex_invoke_structure:nnn { + \tl_if_empty:nTF{ #3 }{ + \prop_set_eq:Nc \l__stex_features_structure_prop { + c_stex_feature_ #2 _prop + } + \tl_clear:N \l_tmpa_tl + \prop_get:NnN \l__stex_features_structure_prop { fields } \l_tmpa_seq + \seq_map_inline:Nn \l_tmpa_seq { + \seq_set_split:Nnn \l_tmpb_seq ? { ##1 } + \seq_get_right:NN \l_tmpb_seq \l_tmpa_str + \cs_if_exist:cT { + stex_notation_ #1/\l_tmpa_str \c_hash_str\c_hash_str _cs + }{ + \tl_if_empty:NF \l_tmpa_tl { + \tl_put_right:Nn \l_tmpa_tl {,} + } + \tl_put_right:Nx \l_tmpa_tl { + \stex_invoke_symbol:n {#1/\l_tmpa_str}! + } + } + } + \exp_args:No \mathstruct \l_tmpa_tl + }{ + \stex_invoke_symbol:n{#1/#3} + } +} + +%%%%%%%%%%%%% features.dtx %%%%%%%%%%%%% + + +\def\titleemph#1{\textbf{#1}} +\keys_define:nn {stex / definiendum }{ + pre .tl_set:N = \l__stex_statements_definiendum_pre_tl, + post .tl_set:N = \l__stex_statements_definiendum_post_tl, + root .str_set_x:N = \l__stex_statements_definiendum_root_str, + gfa .str_set_x:N = \l__stex_statements_definiendum_gfa_str +} +\cs_new_protected:Nn \__stex_statements_definiendum_args:n { + \str_clear:N \l__stex_statements_definiendum_root_str + \tl_clear:N \l__stex_statements_definiendum_post_tl + \str_clear:N \l__stex_statements_definiendum_gfa_str + \keys_set:nn { stex / definiendum }{ #1 } +} +\NewDocumentCommand \definiendum { O{} m m} { + \__stex_statements_definiendum_args:n { #1 } + \stex_get_symbol:n { #2 } + \stex_ref_new_sym_target:n \l_stex_get_symbol_uri_str + \str_if_empty:NTF \l__stex_statements_definiendum_root_str { + \tl_if_empty:NTF \l__stex_statements_definiendum_post_tl { + \tl_set:Nn \l_tmpa_tl { #3 } + } { + \str_set:Nx \l__stex_statements_definiendum_root_str { #3 } + \tl_set:Nn \l_tmpa_tl { + \l__stex_statements_definiendum_pre_tl\l__stex_statements_definiendum_root_str\l__stex_statements_definiendum_post_tl + } + } + } { + \tl_set:Nn \l_tmpa_tl { #3 } + } + + % TODO root + \rustex_if:TF { + \stex_annotate:nnn { definiendum } { \l_stex_get_symbol_uri_str } { \l_tmpa_tl } + } { + \exp_args:Nnx \defemph@uri { \l_tmpa_tl } { \l_stex_get_symbol_uri_str } + } +} +\stex_deactivate_macro:Nn \definiendum {definition~environments} + +\NewDocumentCommand \definame { O{} m } { + \__stex_statements_definiendum_args:n { #1 } + % TODO: root + \stex_get_symbol:n { #2 } + \stex_ref_new_sym_target:n \l_stex_get_symbol_uri_str + \str_set:Nx \l_tmpa_str { + \prop_item:cn { l_stex_symdecl_ \l_stex_get_symbol_uri_str _prop } { name } + } + \exp_args:NNno \str_replace_all:Nnn \l_tmpa_str {-} {~} + \rustex_if:TF { + \stex_annotate:nnn { definiendum } { \l_stex_get_symbol_uri_str } { + \l_tmpa_str\l__stex_statements_definiendum_post_tl + } + } { + \defemph@uri { + \l_tmpa_str\l__stex_statements_definiendum_post_tl + } { \l_stex_get_symbol_uri_str } + } +} +\stex_deactivate_macro:Nn \definame {definition~environments} + +\NewDocumentCommand \Definame { O{} m } { + \__stex_statements_definiendum_args:n { #1 } + \stex_get_symbol:n { #2 } + \str_set:Nx \l_tmpa_str { + \prop_item:cn { l_stex_symdecl_ \l_stex_get_symbol_uri_str _prop } { name } + } + \exp_args:NNno \str_replace_all:Nnn \l_tmpa_str {-} {~} + \stex_ref_new_sym_target:n \l_stex_get_symbol_uri_str + \rustex_if:TF { + \stex_annotate:nnn { definiendum } { \l_stex_get_symbol_uri_str } { + \l_tmpa_str\l__stex_statements_definiendum_post_tl + } + } { + \defemph@uri { + \exp_after:wN \stex_capitalize:n \l_tmpa_str\l__stex_statements_definiendum_post_tl + } { \l_stex_get_symbol_uri_str } + } +} +\stex_deactivate_macro:Nn \Definame {definition~environments} + +\NewDocumentCommand \premise { m }{ + \stex_annotate:nnn{ premise }{}{ #1 } +} +\NewDocumentCommand \conclusion { m }{ + \stex_annotate:nnn{ conclusion }{}{ #1 } +} +\NewDocumentCommand \definiens { m }{ + \stex_annotate:nnn{ definiens }{}{ #1 } +} + +\stex_deactivate_macro:Nn \premise {definition,~example~or~assertion~environments} +\stex_deactivate_macro:Nn \conclusion {example~or~assertion~environments} +\stex_deactivate_macro:Nn \definiens {definition~environments} + + +\keys_define:nn {stex / sdefinition }{ + type .str_set_x:N = \sdefinitiontype, + id .str_set_x:N = \sdefinitionid, + name .str_set_x:N = \sdefinitionname, + for .clist_set:N = \l__stex_statements_sdefinition_for_clist , + title .tl_set:N = \sdefinitiontitle +} +\cs_new_protected:Nn \__stex_statements_sdefinition_args:n { + \str_clear:N \sdefinitiontype + \str_clear:N \sdefinitionid + \str_clear:N \sdefinitionname + \clist_clear:N \l__stex_statements_sdefinition_for_clist + \tl_clear:N \sdefinitiontitle + \keys_set:nn { stex / sdefinition }{ #1 } +} + +\NewDocumentEnvironment{sdefinition}{O{}}{ + \__stex_statements_sdefinition_args:n{ #1 } + \stex_reactivate_macro:N \definiendum + \stex_reactivate_macro:N \definame + \stex_reactivate_macro:N \Definame + \stex_reactivate_macro:N \premise + \stex_reactivate_macro:N \definiens + \stex_if_smsmode:F{ + \seq_clear:N \l_tmpa_seq + \clist_map_inline:Nn \l__stex_statements_sdefinition_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}{definition}{\seq_use:Nn \l_tmpa_seq {,}} + \str_if_empty:NF \sdefinitiontype { + \stex_annotate_invisible:nnn{type}{\sdefinitiontype}{} + } + \clist_set:No \l_tmpa_clist \sdefinitiontype + \tl_clear:N \l_tmpa_tl + \clist_map_inline:Nn \l_tmpa_clist { + \tl_if_exist:cT {__stex_statements_sdefinition_##1_start:}{ + \tl_set:Nn \l_tmpa_tl {\use:c{__stex_statements_sdefinition_##1_start:}} + } + } + \tl_if_empty:NTF \l_tmpa_tl { + \__stex_statements_sdefinition_start: + }{ + \l_tmpa_tl + } + } + \stex_ref_new_doc_target:n \sdefinitionid + \stex_smsmode_do: +}{ + \str_if_empty:NF \sdefinitionname { \stex_symdecl_do:nn{}{\sdefinitionname} } + \stex_if_smsmode:F { + \clist_set:No \l_tmpa_clist \sdefinitiontype + \tl_clear:N \l_tmpa_tl + \clist_map_inline:Nn \l_tmpa_clist { + \tl_if_exist:cT {__stex_statements_sdefinition_##1_end:}{ + \tl_set:Nn \l_tmpa_tl {\use:c{__stex_statements_sdefinition_##1_end:}} + } + } + \tl_if_empty:NTF \l_tmpa_tl { + \__stex_statements_sdefinition_end: + }{ + \l_tmpa_tl + } + \end{stex_annotate_env} + } +} +\cs_new_protected:Nn \__stex_statements_sdefinition_start: { + \par\noindent\titleemph{Definition\tl_if_empty:NF \sdefinitiontitle { + ~(\sdefinitiontitle) + }~} +} +\cs_new_protected:Nn \__stex_statements_sdefinition_end: {\par\medskip} + +\newcommand\stexpatchdefinition[3][] { + \str_set:Nx \l_tmpa_str{ #1 } + \str_if_empty:NTF \l_tmpa_str { + \tl_set:Nn \__stex_statements_sdefinition_start: { #2 } + \tl_set:Nn \__stex_statements_sdefinition_end: { #3 } + }{ + \exp_after:wN \tl_set:Nn \csname __stex_statements_sdefinition_#1_start:\endcsname{ #2 } + \exp_after:wN \tl_set:Nn \csname __stex_statements_sdefinition_#1_end:\endcsname{ #3 } + } +} +\keys_define:nn {stex / inlinedef }{ + type .str_set_x:N = \sdefinitiontype, + id .str_set_x:N = \sdefinitionid, + for .clist_set:N = \l__stex_statements_sdefinition_for_clist , + name .str_set_x:N = \sdefinitionname +} +\cs_new_protected:Nn \__stex_statements_inlinedef_args:n { + \str_clear:N \sdefinitiontype + \str_clear:N \sdefinitionid + \str_clear:N \sdefinitionname + \clist_clear:N \l__stex_statements_sdefinition_for_clist + \keys_set:nn { stex / inlinedef }{ #1 } +} +\NewDocumentCommand \inlinedef { O{} m } { + \begingroup + \__stex_statements_inlinedef_args:n{ #1 } + \stex_reactivate_macro:N \definiendum + \stex_reactivate_macro:N \definame + \stex_reactivate_macro:N \Definame + \stex_reactivate_macro:N \premise + \stex_reactivate_macro:N \definiens + \stex_ref_new_doc_target:n \sdefinitionid + \stex_if_smsmode:TF{ + \str_if_empty:NF \sdefinitionname { \stex_symdecl_do:nn{}{\sdefinitionname} } + }{ + \seq_clear:N \l_tmpa_seq + \clist_map_inline:Nn \l__stex_statements_sdefinition_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:Nnx + \stex_annotate:nnn{definition}{\seq_use:Nn \l_tmpa_seq {,}}{ + \str_if_empty:NF \sdefinitiontype { + \stex_annotate_invisible:nnn{type}{\sdefinitiontype}{} + } + #2 + \str_if_empty:NF \sdefinitionname { \stex_symdecl_do:nn{}{\sdefinitionname} } + } + } + \endgroup + \stex_smsmode_do: +} + +\keys_define:nn {stex / sassertion }{ + type .str_set_x:N = \sassertiontype, + id .str_set_x:N = \sassertionid, + title .tl_set:N = \sassertiontitle , + for .clist_set:N = \l__stex_statements_sassertion_for_clist , + name .str_set_x:N = \sassertionname +} +\cs_new_protected:Nn \__stex_statements_sassertion_args:n { + \str_clear:N \sassertiontype + \str_clear:N \sassertionid + \str_clear:N \sassertionname + \clist_clear:N \l__stex_statements_sassertion_for_clist + \tl_clear:N \sassertiontitle + \keys_set:nn { stex / sassertion }{ #1 } +} + + +\NewDocumentEnvironment{sassertion}{O{}}{ + \__stex_statements_sassertion_args:n{ #1 } + \stex_reactivate_macro:N \premise + \stex_reactivate_macro:N \conclusion + \stex_if_smsmode:F { + \seq_clear:N \l_tmpa_seq + \clist_map_inline:Nn \l__stex_statements_sassertion_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}{assertion}{\seq_use:Nn \l_tmpa_seq {,}} + \str_if_empty:NF \sassertiontype { + \stex_annotate_invisible:nnn{type}{\sassertiontype}{} + } + \clist_set:No \l_tmpa_clist \sassertiontype + \tl_clear:N \l_tmpa_tl + \clist_map_inline:Nn \l_tmpa_clist { + \tl_if_exist:cT {__stex_statements_sassertion_##1_start:}{ + \tl_set:Nn \l_tmpa_tl {\use:c{__stex_statements_sassertion_##1_start:}} + } + } + \tl_if_empty:NTF \l_tmpa_tl { + \__stex_statements_sassertion_start: + }{ + \l_tmpa_tl + } + } + \str_if_empty:NTF \sassertionid { + \str_if_empty:NF \sassertionname { + \stex_ref_new_doc_target:n {} + } + } { + \stex_ref_new_doc_target:n \sassertionid + } + \stex_smsmode_do: +}{ + \str_if_empty:NF \sassertionname { + \stex_symdecl_do:nn{}{\sassertionname} + \stex_ref_new_sym_target:n {\l_stex_current_module_str ? \sassertionname} + } + \stex_if_smsmode:F { + \clist_set:No \l_tmpa_clist \sassertiontype + \tl_clear:N \l_tmpa_tl + \clist_map_inline:Nn \l_tmpa_clist { + \tl_if_exist:cT {__stex_statements_sassertion_##1_end:}{ + \tl_set:Nn \l_tmpa_tl {\use:c{__stex_statements_sassertion_##1_end:}} + } + } + \tl_if_empty:NTF \l_tmpa_tl { + \__stex_statements_sassertion_end: + }{ + \l_tmpa_tl + } + \end{stex_annotate_env} + } +} + +\cs_new_protected:Nn \__stex_statements_sassertion_start: { + \par\noindent\titleemph{Assertion~\tl_if_empty:NF \sassertiontitle { + (\sassertiontitle) + }~} +} +\cs_new_protected:Nn \__stex_statements_sassertion_end: {\par\medskip} + +\newcommand\stexpatchassertion[3][] { + \str_set:Nx \l_tmpa_str{ #1 } + \str_if_empty:NTF \l_tmpa_str { + \tl_set:Nn \__stex_statements_sassertion_start: { #2 } + \tl_set:Nn \__stex_statements_sassertion_end: { #3 } + }{ + \exp_after:wN \tl_set:Nn \csname __stex_statements_sassertion_#1_start:\endcsname{ #2 } + \exp_after:wN \tl_set:Nn \csname __stex_statements_sassertion_#1_end:\endcsname{ #3 } + } +} +\keys_define:nn {stex / inlineass }{ + type .str_set_x:N = \sassertiontype, + id .str_set_x:N = \sassertionid, + for .clist_set:N = \l__stex_statements_sassertion_for_clist , + name .str_set_x:N = \sassertionname +} +\cs_new_protected:Nn \__stex_statements_inlineass_args:n { + \str_clear:N \sassertiontype + \str_clear:N \sassertionid + \str_clear:N \sassertionname + \clist_clear:N \l__stex_statements_sassertion_for_clist + \keys_set:nn { stex / inlineass }{ #1 } +} +\NewDocumentCommand \inlineass { O{} m } { + \begingroup + \stex_reactivate_macro:N \premise + \stex_reactivate_macro:N \conclusion + \__stex_statements_inlineass_args:n{ #1 } + \str_if_empty:NTF \sassertionid { + \str_if_empty:NF \sassertionname { + \stex_ref_new_doc_target:n {} + } + } { + \stex_ref_new_doc_target:n \sassertionid + } + + \stex_if_smsmode:TF{ + \str_if_empty:NF \sassertionname { + \stex_symdecl_do:nn{}{\sassertionname} + \stex_ref_new_sym_target:n {\l_stex_current_module_str ? \sassertionname} + } + }{ + \seq_clear:N \l_tmpa_seq + \clist_map_inline:Nn \l__stex_statements_sassertion_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:Nnx + \stex_annotate:nnn{assertion}{\seq_use:Nn \l_tmpa_seq {,}}{ + \str_if_empty:NF \sassertiontype { + \stex_annotate_invisible:nnn{type}{\sassertiontype}{} + } + #2 + \str_if_empty:NF \sassertionname { + \stex_symdecl_do:nn{}{\sassertionname} + \stex_ref_new_sym_target:n {\l_stex_current_module_str ? \sassertionname} + } + } + } + \endgroup + \stex_smsmode_do: +} + +\keys_define:nn {stex / sexample }{ + type .str_set_x:N = \exampletype, + id .str_set_x:N = \sexampleid, + title .tl_set:N = \sexampletitle, + for .clist_set:N = \l__stex_statements_sexample_for_clist, +} +\cs_new_protected:Nn \__stex_statements_sexample_args:n { + \str_clear:N \sexampletype + \str_clear:N \sexampleid + \tl_clear:N \sexampletitle + \clist_clear:N \l__stex_statements_sexample_for_clist + \keys_set:nn { stex / sexample }{ #1 } +} + +\NewDocumentEnvironment{sexample}{O{}}{ + \__stex_statements_sexample_args:n{ #1 } + \stex_reactivate_macro:N \premise + \stex_reactivate_macro:N \conclusion + \stex_if_smsmode:F { + \seq_clear:N \l_tmpa_seq + \clist_map_inline:Nn \l__stex_statements_sexample_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}{example}{\seq_use:Nn \l_tmpa_seq {,}} + \str_if_empty:NF \sexampletype { + \stex_annotate_invisible:nnn{type}{\sexampletype}{} + } + \clist_set:No \l_tmpa_clist \sexampletype + \tl_clear:N \l_tmpa_tl + \clist_map_inline:Nn \l_tmpa_clist { + \tl_if_exist:cT {__stex_statements_sexample_##1_start:}{ + \tl_set:Nn \l_tmpa_tl {\use:c{__stex_statements_sexample_##1_start:}} + } + } + \tl_if_empty:NTF \l_tmpa_tl { + \__stex_statements_sexample_start: + }{ + \l_tmpa_tl + } + } + \str_if_empty:NF \sexampleid { + \stex_ref_new_doc_target:n \sexampleid + } + \stex_smsmode_do: +}{ + \str_if_empty:NF \sexamplename { \stex_symdecl_do:nn{}{\sexamplename} } + \stex_if_smsmode:F { + \clist_set:No \l_tmpa_clist \sexampletype + \tl_clear:N \l_tmpa_tl + \clist_map_inline:Nn \l_tmpa_clist { + \tl_if_exist:cT {__stex_statements_sexample_##1_end:}{ + \tl_set:Nn \l_tmpa_tl {\use:c{__stex_statements_sexample_##1_end:}} + } + } + \tl_if_empty:NTF \l_tmpa_tl { + \__stex_statements_sexample_end: + }{ + \l_tmpa_tl + } + \end{stex_annotate_env} + } +} + +\cs_new_protected:Nn \__stex_statements_sexample_start: { + \par\noindent\titleemph{Example~\tl_if_empty:NF \sexampletitle { + (\sexampletitle) + }~} +} +\cs_new_protected:Nn \__stex_statements_sexample_end: {\par\medskip} + +\newcommand\stexpatchexample[3][] { + \str_set:Nx \l_tmpa_str{ #1 } + \str_if_empty:NTF \l_tmpa_str { + \tl_set:Nn \__stex_statements_sexample_start: { #2 } + \tl_set:Nn \__stex_statements_sexample_end: { #3 } + }{ + \exp_after:wN \tl_set:Nn \csname __stex_statements_sexample_#1_start:\endcsname{ #2 } + \exp_after:wN \tl_set:Nn \csname __stex_statements_sexample_#1_end:\endcsname{ #3 } + } +} +\keys_define:nn {stex / inlineex }{ + type .str_set_x:N = \sexampletype, + id .str_set_x:N = \sexampleid, + for .clist_set:N = \l__stex_statements_sexample_for_clist , + name .str_set_x:N = \sexamplename +} +\cs_new_protected:Nn \__stex_statements_inlineex_args:n { + \str_clear:N \sexampletype + \str_clear:N \sexampleid + \str_clear:N \sexamplename + \clist_clear:N \l__stex_statements_sexample_for_clist + \keys_set:nn { stex / inlineex }{ #1 } +} +\NewDocumentCommand \inlineex { O{} m } { + \begingroup + \stex_reactivate_macro:N \premise + \stex_reactivate_macro:N \conclusion + \__stex_statements_inlineex_args:n{ #1 } + \str_if_empty:NF \sexampleid { + \stex_ref_new_doc_target:n \sexampleid + } + \stex_if_smsmode:TF{ + \str_if_empty:NF \sexamplename { \stex_symdecl_do:nn{}{\examplename} } + }{ + \seq_clear:N \l_tmpa_seq + \clist_map_inline:Nn \l__stex_statements_sexample_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:Nnx + \stex_annotate:nnn{example}{\seq_use:Nn \l_tmpa_seq {,}}{ + \str_if_empty:NF \sexampletype { + \stex_annotate_invisible:nnn{type}{\sexampletype}{} + } + #2 + \str_if_empty:NF \sexamplename { \stex_symdecl_do:nn{}{\sexamplename} } + } + } + \endgroup + \stex_smsmode_do: +} +\keys_define:nn { stex / sparagraph} { + id .str_set_x:N = \sparagraphid , + title .tl_set:N = \l_stex_sparagraph_title_tl , + type .str_set_x:N = \sparagraphtype , + for .clist_set:N = \l__stex_statements_sparagraph_for_clist , + from .tl_set:N = \sparagraphfrom , + to .tl_set:N = \sparagraphto , + start .tl_set:N = \l_stex_sparagraph_start_tl , + name .str_set:N = \sparagraphname +} + +\cs_new_protected:Nn \stex_sparagraph_args:n { + \tl_clear:N \l_stex_sparagraph_title_tl + \tl_clear:N \sparagraphfrom + \tl_clear:N \sparagraphto + \tl_clear:N \l_stex_sparagraph_start_tl + \str_clear:N \sparagraphid + \str_clear:N \sparagraphtype + \clist_clear:N \l__stex_statements_sparagraph_for_clist + \str_clear:N \sparagraphname + \keys_set:nn { stex / sparagraph }{ #1 } +} +\newif\if@in@omtext\@in@omtextfalse + +\NewDocumentEnvironment {sparagraph} { O{} } { + \stex_sparagraph_args:n { #1 } + \tl_if_empty:NTF \l_stex_sparagraph_start_tl { + \tl_set_eq:NN \sparagraphtitle \l_stex_sparagraph_title_tl + }{ + \tl_set_eq:NN \sparagraphtitle \l_stex_sparagraph_start_tl + } + \@in@omtexttrue + \stex_if_smsmode:F { + \seq_clear:N \l_tmpa_seq + \clist_map_inline:Nn \l__stex_statements_sparagraph_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}{paragraph}{\seq_use:Nn \l_tmpa_seq {,}} + \str_if_empty:NF \sparagraphtype { + \stex_annotate_invisible:nnn{type}{\sparagraphtype}{} + } + \str_if_empty:NF \sparagraphfrom { + \stex_annotate_invisible:nnn{from}{\sparagraphfrom}{} + } + \str_if_empty:NF \sparagraphto { + \stex_annotate_invisible:nnn{to}{\sparagraphto}{} + } + \clist_set:No \l_tmpa_clist \sparagraphtype + \tl_clear:N \l_tmpa_tl + \clist_map_inline:Nn \sparagraphtype { + \tl_if_exist:cT {__stex_statements_sparagraph_##1_start:}{ + \tl_set:Nn \l_tmpa_tl {\use:c{__stex_statements_sparagraph_##1_start:}} + } + } + \tl_if_empty:NTF \l_tmpa_tl { + \__stex_statements_sparagraph_start: + }{ + \l_tmpa_tl + } + } + \clist_set:No \l_tmpa_clist \sparagraphtype + \str_if_empty:NTF \sparagraphid { + \str_if_empty:NTF \sparagraphname { + \exp_args:NNx \clist_if_in:NnT \l_tmpa_clist {\tl_to_str:n{symdoc}}{ + \stex_ref_new_doc_target:n {} + } + } { + \stex_ref_new_doc_target:n {} + } + } { + \stex_ref_new_doc_target:n \sparagraphid + } + \exp_args:NNx + \clist_if_in:NnT \l_tmpa_clist {\tl_to_str:n{symdoc}}{ + \clist_map_inline:Nn \l__stex_statements_sparagraph_for_clist { + \tl_if_empty:nF{ ##1 }{ + \stex_get_symbol:n { ##1 } + \stex_ref_new_sym_target:n \l_stex_get_symbol_uri_str + } + } + } + \stex_smsmode_do: + \ignorespacesandpars +}{ + \str_if_empty:NF \sparagraphname { + \stex_symdecl_do:nn{}{\sparagraphname} + \stex_ref_new_sym_target:n {\l_stex_current_module_str ? \sparagraphname} + } + \stex_if_smsmode:F { + \clist_set:No \l_tmpa_clist \sparagraphtype + \tl_clear:N \l_tmpa_tl + \clist_map_inline:Nn \l_tmpa_clist { + \tl_if_exist:cT {__stex_statements_sparagraph_##1_end:}{ + \tl_set:Nn \l_tmpa_tl {\use:c{__stex_statements_sparagraph_##1_end:}} + } + } + \tl_if_empty:NTF \l_tmpa_tl { + \__stex_statements_sparagraph_end: + }{ + \l_tmpa_tl + } + \end{stex_annotate_env} + } +} + +\cs_new_protected:Nn \__stex_statements_sparagraph_start: { + \par\noindent\tl_if_empty:NTF \l_stex_sparagraph_start_tl { + \tl_if_empty:NF \l_stex_sparagraph_title_tl { + \titleemph{\l_stex_sparagraph_title_tl}:~ + } + }{ + \titleemph{\l_stex_sparagraph_start_tl}~ + } +} +\cs_new_protected:Nn \__stex_statements_sparagraph_end: {\par\medskip} + +\newcommand\stexpatchparagraph[3][] { + \str_set:Nx \l_tmpa_str{ #1 } + \str_if_empty:NTF \l_tmpa_str { + \tl_set:Nn \__stex_statements_sparagraph_start: { #2 } + \tl_set:Nn \__stex_statements_sparagraph_end: { #3 } + }{ + \exp_after:wN \tl_set:Nn \csname __stex_statements_sparagraph_#1_start:\endcsname{ #2 } + \exp_after:wN \tl_set:Nn \csname __stex_statements_sparagraph_#1_end:\endcsname{ #3 } + } +} + +\keys_define:nn { stex / inlinepara} { + id .str_set_x:N = \sparagraphid , + type .str_set_x:N = \sparagraphtype , + for .clist_set:N = \l__stex_statements_sparagraph_for_clist , + from .tl_set:N = \sparagraphfrom , + to .tl_set:N = \sparagraphto , + name .str_set:N = \sparagraphname +} +\cs_new_protected:Nn \__stex_statements_inlinepara_args:n { + \tl_clear:N \sparagraphfrom + \tl_clear:N \sparagraphto + \str_clear:N \sparagraphid + \str_clear:N \sparagraphtype + \clist_clear:N \l__stex_statements_sparagraph_for_clist + \str_clear:N \sparagraphname + \keys_set:nn { stex / inlinepara }{ #1 } +} +\NewDocumentCommand \inlinepara { O{} m } { + \begingroup + \__stex_statements_inlinepara_args:n{ #1 } + \clist_set:No \l_tmpa_clist \sparagraphtype + \str_if_empty:NTF \sparagraphid { + \str_if_empty:NTF \sparagraphname { + \exp_args:NNx \clist_if_in:NnT \l_tmpa_clist {\tl_to_str:n{symdoc}}{ + \stex_ref_new_doc_target:n {} + } + } { + \stex_ref_new_doc_target:n {} + } + } { + \stex_ref_new_doc_target:n \sparagraphid + } + \stex_if_smsmode:TF{ + \str_if_empty:NF \sparagraphname { + \stex_symdecl_do:nn{}{\sparagraphname} + \stex_ref_new_sym_target:n {\l_stex_current_module_str ? \sparagraphname} + } + }{ + \seq_clear:N \l_tmpa_seq + \clist_map_inline:Nn \l__stex_statements_sparagraph_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:Nnx + \stex_annotate:nnn{paragraph}{\seq_use:Nn \l_tmpa_seq {,}}{ + \str_if_empty:NF \sparagraphtype { + \stex_annotate_invisible:nnn{type}{\sparagraphtype}{} + } + \str_if_empty:NF \sparagraphfrom { + \stex_annotate_invisible:nnn{from}{\sparagraphfrom}{} + } + \str_if_empty:NF \sparagraphto { + \stex_annotate_invisible:nnn{to}{\sparagraphto}{} + } + \str_if_empty:NF \sparagraphname { + \stex_symdecl_do:nn{}{\sparagraphname} + \stex_ref_new_sym_target:n {\l_stex_current_module_str ? \sparagraphname} + } + \exp_args:NNx \clist_if_in:NnT \l_tmpa_clist {\tl_to_str:n{symdoc}}{ + \clist_map_inline:Nn \l_tmpa_seq { + \stex_ref_new_sym_target:n {##1} + } + } + #2 + } + } + \endgroup + \stex_smsmode_do: +} + + + +%%%%%%%%%%%%% sproof.dtx %%%%%%%%%%%%% + +\keys_define:nn { stex / spf } { + id .str_set_x:N = \spfid, + for .clist_set:N = \l__stex_sproof_spf_for_clist , + from .tl_set:N = \l__stex_sproof_spf_from_tl , + proofend .tl_set:N = \l__stex_sproof_spf_proofend_tl, + type .str_set_x:N = \spftype, + 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 +} +\cs_new_protected:Nn \__stex_sproof_spf_args:n { +\str_clear:N \spfid +\tl_clear:N \l__stex_sproof_spf_for_tl +\tl_clear:N \l__stex_sproof_spf_from_tl +\tl_set:Nn \l__stex_sproof_spf_proofend_tl {\sproof@box} +\str_clear:N \spftype +\tl_clear:N \spftitle +\tl_clear:N \l__stex_sproof_spf_continues_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 +\keys_set:nn { stex / spf }{ #1 } +} +\str_set:Nn\c__stex_sproof_flow_str{inline} +\intarray_new:Nn\l__stex_sproof_counter_intarray{50} +\cs_new_protected:Npn \sproofnumber { + \int_set:Nn \l_tmpa_int {1} + \bool_while_do:nn { + \int_compare_p:nNn { + \intarray_item:Nn \l__stex_sproof_counter_intarray \l_tmpa_int + } > 0 + }{ + \intarray_item:Nn \l__stex_sproof_counter_intarray \l_tmpa_int . + \int_incr:N \l_tmpa_int + } +} +\cs_new_protected:Npn \__stex_sproof_inc_counter: { + \int_set:Nn \l_tmpa_int {1} + \bool_while_do:nn { + \int_compare_p:nNn { + \intarray_item:Nn \l__stex_sproof_counter_intarray \l_tmpa_int + } > 0 + }{ + \int_incr:N \l_tmpa_int + } + \int_compare:nNnF \l_tmpa_int = 1 { + \int_decr:N \l_tmpa_int + } + \intarray_gset:Nnn \l__stex_sproof_counter_intarray \l_tmpa_int { + \intarray_item:Nn \l__stex_sproof_counter_intarray \l_tmpa_int + 1 + } +} + +\cs_new_protected:Npn \__stex_sproof_add_counter: { + \int_set:Nn \l_tmpa_int {1} + \bool_while_do:nn { + \int_compare_p:nNn { + \intarray_item:Nn \l__stex_sproof_counter_intarray \l_tmpa_int + } > 0 + }{ + \int_incr:N \l_tmpa_int + } + \intarray_gset:Nnn \l__stex_sproof_counter_intarray \l_tmpa_int { 1 } +} + +\cs_new_protected:Npn \__stex_sproof_remove_counter: { + \int_set:Nn \l_tmpa_int {1} + \bool_while_do:nn { + \int_compare_p:nNn { + \intarray_item:Nn \l__stex_sproof_counter_intarray \l_tmpa_int + } > 0 + }{ + \int_incr:N \l_tmpa_int + } + \int_decr:N \l_tmpa_int + \intarray_gset:Nnn \l__stex_sproof_counter_intarray \l_tmpa_int { 0 } +} +\def\sproof@box{ + \hbox{\vrule\vbox{\hrule width 6 pt\vskip 6pt\hrule}\vrule} +} +\def\sproofend{ + \tl_if_empty:NF \l__stex_sproof_spf_proofend_tl { + \hfil\null\nobreak\hfill\l__stex_sproof_spf_proofend_tl\par\smallskip + } +} +\def\spf@proofsketch@kw{Proof~Sketch} +\def\spf@proof@kw{Proof} +\def\spf@step@kw{Step} +\AddToHook{begindocument}{ + \ltx@ifpackageloaded{babel}{ + \makeatletter + \clist_set:Nx \l_tmpa_clist {\bbl@loaded} + \clist_if_in:NnT \l_tmpa_clist {ngerman}{ + \input{sproof-ngerman.ldf} + } + \clist_if_in:NnT \l_tmpa_clist {finnish}{ + \input{sproof-finnish.ldf} + } + \clist_if_in:NnT \l_tmpa_clist {french}{ + \input{sproof-french.ldf} + } + \clist_if_in:NnT \l_tmpa_clist {russian}{ + \input{sproof-russian.ldf} + } + \makeatother + }{} +} +\newcommand\spfsketch[2][]{ + \begingroup + \let \premise \stex_proof_premise: + \__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:Nnx + \stex_annotate:nnn{proofsketch}{\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 { + \titleemph{ + \tl_if_empty:NTF \spftitle { + \spf@proofsketch@kw + }{ + \spftitle + } + }:~ + } + \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 + } + } + \str_if_empty:NF \spfid { + \stex_ref_new_doc_target:n \spfid + } + \l_tmpa_tl #2 \sproofend + } + } + \endgroup + \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}{} + } + + \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} + } + \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:}} + } + } + \tl_if_empty:NTF \l_tmpa_tl { + \__stex_sproof_spfeq_end: + }{ + \l_tmpa_tl + } + \end{stex_annotate_env} + } +} + +\cs_new_protected:Nn \__stex_sproof_spfeq_start: { + \titleemph{ + \tl_if_empty:NTF \spftitle { + \spf@proof@kw + }{ + \spftitle + } + }: +} +\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 } + } +} + +\newenvironment{sproof}[2][]{ + \let \premise \stex_proof_premise: + \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_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}{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 + }{~#2} + \str_if_empty:NF \spfid { + \stex_ref_new_doc_target:n \spfid + } + \begin{description} + } + \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} + } +} + +\cs_new_protected:Nn \__stex_sproof_sproof_start: { + \par\noindent\titleemph{ + \tl_if_empty:NTF \spftype { + \spf@proof@kw + }{ + \spftype + } + }: +} +\cs_new_protected:Nn \__stex_sproof_sproof_end: {\sproofend} + +\newcommand\stexpatchsproof[3][] { + \str_set:Nx \l_tmpa_str{ #1 } + \str_if_empty:NTF \l_tmpa_str { + \tl_set:Nn \__stex_sproof_sproof_start: { #2 } + \tl_set:Nn \__stex_sproof_sproof_end: { #3 } + }{ + \exp_after:wN \tl_set:Nn \csname __stex_sproof_sproof_#1_start:\endcsname{ #2 } + \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 +} +\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 + \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}{spfstep}{\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 \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} + } +} +\newenvironment{sproofcomment}[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: + } +} +\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}{} + } + + \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} + } +} +\newenvironment{spfcases}[2][]{ + \tl_if_empty:nTF{#1}{ + \begin{subproof}[method=by-cases]{#2} + }{ + \begin{subproof}[#1,method=by-cases]{#2} + } +}{ + \end{subproof} +} +\newenvironment{spfcase}[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}{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} +} +\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 +} +\newenvironment{justification}[1][]{}{} +\newcommand\stex_proof_premise:[2][]{#2} +\newcommand\justarg[2][]{#2} + +%%%%%%%%%%%%% others.dtx %%%%%%%%%%%%% + + % None +\NewDocumentCommand \MSC {m} { + % TODO +} +\@ifpackageloaded{tikzinput}{ + \RequirePackage{stex-tikzinput} +}{} + +%%%%%%%%%%%%% metatheory.dtx %%%%%%%%%%%%% + +\str_const:Nn \c_stex_metatheory_ns_str {http://mathhub.info/sTeX} +\begingroup +\stex_module_setup:nn{ + ns=\c_stex_metatheory_ns_str, + meta=NONE +}{Metatheory} +\stex_reactivate_macro:N \symdecl +\stex_reactivate_macro:N \notation +\stex_reactivate_macro:N \symdef +\ExplSyntaxOff +\csname stex_suppress_html:n\endcsname{ + % is-a (a:A, a \in A, a is an A, etc.) + \symdecl{isa}[args=ai] + \notation{isa}[typed]{#1 \comp{:} #2}{##1 \comp, ##2} + \notation{isa}[in]{#1 \comp\in #2}{##1 \comp, ##2} + \notation{isa}[pred]{#2\comp(#1 \comp)}{##1 \comp, ##2} + + % bind (\forall, \Pi, \lambda etc.) + \symdecl{bind}[args=Bi] + \notation{bind}[forall]{\comp\forall #1.\;#2}{##1 \comp, ##2} + \notation{bind}[Pi]{\comp\prod_{#1}#2}{##1 \comp, ##2} + \notation{bind}[depfun]{\comp( #1 \comp{)\;\to\;} #2}{##1 \comp, ##2} + + % dummy variable + \symdecl{dummyvar} + \notation{dummyvar}[underscore]{\comp\_} + \notation{dummyvar}[dot]{\comp\cdot} + \notation{dummyvar}[dash]{\comp{{\rm --}}} + + %fromto (function space, Hom-set, implication etc.) + \symdecl{fromto}[args=ai] + \notation{fromto}[xarrow]{#1 \comp\to #2}{##1 \comp\times ##2} + \notation{fromto}[arrow]{#1 \comp\to #2}{##1 \comp\to ##2} + + % mapto (lambda etc.) + %\symdecl{mapto}[args=Bi] + %\notation{mapto}[mapsto]{#1 \comp\mapsto #2}{#1 \comp, #2} + %\notation{mapto}[lambda]{\comp\lambda #1 \comp.\; #2}{#1 \comp, #2} + %\notation{mapto}[lambdau]{\comp\lambda_{#1} \comp.\; #2}{#1 \comp, #2} + + % function/operator application + \symdecl{apply}[args=ia] + \notation{apply}[prec=0;0x\infprec,parens]{#1 \comp( #2 \comp)}{##1 \comp, ##2} + \notation{apply}[prec=0;0x\infprec,lambda]{#1 \; #2 }{##1 \; ##2} + + % ``type'' of all collections (sets,classes,types,kinds) + \symdecl{collection} + \notation{collection}[U]{\comp{\mathcal{U}}} + \notation{collection}[set]{\comp{\textsf{Set}}} + + % collection of propositions/booleans/truth values + \symdecl{prop}[name=proposition] + \notation{prop}[prop]{\comp{{\rm prop}}} + \notation{prop}[BOOL]{\comp{{\rm BOOL}}} + + % sequences + \symdecl{seqtype}[args=1] + \notation{seqtype}[kleene]{#1^{\comp\ast}} + + \symdef{sequence-index}[args=2,li,prec=nobrackets]{{#1}_{#2}} + \notation{sequence-index}[ui,prec=nobrackets]{{#1}^{#2}} + + \symdef{aseqdots}[args=a,prec=nobrackets]{#1\comp{,\ellipses}}{##1\comp,##2} + \symdef{aseqfromto}[args=ai,prec=nobrackets]{#1\comp{,\ellipses,}#2}{##1\comp,##2} + \symdef{aseqfromtovia}[args=aii,prec=nobrackets]{#1\comp{,\ellipses,}#2\comp{,\ellipses,}#3}{##1\comp,##2} + + % letin (``let'', local definitions, variable substitution) + \symdecl{letin}[args=bii] + \notation{letin}[let]{\comp{{\rm let}}\;#1\comp{=}#2\;\comp{{\rm in}}\;#3} + \notation{letin}[subst]{#3 \comp[ #1 \comp/ #2 \comp]} + \notation{letin}[frac]{#3 \comp[ \frac{#2}{#1} \comp]} + + % structures + \symdecl*{module-type}[args=1] + \notation{module-type}{\mathtt{MOD} #1} + \symdecl{mathstruct}[name=mathematical-structure,args=a] % TODO + \notation{mathstruct}[angle,prec=nobrackets]{\comp\langle #1 \comp\rangle}{##1 \comp, ##2} + +} + \ExplSyntaxOn + \stex_add_to_current_module:n{ + \let\nappa\apply + \def\nappli#1#2#3#4{\apply{#1}{\naseqli{#2}{#3}{#4}}} + \def\nappui#1#2#3#4{\apply{#1}{\nasequi{#2}{#3}{#4}}} + \def\livar{\csname sequence-index\endcsname[li]} + \def\uivar{\csname sequence-index\endcsname[ui]} + \def\naseqli#1#2#3{\aseqfromto{\livar{#1}{#2}}{\livar{#1}{#3}}} + \def\nasequi#1#2#3{\aseqfromto{\uivar{#1}{#2}}{\uivar{#1}{#3}}} + \def\nappe#1#2#3{\apply{#1}{\aseqfromto{#2}{#3}}} + } +\__stex_modules_end_module: +\endgroup + +\endinput +%% +%% End of file `stex.sty'. |