%% %% 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-metatheory.dtx (with options: `package') %% stex-others.dtx (with options: `package') %% %%%%%%%%%%%%% basics.dtx %%%%%%%%%%%%% \RequirePackage{expl3,l3keys2e,ltxcmds} \ProvidesExplPackage{stex}{2022/05/24}{3.1.0}{sTeX package} \bool_if_exist:NF \c_stex_document_class_bool { \bool_set_false:N \c_stex_document_class_bool \RequirePackage{standalone} } \message{^^J*~This~is~sTeX~version~3.1.0~*^^J} \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 , usesms .bool_set:N = \c_stex_persist_mode_bool , writesms .bool_set:N = \c_stex_persist_write_mode_bool , image .bool_set:N = \c_tikzinput_image_bool, unknown .code:n = {} } \ProcessKeysOptions { stex } \RequirePackage{stex-logo} % externalized for backwards-compatibility reasons \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 } { \msg_set:nnn{stex}{debug / #1}{ \\Debug~#1:~#2\\ } \msg_none:nn{stex}{debug / #1} }{ \clist_if_in:NnT \c_stex_debug_clist { #1 } { \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} \tl_new:N \l_stex_html_arg_tl \cs_new_protected:Nn \_stex_html_checkempty:n { \tl_set:Nn \l_stex_html_arg_tl { #1 } \tl_if_empty:NT \l_stex_html_arg_tl { \tl_set_eq:NN \l_stex_html_arg_tl \c_stex_html_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 } } } \tl_if_exist:NF\stex@backend{ \ifcsname if@rustex\endcsname \def\stex@backend{rustex} \else \ifcsname if@latexml\endcsname \def\stex@backend{latexml} \else \def\stex@backend{pdflatex} \fi \fi } \input{stex-backend-\stex@backend.cfg} \newif\ifstexhtml \stex_html_backend:TF\stexhtmltrue\stexhtmlfalse \exp_args:NNx \prop_const_from_keyval:Nn \c_stex_languages_prop { \tl_to_str:n { en = english , de = ngerman , ar = arabic , bg = bulgarian , ru = russian , fi = finnish , ro = romanian , tr = turkish , fr = french }} \exp_args:NNx \prop_const_from_keyval:Nn \c_stex_language_abbrevs_prop { \tl_to_str:n { english = en , ngerman = de , arabic = ar , bulgarian = bg , russian = ru , finnish = fi , romanian = ro , turkish = tr , french = fr }} \cs_new_protected:Nn \stex_set_language:Nn { \str_set:Nx \l_tmpa_str {#2} \prop_get:NoNT \c_stex_languages_prop \l_tmpa_str #1 { \ifx\@onlypreamble\@notprerr \ltx@ifpackageloaded{babel}{ \exp_args:No \selectlanguage #1 }{} \else \exp_args:No \str_if_eq:nnTF #1 {turkish} { \RequirePackage[#1,shorthands=:!]{babel} }{ \RequirePackage[#1]{babel} } \fi } } \clist_if_empty:NF \c_stex_languages_clist { \bool_set_false:N \l_tmpa_bool \clist_clear:N \l_tmpa_clist \clist_map_inline:Nn \c_stex_languages_clist { \str_set:Nx \l_tmpa_str {#1} \str_if_eq:nnT {#1}{tr}{ \bool_set_true:N \l_tmpa_bool } \prop_get:NoNTF \c_stex_languages_prop \l_tmpa_str \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 {,~} } \bool_if:NTF \l_tmpa_bool { \RequirePackage[\clist_use:Nn \l_tmpa_clist,,shorthands=:!]{babel} }{ \RequirePackage[\clist_use:Nn \l_tmpa_clist,]{babel} } } \AtBeginDocument{ \stex_html_backend:T { \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 % \seq_if_empty:NF \l_tmpa_seq { %remaining element should be language \seq_pop_right:NN \l_tmpa_seq \l_tmpa_str \stex_debug:nn{basics} {Language~\l_tmpa_str~ inferred~from~file~name} \stex_annotate_invisible:nnn{language}{ \l_tmpa_str }{} } } } \bool_if:NTF \c_stex_persist_mode_bool { \def \stex_persist:n #1 {} \def \stex_persist:x #1 {} }{ \bool_if:NTF \c_stex_persist_write_mode_bool { \iow_new:N \c__stex_persist_iow \iow_open:Nn \c__stex_persist_iow{\jobname.sms} \AtEndDocument{ \iow_close:N \c__stex_persist_iow } \cs_new_protected:Nn \stex_persist:n { \tl_set:Nn \l_tmpa_tl { #1 } \regex_replace_all:nnN { \cP\# } { \cO\# } \l_tmpa_tl \regex_replace_all:nnN { \ } { \~ } \l_tmpa_tl \exp_args:NNo \iow_now:Nn \c__stex_persist_iow \l_tmpa_tl } \cs_generate_variant:Nn \stex_persist:n {x} }{ \def \stex_persist:n #1 {} \def \stex_persist:x #1 {} } } \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}{\detokenize{#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 } } \cs_new_protected:Nn \stex_copy_control_sequence:NNN { \tl_set:Nx \_tmp_args_tl {\cs_argument_spec:N #2} \exp_args:NNo \tl_remove_all:Nn \_tmp_args_tl \c_hash_str \int_set:Nn \l_tmpa_int {\tl_count:N \_tmp_args_tl} \tl_clear:N \_tmp_args_tl \int_step_inline:nn \l_tmpa_int { \tl_put_right:Nx \_tmp_args_tl {{\exp_not:n{####}\exp_not:n{##1}}} } \tl_set:Nn #3 {\cs_generate_from_arg_count:NNnn #1 \cs_set:Npn} \tl_put_right:Nx #3 { {\int_use:N \l_tmpa_int}{ \exp_after:wN\exp_after:wN\exp_after:wN \exp_not:n \exp_after:wN\exp_after:wN\exp_after:wN { \exp_after:wN #2 \_tmp_args_tl } }} } \cs_generate_variant:Nn \stex_copy_control_sequence:NNN {cNN} \cs_generate_variant:Nn \stex_copy_control_sequence:NNN {NcN} \cs_generate_variant:Nn \stex_copy_control_sequence:NNN {ccN} \cs_new_protected:Nn \stex_copy_control_sequence_ii:NNN { \tl_set:Nx \_tmp_args_tl {\cs_argument_spec:N #2} \exp_args:NNo \tl_remove_all:Nn \_tmp_args_tl \c_hash_str \int_set:Nn \l_tmpa_int {\tl_count:N \_tmp_args_tl} \tl_clear:N \_tmp_args_tl \int_step_inline:nn \l_tmpa_int { \tl_put_right:Nx \_tmp_args_tl {{\exp_not:n{########}\exp_not:n{##1}}} } \edef \_tmp_args_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 #2 \_tmp_args_tl } } \exp_after:wN \def \exp_after:wN \_tmp_args_tl \exp_after:wN ##\exp_after:wN 1 \exp_after:wN ##\exp_after:wN 2 \exp_after:wN { \_tmp_args_tl } \edef \_tmp_args_tl { \exp_after:wN \exp_not:n \exp_after:wN { \_tmp_args_tl {####1}{####2} } } \tl_set:Nn #3 {\cs_generate_from_arg_count:NNnn #1 \cs_set:Npn} \tl_put_right:Nx #3 { {\int_use:N \l_tmpa_int}{ \exp_after:wN\exp_not:n\exp_after:wN{\_tmp_args_tl} }} } \cs_generate_variant:Nn \stex_copy_control_sequence_ii:NNN {cNN} \cs_generate_variant:Nn \stex_copy_control_sequence_ii:NNN {NcN} \cs_generate_variant:Nn \stex_copy_control_sequence_ii:NNN {ccN} \NewDocumentCommand \MMTrule {m m}{ \seq_set_split:Nnn \l_tmpa_seq , {#2} \int_zero:N \l_tmpa_int \stex_annotate_invisible:nnn{mmtrule}{scala://#1}{ \seq_if_empty:NF \l_tmpa_seq { $\seq_map_inline:Nn \l_tmpa_seq { \int_incr:N \l_tmpa_int \stex_annotate:nnn{arg}{i\int_use:N \l_tmpa_int}{##1} }$ } } } \NewDocumentCommand \MMTinclude {m}{ \stex_annotate_invisible:nnn{import}{#1}{} } \tl_new:N \g_stex_document_title \cs_new_protected:Npn \STEXtitle #1 { \tl_if_empty:NT \g_stex_document_title { \tl_gset:Nn \g_stex_document_title { #1 } } } \cs_new_protected:Nn \stex_document_title:n { \tl_if_empty:NT \g_stex_document_title { \tl_gset:Nn \g_stex_document_title { #1 } \stex_annotate_invisible:n{\noindent \stex_annotate:nnn{doctitle}{}{ #1 } \par} } } \AtBeginDocument { \let \STEXtitle \stex_document_title:n \tl_if_empty:NF \g_stex_document_title { \stex_annotate_invisible:n{\noindent \stex_annotate:nnn{doctitle}{}{ \g_stex_document_title } \par} } \let\_stex_maketitle:\maketitle \def\maketitle{ \tl_if_empty:NF \@title { \exp_args:No \stex_document_title:n \@title } \_stex_maketitle: } } \cs_new_protected:Nn \stex_par: { \mode_if_vertical:F{ \if@minipage\else\if@nobreak\else\par\fi\fi } } %%%%%%%%%%%%% 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 {\begingroup \catcode`\ =12 \sys_get_shell:nnN { kpsewhich ~ #1 } { } \l_tmpa_tl \tl_gset_eq:NN \l_tmpa_tl \l_tmpa_tl \endgroup \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:NT \c_stex_mathhub_str { \sys_if_platform_windows:TF{ \begingroup\escapechar=-1\catcode`\\=12 \exp_args:Nx\stex_kpsewhich:n{-var-value~HOME} \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~HOME} } \ior_open:NnT \l_tmpa_ior{\l_stex_kpsewhich_return_str / .stex / mathhub.path}{ \begingroup\escapechar=-1\catcode`\\=12 \ior_str_get:NN \l_tmpa_ior \l_tmpa_str \sys_if_platform_windows:T{ \exp_args:NNx\str_replace_all:Nnn\l_tmpa_str{\c_backslash_str}/ } \str_gset_eq:NN \c_stex_mathhub_str\l_tmpa_str \endgroup \ior_close:N \l_tmpa_ior } } \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 } \input{Fatal~Error!} } { \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 \stex_persist:x { \prop_set_from_keyval:cn{ c_stex_mathhub_#1_manifest_prop }{ \exp_after:wN \prop_to_keyval:N \csname c_stex_mathhub_#1_manifest_prop\endcsname } } } \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 } } } \bool_if:NF \c_stex_persist_mode_bool { \__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_mathhub_mhinput:nn{ #1 }{ #2 } } \cs_new_protected:Nn \__stex_mathhub_inputref:nn { \stex_in_repository:nn {#1} { \stex_html_backend:TF { \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 {} } \tl_if_empty:nTF{ ##1 }{ \IfFileExists{#2}{ \stex_annotate_invisible:nnn{inputref}{ \l_tmpa_str / #2 }{} }{ \input{#2} } }{ \IfFileExists{ \c_stex_mathhub_str / ##1 / source / #2 }{ \stex_annotate_invisible:nnn{inputref}{ \l_tmpa_str / #2 }{} }{ \input{ \c_stex_mathhub_str / ##1 / source / #2 } } } }{ \begingroup \inputreftrue \tl_if_empty:nTF{ ##1 }{ \input{#2} }{ \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}} \providecommand\mhgraphics[2][]{% \def\Gin@mhrepos{}\setkeys{Gin}{#1}% \includegraphics[#1]{\mhpath\Gin@mhrepos{#2}}} \providecommand\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 %%%%%%%%%%%%% \AtBeginDocument{ } \AtEndDocument{ } \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 \exp_not:N\detokenize{sref_sym_#1_label_str}\exp_not:N\endcsname{ \l__stex_refs_curr_label_str } } } } } \str_new:N \l__stex_refs_indocument_str \keys_define:nn { stex / sref } { linktext .tl_set:N = \l__stex_refs_linktext_tl , fallback .tl_set:N = \l__stex_refs_fallback_tl , pre .tl_set:N = \l__stex_refs_pre_tl , post .tl_set:N = \l__stex_refs_post_tl , } \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_execute_in_module:n { \stex_if_in_module:T { \stex_add_to_current_module:n { #1 } \stex_do_up_to_module:n { #1 } }} \cs_generate_variant:Nn \stex_execute_in_module:n {x} \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_generate_variant:Nn \stex_add_to_current_module:n {x} \cs_new_protected:Npn \STEXexport { \ExplSyntaxOn \__stex_modules_export:n } \cs_new_protected:Nn \__stex_modules_export:n { \ignorespacesandpars#1\ExplSyntaxOff \stex_add_to_current_module:n { \ignorespacesandpars#1} \stex_smsmode_do: } \let \stex_module_export_helper:n \use:n \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 \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 \csname l__stex_modules_aftergroup_\l_stex_current_module_str _tl \expandafter\expandafter\expandafter\endcsname \expandafter\expandafter\expandafter { \csname l__stex_modules_aftergroup_\l_stex_current_module_str _tl\endcsname #1 } \aftergroup\__stex_modules_aftergroup_do: } } \cs_generate_variant:Nn \stex_do_up_to_module:n {x} \cs_new_protected:Nn \__stex_modules_aftergroup_do: { \stex_debug:nn{aftergroup}{\cs_meaning:c{ l__stex_modules_aftergroup_\l_stex_current_module_str _tl }} \int_compare:nNnTF \l__stex_modules_group_depth_int = \currentgrouplevel { \use:c{l__stex_modules_aftergroup_\l_stex_current_module_str _tl} \tl_gclear:c{l__stex_modules_aftergroup_\l_stex_current_module_str _tl} }{ \use:c{l__stex_modules_aftergroup_\l_stex_current_module_str _tl} \aftergroup\__stex_modules_aftergroup_do: } } \cs_new_protected:Nn \_stex_reset_up_to_module:n { \expandafter\let\csname l__stex_modules_aftergroup_#1_tl\endcsname\undefined } \str_new:N \l_stex_module_ns_str \str_new:N \l_stex_module_subpath_str \cs_new_protected:Nn \__stex_modules_compute_namespace:nN { \seq_set_eq:NN \l_tmpa_seq #2 % split off file extension \seq_pop_right:NN \l_tmpa_seq \l_tmpb_str % <- filename \exp_args:NNno \seq_set_split:Nnn \l_tmpb_seq . \l_tmpb_str \seq_get_left:NN \l_tmpb_seq \l_tmpb_str % <- filename without suffixes \seq_put_right:No \l_tmpa_seq \l_tmpb_str % <- file path including name without suffixes \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_module_subpath_str % \l_tmpa_seq <- sub-path relative to archive \str_if_empty:NTF \l_stex_module_subpath_str { \str_set:Nx \l_stex_module_ns_str {#1} }{ \str_set:Nx \l_stex_module_ns_str { #1/\l_stex_module_subpath_str } } } \cs_new_protected:Nn \stex_modules_current_namespace: { \str_clear:N \l_stex_module_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_module_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 { \int_set:Nn \l__stex_modules_group_depth_int {\currentgrouplevel} \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 } \str_if_empty:NT \l_stex_module_lang_str { \str_set:Nx \l_stex_module_lang_str { \prop_item:cn {c_stex_module_\l_stex_current_module_str _prop} { lang } } } }{ % not nested: \str_if_empty:NT \l_stex_module_ns_str { \stex_modules_current_namespace: \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 \exp_args:No \str_if_eq:nnF \l_tmpa_str {tex} { \exp_args:No \str_if_eq:nnF \l_tmpa_str {dtx} { \exp_args:NNo \seq_put_right:Nn \l_tmpa_seq \l_tmpa_str } } \seq_pop_left:NN \l_tmpa_seq \l_tmpa_str % \seq_if_empty:NF \l_tmpa_seq { %remaining element should be [.]language \seq_pop_right:NN \l_tmpa_seq \l_stex_module_lang_str \stex_debug:nn{modules} {Language~\l_stex_module_lang_str~ inferred~from~file~name} } } \stex_if_smsmode:F { \str_if_empty:NF \l_stex_module_lang_str { \exp_args:NNo \stex_set_language:Nn \l_tmpa_str \l_stex_module_lang_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} \seq_clear:c {c_stex_module_\l_stex_module_ns_str?\l_stex_module_name_str _copymodules} \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} } \stex_debug:nn{modules}{Signature~\l_stex_module_sig_str~for~\l_stex_module_ns_str?\l_stex_module_name_str} \stex_if_module_exists:nTF{\l_stex_module_ns_str?\l_stex_module_name_str}{ \stex_debug:nn{modules}{(already exists)} }{ \stex_debug:nn{modules}{(needs loading)} \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 % \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} } }{ \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 } \tl_clear:c{l__stex_modules_aftergroup_\l_stex_module_ns_str ? \l_stex_module_name_str _tl} } \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_do_html:T{ \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}{} } } } % 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 }} \_stex_reset_up_to_module:n \l_stex_current_module_str \stex_if_smsmode:T { \stex_persist:x { \prop_set_from_keyval:cn{c_stex_module_\l_stex_current_module_str _prop}{ \exp_after:wN \prop_to_keyval:N \csname c_stex_module_\l_stex_current_module_str _prop\endcsname } \seq_set_from_clist:cn{c_stex_module_\l_stex_current_module_str _constants}{ \seq_use:cn{c_stex_module_\l_stex_current_module_str _constants}, } \seq_set_from_clist:cn{c_stex_module_\l_stex_current_module_str _imports}{ \seq_use:cn{c_stex_module_\l_stex_current_module_str _imports}, } \tl_set:cn {c_stex_module_\l_stex_current_module_str _code} } \exp_after:wN \let \exp_after:wN \l_tmpa_tl \csname c_stex_module_\l_stex_current_module_str _code\endcsname \exp_after:wN \stex_persist:n \exp_after:wN { \exp_after:wN { \l_tmpa_tl } } } } \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_if_empty:NF \smoduletitle { \exp_args:No \stex_document_title:n \smoduletitle } \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} \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 \assign \renamedecl \donotcopy \instantiate \textsymdecl } \exp_args:NNx \seq_set_from_clist:Nn \g_stex_smsmode_allowedenvs_seq { \tl_to_str:n { smodule, copymodule, interpretmodule, realization, sdefinition, sexample, sassertion, sparagraph, mathstructure } } \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 { \stex_suppress_html:n { \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 \NewDocumentCommand \__stex_smsmode_importmodule: { O{} m} { \seq_gput_right:Nn \l__stex_smsmode_importmodules_seq {{#1}{#2}} \stex_smsmode_do: } \cs_new_protected:Nn \__stex_smsmode_module:nn { \__stex_modules_args:n{#1} \stex_if_in_module:F { \str_if_empty:NF \l_stex_module_sig_str { \stex_modules_current_namespace: \str_set:Nx \l_stex_module_name_str { #2 } \stex_if_module_exists:nF{\l_stex_module_ns_str?\l_stex_module_name_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 % \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:NNx \seq_gput_right:Nn \l__stex_smsmode_sigmodules_seq \l_tmpa_str }{ \msg_error:nnx{stex}{error/unknownmodule}{for~signature~\l_tmpa_str} } } } } } \prg_new_conditional:Nnn \__stex_smsmode_check_import_pair:nn {T,F,TF} { %\stex_debug:nn{import-pair}{\detokenize{{#1}~{#2}}} \tl_if_empty:nTF{#1}{ \prop_if_exist:NTF \l_stex_current_repository_prop { %\stex_debug:nn{import-pair}{in repository \prop_item:Nn \l_stex_current_repository_prop {id}} \prg_return_true: } { \seq_set_split:Nnn \l_tmpa_seq ? {#2} \seq_get_left:NN \l_tmpa_seq \l_tmpa_tl \tl_if_empty:NT \l_tmpa_tl { \seq_pop_left:NN \l_tmpa_seq \l_tmpa_tl } %\stex_debug:nn{import-pair}{\seq_use:Nn \l_tmpa_seq,~of~length~\seq_count:N \l_tmpa_seq} \int_compare:nNnTF {\seq_count:N \l_tmpa_seq} > 1 \prg_return_true: \prg_return_false: } }\prg_return_true: } \cs_new_protected:Nn \stex_file_in_smsmode:nn { \stex_filestack_push:n{#1} \seq_gclear:N \l__stex_smsmode_importmodules_seq \seq_gclear:N \l__stex_smsmode_sigmodules_seq % ----- new ----------------------------- \__stex_smsmode_in_smsmode:nn{#1}{ \let\importmodule\__stex_smsmode_importmodule: \let\stex_module_setup:nn\__stex_smsmode_module:nn \let\__stex_modules_begin_module:\relax \let\__stex_modules_end_module:\relax \seq_clear:N \g_stex_smsmode_allowedenvs_seq \exp_args:NNx \seq_put_right:Nn \g_stex_smsmode_allowedenvs_seq {\tl_to_str:n{smodule}} \tl_clear:N \g_stex_smsmode_allowedmacros_tl \tl_clear:N \g_stex_smsmode_allowedmacros_escape_tl \tl_put_right:Nn \g_stex_smsmode_allowedmacros_escape_tl {\importmodule} \everyeof{\q__stex_smsmode_break\noexpand} \expandafter\expandafter\expandafter \stex_smsmode_do: \csname @ @ input\endcsname "#1"\relax \seq_map_inline:Nn \l__stex_smsmode_sigmodules_seq { \stex_filestack_push:n{##1} \expandafter\expandafter\expandafter \stex_smsmode_do: \csname @ @ input\endcsname "##1"\relax \stex_filestack_pop: } } % ----- new ----------------------------- \__stex_smsmode_in_smsmode:nn{#1} { #2 % ----- new ----------------------------- \begingroup %\stex_debug:nn{smsmode}{Here:~\seq_use:Nn\l__stex_smsmode_importmodules_seq, } \seq_map_inline:Nn \l__stex_smsmode_importmodules_seq { \__stex_smsmode_check_import_pair:nnT ##1 { \begingroup \stex_import_module_uri:nn ##1 \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 \endgroup } } \endgroup \stex_debug:nn{smsmode}{Actually~loading~file~#1} % ----- new ----------------------------- \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_module_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 { \stex_path_from_string:Nn \l_tmpb_seq { \l_stex_module_ns_str / .. / \l_stex_import_path_str } \str_set:Nx \l_stex_import_ns_str {\stex_path_to_string:N \l_tmpb_seq} \str_replace_once:Nnn \l_stex_import_ns_str {file:/} {file://} } }{ \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 } { \stex_debug:nn{requiremodule}{Here:\\~~1:~#1\\~~2:~#2\\~~3:~#3\\~~4:~#4} \exp_args:NNxx \seq_set_split:Nnn \l_tmpa_seq {\tl_to_str:n{/}} {#4} \seq_get_left:NN \l_tmpa_seq \l_tmpc_str %\stex_debug:nn{requiremodule}{Top~module:\l_tmpc_str} % 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 \seq_put_right:Nn \l_tmpa_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 / \l_tmpc_str } \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~a1~\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~a2~\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~a3~\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_tmpb_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_canonicalize:N \l_tmpb_seq \stex_path_to_string:NN \l_tmpb_seq \l_tmpa_str \stex_debug:nn{modules}{Checking~b1~\l_tmpa_str/\l_tmpc_str.\l_tmpb_str.tex} \IfFileExists{ \l_tmpa_str/\l_tmpc_str.\l_tmpb_str.tex }{ \str_gset:Nx \g__stex_importmodule_file_str { \l_tmpa_str/\l_tmpc_str.\l_tmpb_str.tex } }{ \stex_debug:nn{modules}{Checking~b2~\l_tmpa_str/\l_tmpc_str.tex} \IfFileExists{ \l_tmpa_str/\l_tmpc_str.tex }{ \str_gset:Nx \g__stex_importmodule_file_str { \l_tmpa_str/\l_tmpc_str.tex } }{ % try english as default \stex_debug:nn{modules}{Checking~b3~\l_tmpa_str/\l_tmpc_str.en.tex} \IfFileExists{ \l_tmpa_str/\l_tmpc_str.en.tex }{ \str_gset:Nx \g__stex_importmodule_file_str { \l_tmpa_str/\l_tmpc_str.en.tex } }{ \stex_debug:nn{modules}{Checking~b4~\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~b4~\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~b5~\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} } } } } } } } \str_if_eq:eeF{\g__stex_importmodule_file_str}{\seq_use:Nn \g_stex_currentfile_seq /}{ \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_import_require_module:nnnn { \l_stex_import_ns_str } { \l_stex_import_archive_str } { \l_stex_import_path_str } { \l_stex_import_name_str } \stex_if_smsmode:F { \stex_annotate_invisible:nnn {import} {\l_stex_import_ns_str ? \l_stex_import_name_str} {} } \exp_args:Nx \stex_add_to_current_module:n { \stex_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 } \cs_new_protected:Nn \stex_csl_to_imports:Nn { \tl_if_empty:nF{#2}{ \clist_set:Nn \l_tmpa_clist {#2} \clist_map_inline:Nn \l_tmpa_clist { \tl_if_head_eq_charcode:nNTF {##1}[{ #1 ##1 }{ #1{##1} } } } } \cs_generate_variant:Nn \stex_csl_to_imports:Nn {No} %%%%%%%%%%%%% 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 } \msg_new:nnn{stex}{error/unknownsymbol}{ No~symbol~#1~found! } \msg_new:nnn{stex}{error/seqlength}{ Expected~#1~arguments;~got~#2! } \msg_new:nnn{stex}{error/unknownnotation}{ Unknown~notation~#1~for~#2! } \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 , reorder .str_set_x:N = \l_stex_symdecl_reorder_str , 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_reorder_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 } \tl_if_empty:NTF \l_stex_symdecl_definiens_tl { \prop_put:Nnx \l_tmpa_prop { defined }{ false } }{ \prop_put:Nnx \l_tmpa_prop { defined }{ true } } % 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 }} } } \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 }^^J Definiens:~\exp_not:o {\l_stex_symdecl_definiens_tl} } % circular dependencies require this: \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_if_empty:NF \l_stex_symdecl_reorder_str { \stex_annotate_invisible:nnn{reorderargs}{\l_stex_symdecl_reorder_str}{} } } } \prop_if_exist:cF { l_stex_symdecl_ \l_stex_current_module_str ? \l_stex_symdecl_name_str _prop } { \bool_if:NTF \l_stex_symdecl_local_bool \stex_do_up_to_module:x \stex_execute_in_module:x { \__stex_symdecl_restore_symbol:nnnnnnn {\l_stex_symdecl_name_str} { \prop_item:Nn \l_tmpa_prop {args} } { \prop_item:Nn \l_tmpa_prop {arity} } { \prop_item:Nn \l_tmpa_prop {assocs} } { \prop_item:Nn \l_tmpa_prop {defined} } {\bool_if:NT \l_stex_symdecl_make_macro_bool {#1} } {\l_stex_current_module_str} } } } \cs_new_protected:Nn \__stex_symdecl_restore_symbol:nnnnnnn { \prop_clear:N \l_tmpa_prop \prop_put:Nnn \l_tmpa_prop { module } { #7 } \prop_put:Nnn \l_tmpa_prop { name } { #1} \prop_put:Nnn \l_tmpa_prop { args } {#2} \prop_put:Nnn \l_tmpa_prop { arity } { #3 } \prop_put:Nnn \l_tmpa_prop { assocs } { #4 } \prop_put:Nnn \l_tmpa_prop { defined } { #5 } \tl_if_empty:nF{#6}{ \tl_set:cx{#6}{\stex_invoke_symbol:n{\detokenize{#7 ? #1}}} } \prop_set_eq:cN{l_stex_symdecl_ \detokenize{#7 ? #1} _prop}\l_tmpa_prop \seq_clear:c{l_stex_symdecl_ \detokenize{#7 ? #1} _notations} } \keys_define:nn { stex / textsymdecl } { name .str_set_x:N = \l__stex_symdecl_name_str , type .tl_set:N = \l__stex_symdecl_type_tl } \cs_new_protected:Nn \_stex_textsymdecl_args:n { \str_clear:N \l__stex_symdecl_name_str \tl_clear:N \l__stex_symdecl_type_tl \keys_set:nn { stex / textsymdecl } { #1 } } \NewDocumentCommand \textsymdecl {m O{} m} { \_stex_textsymdecl_args:n { #2 } \str_if_empty:NTF \l__stex_symdecl_name_str { \__stex_symdecl_args:n{name=#1,#2} }{ \__stex_symdecl_args:n{#2} } \bool_set_true:N \l_stex_symdecl_make_macro_bool \stex_symdecl_do:n{#1-sym} \stex_execute_in_module:n{ \cs_set_nopar:cpn{#1name}{ \ifvmode\hbox_unpack:N\c_empty_box\fi \hbox{#3}\xspace } \cs_set_nopar:cpn{#1}{ \ifmmode\csname#1-sym\expandafter\endcsname\else \ifvmode\hbox_unpack:N\c_empty_box\fi \symref{#1-sym}{\hbox{#3}}\expandafter\xspace \fi } } \stex_execute_in_module:x{ \__stex_notation_restore_notation:nnnnn {\l_stex_current_module_str?\tl_if_empty:NTF\l__stex_symdecl_name_str{#1}\l__stex_symdecl_name_str} {}{0} {\exp_not:n{\STEXInternalTermMathOMSiiii{\STEXInternalCurrentSymbolStr}{}{\neginfprec}{ \comp{\hbox{#3}}\STEXInternalSymbolAfterInvokationTL }}} {} } \stex_smsmode_do: } \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 { \tl_set:Nn \l_tmpa_tl { #1 } \__stex_symdecl_get_symbol_from_cs: }{ % 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 { \__stex_symdecl_get_symbol_from_cs: }{ \__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_error:nnn{stex}{error/unknownsymbol}{#1} } \str_set:Nn \l_tmpa_str { #1 } %\int_set:Nn \l_tmpa_int { \str_count:N \l_tmpa_str } \str_if_in:NnTF \l_tmpa_str ? { \exp_args:NNno \seq_set_split:Nnn \l_tmpa_seq ? \l_tmpa_str \seq_pop_right:NN \l_tmpa_seq \l_tmpa_str \str_set:Nx \l_tmpb_str {\seq_use:Nn \l_tmpa_seq ?} }{ \str_clear:N \l_tmpb_str } \str_if_empty:NTF \l_tmpb_str { \seq_map_inline:Nn \l_stex_all_modules_seq { \seq_map_inline:cn{c_stex_module_##1_constants}{ \exp_args:Nno \str_if_eq:nnT{####1} \l_tmpa_str { \seq_map_break:n{\seq_map_break:n{ \tl_set:Nn \l_tmpa_tl { \str_set:Nn \l_stex_get_symbol_uri_str { ##1 ? ####1 } } }} } } } }{ \int_set:Nn \l_tmpa_int { \str_count:N \l_tmpb_str } \seq_map_inline:Nn \l_stex_all_modules_seq { \str_if_eq:eeT{ \l_tmpb_str }{ \str_range:nnn {##1}{-\l_tmpa_int}{-1}}{ \seq_map_inline:cn{c_stex_module_##1_constants}{ \exp_args:Nno \str_if_eq:nnT{####1} \l_tmpa_str { \seq_map_break:n{\seq_map_break:n{ \tl_set:Nn \l_tmpa_tl { \str_set:Nn \l_stex_get_symbol_uri_str { ##1 ? ####1 } } }} } } } } } \l_tmpa_tl } \cs_new_protected:Nn \__stex_symdecl_get_symbol_from_cs: { \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 } { 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_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:\ignorespacesandpars } \stex_notation_do:nnnnn { \prop_item:cn {l_stex_symdecl_\l_stex_get_symbol_uri_str _prop } { args } } { \prop_item:cn { l_stex_symdecl_\l_stex_get_symbol_uri_str _prop } { arity } } { \l__stex_notation_variant_str } { \l__stex_notation_prec_str} } \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 \STEXInternalSymbolAfterInvokationTL \cs_new_protected:Nn \stex_notation_do:nnnnn { \let\STEXInternalCurrentSymbolStr\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 \l__stex_notation_suffix_str { #3 } \str_set:Nx \l__stex_notation_prec_str { #4 } % 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 { \STEXInternalTermMathOMSiiii { \STEXInternalCurrentSymbolStr } { \l__stex_notation_suffix_str } { \l__stex_notation_opprec_tl } { \exp_not:n { #5 } } } \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 } { { \STEXInternalTermMathOMBiiii { \STEXInternalCurrentSymbolStr } { \l__stex_notation_suffix_str } { \l__stex_notation_opprec_tl } { \exp_not:n { #5 } } }} }{ \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 } { { \STEXInternalTermMathOMBiiii { \STEXInternalCurrentSymbolStr } { \l__stex_notation_suffix_str } { \l__stex_notation_opprec_tl } { \exp_not:n { #5 } } } } }{ \exp_args:Nne \use:nn { \cs_generate_from_arg_count:NNnn \l_stex_notation_macrocode_cs \cs_set:Npn \l__stex_notation_arity_str } { { \STEXInternalTermMathOMAiiii { \STEXInternalCurrentSymbolStr } { \l__stex_notation_suffix_str } { \l__stex_notation_opprec_tl } { \exp_not:n { #5 } } } } } } \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:nn{a} }{ \str_if_eq:VnTF \l_tmpa_str B { \__stex_notation_argument_assoc:nn{B} }{ \seq_pop_left:NN \l__stex_notation_remaining_precs_seq \l_tmpb_str \tl_put_right:Nx \l_stex_notation_dummyargs_tl { { \STEXInternalTermMathArgiii { \l_tmpa_str\int_use:N \l__stex_notation_currarg_int } { \l_tmpb_str } { ####\int_use:N \l__stex_notation_currarg_int } } } \__stex_notation_arguments: } } } } \cs_new_protected:Nn \__stex_notation_argument_assoc:nn { \cs_generate_from_arg_count:NNnn \l_tmpa_cs \cs_set:Npn {\l__stex_notation_arity_str}{ #2 } \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{##1\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 { { \STEXInternalTermMathAssocArgiiii { #1\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_restore_notation:nnnnn { \cs_generate_from_arg_count:cNnn{stex_notation_\detokenize{#1} \c_hash_str \detokenize{#2}_cs} \cs_set_nopar:Npn {#3}{#4} \tl_if_empty:nF {#5}{ \tl_set:cn{stex_op_notation_\detokenize{#1} \c_hash_str \detokenize{#2}_cs}{ \comp{ #5 } } } \seq_if_exist:cT { l_stex_symdecl_\detokenize{#1} _notations }{ \seq_put_right:cx { l_stex_symdecl_\detokenize{#1} _notations } { \detokenize{#2} } } } \cs_new_protected:Nn \__stex_notation_final: { \stex_execute_in_module:x { \__stex_notation_restore_notation:nnnnn {\l_stex_get_symbol_uri_str} {\l__stex_notation_suffix_str} {\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 \STEXInternalSymbolAfterInvokationTL} } {\exp_args:No \exp_not:n \l__stex_notation_op_tl } } \stex_debug:nn{symbols}{ Notation~\l__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 \l__stex_notation_suffix_str _cs } } % HTML annotations \stex_if_do_html:T { \stex_annotate_invisible:nnn { notation } { \l_stex_get_symbol_uri_str } { \stex_annotate_invisible:nnn { notationfragment } { \l__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 { \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int a}{} , \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int b}{} } } }{ \str_if_eq:VnTF \l_tmpb_str B { \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int a}{} , \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int b}{} } } }{ \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int}{} } } } } } \stex_annotate_invisible:nnn { notationcomp }{}{ \str_set:Nx \STEXInternalCurrentSymbolStr {\l_stex_get_symbol_uri_str } $ \exp_args:Nno \use:nn { \use:c { stex_notation_ \STEXInternalCurrentSymbolStr \c_hash_str \l__stex_notation_suffix_str _cs } } { \l_tmpa_tl } $ } \tl_if_empty:NF \l__stex_notation_op_tl { \stex_annotate_invisible:nnn { notationopcomp }{}{ $\l__stex_notation_op_tl$ } } } } } \keys_define:nn { stex / setnotation } { 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_notation_setnotation:nn { \seq_if_exist:cT{l_stex_symdecl_#1_notations}{ \seq_remove_all:cn { l_stex_symdecl_#1 _notations }{ #2 } \seq_put_left:cn { l_stex_symdecl_#1 _notations }{ #2 } } } \cs_new_protected:Nn \stex_setnotation:n { \exp_args:Nnx \seq_if_in:cnTF { l_stex_symdecl_#1 _notations } { \l__stex_notation_variant_str }{ \stex_execute_in_module:x{ \__stex_notation_setnotation:nn {#1}{\l__stex_notation_variant_str} } \stex_debug:nn {notations}{ Setting~default~notation~ {\l__stex_notation_variant_str }~for~ #1 \\ \expandafter\meaning\csname l_stex_symdecl_#1 _notations\endcsname } }{ \msg_error:nnxx{stex}{unknownnotation}{\l__stex_notation_variant_str}{#1} } } \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:\ignorespacesandpars } \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}{\begingroup \stex_debug:nn{Here}{Here:~##1} \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_after:wN \def \exp_after:wN \l_tmpa_tl \exp_after:wN ####\exp_after:wN 1 \exp_after:wN ####\exp_after:wN 2 \exp_after:wN { \l_tmpa_tl } \edef \l_tmpa_tl { \exp_after:wN \exp_not:n \exp_after:wN { \l_tmpa_tl {######## 1}{######## 2} } } \stex_debug:nn{Here}{Here:~\expandafter\detokenize\expandafter{\l_tmpa_tl}} \stex_execute_in_module:x { \__stex_notation_restore_notation:nnnnn {#1}{##1} { \prop_item:cn {l_stex_symdecl_#2_prop}{ arity } } { \exp_after:wN\exp_not:n\exp_after:wN{\l_tmpa_tl} } { \cs_if_exist:cT{stex_op_notation_ #2\c_hash_str ##1 _cs}{ \exp_args:NNo\exp_args:No\exp_not:n{\csname stex_op_notation_ #2\c_hash_str ##1 _cs\endcsname} } } }\endgroup } } \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 \stex_smsmode_do:\ignorespacesandpars } \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 , reorder .str_set_x:N = \l_stex_symdecl_reorder_str , op .tl_set:N = \l__stex_notation_op_tl , % lang .str_set_x:N = \l__stex_notation_lang_str , variant .str_set_x:N = \l__stex_notation_variant_str , prec .str_set_x:N = \l__stex_notation_prec_str , 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 \str_clear:N \l_stex_symdecl_reorder_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:\ignorespacesandpars } \str_set:Nx \l_stex_get_symbol_uri_str { \l_stex_current_module_str ? \l_stex_symdecl_name_str } \exp_args:Nx \stex_notation_do:nnnnn { \prop_item:cn {l_stex_symdecl_\l_stex_get_symbol_uri_str _prop } { args } } { \prop_item:cn { l_stex_symdecl_\l_stex_get_symbol_uri_str _prop } { arity } } { \l__stex_notation_variant_str } { \l__stex_notation_prec_str} } \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 , reorder .str_set_x:N = \l__stex_variables_reorder_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_reorder_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 } { \exp_not:N\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 \STEXInternalSymbolAfterInvokationTL} }} \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}{} } \str_if_empty:NF \l__stex_variables_reorder_str { \stex_annotate_invisible:nnn{reorderargs}{\l__stex_variables_reorder_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 { \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int a}{} , \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int b}{} } } }{ \str_if_eq:VnTF \l_tmpb_str B { \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int a}{} , \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int b}{} } } }{ \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int}{} } } } } } \stex_annotate_invisible:nnn { notationcomp }{}{ \str_set:Nx \STEXInternalCurrentSymbolStr {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 } $ } \tl_if_empty:NF \l__stex_variables_op_tl { \stex_annotate_invisible:nnn { notationopcomp }{}{ $\l__stex_variables_op_tl$ } } } \str_if_empty:NF \l__stex_variables_bind_str { \stex_annotate_invisible:nnn {bindtype}{\l__stex_variables_bind_str,\l__stex_variables_name_str}{} } }\ignorespacesandpars } \stex_notation_do:nnnnn { \l__stex_variables_args_str } { \prop_item:Nn \l_tmpa_prop { arity } } {}{ \l__stex_variables_prec_str} } \cs_new:Nn \_stex_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 {vardecl}{\clist_use:Nn\l__stex_variables_names,}{ #2 } }{ \_stex_reset:N \varnot \_stex_reset:N \vartype \_stex_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 }{ \exp_args:Nnx \use:nn { \def\comp{\_varcomp} \str_set:Nx \STEXInternalCurrentSymbolStr { var://\l_tmpa_str } \comp{ #2 } }{ \_stex_reset:N \comp \_stex_reset:N \STEXInternalCurrentSymbolStr } } } \keys_define:nn { stex / varseq } { name .str_set_x:N = \l__stex_variables_name_str , args .int_set:N = \l__stex_variables_args_int , type .tl_set:N = \l__stex_variables_type_tl , mid .tl_set:N = \l__stex_variables_mid_tl , bind .choices:nn = {forall,exists} {\str_set:Nx \l__stex_variables_bind_str {\l_keys_choice_tl}} } \cs_new_protected:Nn \__stex_variables_seq_args:n { \str_clear:N \l__stex_variables_name_str \int_set:Nn \l__stex_variables_args_int 1 \tl_clear:N \l__stex_variables_type_tl \str_clear:N \l__stex_variables_bind_str \keys_set:nn { stex / varseq } { #1 } } \NewDocumentCommand \varseq {m O{} m m m}{ \__stex_variables_seq_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:Nnx \l_tmpa_prop { arity }{\int_use:N \l__stex_variables_args_int} \seq_set_from_clist:Nn \l_tmpa_seq {#3} \int_compare:nNnF {\seq_count:N \l_tmpa_seq} = \l__stex_variables_args_int { \msg_error:nnxx{stex}{error/seqlength} {\int_use:N \l__stex_variables_args_int} {\seq_count:N \l_tmpa_seq} } \seq_set_from_clist:Nn \l_tmpb_seq {#4} \int_compare:nNnF {\seq_count:N \l_tmpb_seq} = \l__stex_variables_args_int { \msg_error:nnxx{stex}{error/seqlength} {\int_use:N \l__stex_variables_args_int} {\seq_count:N \l_tmpb_seq} } \prop_put:Nnn \l_tmpa_prop {starts} {#3} \prop_put:Nnn \l_tmpa_prop {ends} {#4} \cs_generate_from_arg_count:cNnn {stex_varseq_\l__stex_variables_name_str _cs} \cs_set:Npn {\int_use:N \l__stex_variables_args_int} { #5 } \exp_args:NNo \tl_set:No \l_tmpa_tl {\use:c{stex_varseq_\l__stex_variables_name_str _cs}} \int_step_inline:nn \l__stex_variables_args_int { \tl_put_right:Nx \l_tmpa_tl { {\seq_item:Nn \l_tmpa_seq {##1}} } } \tl_set:Nx \l_tmpa_tl {\exp_args:NNo \exp_args:No \exp_not:n{\l_tmpa_tl}} \tl_put_right:Nn \l_tmpa_tl {,\ellipses,} \tl_if_empty:NF \l__stex_variables_mid_tl { \tl_put_right:No \l_tmpa_tl \l__stex_variables_mid_tl \tl_put_right:Nn \l_tmpa_tl {,\ellipses,} } \exp_args:NNo \tl_set:No \l_tmpb_tl {\use:c{stex_varseq_\l__stex_variables_name_str _cs}} \int_step_inline:nn \l__stex_variables_args_int { \tl_put_right:Nx \l_tmpb_tl { {\seq_item:Nn \l_tmpb_seq {##1}} } } \tl_set:Nx \l_tmpb_tl {\exp_args:NNo \exp_args:No \exp_not:n{\l_tmpb_tl}} \tl_put_right:No \l_tmpa_tl \l_tmpb_tl \prop_put:Nno \l_tmpa_prop { notation }\l_tmpa_tl \tl_set:cx {#1} {\stex_invoke_sequence:n {\l__stex_variables_name_str}} \exp_args:NNo \tl_set:No \l_tmpa_tl {\use:c{stex_varseq_\l__stex_variables_name_str _cs}} \int_step_inline:nn \l__stex_variables_args_int { \tl_set:Nx \l_tmpa_tl {\exp_args:No \exp_not:n \l_tmpa_tl { \STEXInternalTermMathArgiii{i##1}{0}{\exp_not:n{####}##1} }} } \tl_set:Nx \l_tmpa_tl { \STEXInternalTermMathOMAiiii { varseq://\l__stex_variables_name_str}{}{0}{ \exp_args:NNo \exp_args:No \exp_not:n {\l_tmpa_tl} } } \tl_set:No \l_tmpa_tl { \exp_after:wN { \l_tmpa_tl \STEXInternalSymbolAfterInvokationTL} } \exp_args:Nno \use:nn { \cs_generate_from_arg_count:cNnn {stex_varseq_\l__stex_variables_name_str _cs} \cs_set:Npn {\int_use:N \l__stex_variables_args_int}}{\l_tmpa_tl} \stex_debug:nn{sequences}{New~Sequence:~ \expandafter\meaning\csname stex_varseq_\l__stex_variables_name_str _cs\endcsname\\~\\ \prop_to_keyval:N \l_tmpa_prop } \stex_if_do_html:T{\stex_annotate_invisible:nnn{varseq}{\l__stex_variables_name_str}{ \tl_if_empty:NF \l__stex_variables_type_tl { \stex_annotate:nnn {type}{}{$\l__stex_variables_type_tl$} } \stex_annotate:nnn {args}{\int_use:N \l__stex_variables_args_int}{} \str_if_empty:NF \l__stex_variables_bind_str { \stex_annotate:nnn {bindtype}{\l__stex_variables_bind_str}{} } \stex_annotate:nnn{startindex}{}{$#3$} \stex_annotate:nnn{endindex}{}{$#4$} \tl_clear:N \l_tmpa_tl \int_step_inline:nn \l__stex_variables_args_int { \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { \stex_annotate:nnn{argmarker}{##1}{} } } } \stex_annotate_invisible:nnn { notationcomp }{}{ \str_set:Nx \STEXInternalCurrentSymbolStr {varseq://\l__stex_variables_name_str } $ \exp_args:Nno \use:nn { \use:c { stex_varseq_\l__stex_variables_name_str _cs } } { \l_tmpa_tl } $ } \stex_annotate_invisible:nnn { notationopcomp }{}{ $ \prop_item:Nn \l_tmpa_prop { notation } $ } }} \prop_set_eq:cN {stex_varseq_\l__stex_variables_name_str _prop}\l_tmpa_prop \ignorespacesandpars } %%%%%%%%%%%%% 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~invokation~#1~not~allowed~in~notation~component~of~#2 } \msg_new:nnn{stex}{error/doubleargument}{ Argument~#1~of~symbol~#2~already~assigned } \msg_new:nnn{stex}{error/overarity}{ Argument~#1~invalid~for~symbol~#2~with~arity~#3 } \bool_new:N \l_stex_allow_semantic_bool \bool_set_true:N \l_stex_allow_semantic_bool \cs_new_protected:Nn \stex_invoke_symbol:n { \ifvmode\indent\fi \bool_if:NTF \l_stex_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}{\STEXInternalCurrentSymbolStr} } } \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 { \def\comp{\_comp} \str_set:Nn \STEXInternalCurrentSymbolStr { #1 } \bool_set_false:N \l_stex_allow_semantic_bool \_stex_term_oms:nnn {#1}{#1 \c_hash_str CUSTOM-}{ \comp{ #2 } } }{ \_stex_reset:N \comp \_stex_reset:N \STEXInternalCurrentSymbolStr \bool_set_true:N \l_stex_allow_semantic_bool } } \keys_define:nn { stex / terms } { 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_terms_args:n { % \str_clear:N \l_stex_notation_lang_str \str_clear:N \l_stex_notation_variant_str \keys_set:nn { stex / terms } { #1 } } \cs_new_protected:Nn \stex_find_notation:nn { \__stex_terms_args:n { #2 } \seq_if_empty:cTF { l_stex_symdecl_ #1 _notations } { \msg_error:nnxx{stex}{error/nonotation}{#1}{s} } { \str_if_empty:NTF \l_stex_notation_variant_str { \seq_get_left:cN {l_stex_symdecl_#1_notations}\l_stex_notation_variant_str }{ \seq_if_in:cxTF {l_stex_symdecl_#1_notations}{ \l_stex_notation_variant_str }{ % \str_set:Nx \l_stex_notation_variant_str { \l_stex_notation_variant_str \c_hash_str \l_stex_notation_lang_str } }{ \msg_error:nnxx{stex}{error/nonotation}{#1}{ ~\l_stex_notation_variant_str } } } } } \cs_new_protected:Npn \__stex_terms_invoke_op_notation:nw #1 [#2] { \exp_args:Nnx \use:nn { \def\comp{\_comp} \str_set:Nn \STEXInternalCurrentSymbolStr { #1 } \stex_find_notation:nn { #1 }{ #2 } \bool_set_false:N \l_stex_allow_semantic_bool \cs_if_exist:cTF { stex_op_notation_ #1 \c_hash_str \l_stex_notation_variant_str _cs }{ \_stex_term_oms:nnn { #1 }{ #1 \c_hash_str \l_stex_notation_variant_str }{ \use:c{stex_op_notation_ #1 \c_hash_str \l_stex_notation_variant_str _cs} } }{ \int_compare:nNnTF {\prop_item:cn {l_stex_symdecl_#1_prop}{arity}} = 0{ \cs_if_exist:cTF { stex_notation_ #1 \c_hash_str \l_stex_notation_variant_str _cs }{ \tl_set:Nx \STEXInternalSymbolAfterInvokationTL { \_stex_reset:N \comp \_stex_reset:N \STEXInternalSymbolAfterInvokationTL \_stex_reset:N \STEXInternalCurrentSymbolStr \bool_set_true:N \l_stex_allow_semantic_bool } \def\comp{\_comp} \str_set:Nn \STEXInternalCurrentSymbolStr { #1 } \bool_set_false:N \l_stex_allow_semantic_bool \use:c{stex_notation_ #1 \c_hash_str \l_stex_notation_variant_str _cs} }{ \msg_error:nnxx{stex}{error/nonotation}{#1}{ ~\l_stex_notation_variant_str } } }{ \msg_error:nnxx{stex}{error/noop}{#1}{\l_stex_notation_variant_str} } } }{ \_stex_reset:N \comp \_stex_reset:N \STEXInternalCurrentSymbolStr \bool_set_true:N \l_stex_allow_semantic_bool } } \cs_new_protected:Npn \__stex_terms_invoke_notation:nw #1 [#2] { \stex_find_notation:nn { #1 }{ #2 } \cs_if_exist:cTF { stex_notation_ #1 \c_hash_str \l_stex_notation_variant_str _cs }{ \tl_set:Nx \STEXInternalSymbolAfterInvokationTL { \_stex_reset:N \comp \_stex_reset:N \STEXInternalSymbolAfterInvokationTL \_stex_reset:N \STEXInternalCurrentSymbolStr \bool_set_true:N \l_stex_allow_semantic_bool } \def\comp{\_comp} \str_set:Nn \STEXInternalCurrentSymbolStr { #1 } \bool_set_false:N \l_stex_allow_semantic_bool \use:c{stex_notation_ #1 \c_hash_str \l_stex_notation_variant_str _cs} }{ \msg_error:nnxx{stex}{error/nonotation}{#1}{ ~\l_stex_notation_variant_str } } } \prop_new:N \l__stex_terms_custom_args_prop \cs_new_protected:Nn\__stex_terms_custom_comp:n{\bool_set_false:N \l_stex_allow_semantic_bool\_comp{#1}\bool_set_true:N \l_stex_allow_semantic_bool} \cs_new_protected:Nn \__stex_terms_invoke_custom:nn { \exp_args:Nnx \use:nn { \def\comp{\__stex_terms_custom_comp:n} \str_set:Nn \STEXInternalCurrentSymbolStr { #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\c_hash_str CUSTOM-}{\ignorespaces#2} }{ \str_if_in:NnTF \l_tmpa_str b { \_stex_term_ombind:nnn {#1}{#1\c_hash_str CUSTOM-\l_tmpa_str}{\ignorespaces#2} }{ \str_if_in:NnTF \l_tmpa_str B { \_stex_term_ombind:nnn {#1}{#1\c_hash_str CUSTOM-\l_tmpa_str}{\ignorespaces#2} }{ \_stex_term_oma:nnn {#1}{#1\c_hash_str CUSTOM-\l_tmpa_str}{\ignorespaces#2} } } } % TODO check that all arguments exist }{ \_stex_reset:N \STEXInternalCurrentSymbolStr \_stex_reset:N \arg \_stex_reset:N \comp \_stex_reset:N \l__stex_terms_custom_args_prop %\bool_set_true:N \l_stex_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 } } \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} { \msg_error:nnxxx{stex}{error/overarity} {\int_use:N \l_tmpa_int} {\STEXInternalCurrentSymbolStr} {\str_count:N \l_tmpa_str} } \str_set:Nx \l_tmpa_str {\str_item:Nn \l_tmpa_str \l_tmpa_int} \exp_args:NNx \prop_if_in:NnT \l__stex_terms_custom_args_prop {\int_use:N \l_tmpa_int} { \bool_lazy_any:nF { {\str_if_eq_p:Vn \l_tmpa_str {a}} {\str_if_eq_p:Vn \l_tmpa_str {B}} }{ \msg_error:nnxx{stex}{error/doubleargument} {\int_use:N \l_tmpa_int} {\STEXInternalCurrentSymbolStr} } } \exp_args:NNx \prop_put:Nnn \l__stex_terms_custom_args_prop {\int_use:N \l_tmpa_int} {\ignorespaces#3} \bool_set_true:N \l_stex_allow_semantic_bool \IfBooleanTF#1{ \stex_annotate_invisible:n { %TODO \exp_args:No \_stex_term_arg:nn {\l_tmpa_str\int_use:N \l_tmpa_int}{\ignorespaces#3} } }{ %TODO \exp_args:No \_stex_term_arg:nn {\l_tmpa_str\int_use:N \l_tmpa_int}{\ignorespaces#3} } \bool_set_false:N \l_stex_allow_semantic_bool } \cs_new_protected:Nn \_stex_term_arg:nn { \bool_set_true:N \l_stex_allow_semantic_bool \stex_annotate:nnn{ arg }{ #1 }{ #2 } \bool_set_false:N \l_stex_allow_semantic_bool } \cs_new_protected:Npn \STEXInternalTermMathArgiii #1#2#3 { \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 } } } \cs_new_protected:Npn \STEXInternalTermMathAssocArgiiii #1#2#3#4 { \cs_set:Npn \l_tmpa_cs ##1 ##2 { #4 } \tl_set:Nn \l_tmpb_tl {\STEXInternalTermMathArgiii{#1}{#2}} \tl_if_empty:nTF { #3 }{ \STEXInternalTermMathArgiii{#1}{#2}{} }{ \exp_args:Nx \tl_if_empty:nTF { \tl_tail:n{ #3 }}{ \expandafter\if\expandafter\relax\noexpand#3 \tl_set:Nn \l_tmpa_tl {\__stex_terms_math_assoc_arg_maybe_sequence:Nn#3{#1}} \else \tl_set:Nn \l_tmpa_tl {\__stex_terms_math_assoc_arg_simple:nn{#1}{#3}} \fi \l_tmpa_tl }{ \__stex_terms_math_assoc_arg_simple:nn{#1}{#3} } } } \cs_new_protected:Nn \__stex_terms_math_assoc_arg_maybe_sequence:Nn { \str_set:Nx \l_tmpa_str { \cs_argument_spec:N #1 } \str_if_empty:NTF \l_tmpa_str { \exp_args:Nx \cs_if_eq:NNTF { \tl_head:N #1 } \stex_invoke_sequence:n { \tl_set:Nx \l_tmpa_tl {\tl_tail:N #1} \str_set:Nx \l_tmpa_str {\exp_after:wN \use:n \l_tmpa_tl} \tl_set:Nx \l_tmpa_tl {\prop_item:cn {stex_varseq_\l_tmpa_str _prop}{notation}} \exp_args:NNo \seq_set_from_clist:Nn \l_tmpa_seq \l_tmpa_tl \tl_set:Nx \l_tmpa_tl {{\exp_not:N \exp_not:n{ \exp_not:n{\exp_args:Nnx \use:nn} { \exp_not:n { \def\comp{\_varcomp} \str_set:Nn \STEXInternalCurrentSymbolStr } {varseq://\l_tmpa_str} \exp_not:n{ ##1 } }{ \exp_not:n { \_stex_reset:N \comp \_stex_reset:N \STEXInternalCurrentSymbolStr } } }}} \exp_args:Nno \use:nn {\seq_set_map:NNn \l_tmpa_seq \l_tmpa_seq} \l_tmpa_tl \seq_reverse:N \l_tmpa_seq \seq_pop:NN \l_tmpa_seq \l_tmpa_tl \seq_map_inline:Nn \l_tmpa_seq { \exp_args:NNNo \exp_args:NNo \tl_set:No \l_tmpa_tl { \exp_args:Nno \l_tmpa_cs { ##1 } \l_tmpa_tl } } \tl_set:Nx \l_tmpa_tl { \_stex_term_omv:nn {varseq://\l_tmpa_str}{ \exp_args:No \exp_not:n \l_tmpa_tl } } \exp_args:No\l_tmpb_tl\l_tmpa_tl }{ \__stex_terms_math_assoc_arg_simple:nn{#2} { #1 } } } { \__stex_terms_math_assoc_arg_simple:nn{#2} { #1 } } } \cs_new_protected:Nn \__stex_terms_math_assoc_arg_simple:nn { \clist_set:Nn \l_tmpa_clist{ #2 } \int_compare:nNnTF { \clist_count:N \l_tmpa_clist } < 2 { \tl_set:Nn \l_tmpa_tl { \_stex_term_arg:nn{A#1}{ #2 } } }{ \clist_reverse:N \l_tmpa_clist \clist_pop:NN \l_tmpa_clist \l_tmpa_tl \tl_set:Nx \l_tmpa_tl { \_stex_term_arg:nn{A#1}{ \exp_args:No \exp_not:n \l_tmpa_tl }} \clist_map_inline:Nn \l_tmpa_clist { \exp_args:NNNo \exp_args:NNo \tl_set:No \l_tmpa_tl { \exp_args:Nno \l_tmpa_cs { \_stex_term_arg:nn{A#1}{##1} } \l_tmpa_tl } } } \exp_args:No\l_tmpb_tl\l_tmpa_tl } \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 }{ #3 } } \cs_new_protected:Npn \STEXInternalTermMathOMSiiii #1#2#3#4 { \__stex_terms_maybe_brackets:nn { #3 }{ \_stex_term_oms:nnn { #1 } { #1\c_hash_str#2 } { #4 } } } \cs_new_protected:Nn \_stex_term_omv:nn { \stex_annotate:nnn{ OMV }{ #1 }{ #2 } } \cs_new_protected:Nn \_stex_term_oma:nnn { \stex_annotate:nnn{ OMA }{ #2 }{ #3 } } \cs_new_protected:Npn \STEXInternalTermMathOMAiiii #1#2#3#4 { \__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 }{ #3 } } \cs_new_protected:Npn \STEXInternalTermMathOMBiiii #1#2#3#4 { \__stex_terms_maybe_brackets:nn { #3 }{ \_stex_term_ombind:nnn { #1 } { #1\c_hash_str#2 } { #4 } } } \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 }!\ifmmode*\fi{ \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 }!\ifmmode*\fi{ \exp_after:wN \stex_capitalize:n \l_tmpa_str \l__stex_terms_post_tl } } \let\compemph@uri\compemph_uri_prev: } \cs_new_protected:Npn \_comp #1 { \str_if_empty:NF \STEXInternalCurrentSymbolStr { \stex_html_backend:TF { \stex_annotate:nnn { comp }{ \STEXInternalCurrentSymbolStr }{ #1 } }{ \exp_args:Nnx \compemph@uri { #1 } { \STEXInternalCurrentSymbolStr } } } } \cs_new_protected:Npn \_varcomp #1 { \str_if_empty:NF \STEXInternalCurrentSymbolStr { \stex_html_backend:TF { \stex_annotate:nnn { varcomp }{ \STEXInternalCurrentSymbolStr }{ #1 } }{ \exp_args:Nnx \varemph@uri { #1 } { \STEXInternalCurrentSymbolStr } } } } \def\comp{\_comp} \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 { \emph{#1} } \cs_new_protected:Npn \varemph@uri #1 #2 { \varemph{#1} } \cs_new_protected:Npn \varemph #1 { #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 { \peek_charcode_remove:NTF ! { \__stex_variables_invoke_op_custom:nn {#1} }{ \__stex_variables_invoke_custom:nn {#1} } } \cs_new_protected:Nn \__stex_variables_invoke_math:n { \peek_charcode_remove:NTF ! { \peek_charcode_remove:NTF ! { \peek_charcode:NTF [ { % TODO throw error }{ \__stex_variables_invoke_op_custom:nn } }{ \__stex_variables_invoke_op:n { #1 } } }{ \peek_charcode_remove:NTF * { \__stex_variables_invoke_custom:nn { #1 } }{ \__stex_variables_invoke_math_ii:n { #1 } } } } \cs_new_protected:Nn \__stex_variables_invoke_op_custom:nn { \exp_args:Nnx \use:nn { \def\comp{\_varcomp} \str_set:Nn \STEXInternalCurrentSymbolStr { var://#1 } \bool_set_false:N \l_stex_allow_semantic_bool \_stex_term_omv:nn {var://#1}{ \comp{ #2 } } }{ \_stex_reset:N \comp \_stex_reset:N \STEXInternalCurrentSymbolStr \bool_set_true:N \l_stex_allow_semantic_bool } } \cs_new_protected:Nn \__stex_variables_invoke_op:n { \cs_if_exist:cTF { stex_var_op_notation_ #1 _cs }{ \exp_args:Nnx \use:nn { \def\comp{\_varcomp} \str_set:Nn \STEXInternalCurrentSymbolStr { var://#1 } \_stex_term_omv:nn { var://#1 }{ \use:c{stex_var_op_notation_ #1 _cs } } }{ \_stex_reset:N \comp \_stex_reset:N \STEXInternalCurrentSymbolStr } }{ \int_compare:nNnTF {\prop_item:cn {l_stex_variable_#1_prop}{arity}} = 0{ \__stex_variables_invoke_math_ii:n {#1} }{ \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 }{ \tl_set:Nx \STEXInternalSymbolAfterInvokationTL { \_stex_reset:N \comp \_stex_reset:N \STEXInternalSymbolAfterInvokationTL \_stex_reset:N \STEXInternalCurrentSymbolStr \bool_set_true:N \l_stex_allow_semantic_bool } \def\comp{\_varcomp} \str_set:Nn \STEXInternalCurrentSymbolStr { var://#1 } \bool_set_false:N \l_stex_allow_semantic_bool \use:c{stex_var_notation_#1_cs} }{ \msg_error:nnxx{stex}{error/nonotation}{variable~#1}{s} } } \cs_new_protected:Nn \__stex_variables_invoke_custom:nn { \exp_args:Nnx \use:nn { \def\comp{\_varcomp} \str_set:Nn \STEXInternalCurrentSymbolStr { var://#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_variable_#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_omv:nn {var://#1}{\ignorespaces#2} }{ \str_if_in:NnTF \l_tmpa_str b { \_stex_term_ombind:nnn {var://#1}{}{\ignorespaces#2} }{ \str_if_in:NnTF \l_tmpa_str B { \_stex_term_ombind:nnn {var://#1}{}{\ignorespaces#2} }{ \_stex_term_oma:nnn {var://#1}{}{\ignorespaces#2} } } } % TODO check that all arguments exist }{ \_stex_reset:N \STEXInternalCurrentSymbolStr \_stex_reset:N \arg \_stex_reset:N \comp \_stex_reset:N \l__stex_terms_custom_args_prop %\bool_set_true:N \l_stex_allow_semantic_bool } } \cs_new_protected:Nn \stex_invoke_sequence:n { \peek_charcode_remove:NTF ! { \_stex_term_omv:nn {varseq://#1}{ \exp_args:Nnx \use:nn { \def\comp{\_varcomp} \str_set:Nn \STEXInternalCurrentSymbolStr {varseq://#1} \prop_item:cn{stex_varseq_#1_prop}{notation} }{ \_stex_reset:N \comp \_stex_reset:N \STEXInternalCurrentSymbolStr } } }{ \bool_set_false:N \l_stex_allow_semantic_bool \def\comp{\_varcomp} \str_set:Nn \STEXInternalCurrentSymbolStr {varseq://#1} \tl_set:Nx \STEXInternalSymbolAfterInvokationTL { \_stex_reset:N \comp \_stex_reset:N \STEXInternalSymbolAfterInvokationTL \_stex_reset:N \STEXInternalCurrentSymbolStr \bool_set_true:N \l_stex_allow_semantic_bool } \use:c { stex_varseq_#1_cs } } } %%%%%%%%%%%%% 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 } \msg_new:nnn{stex}{error/unknownstructure}{ No~structure~#1~found! } \msg_new:nnn{stex}{error/unknownfield}{ No~field~#1~in~instance~#2~found!\\#3 } \msg_new:nnn{stex}{error/keyval}{ Invalid~key=value~pair:#1 } \msg_new:nnn{stex}{error/instantiate/missing}{ Assignments~missing~in~instantiate:~#1 } \msg_new:nnn{stex}{error/incompatible}{ Incompatible~signature:~#1~(#2)~and~#3~(#4) } \cs_new_protected:Nn \stex_get_symbol_in_seq:nn { \tl_if_head_eq_catcode:nNTF { #1 } \relax { \tl_set:Nn \l_tmpa_tl { #1 } \__stex_copymodule_get_symbol_from_cs: }{ % 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 { \__stex_copymodule_get_symbol_from_cs:n{ #2 } }{ \__stex_copymodule_get_symbol_from_string:nn { #1 }{ #2 } } } { \__stex_copymodule_get_symbol_from_string:nn { #1 }{ #2 } } }{ % argument is not a command name \__stex_copymodule_get_symbol_from_string:nn { #1 }{ #2 } % \l_stex_all_symbols_seq } } } \cs_new_protected:Nn \__stex_copymodule_get_symbol_from_string:nn { \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_error:nnn{stex}{error/unknownsymbol}{#1} } \str_set:Nn \l_tmpa_str { #1 } \int_set:Nn \l_tmpa_int { \str_count:N \l_tmpa_str } \seq_map_inline:Nn #2 { \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 } } } } } \l_tmpa_tl } } \cs_new_protected:Nn \__stex_copymodule_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_copymodule_get_symbol_check:n { #1 } }{ % TODO % tail is not a single group } }{ % TODO % tail is not a single group } } \cs_new_protected:Nn \__stex_copymodule_get_symbol_check:n { \exp_args:NNx \seq_if_in:NnF #1 \l_stex_get_symbol_uri_str { \msg_error:nnxx{stex}{error/copymodule/notallowed}{\l_stex_get_symbol_uri_str}{ :~\seq_use:Nn #1 {,~} } } } \cs_new_protected:Nn \stex_copymodule_start:nnnn { % import module \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_copymodule_copymodule_modules_seq \l_stex_collect_imports_seq % fields \seq_clear:N \l__stex_copymodule_copymodule_fields_seq \seq_map_inline:Nn \l__stex_copymodule_copymodule_modules_seq { \seq_map_inline:cn {c_stex_module_##1_constants}{ \exp_args:NNx \seq_put_right:Nn \l__stex_copymodule_copymodule_fields_seq { ##1 ? ####1 } } } % setup prop \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_copymodule_copymodule_modules_seq {,~}} \stex_debug:nn{copymodule}{fields:\seq_use:Nn \l__stex_copymodule_copymodule_fields_seq {,~}} \stex_if_do_html:T { \begin{stex_annotate_env} {#4} { \l_stex_current_module_str?\l_stex_current_copymodule_name_str } \stex_annotate_invisible:nnn{domain}{\l_stex_import_ns_str ?\l_stex_import_name_str}{} } } \cs_new_protected:Nn \stex_copymodule_end:n { % apply to every field \def \l_tmpa_cs ##1 ##2 {#1} \tl_clear:N \__stex_copymodule_module_tl \tl_clear:N \__stex_copymodule_exec_tl %\prop_get:NnN \l_stex_current_copymodule_prop {fields} \l_tmpa_seq \seq_clear:N \__stex_copymodule_fields_seq \seq_map_inline:Nn \l__stex_copymodule_copymodule_modules_seq { \seq_map_inline:cn {c_stex_module_##1_constants}{ \tl_clear:N \__stex_copymodule_curr_symbol_tl % <- wrap in current symbol html \l_tmpa_cs{##1}{####1} \str_if_exist:cTF {l__stex_copymodule_copymodule_##1?####1_name_str} { \str_set_eq:Nc \__stex_copymodule_curr_name_str {l__stex_copymodule_copymodule_##1?####1_name_str} \stex_if_do_html:T { \tl_put_right:Nx \__stex_copymodule_curr_symbol_tl { \stex_annotate_invisible:nnn{alias}{\use:c{l__stex_copymodule_copymodule_##1?####1_name_str}}{} } } }{ \str_set:Nx \__stex_copymodule_curr_name_str { \l_stex_current_copymodule_name_str / ####1 } } \prop_set_eq:Nc \l_tmpa_prop {l_stex_symdecl_ ##1?####1 _prop} \prop_put:Nnx \l_tmpa_prop { name } \__stex_copymodule_curr_name_str \prop_put:Nnx \l_tmpa_prop { module } \l_stex_current_module_str \tl_if_exist:cT {l__stex_copymodule_copymodule_##1?####1_def_tl}{ \stex_if_do_html:T { \tl_put_right:Nx \__stex_copymodule_curr_symbol_tl { $\stex_annotate_invisible:nnn{definiens}{}{\exp_after:wN \exp_not:N\csname l__stex_copymodule_copymodule_##1?####1_def_tl\endcsname}$ } } \prop_put:Nnn \l_tmpa_prop { defined } { true } } \stex_add_constant_to_current_module:n \__stex_copymodule_curr_name_str \tl_put_right:Nx \__stex_copymodule_module_tl { \seq_clear:c {l_stex_symdecl_ \l_stex_current_module_str ? \__stex_copymodule_curr_name_str _notations} \prop_set_from_keyval:cn { l_stex_symdecl_\l_stex_current_module_str ? \__stex_copymodule_curr_name_str _prop }{ \prop_to_keyval:N \l_tmpa_prop } } \str_if_exist:cT {l__stex_copymodule_copymodule_##1?####1_macroname_str} { \stex_if_do_html:T { \tl_put_right:Nx \__stex_copymodule_curr_symbol_tl { \stex_annotate_invisible:nnn{macroname}{\use:c{l__stex_copymodule_copymodule_##1?####1_macroname_str}}{} } } \tl_put_right:Nx \__stex_copymodule_module_tl { \tl_set:cx {\use:c{l__stex_copymodule_copymodule_##1?####1_macroname_str}}{ \stex_invoke_symbol:n { \l_stex_current_module_str ? \__stex_copymodule_curr_name_str } } } } \seq_put_right:Nx \__stex_copymodule_fields_seq {\l_stex_current_module_str ? \__stex_copymodule_curr_name_str } \tl_put_right:Nx \__stex_copymodule_exec_tl { \stex_copy_notations:nn {\l_stex_current_module_str ? \__stex_copymodule_curr_name_str} { ##1 ? ####1 } } \tl_put_right:Nx \__stex_copymodule_exec_tl { \stex_if_do_html:TF{ \stex_annotate_invisible:nnn{assignment} {##1?####1} { \exp_after:wN \exp_not:n \exp_after:wN {\__stex_copymodule_curr_symbol_tl} } }{ \exp_after:wN \exp_not:n \exp_after:wN {\__stex_copymodule_curr_symbol_tl} } } } } \prop_put:Nno \l_stex_current_copymodule_prop {fields} \__stex_copymodule_fields_seq \tl_put_left:Nx \__stex_copymodule_module_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 } } \seq_gput_right:cx{c_stex_module_\l_stex_current_module_str _copymodules}{ \l_stex_current_module_str?\l_stex_current_copymodule_name_str } \exp_args:No \stex_execute_in_module:n \__stex_copymodule_module_tl \stex_debug:nn{copymodule}{result:\meaning \__stex_copymodule_module_tl} \stex_debug:nn{copymodule}{output:\meaning \__stex_copymodule_exec_tl} \__stex_copymodule_exec_tl \stex_if_do_html:T { \end{stex_annotate_env} } } \NewDocumentEnvironment {copymodule} { O{} m m}{ \stex_copymodule_start:nnnn { #1 }{ #2 }{ #3 }{ copymodule } \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 }{ interpretmodule } \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_copymodule_copymodule_##1?##2_def_tl }{ \str_if_eq:eeF { \prop_item:cn{ l_stex_symdecl_ ##1 ? ##2 _prop }{ defined } }{ true }{ \msg_error:nnxx{stex}{error/interpretmodule/nodefiniens}{ ##1?##2 }{\l_stex_current_copymodule_name_str} } } } } \iffalse \begin{stex_annotate_env} \fi \NewDocumentEnvironment {realization} { O{} m}{ \stex_copymodule_start:nnnn { #1 }{ #2 }{ #2 }{ realize } \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 \donotcopy \stex_reactivate_macro:N \assign \stex_smsmode_do: }{ \stex_import_module_uri:nn { #1 } { #2 } \tl_clear:N \__stex_copymodule_exec_tl \tl_set:Nx \__stex_copymodule_module_tl { \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 } } \seq_map_inline:Nn \l__stex_copymodule_copymodule_modules_seq { \seq_map_inline:cn {c_stex_module_##1_constants}{ \str_set:Nx \__stex_copymodule_curr_name_str { \l_stex_current_copymodule_name_str / ####1 } \tl_if_exist:cT {l__stex_copymodule_copymodule_##1?####1_def_tl}{ \stex_if_do_html:T { \tl_put_right:Nx \__stex_copymodule_exec_tl { \stex_annotate_invisible:nnn{assignment} {##1?####1} { $\stex_annotate_invisible:nnn{definiens}{}{\exp_after:wN \exp_not:N\csname l__stex_copymodule_copymodule_##1?####1_def_tl\endcsname}$ } } } \tl_put_right:Nx \__stex_copymodule_module_tl { \prop_put:cnn {l_stex_symdecl_##1?####1_prop}{ defined }{ true } } } }} \exp_args:No \stex_execute_in_module:n \__stex_copymodule_module_tl \__stex_copymodule_exec_tl \stex_if_do_html:T {\end{stex_annotate_env}} } \NewDocumentCommand \donotcopy { m }{ \str_clear:N \l_stex_import_name_str \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_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 { \stex_if_do_html:T { \stex_if_smsmode:F { \stex_annotate_invisible:nnn{donotcopy}{##1}{ \stex_annotate:nnn{domain}{##1}{} } } } \str_set_eq:NN \l_stex_import_name_str \l_tmpb_str } } \seq_map_inline:cn {c_stex_module_##1_copymodules}{ \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 {\seq_map_break:n { \stex_if_do_html:T { \stex_if_smsmode:F { \stex_annotate_invisible:nnn{donotcopy}{####1}{ \stex_annotate:nnn{domain}{ \prop_item:cn {l_stex_copymodule_ ####1 _prop}{module} }{} } } } \str_set:Nx \l_stex_import_name_str { \prop_item:cn {l_stex_copymodule_ ####1 _prop}{module} } }} } } } \str_if_empty:NTF \l_stex_import_name_str { % TODO throw error }{ \stex_collect_imports:n {\l_stex_import_name_str } \seq_map_inline:Nn \l_stex_collect_imports_seq { \seq_remove_all:Nn \l__stex_copymodule_copymodule_modules_seq { ##1 } \seq_map_inline:cn {c_stex_module_##1_constants}{ \seq_remove_all:Nn \l__stex_copymodule_copymodule_fields_seq { ##1 ? ####1 } \bool_lazy_any:nT { { \cs_if_exist_p:c {l__stex_copymodule_copymodule_##1?####1_name_str}} { \cs_if_exist_p:c {l__stex_copymodule_copymodule_##1?####1_macroname_str}} { \cs_if_exist_p:c {l__stex_copymodule_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_name_str } \prop_put:Nno \l_stex_current_copymodule_prop {includes} \l_tmpa_seq } \stex_smsmode_do: } \NewDocumentCommand \assign { m m }{ \stex_get_symbol_in_seq:nn {#1} \l__stex_copymodule_copymodule_fields_seq \stex_debug:nn{assign}{defining~{\l_stex_get_symbol_uri_str}~as~\detokenize{#2}} \tl_set:cn {l__stex_copymodule_copymodule_\l_stex_get_symbol_uri_str _def_tl}{#2} \stex_smsmode_do: } \keys_define:nn { stex / renamedecl } { name .str_set_x:N = \l_stex_renamedecl_name_str } \cs_new_protected:Nn \__stex_copymodule_renamedecl_args:n { \str_clear:N \l_stex_renamedecl_name_str \keys_set:nn { stex / renamedecl } { #1 } } \NewDocumentCommand \renamedecl { O{} m m}{ \__stex_copymodule_renamedecl_args:n { #1 } \stex_get_symbol_in_seq:nn {#2} \l__stex_copymodule_copymodule_fields_seq \stex_debug:nn{renamedecl}{renaming~{\l_stex_get_symbol_uri_str}~to~#3} \str_set:cx {l__stex_copymodule_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_copymodule_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_copymodule_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_smsmode_do: } \stex_deactivate_macro:Nn \assign {copymodules} \stex_deactivate_macro:Nn \renamedecl {copymodules} \stex_deactivate_macro:Nn \donotcopy {copymodules} \NewDocumentEnvironment{structural_feature_module}{ 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_eq:NN \l_stex_feature_parent_str \l_stex_current_module_str \stex_module_setup:nn{meta=NONE}{#2 - #1} \stex_if_do_html:T { \begin{stex_annotate_env}{ feature:#1 }{\l_stex_feature_parent_str ? #2 - #1} \stex_annotate_invisible:nnn{header}{}{ #3 } } }{ \str_gset_eq:NN \l_stex_last_feature_str \l_stex_current_module_str \prop_gput:cnn {c_stex_module_ \l_stex_current_module_str _prop}{feature}{#1} \stex_debug:nn{features}{ Feature: \l_stex_last_feature_str } \stex_if_do_html:T { \end{stex_annotate_env} } } \cs_new_protected:Nn \stex_add_structure_to_current_module:nn { \prop_if_exist:cF {c_stex_module_\l_stex_current_module_str _structures}{ \prop_new:c {c_stex_module_\l_stex_current_module_str _structures} } \prop_gput:cxx{c_stex_module_\l_stex_current_module_str _structures} {#1}{#2} } \keys_define:nn { stex / features / structure } { name .str_set_x:N = \l__stex_structures_name_str , } \cs_new_protected:Nn \__stex_structures_structure_args:n { \str_clear:N \l__stex_structures_name_str \keys_set:nn { stex / features / structure } { #1 } } \NewDocumentEnvironment{mathstructure}{m O{}}{ \__stex_structures_structure_args:n { #2 } \str_if_empty:NT \l__stex_structures_name_str { \str_set:Nx \l__stex_structures_name_str { #1 } } \stex_suppress_html:n { \bool_set_true:N \l_stex_symdecl_make_macro_bool \exp_args:Nx \stex_symdecl_do:nn { name = \l__stex_structures_name_str , def = {\STEXsymbol{module-type}{ \STEXInternalTermMathOMSiiii { \prop_item:cn {c_stex_module_\l_stex_current_module_str _prop} { ns } ? \prop_item:cn {c_stex_module_\l_stex_current_module_str _prop} { name } / \l__stex_structures_name_str - structure }{}{0}{} }} }{ #1 } } \exp_args:Nnnx \begin{structural_feature_module}{ structure } { \l__stex_structures_name_str }{} \stex_smsmode_do: }{ \end{structural_feature_module} \_stex_reset_up_to_module:n \l_stex_last_feature_str \exp_args:No \stex_collect_imports:n \l_stex_last_feature_str \seq_clear:N \l_tmpa_seq \seq_map_inline:Nn \l_stex_collect_imports_seq { \seq_map_inline:cn{c_stex_module_##1_constants}{ \seq_put_right:Nn \l_tmpa_seq { ##1 ? ####1 } } } \exp_args:Nnno \prop_gput:cnn {c_stex_module_ \l_stex_last_feature_str _prop}{fields}\l_tmpa_seq \stex_debug:nn{structure}{Fields:~\seq_use:Nn \l_tmpa_seq ,} \stex_add_structure_to_current_module:nn \l__stex_structures_name_str \l_stex_last_feature_str \stex_execute_in_module:x { \tl_set:cn { #1 }{ \exp_not:N \stex_invoke_structure:nn {\l_stex_current_module_str }{ \l__stex_structures_name_str} } } } \cs_new:Nn \stex_invoke_structure:nn { \stex_invoke_symbol:n { #1?#2 } } \cs_new_protected:Nn \stex_get_structure:n { \tl_if_head_eq_catcode:nNTF { #1 } \relax { \tl_set:Nn \l_tmpa_tl { #1 } \__stex_structures_get_from_cs: }{ \cs_if_exist:cTF { #1 }{ \cs_set_eq:Nc \l_tmpa_cs { #1 } \str_set:Nx \l_tmpa_str {\cs_argument_spec:N \l_tmpa_cs } \str_if_empty:NTF \l_tmpa_str { \cs_if_eq:NNTF { \tl_head:N \l_tmpa_cs} \stex_invoke_structure:nn { \__stex_structures_get_from_cs: }{ \__stex_structures_get_from_string:n { #1 } } }{ \__stex_structures_get_from_string:n { #1 } } }{ \__stex_structures_get_from_string:n { #1 } } } } \cs_new_protected:Nn \__stex_structures_get_from_cs: { \exp_args:NNx \tl_set:Nn \l_tmpa_tl { \tl_tail:N \l_tmpa_tl } \str_set:Nx \l_tmpa_str { \exp_after:wN \use_i:nn \l_tmpa_tl } \str_set:Nx \l_tmpb_str { \exp_after:wN \use_ii:nn \l_tmpa_tl } \str_set:Nx \l_stex_get_structure_str { \l_tmpa_str ? \l_tmpb_str } \str_set:Nx \l_stex_get_structure_module_str { \exp_args:Nno \prop_item:cn {c_stex_module_\l_tmpa_str _structures}{\l_tmpb_str} } } \cs_new_protected:Nn \__stex_structures_get_from_string:n { \tl_set:Nn \l_tmpa_tl { \msg_error:nnn{stex}{error/unknownstructure}{#1} } \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_all_modules_seq { \prop_if_exist:cT {c_stex_module_##1_structures} { \prop_map_inline:cn {c_stex_module_##1_structures} { \str_if_eq:eeT { \l_tmpa_str }{ \str_range:nnn {##1?####1}{-\l_tmpa_int}{-1}}{ \prop_map_break:n{\seq_map_break:n{ \tl_set:Nn \l_tmpa_tl { \str_set:Nn \l_stex_get_structure_str {##1?####1} \str_set:Nn \l_stex_get_structure_module_str {####2} } }} } } } } \l_tmpa_tl } \keys_define:nn { stex / instantiate } { name .str_set_x:N = \l__stex_structures_name_str } \cs_new_protected:Nn \__stex_structures_instantiate_args:n { \str_clear:N \l__stex_structures_name_str \keys_set:nn { stex / instantiate } { #1 } } \NewDocumentCommand \instantiate {m O{} m m O{}}{ \begingroup \stex_get_structure:n {#3} \__stex_structures_instantiate_args:n { #2 } \str_if_empty:NT \l__stex_structures_name_str { \str_set:Nn \l__stex_structures_name_str { #1 } } \exp_args:No \stex_activate_module:n \l_stex_get_structure_module_str \seq_clear:N \l__stex_structures_fields_seq \exp_args:Nx \stex_collect_imports:n \l_stex_get_structure_module_str \seq_map_inline:Nn \l_stex_collect_imports_seq { \seq_map_inline:cn {c_stex_module_##1_constants}{ \seq_put_right:Nx \l__stex_structures_fields_seq { ##1 ? ####1 } } } \tl_if_empty:nF{#5}{ \seq_set_split:Nnn \l_tmpa_seq , {#5} \prop_clear:N \l_tmpa_prop \seq_map_inline:Nn \l_tmpa_seq { \seq_set_split:Nnn \l_tmpb_seq = { ##1 } \int_compare:nNnF { \seq_count:N \l_tmpb_seq } = 2 { \msg_error:nnn{stex}{error/keyval}{##1} } \exp_args:Nx \stex_get_symbol_in_seq:nn {\seq_item:Nn \l_tmpb_seq 1} \l__stex_structures_fields_seq \str_set_eq:NN \l__stex_structures_dom_str \l_stex_get_symbol_uri_str \exp_args:NNx \seq_remove_all:Nn \l__stex_structures_fields_seq \l_stex_get_symbol_uri_str \exp_args:Nx \stex_get_symbol:n {\seq_item:Nn \l_tmpb_seq 2} \exp_args:Nxx \str_if_eq:nnF {\prop_item:cn{l_stex_symdecl_\l__stex_structures_dom_str _prop}{args}} {\prop_item:cn{l_stex_symdecl_\l_stex_get_symbol_uri_str _prop}{args}}{ \msg_error:nnxxxx{stex}{error/incompatible} {\l__stex_structures_dom_str} {\prop_item:cn{l_stex_symdecl_\l__stex_structures_dom_str _prop}{args}} {\l_stex_get_symbol_uri_str} {\prop_item:cn{l_stex_symdecl_\l_stex_get_symbol_uri_str _prop}{args}} } \prop_put:Nxx \l_tmpa_prop {\seq_item:Nn \l_tmpb_seq 1} \l_stex_get_symbol_uri_str } } \seq_map_inline:Nn \l__stex_structures_fields_seq { \str_set:Nx \l_tmpa_str {field:\l__stex_structures_name_str . \prop_item:cn {l_stex_symdecl_##1_prop}{name} } \stex_debug:nn{instantiate}{Field~\l_tmpa_str :~##1} \stex_add_constant_to_current_module:n {\l_tmpa_str} \stex_execute_in_module:x { \prop_set_from_keyval:cn { l_stex_symdecl_ \l_stex_current_module_str?\l_tmpa_str _prop}{ name = \l_tmpa_str , args = \prop_item:cn {l_stex_symdecl_##1_prop}{args} , arity = \prop_item:cn {l_stex_symdecl_##1_prop}{arity} , assocs = \prop_item:cn {l_stex_symdecl_##1_prop}{assocs} } \seq_clear:c {l_stex_symdecl_\l_stex_current_module_str?\l_tmpa_str _notations} } \seq_if_empty:cF{l_stex_symdecl_##1_notations}{ \stex_find_notation:nn{##1}{} \stex_execute_in_module:x { \seq_put_right:cn {l_stex_symdecl_\l_stex_current_module_str?\l_tmpa_str _notations}{\l_stex_notation_variant_str} } \stex_copy_control_sequence_ii:ccN {stex_notation_\l_stex_current_module_str?\l_tmpa_str\c_hash_str \l_stex_notation_variant_str _cs} {stex_notation_##1\c_hash_str \l_stex_notation_variant_str _cs} \l_tmpa_tl \exp_args:No \stex_execute_in_module:n \l_tmpa_tl \cs_if_exist:cT{stex_op_notation_##1\c_hash_str \l_stex_notation_variant_str _cs}{ \tl_set_eq:Nc \l_tmpa_cs {stex_op_notation_##1\c_hash_str \l_stex_notation_variant_str _cs} \stex_execute_in_module:x { \tl_set:cn {stex_op_notation_\l_stex_current_module_str?\l_tmpa_str\c_hash_str \l_stex_notation_variant_str _cs} { \exp_args:No \exp_not:n \l_tmpa_cs} } } } \prop_put:Nxx \l_tmpa_prop {\prop_item:cn {l_stex_symdecl_##1_prop}{name}}{\l_stex_current_module_str?\l_tmpa_str} } \stex_execute_in_module:x { \prop_set_from_keyval:cn {l_stex_instance_\l_stex_current_module_str?\l__stex_structures_name_str _prop}{ domain = \l_stex_get_structure_module_str , \prop_to_keyval:N \l_tmpa_prop } \tl_set:cn{ #1 }{\stex_invoke_instance:n{ \l_stex_current_module_str?\l__stex_structures_name_str} } } \stex_debug:nn{instantiate}{ Instance~\l_stex_current_module_str?\l__stex_structures_name_str \\ \prop_to_keyval:N \l_tmpa_prop } \exp_args:Nxx \stex_symdecl_do:nn { type={\STEXsymbol{module-type}{ \STEXInternalTermMathOMSiiii { \l_stex_get_structure_module_str }{}{0}{} }} }{\l__stex_structures_name_str} \str_set:Nx \l_stex_get_symbol_uri_str {\l_stex_current_module_str?\l__stex_structures_name_str} \tl_set:Nn \l_stex_notation_after_do_tl {\__stex_notation_final:} \stex_notation_do:nnnnn{}{0}{}{}{\comp{#4}} % } %\exp_args:Nx \notation{\l__stex_structures_name_str}{\comp{#5}} \endgroup \stex_smsmode_do:\ignorespacesandpars } \cs_new_protected:Nn \stex_symbol_or_var:n { \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_variable:n { \bool_set_true:N \l_stex_symbol_or_var_bool \bool_set_false:N \l_stex_instance_or_symbol_bool \tl_set:Nx \l_tmpa_tl {\tl_tail:N \l_tmpa_tl} \tl_set:Nx \l_tmpa_tl {\exp_after:wN \use:n \l_tmpa_tl} \str_set:Nx \l_stex_get_symbol_uri_str { \exp_after:wN \use:n \l_tmpa_tl } }{ % TODO \stex_invoke_varinstance:n \exp_args:Nx \cs_if_eq:NNTF { \tl_head:N \l_tmpa_tl } \stex_invoke_varinstance:n { \bool_set_true:N \l_stex_symbol_or_var_bool \bool_set_true:N \l_stex_instance_or_symbol_bool \tl_set:Nx \l_tmpa_tl {\tl_tail:N \l_tmpa_tl} \tl_set:Nx \l_tmpa_tl {\exp_after:wN \use:n \l_tmpa_tl} \str_set:Nx \l_stex_get_symbol_uri_str { \exp_after:wN \use:n \l_tmpa_tl } }{ \bool_set_false:N \l_stex_symbol_or_var_bool \stex_get_symbol:n{#1} } } }{ \__stex_structures_symbolorvar_from_string:n{ #1 } } }{ \__stex_structures_symbolorvar_from_string:n{ #1 } } } \cs_new_protected:Nn \__stex_structures_symbolorvar_from_string:n { \prop_if_exist:cTF {l_stex_variable_#1 _prop}{ \bool_set_true:N \l_stex_symbol_or_var_bool \str_set:Nn \l_stex_get_symbol_uri_str { #1 } }{ \bool_set_false:N \l_stex_symbol_or_var_bool \stex_get_symbol:n{#1} } } \keys_define:nn { stex / varinstantiate } { name .str_set_x:N = \l__stex_structures_name_str, bind .choices:nn = {forall,exists} {\str_set:Nx \l__stex_structures_bind_str {\l_keys_choice_tl}} } \cs_new_protected:Nn \__stex_structures_varinstantiate_args:n { \str_clear:N \l__stex_structures_name_str \str_clear:N \l__stex_structures_bind_str \keys_set:nn { stex / varinstantiate } { #1 } } \NewDocumentCommand \varinstantiate {m O{} m m O{}}{ \begingroup \stex_get_structure:n {#3} \__stex_structures_varinstantiate_args:n { #2 } \str_if_empty:NT \l__stex_structures_name_str { \str_set:Nn \l__stex_structures_name_str { #1 } } \stex_if_do_html:TF{ \stex_annotate:nnn{varinstance}{\l__stex_structures_name_str} }{\use:n} { \stex_if_do_html:T{ \stex_annotate_invisible:nnn{domain}{\l_stex_get_structure_module_str}{} } \seq_clear:N \l__stex_structures_fields_seq \exp_args:Nx \stex_collect_imports:n \l_stex_get_structure_module_str \seq_map_inline:Nn \l_stex_collect_imports_seq { \seq_map_inline:cn {c_stex_module_##1_constants}{ \seq_put_right:Nx \l__stex_structures_fields_seq { ##1 ? ####1 } } } \exp_args:No \stex_activate_module:n \l_stex_get_structure_module_str \prop_clear:N \l_tmpa_prop \tl_if_empty:nF {#5} { \seq_set_split:Nnn \l_tmpa_seq , {#5} \seq_map_inline:Nn \l_tmpa_seq { \seq_set_split:Nnn \l_tmpb_seq = { ##1 } \int_compare:nNnF { \seq_count:N \l_tmpb_seq } = 2 { \msg_error:nnn{stex}{error/keyval}{##1} } \exp_args:Nx \stex_get_symbol_in_seq:nn {\seq_item:Nn \l_tmpb_seq 1} \l__stex_structures_fields_seq \str_set_eq:NN \l__stex_structures_dom_str \l_stex_get_symbol_uri_str \exp_args:NNx \seq_remove_all:Nn \l__stex_structures_fields_seq \l_stex_get_symbol_uri_str \exp_args:Nx \stex_symbol_or_var:n {\seq_item:Nn \l_tmpb_seq 2} \stex_if_do_html:T{ \stex_annotate:nnn{assign}{\l__stex_structures_dom_str, \bool_if:NTF\l_stex_symbol_or_var_bool{var://}{}\l_stex_get_symbol_uri_str}{} } \bool_if:NTF \l_stex_symbol_or_var_bool { \exp_args:Nxx \str_if_eq:nnF {\prop_item:cn{l_stex_symdecl_\l__stex_structures_dom_str _prop}{args}} {\prop_item:cn{l_stex_variable_\l_stex_get_symbol_uri_str _prop}{args}}{ \msg_error:nnxxxx{stex}{error/incompatible} {\l__stex_structures_dom_str} {\prop_item:cn{l_stex_symdecl_\l__stex_structures_dom_str _prop}{args}} {\l_stex_get_symbol_uri_str} {\prop_item:cn{l_stex_variable_\l_stex_get_symbol_uri_str _prop}{args}} } \prop_put:Nxx \l_tmpa_prop {\seq_item:Nn \l_tmpb_seq 1} {\stex_invoke_variable:n {\l_stex_get_symbol_uri_str}} }{ \exp_args:Nxx \str_if_eq:nnF {\prop_item:cn{l_stex_symdecl_\l__stex_structures_dom_str _prop}{args}} {\prop_item:cn{l_stex_symdecl_\l_stex_get_symbol_uri_str _prop}{args}}{ \msg_error:nnxxxx{stex}{error/incompatible} {\l__stex_structures_dom_str} {\prop_item:cn{l_stex_symdecl_\l__stex_structures_dom_str _prop}{args}} {\l_stex_get_symbol_uri_str} {\prop_item:cn{l_stex_symdecl_\l_stex_get_symbol_uri_str _prop}{args}} } \prop_put:Nxx \l_tmpa_prop {\seq_item:Nn \l_tmpb_seq 1} {\stex_invoke_symbol:n {\l_stex_get_symbol_uri_str}} } } } \tl_gclear:N \g__stex_structures_aftergroup_tl \seq_map_inline:Nn \l__stex_structures_fields_seq { \str_set:Nx \l_tmpa_str {\l__stex_structures_name_str . \prop_item:cn {l_stex_symdecl_##1_prop}{name} } \stex_debug:nn{varinstantiate}{Field~\l_tmpa_str :~##1} \seq_if_empty:cF{l_stex_symdecl_##1_notations}{ \stex_find_notation:nn{##1}{} \cs_gset_eq:cc{g__stex_structures_tmpa_\l_tmpa_str _cs} {stex_notation_##1\c_hash_str \l_stex_notation_variant_str _cs} \stex_debug:nn{varinstantiate}{Notation:~\cs_meaning:c{g__stex_structures_tmpa_\l_tmpa_str _cs}} \cs_if_exist:cT{stex_op_notation_##1\c_hash_str \l_stex_notation_variant_str _cs}{ \cs_gset_eq:cc {g__stex_structures_tmpa_op_\l_tmpa_str _cs} {stex_op_notation_##1\c_hash_str \l_stex_notation_variant_str _cs} \stex_debug:nn{varinstantiate}{Operator~Notation:~\cs_meaning:c{g__stex_structures_tmpa_op_\l_tmpa_str _cs}} } } \exp_args:NNx \tl_gput_right:Nn \g__stex_structures_aftergroup_tl { \prop_set_from_keyval:cn { l_stex_variable_ \l_tmpa_str _prop}{ name = \l_tmpa_str , args = \prop_item:cn {l_stex_symdecl_##1_prop}{args} , arity = \prop_item:cn {l_stex_symdecl_##1_prop}{arity} , assocs = \prop_item:cn {l_stex_symdecl_##1_prop}{assocs} } \cs_set_eq:cc {stex_var_notation_\l_tmpa_str _cs} {g__stex_structures_tmpa_\l_tmpa_str _cs} \cs_set_eq:cc {stex_var_op_notation_\l_tmpa_str _cs} {g__stex_structures_tmpa_op_\l_tmpa_str _cs} } \prop_put:Nxx \l_tmpa_prop {\prop_item:cn {l_stex_symdecl_##1_prop}{name}}{\stex_invoke_variable:n {\l_tmpa_str}} } \exp_args:NNx \tl_gput_right:Nn \g__stex_structures_aftergroup_tl { \prop_set_from_keyval:cn {l_stex_varinstance_\l__stex_structures_name_str _prop }{ domain = \l_stex_get_structure_module_str , \prop_to_keyval:N \l_tmpa_prop } \tl_set:cn { #1 }{\stex_invoke_varinstance:n {\l__stex_structures_name_str}} \tl_set:cn {l_stex_varinstance_\l__stex_structures_name_str _op_tl}{ \exp_args:Nnx \exp_not:N \use:nn { \str_set:Nn \exp_not:N \STEXInternalCurrentSymbolStr {var://\l__stex_structures_name_str} \_stex_term_omv:nn {var://\l__stex_structures_name_str}{ \exp_not:n{ \_varcomp{#4} } } }{ \exp_not:n{\_stex_reset:N \STEXInternalCurrentSymbolStr} } } } } \stex_debug:nn{varinstantiate}{\expandafter\detokenize\expandafter{\g__stex_structures_aftergroup_tl}} \aftergroup\g__stex_structures_aftergroup_tl \endgroup \stex_smsmode_do:\ignorespacesandpars } \cs_new_protected:Nn \stex_invoke_instance:n { \peek_charcode_remove:NTF ! { \stex_invoke_symbol:n{#1} }{ \_stex_invoke_instance:nn {#1} } } \cs_new_protected:Nn \stex_invoke_varinstance:n { \peek_charcode_remove:NTF ! { \exp_args:Nnx \use:nn { \def\comp{\_varcomp} \use:c{l_stex_varinstance_#1_op_tl} }{ \_stex_reset:N \comp } }{ \_stex_invoke_varinstance:nn {#1} } } \cs_new_protected:Nn \_stex_invoke_instance:nn { \prop_if_in:cnTF {l_stex_instance_ #1 _prop}{#2}{ \exp_args:Nx \stex_invoke_symbol:n {\prop_item:cn{l_stex_instance_ #1 _prop}{#2}} }{ \prop_set_eq:Nc \l_tmpa_prop{l_stex_instance_ #1 _prop} \msg_error:nnxxx{stex}{error/unknownfield}{#2}{#1}{ \prop_to_keyval:N \l_tmpa_prop } } } \cs_new_protected:Nn \_stex_invoke_varinstance:nn { \prop_if_in:cnTF {l_stex_varinstance_ #1 _prop}{#2}{ \prop_get:cnN{l_stex_varinstance_ #1 _prop}{#2}\l_tmpa_tl \l_tmpa_tl }{ \msg_error:nnnnn{stex}{error/unknownfield}{#2}{#1}{} } } \cs_new_protected:Nn \stex_invoke_structure:nnn { \tl_if_empty:nTF{ #3 }{ \prop_set_eq:Nc \l__stex_structures_structure_prop { c_stex_feature_ #2 _prop } \tl_clear:N \l_tmpa_tl \prop_get:NnN \l__stex_structures_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 \stex_html_backend: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 } } \str_replace_all:Nnn \l_tmpa_str {-} {~} \stex_html_backend:TF { \stex_if_do_html:T { \stex_annotate:nnn { definiendum } { \l_stex_get_symbol_uri_str } { \l_tmpa_str\l__stex_statements_definiendum_post_tl } } } { \exp_args:Nnx \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 \stex_html_backend:TF { \stex_if_do_html:T { \stex_annotate:nnn { definiendum } { \l_stex_get_symbol_uri_str } { \exp_after:wN \stex_capitalize:n \l_tmpa_str\l__stex_statements_definiendum_post_tl } } } { \exp_args:Nnx \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 }{ \noindent\stex_annotate:nnn{ premise }{}{\ignorespaces #1 } } \NewDocumentCommand \conclusion { m }{ \noindent\stex_annotate:nnn{ conclusion }{}{\ignorespaces #1 } } \NewDocumentCommand \definiens { O{} m }{ \str_clear:N \l_stex_get_symbol_uri_str \tl_if_empty:nF {#1} { \stex_get_symbol:n { #1 } } \str_if_empty:NT \l_stex_get_symbol_uri_str { \int_compare:nNnTF {\clist_count:N \l__stex_statements_sdefinition_for_clist} = 1 { \str_set:Nx \l_stex_get_symbol_uri_str {\clist_item:Nn \l__stex_statements_sdefinition_for_clist 1} }{ % TODO throw error } } \str_if_eq:eeT {\prop_item:cn {l_stex_symdecl_ \l_stex_get_symbol_uri_str _prop}{module}} {\l_stex_current_module_str}{ \str_if_eq:eeF {\prop_item:cn {l_stex_symdecl_ \l_stex_get_symbol_uri_str _prop}{defined}} {true}{ \prop_put:cnn{l_stex_symdecl_ \l_stex_get_symbol_uri_str _prop}{defined}{true} \exp_args:Nx \stex_add_to_current_module:n { \prop_put:cnn{l_stex_symdecl_ \l_stex_get_symbol_uri_str _prop}{defined}{true} } } } \stex_annotate:nnn{ definiens }{\l_stex_get_symbol_uri_str}{ #2 } } \NewDocumentCommand \varbindforall {m}{ \stex_symbol_or_var:n {#1} \bool_if:NTF\l_stex_symbol_or_var_bool{ \stex_if_do_html:T { \stex_annotate_invisible:nnn {bindtype}{forall,\l_stex_get_symbol_uri_str}{} } }{ % todo throw error } } \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} \stex_deactivate_macro:Nn \varbindforall {definition~or~assertion~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_reactivate_macro:N \varbindforall \stex_if_smsmode:F{ \seq_clear:N \l_tmpb_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_tmpb_seq { \l_stex_get_symbol_uri_str } } } \clist_set_from_seq:NN \l__stex_statements_sdefinition_for_clist \l_tmpb_seq \exp_args:Nnnx \begin{stex_annotate_env}{definition}{\seq_use:Nn \l_tmpb_seq {,}} \str_if_empty:NF \sdefinitiontype { \stex_annotate_invisible:nnn{typestrings}{\sdefinitiontype}{} } \str_if_empty:NF \sdefinitionname { \stex_annotate_invisible:nnn{statementname}{\sdefinitionname}{} } \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: }{ \stex_suppress_html:n { \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: { \stex_par:\noindent\titleemph{Definition\tl_if_empty:NF \sdefinitiontitle { ~(\sdefinitiontitle) }~} } \cs_new_protected:Nn \__stex_statements_sdefinition_end: {\stex_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_reactivate_macro:N \varbindforall \stex_ref_new_doc_target:n \sdefinitionid \stex_if_smsmode:TF{\stex_suppress_html:n { \str_if_empty:NF \sdefinitionname { \stex_symdecl_do:nn{}{\sdefinitionname} } }}{ \seq_clear:N \l_tmpb_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_tmpb_seq { \l_stex_get_symbol_uri_str } } } \clist_set_from_seq:NN \l__stex_statements_sdefinition_for_clist \l_tmpb_seq \exp_args:Nnx \stex_annotate:nnn{definition}{\seq_use:Nn \l_tmpb_seq {,}}{ \str_if_empty:NF \sdefinitiontype { \stex_annotate_invisible:nnn{typestrings}{\sdefinitiontype}{} } #2 \str_if_empty:NF \sdefinitionname { \stex_suppress_html:n{\stex_symdecl_do:nn{}{\sdefinitionname}} \stex_annotate_invisible:nnn{statementname}{\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_reactivate_macro:N \varbindforall \stex_if_smsmode:F { \seq_clear:N \l_tmpb_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_tmpb_seq { \l_stex_get_symbol_uri_str } } } \exp_args:Nnnx \begin{stex_annotate_env}{assertion}{\seq_use:Nn \l_tmpb_seq {,}} \str_if_empty:NF \sassertiontype { \stex_annotate_invisible:nnn{type}{\sassertiontype}{} } \str_if_empty:NF \sassertionname { \stex_annotate_invisible:nnn{statementname}{\sassertionname}{} } \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_suppress_html:n{\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: { \stex_par:\noindent\titleemph{Assertion~\tl_if_empty:NF \sassertiontitle { (\sassertiontitle) }~} } \cs_new_protected:Nn \__stex_statements_sassertion_end: {\stex_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_reactivate_macro:N \varbindforall \__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_suppress_html:n{\stex_symdecl_do:nn{}{\sassertionname}} \stex_ref_new_sym_target:n {\l_stex_current_module_str ? \sassertionname} } }{ \seq_clear:N \l_tmpb_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_tmpb_seq { \l_stex_get_symbol_uri_str } } } \exp_args:Nnx \stex_annotate:nnn{assertion}{\seq_use:Nn \l_tmpb_seq {,}}{ \str_if_empty:NF \sassertiontype { \stex_annotate_invisible:nnn{typestrings}{\sassertiontype}{} } #2 \str_if_empty:NF \sassertionname { \stex_suppress_html:n{\stex_symdecl_do:nn{}{\sassertionname}} \stex_ref_new_sym_target:n {\l_stex_current_module_str ? \sassertionname} \stex_annotate_invisible:nnn{statementname}{\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, name .str_set_x:N = \sexamplename , 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 \str_clear:N \sexamplename \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_tmpb_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_tmpb_seq { \l_stex_get_symbol_uri_str } } } \exp_args:Nnnx \begin{stex_annotate_env}{example}{\seq_use:Nn \l_tmpb_seq {,}} \str_if_empty:NF \sexampletype { \stex_annotate_invisible:nnn{typestrings}{\sexampletype}{} } \str_if_empty:NF \sexamplename { \stex_annotate_invisible:nnn{statementname}{\sexamplename}{} } \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_suppress_html:n{\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: { \stex_par:\noindent\titleemph{Example~\tl_if_empty:NF \sexampletitle { (\sexampletitle) }~} } \cs_new_protected:Nn \__stex_statements_sexample_end: {\stex_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_suppress_html:n{\stex_symdecl_do:nn{}{\examplename}} } }{ \seq_clear:N \l_tmpb_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_tmpb_seq { \l_stex_get_symbol_uri_str } } } \exp_args:Nnx \stex_annotate:nnn{example}{\seq_use:Nn \l_tmpb_seq {,}}{ \str_if_empty:NF \sexampletype { \stex_annotate_invisible:nnn{typestrings}{\sexampletype}{} } #2 \str_if_empty:NF \sexamplename { \stex_suppress_html:n{\stex_symdecl_do:nn{}{\sexamplename}} \stex_annotate_invisible:nnn{statementname}{\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 , imports .tl_set:N = \l__stex_statements_sparagraph_imports_tl } \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 \tl_clear:N \l__stex_statements_sparagraph_imports_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_tmpb_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_tmpb_seq { \l_stex_get_symbol_uri_str } } } \exp_args:Nnnx \begin{stex_annotate_env}{paragraph}{\seq_use:Nn \l_tmpb_seq {,}} \str_if_empty:NF \sparagraphtype { \stex_annotate_invisible:nnn{typestrings}{\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_annotate_invisible:nnn{statementname}{\sparagraphname}{} } \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:}} } } \stex_csl_to_imports:No \usemodule \l__stex_statements_sparagraph_imports_tl \tl_if_empty:NTF \l_tmpa_tl { \__stex_statements_sparagraph_start: }{ \l_tmpa_tl } } \clist_set:No \l_tmpa_clist \sparagraphtype \exp_args:NNx \clist_if_in:NnT \l_tmpa_clist {\tl_to_str:n{symdoc}} { \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 } \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_suppress_html:n{\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: { \stex_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: {\stex_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_suppress_html:n{\stex_symdecl_do:nn{}{\sparagraphname}} \stex_ref_new_sym_target:n {\l_stex_current_module_str ? \sparagraphname} } }{ \seq_clear:N \l_tmpb_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_tmpb_seq { \l_stex_get_symbol_uri_str } } } \exp_args:Nnx \stex_annotate:nnn{paragraph}{\seq_use:Nn \l_tmpb_seq {,}}{ \str_if_empty:NF \sparagraphtype { \stex_annotate_invisible:nnn{typestrings}{\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_suppress_html:n{\stex_symdecl_do:nn{}{\sparagraphname}} \stex_annotate_invisible:nnn{statementname}{\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_tmpb_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\stexpatchproof[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 \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 \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}{} } \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{spfcomment}[1][]{ \__stex_sproof_spf_args:n{#1} \clist_set:No \l_tmpa_clist \spftype \tl_set:Nn \l_tmpa_tl { \item[\sproofnumber] \bool_set_true:N \l__stex_sproof_inc_counter_bool } \clist_map_inline:Nn \l_tmpa_clist { \exp_args:No \str_if_eq:nnT \c__stex_sproof_flow_str {##1} { \tl_clear:N \l_tmpa_tl } } \l_tmpa_tl }{ \bool_if:NT \l__stex_sproof_inc_counter_bool { \__stex_sproof_inc_counter: } } \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 } \newcommand\spfjust[1][]{} \newcommand\stex_proof_premise:[2][]{#2} \newcommand\justarg[2][]{#2} %%%%%%%%%%%%% metatheory.dtx %%%%%%%%%%%%% \str_const:Nn \c_stex_metatheory_ns_str {http://mathhub.info/sTeX/meta} \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,op=:]{#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,assoc=pre] \notation{bind}[depfun,prec=nobrackets,op={(\cdot)\;\to\;\cdot}]{\comp( #1 \comp{)\;\to\;} #2}{##1 \comp, ##2} \notation{bind}[forall]{\comp\forall #1.\;#2}{##1 \comp, ##2} \notation{bind}[Pi]{\comp\prod_{#1}#2}{##1 \comp, ##2} % implicit bind \symdecl{implicitbind}[args=Bi,assoc=pre] \notation{implicitbind}[braces,prec=nobrackets,op={\{\cdot\}_I\;\cdot}]{\comp\{ #1 \comp{\}_I\;} #2}{##1 \comp, ##2} \notation{implicitbind}[depfun,prec=nobrackets]{\comp( #1 \comp{)\;\to_I\;} #2}{##1 \comp, ##2} \notation{implicitbind}[Pi]{\comp\prod^I_{#1}#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,op=\cdot(\cdot)]{#1 \comp( #2 \comp)}{##1 \comp, ##2} \notation{apply}[prec=0;0x\infprec,lambda]{#1 \; #2 }{##1 \; ##2} % collection of propositions/booleans/truth values \symdecl{prop}[name=proposition] \notation{prop}[prop]{\comp{{\rm prop}}} \notation{prop}[BOOL]{\comp{{\rm BOOL}}} \symdecl{judgmentholds}[args=1] \notation{judgmentholds}[vdash,op=\vdash]{\comp\vdash\; #1} % sequences \symdecl{seqtype}[args=1] \notation{seqtype}[kleene]{#1^{\comp\ast}} \symdecl{seqexpr}[args=a] \notation{seqexpr}[angle,prec=nobrackets]{\comp\langle #1\comp\rangle}{##1\comp,##2} \symdef{seqmap}[args=abi,setlike]{\comp\{#3 \comp| #2\comp\in \dobrackets{#1} \comp\}}{##1 \comp, ##2} \symdef{seqprepend}[args=ia]{#1 \comp{::} #2}{##1 \comp, ##2} \symdef{seqappend}[args=ai]{#1 \comp{::} #2}{##1 \comp, ##2} \symdef{seqfoldleft}[args=iabbi]{ \comp{foldl}\dobrackets{#1,#2}\dobrackets{#3\comp,#4\comp\mapsto#5}}{##1 \comp, ##2} \symdef{seqfoldright}[args=iabbi,op=foldr]{ \comp{foldr}\dobrackets{#1,#2}\dobrackets{#3\comp,#4\comp\mapsto#5}}{##1 \comp, ##2} \symdef{seqhead}[args=a]{\comp{head}\dobrackets{#1}}{##1 \comp, ##2} \symdef{seqtail}[args=a]{\comp{tail}\dobrackets{#1}}{##1 \comp, ##2} \symdef{seqlast}[args=a]{\comp{last}\dobrackets{#1}}{##1 \comp, ##2} \symdef{seqinit}[args=a]{\comp{tail}\dobrackets{#1}}{##1 \comp, ##2} \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} % nat literals \symdef{natliteral}{\comp{\mathtt{Ord}}} % 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}{\comp{\mathtt{MOD}} #1} \symdecl{mathstruct}[name=mathematical-structure,args=a] % TODO \notation{mathstruct}[angle,prec=nobrackets]{\comp\langle #1 \comp\rangle}{##1 \comp, ##2} % objects \symdecl{object} \notation{object}{\comp{\mathtt{OBJECT}}} } \ExplSyntaxOn \stex_add_to_current_module:n{ \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}}} } \__stex_modules_end_module: \endgroup %%%%%%%%%%%%% others.dtx %%%%%%%%%%%%% % None \NewDocumentCommand \MSC {m} { % TODO } \@ifpackageloaded{tikzinput}{ \RequirePackage{stex-tikzinput} }{} \bool_if:NT \c_stex_persist_mode_bool { \let\__stex_notation_restore_notation_old:nnnnn \__stex_notation_restore_notation:nnnnn \def\__stex_notation_restore_notation_new:nnnnn#1#2#3#4#5{ \__stex_notation_restore_notation_old:nnnnn{#1}{#2}{#3}{#4}{#5} \ExplSyntaxOn } \def\__stex_notation_restore_notation:nnnnn{ \ExplSyntaxOff \catcode`~10 \__stex_notation_restore_notation_new:nnnnn } \input{\jobname.sms} \let\__stex_notation_restore_notation:nnnnn \__stex_notation_restore_notation_old:nnnnn \prop_if_exist:NT\c_stex_mathhub_main_manifest_prop{ \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 } } } \endinput %% %% End of file `stex.sty'.