diff options
Diffstat (limited to 'Master/texmf-dist/tex/latex/stex/stex.sty')
-rw-r--r-- | Master/texmf-dist/tex/latex/stex/stex.sty | 3495 |
1 files changed, 2272 insertions, 1223 deletions
diff --git a/Master/texmf-dist/tex/latex/stex/stex.sty b/Master/texmf-dist/tex/latex/stex/stex.sty index 2c28b1ee36e..c4af84bc87b 100644 --- a/Master/texmf-dist/tex/latex/stex/stex.sty +++ b/Master/texmf-dist/tex/latex/stex/stex.sty @@ -14,32 +14,34 @@ %% stex-features.dtx (with options: `package') %% stex-statements.dtx (with options: `package') %% stex-proofs.dtx (with options: `package') -%% stex-others.dtx (with options: `package') %% stex-metatheory.dtx (with options: `package') +%% stex-others.dtx (with options: `package') %% %%%%%%%%%%%%% basics.dtx %%%%%%%%%%%%% \RequirePackage{expl3,l3keys2e,ltxcmds} -\ProvidesExplPackage{stex}{2022/02/26}{3.0.1}{sTeX package} +\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 , - sms .bool_set:N = \c_stex_persist_mode_bool , + 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 } -\protected\def\stex{% - \@ifundefined{texorpdfstring}% - {\let\texorpdfstring\@firstoftwo}% - {}% - \texorpdfstring{\raisebox{-.5ex}S\kern-.5ex\TeX}{sTeX}\xspace% -} -\def\sTeX{\stex} +\RequirePackage{stex-logo} % externalized for backwards-compatibility reasons \msg_new:nnn{stex}{error/unknownlanguage}{ Unknown~language:~#1 } @@ -52,13 +54,13 @@ } \cs_new_protected:Nn \stex_debug:nn { \clist_if_in:NnTF \c_stex_debug_clist { all } { - \exp_args:Nnnx\msg_set:nnn{stex}{debug / #1}{ + \msg_set:nnn{stex}{debug / #1}{ \\Debug~#1:~#2\\ } \msg_none:nn{stex}{debug / #1} }{ \clist_if_in:NnT \c_stex_debug_clist { #1 } { - \exp_args:Nnnx\msg_set:nnn{stex}{debug / #1}{ + \msg_set:nnn{stex}{debug / #1}{ \\Debug~#1:~#2\\ } \msg_none:nn{stex}{debug / #1} @@ -74,28 +76,11 @@ } \stex_debug:nn{log}{debug~mode~on} -\RequirePackage{rustex} -\rustex_add_Namespace:nn{stex}{http://kwarc.info/ns/sTeX} -\ifcsname if@latexml\endcsname\else - \expandafter\newif\csname if@latexml\endcsname\@latexmlfalse -\fi -\prg_new_conditional:Nnn \latexml_if: {p, T, F, TF} { - \if@latexml - \prg_return_true: - \else: - \prg_return_false: - \fi: -} -\tl_new:N \l__stex_annotate_arg_tl -\tl_const:Nx \c__stex_annotate_emptyarg_tl { - \rustex_if:TF { - \rustex_direct_HTML:n { \c_ampersand_str lrm; } - }{~} -} -\cs_new_protected:Nn \__stex_annotate_checkempty:n { - \tl_set:Nn \l__stex_annotate_arg_tl { #1 } - \tl_if_empty:NT \l__stex_annotate_arg_tl { - \tl_set_eq:NN \l__stex_annotate_arg_tl \c__stex_annotate_emptyarg_tl +\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 @@ -115,102 +100,23 @@ } } } -\rustex_if:TF{ - \cs_new_protected:Nn \stex_annotate:nnn { - \__stex_annotate_checkempty:n { #3 } - \rustex_annotate_HTML:nn { - property="stex:#1" ~ - resource="#2" - } { - \mode_if_vertical:TF{ - \tl_use:N \l__stex_annotate_arg_tl\par - }{ - \tl_use:N \l__stex_annotate_arg_tl - } - } - } - \cs_new_protected:Nn \stex_annotate_invisible:n { - \__stex_annotate_checkempty:n { #1 } - \rustex_annotate_HTML:nn { - stex:visible="false" ~ - style:display="none" - } { - \mode_if_vertical:TF{ - \tl_use:N \l__stex_annotate_arg_tl\par - }{ - \tl_use:N \l__stex_annotate_arg_tl - } - } - } - \cs_new_protected:Nn \stex_annotate_invisible:nnn { - \__stex_annotate_checkempty:n { #3 } - \rustex_annotate_HTML:nn { - property="stex:#1" ~ - resource="#2" ~ - stex:visible="false" ~ - style:display="none" - } { - \mode_if_vertical:TF{ - \tl_use:N \l__stex_annotate_arg_tl\par - }{ - \tl_use:N \l__stex_annotate_arg_tl - } - } - } - \NewDocumentEnvironment{stex_annotate_env} { m m } { - \par - \rustex_annotate_HTML_begin:n { - property="stex:#1" ~ - resource="#2" - } - }{ - \par\rustex_annotate_HTML_end: - } -}{ - \latexml_if:TF { - \cs_new_protected:Nn \stex_annotate:nnn { - \__stex_annotate_checkempty:n { #3 } - \mode_if_math:TF { - \cs:w latexml@annotate@math\cs_end:{#1}{#2}{ - \tl_use:N \l__stex_annotate_arg_tl - } - }{ - \cs:w latexml@annotate@text\cs_end:{#1}{#2}{ - \tl_use:N \l__stex_annotate_arg_tl - } - } - } - \cs_new_protected:Nn \stex_annotate_invisible:n { - \__stex_annotate_checkempty:n { #1 } - \mode_if_math:TF { - \cs:w latexml@invisible@math\cs_end:{ - \tl_use:N \l__stex_annotate_arg_tl - } - } { - \cs:w latexml@invisible@text\cs_end:{ - \tl_use:N \l__stex_annotate_arg_tl - } - } - } - \cs_new_protected:Nn \stex_annotate_invisible:nnn { - \__stex_annotate_checkempty:n { #3 } - \cs:w latexml@annotate@invisible\cs_end:{#1}{#2}{ - \tl_use:N \l__stex_annotate_arg_tl - } - } - \NewDocumentEnvironment{stex_annotate_env} { m m } { - \par\begin{latexml@annotateenv}{#1}{#2} - }{ - \par\end{latexml@annotateenv} - } - }{ - \cs_new_protected:Nn \stex_annotate:nnn {#3} - \cs_new_protected:Nn \stex_annotate_invisible:n {} - \cs_new_protected:Nn \stex_annotate_invisible:nnn {} - \NewDocumentEnvironment{stex_annotate_env} { m m } {}{} - } +\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 } -\prop_const_from_keyval:Nn \c_stex_languages_prop { +\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 , @@ -220,9 +126,9 @@ ro = romanian , tr = turkish , fr = french -} +}} -\prop_const_from_keyval:Nn \c_stex_language_abbrevs_prop { +\exp_args:NNx \prop_const_from_keyval:Nn \c_stex_language_abbrevs_prop { \tl_to_str:n { english = en , ngerman = de , arabic = ar , @@ -232,23 +138,86 @@ 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 { - \prop_get:NnNTF \c_stex_languages_prop { #1 } \l_tmpa_str { + \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 {,~} } - \RequirePackage[\clist_use:Nn \l_tmpa_clist,]{babel} + \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 % <filename> + \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}{#1}{#2} + \msg_error:nnnn{stex}{error/deactivated-macro}{\detokenize{#1}}{#2} } } \cs_new_protected:Nn \stex_reactivate_macro:N { @@ -263,6 +232,118 @@ } } +\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}{ @@ -361,8 +442,11 @@ } } \str_new:N\l_stex_kpsewhich_return_str -\cs_new_protected:Nn \stex_kpsewhich:n { +\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 } @@ -421,6 +505,26 @@ } \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} }{ @@ -448,6 +552,7 @@ \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 } } @@ -530,6 +635,11 @@ }{} } \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 } @@ -543,19 +653,20 @@ \__stex_mathhub_do_manifest:n { #1 } } } - -\__stex_mathhub_find_manifest:N \c_stex_pwd_seq -\seq_if_empty:NTF \l__stex_mathhub_manifest_file_seq { - \stex_debug:nn{mathhub}{Not~currently~in~a~MathHub~repository} -} { - \__stex_mathhub_parse_manifest:n { main } - \prop_get:NnN \c_stex_mathhub_main_manifest_prop {id} - \l_tmpa_str - \prop_set_eq:cN { c_stex_mathhub_\l_tmpa_str _manifest_prop } - \c_stex_mathhub_main_manifest_prop - \exp_args:Nx \stex_set_current_repository:n { \l_tmpa_str } - \stex_debug:nn{mathhub}{Current~repository:~ - \prop_item:Nn \l_stex_current_repository_prop {id} +\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 { @@ -619,26 +730,43 @@ } } \NewDocumentCommand \mhinput { O{} m}{ - \stex_mhinput:nn{ #1 }{ #2 } + \__stex_mathhub_mhinput:nn{ #1 }{ #2 } } \cs_new_protected:Nn \__stex_mathhub_inputref:nn { \stex_in_repository:nn {#1} { - \bool_lazy_any:nTF { - {\rustex_if_p:} - {\latexml_if_p:} - } { + \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 {} } - \stex_annotate_invisible:nnn{inputref}{ - \l_tmpa_str / #2 - }{} + + \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 - \input{ \c_stex_mathhub_str / ##1 / source / #2 } + \tl_if_empty:nTF{ ##1 }{ + \input{#2} + }{ + \input{ \c_stex_mathhub_str / ##1 / source / #2 } + } \endgroup } } @@ -728,10 +856,10 @@ \AddToHook{begindocument}{ \ltx@ifpackageloaded{graphicx}{ \define@key{Gin}{mhrepos}{\def\Gin@mhrepos{#1}} - \newcommand\mhgraphics[2][]{% + \providecommand\mhgraphics[2][]{% \def\Gin@mhrepos{}\setkeys{Gin}{#1}% \includegraphics[#1]{\mhpath\Gin@mhrepos{#2}}} - \newcommand\cmhgraphics[2][]{\begin{center}\mhgraphics[#1]{#2}\end{center}} + \providecommand\cmhgraphics[2][]{\begin{center}\mhgraphics[#1]{#2}\end{center}} }{} \ltx@ifpackageloaded{listings}{ \define@key{lst}{mhrepos}{\def\lst@mhrepos{#1}} @@ -746,9 +874,9 @@ %%%%%%%%%%%%% references.dtx %%%%%%%%%%%%% -\AddToHook{begindocument}{ +\AtBeginDocument{ } -\AddToHook{enddocument}{ +\AtEndDocument{ } \str_set:Nn \g__stex_refs_title_tl {Unnamed~Document} @@ -895,7 +1023,7 @@ \str_if_empty:NF \l__stex_refs_curr_label_str { \str_gset_eq:cN {sref_sym_#1_label_str}\l__stex_refs_curr_label_str \immediate\write\@auxout{ - \exp_not:N\expandafter\def\exp_not:N\csname sref_sym_#1_label_str\exp_not:N\endcsname{ + \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 } } @@ -1058,21 +1186,26 @@ \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 { - \begingroup - \newlinechar=-1\relax - \endlinechar=-1\relax - %\catcode`\ = 9\relax - \expandafter\endgroup\__stex_modules_export:n + \ExplSyntaxOn + \__stex_modules_export:n } \cs_new_protected:Nn \__stex_modules_export:n { - \ignorespaces #1 - \stex_add_to_current_module:n { \ignorespaces #1 } + \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 } @@ -1100,36 +1233,45 @@ } } \int_new:N \l__stex_modules_group_depth_int -\tl_new:N \l__stex_modules_aftergroup_tl \cs_new_protected:Nn \stex_do_up_to_module:n { \int_compare:nNnTF \l__stex_modules_group_depth_int = \currentgrouplevel { #1 }{ #1 - \expandafter \tl_gset:Nn \expandafter \l__stex_modules_aftergroup_tl \expandafter { \l__stex_modules_aftergroup_tl #1 } + \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 { - \l__stex_modules_aftergroup_tl - \tl_clear:N \l__stex_modules_aftergroup_tl + \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} }{ - \l__stex_modules_aftergroup_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_modules_ns_str -\str_new:N \l_stex_modules_subpath_str +\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 { - \str_set:Nx \l_tmpa_str { #1 } \seq_set_eq:NN \l_tmpa_seq #2 % split off file extension - \seq_pop_right:NN \l_tmpa_seq \l_tmpb_str + \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 - \seq_put_right:No \l_tmpa_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 { @@ -1143,18 +1285,19 @@ } } - \stex_path_to_string:NN \l_tmpa_seq \l_stex_modules_subpath_str - \str_if_empty:NTF \l_stex_modules_subpath_str { - \str_set_eq:NN \l_stex_modules_ns_str \l_tmpa_str + \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_modules_ns_str { - \l_tmpa_str/\l_stex_modules_subpath_str + \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_modules_subpath_str + \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 @@ -1165,7 +1308,7 @@ \exp_args:NNno \seq_set_split:Nnn \l_tmpb_seq . \l_tmpb_str \seq_get_left:NN \l_tmpb_seq \l_tmpb_str \seq_put_right:No \l_tmpa_seq \l_tmpb_str - \str_set:Nx \l_stex_modules_ns_str { + \str_set:Nx \l_stex_module_ns_str { file:/\stex_path_to_string:N \l_tmpa_seq } } @@ -1201,6 +1344,7 @@ \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 { @@ -1211,11 +1355,16 @@ \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: - \str_set_eq:NN \l_stex_module_ns_str \l_stex_modules_ns_str \exp_args:NNNo \seq_set_split:Nnn \l_tmpa_seq / {\l_stex_module_ns_str} \seq_pop_right:NN \l_tmpa_seq \l_tmpa_str @@ -1230,23 +1379,21 @@ \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 % <filename> - \seq_if_empty:NF \l_tmpa_seq { %remaining element should be language + \seq_if_empty:NF \l_tmpa_seq { %remaining element should be [<something>.]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} - \seq_pop_left:NN \l_tmpa_seq \l_stex_module_lang_str } } \stex_if_smsmode:F { \str_if_empty:NF \l_stex_module_lang_str { - \prop_get:NVNTF \c_stex_languages_prop \l_stex_module_lang_str - \l_tmpa_str { - \ltx@ifpackageloaded{babel}{ - \exp_args:Nx \selectlanguage { \l_tmpa_str } - }{} - } { - \msg_error:nnx{stex}{error/unknownlanguage}{\l_tmpa_str} - } + \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 { @@ -1262,6 +1409,7 @@ } \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 { @@ -1285,24 +1433,29 @@ \l_stex_module_ns_str?\l_stex_module_name_str }{\l_stex_module_sig_str} } - - \seq_set_eq:NN \l_tmpa_seq \g_stex_currentfile_seq - \seq_pop_right:NN \l_tmpa_seq \l_tmpa_str - \seq_set_split:NnV \l_tmpb_seq . \l_tmpa_str - \seq_pop_right:NN \l_tmpb_seq \l_tmpa_str % .tex - \seq_pop_left:NN \l_tmpb_seq \l_tmpa_str % <filename> - \str_set:Nx \l_tmpa_str { - \stex_path_to_string:N \l_tmpa_seq / - \l_tmpa_str . \l_stex_module_sig_str .tex - } - \IfFileExists \l_tmpa_str { - \exp_args:No \stex_file_in_smsmode:nn { \l_tmpa_str } { - \str_clear:N \l_stex_current_module_str - \seq_clear:N \l_stex_all_modules_seq - \stex_debug:nn{modules}{Loading~signature~\l_tmpa_str} - } + \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)} }{ - \msg_error:nnx{stex}{error/unknownmodule}{for~signature~\l_tmpa_str} + \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 % <filename> + \str_set:Nx \l_tmpa_str { + \stex_path_to_string:N \l_tmpa_seq / + \l_tmpa_str . \l_stex_module_sig_str .tex + } + \IfFileExists \l_tmpa_str { + \exp_args:No \stex_file_in_smsmode:nn { \l_tmpa_str } { + \str_clear:N \l_stex_current_module_str + \seq_clear:N \l_stex_all_modules_seq + \stex_debug:nn{modules}{Loading~signature} + } + }{ + \msg_error:nnx{stex}{error/unknownmodule}{for~signature~\l_tmpa_str} + } } \stex_if_smsmode:F { \stex_activate_module:n { @@ -1321,6 +1474,7 @@ \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 @@ -1339,7 +1493,7 @@ File:~\stex_path_to_string:N \g_stex_currentfile_seq } - \stex_if_smsmode:F{ + \stex_if_do_html:T{ \begin{stex_annotate_env} {theory} { \l_stex_module_ns_str ? \l_stex_module_name_str } @@ -1355,18 +1509,37 @@ } } } - \int_set:Nn \l__stex_modules_group_depth_int {\currentgrouplevel} % TODO: Inherit metatheory for nested modules? } \iffalse \end{stex_annotate_env} \fi %^^A make syntax highlighting work again \cs_new_protected:Nn \__stex_modules_end_module: { \stex_debug:nn{modules}{Closing~module~\prop_item:cn {c_stex_module_\l_stex_current_module_str _prop} { name }} + \_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 + %\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:}{ @@ -1463,9 +1636,6 @@ \bool_set_false:N \l_stex_in_meta_bool \cs_new_protected:Nn \stex_activate_module:n { \stex_debug:nn{modules}{Activating~module~#1} - \seq_if_in:NnT \l_stex_implicit_morphisms_seq { #1 }{ - \msg_error:nnn{stex}{error/conflictingmodules}{ #1 } - } \exp_args:NNx \seq_if_in:NnF \l_stex_all_modules_seq { #1 } { \seq_put_right:Nx \l_stex_all_modules_seq { #1 } \use:c{ c_stex_module_#1_code } @@ -1498,6 +1668,11 @@ \endinput \setnotation \copynotation + \assign + \renamedecl + \donotcopy + \instantiate + \textsymdecl } \exp_args:NNx \seq_set_from_clist:Nn \g_stex_smsmode_allowedenvs_seq { @@ -1505,10 +1680,12 @@ smodule, copymodule, interpretmodule, + realization, sdefinition, sexample, sassertion, - sparagraph + sparagraph, + mathstructure } } \bool_new:N \g__stex_smsmode_bool @@ -1516,7 +1693,7 @@ \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 { +\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 @@ -1524,13 +1701,107 @@ \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 % <filename> + \str_set:Nx \l_tmpa_str { + \stex_path_to_string:N \l_tmpa_seq / + \l_tmpa_str . \l_stex_module_sig_str .tex + } + \IfFileExists \l_tmpa_str { + \exp_args: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: @@ -1603,7 +1874,7 @@ {\str_if_empty_p:N \l_stex_import_path_str} {\stex_if_module_exists_p:n { \l_stex_module_ns_str ? \l_stex_import_name_str } } }{ - \str_set_eq:NN \l_stex_import_path_str \l_stex_modules_subpath_str + \str_set_eq:NN \l_stex_import_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 { @@ -1613,9 +1884,11 @@ } \str_if_empty:NTF \l_stex_import_archive_str { \str_if_empty:NF \l_stex_import_path_str { - \str_set:Nx \l_stex_import_ns_str { - \l_stex_module_ns_str / \l_stex_import_path_str + \stex_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 @@ -1636,10 +1909,18 @@ \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 @@ -1649,7 +1930,7 @@ % path \str_set:Nx \l_tmpb_str { #3 } \str_if_empty:NTF \l_tmpb_str { - \str_set:Nx \l_tmpa_str { \stex_path_to_string:N \l_tmpa_seq / #4 } + \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 @@ -1660,16 +1941,16 @@ \str_clear:N \l_tmpb_str } - \stex_debug:nn{modules}{Checking~\l_tmpa_str.\l_tmpb_str.tex} + \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~\l_tmpa_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~\l_tmpa_str.en.tex} + \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 } }{ @@ -1680,7 +1961,7 @@ } { \seq_set_split:NnV \l_tmpb_seq / \l_tmpb_str - \seq_concat:NNN \l_tmpa_seq \l_tmpa_seq \l_tmpb_seq + \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 @@ -1691,31 +1972,32 @@ \str_clear:N \l_tmpb_str } - \stex_path_to_string:NN \l_tmpa_seq \l_tmpa_str + \stex_path_canonicalize:N \l_tmpb_seq + \stex_path_to_string:NN \l_tmpb_seq \l_tmpa_str - \stex_debug:nn{modules}{Checking~\l_tmpa_str/#4.\l_tmpb_str.tex} - \IfFileExists{ \l_tmpa_str/#4.\l_tmpb_str.tex }{ - \str_gset:Nx \g__stex_importmodule_file_str { \l_tmpa_str/#4.\l_tmpb_str.tex } + \stex_debug:nn{modules}{Checking~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~\l_tmpa_str/#4.tex} - \IfFileExists{ \l_tmpa_str/#4.tex }{ - \str_gset:Nx \g__stex_importmodule_file_str { \l_tmpa_str/#4.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~\l_tmpa_str/#4.en.tex} - \IfFileExists{ \l_tmpa_str/#4.en.tex }{ - \str_gset:Nx \g__stex_importmodule_file_str { \l_tmpa_str/#4.en.tex } + \stex_debug:nn{modules}{Checking~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~\l_tmpa_str.\l_tmpb_str.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~\l_tmpa_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~\l_tmpa_str.en.tex} + \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 } }{ @@ -1728,21 +2010,24 @@ } } - \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 } + \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_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_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 } } @@ -1751,10 +2036,10 @@ \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_import_require_module:nnnn - { \l_stex_import_ns_str } { \l_stex_import_archive_str } - { \l_stex_import_path_str } { \l_stex_import_name_str } \stex_annotate_invisible:nnn {import} {\l_stex_import_ns_str ? \l_stex_import_name_str} {} } @@ -1782,6 +2067,20 @@ \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 %%%%%%%%%%%%% @@ -1789,6 +2088,15 @@ 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 { @@ -1812,6 +2120,7 @@ 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}} @@ -1823,6 +2132,7 @@ \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 @@ -1928,6 +2238,12 @@ } \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 { @@ -1936,91 +2252,118 @@ \l_stex_current_module_str ? \l_stex_symdecl_name_str }} } - - \bool_if:NF \l_stex_symdecl_local_bool { - \exp_args:Nx \stex_add_to_current_module:n { - \tl_set:cn { #1 } { \stex_invoke_symbol:n { - \l_stex_current_module_str ? \l_stex_symdecl_name_str - } } - } - } } \stex_debug:nn{symbols}{New~symbol:~ \l_stex_current_module_str ? \l_stex_symdecl_name_str^^J Type:~\exp_not:o { \l_stex_symdecl_type_tl }^^J - Args:~\prop_item:Nn \l_tmpa_prop { args } + 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 } { - \prop_set_eq:cN { - l_stex_symdecl_ - \l_stex_current_module_str ? \l_stex_symdecl_name_str - _prop - } \l_tmpa_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} + } } - - \seq_clear:c { - l_stex_symdecl_ - \l_stex_current_module_str ? \l_stex_symdecl_name_str - _notations +} +\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} +} - \bool_if:NF \l_stex_symdecl_local_bool { - \exp_args:Nx - \stex_add_to_current_module:n { - \seq_clear:c { - l_stex_symdecl_ - \l_stex_current_module_str ? \l_stex_symdecl_name_str - _notations - } - \prop_set_from_keyval:cn { - l_stex_symdecl_ - \l_stex_current_module_str ? \l_stex_symdecl_name_str - _prop - } { - name = \prop_item:Nn \l_tmpa_prop { name } , - module = \prop_item:Nn \l_tmpa_prop { module } , - type = \prop_item:Nn \l_tmpa_prop { type } , - args = \prop_item:Nn \l_tmpa_prop { args } , - arity = \prop_item:Nn \l_tmpa_prop { arity } , - assocs = \prop_item:Nn \l_tmpa_prop { assocs } - } - } - } +\keys_define:nn { stex / textsymdecl } { + name .str_set_x:N = \l__stex_symdecl_name_str , + type .tl_set:N = \l__stex_symdecl_type_tl +} - \stex_if_smsmode:F { - \stex_if_do_html:T { - \stex_annotate_invisible:nnn {symdecl} { - \l_stex_current_module_str ? \l_stex_symdecl_name_str - } { - \tl_if_empty:NF \l_stex_symdecl_type_tl {\stex_annotate_invisible:nnn{type}{}{$\l_stex_symdecl_type_tl$}} - \stex_annotate_invisible:nnn{args}{}{ - \prop_item:Nn \l_tmpa_prop { args } - } - \stex_annotate_invisible:nnn{macroname}{#1}{} - \tl_if_empty:NF \l_stex_symdecl_definiens_tl { - \stex_annotate_invisible:nnn{definiens}{} - {$\l_stex_symdecl_definiens_tl$} - } - \str_if_empty:NF \l_stex_symdecl_assoctype_str { - \stex_annotate_invisible:nnn{assoctype}{\l_stex_symdecl_assoctype_str}{} - } - } - } +\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 { - \__stex_symdecl_get_symbol_from_cs:n { #1 } + \tl_set:Nn \l_tmpa_tl { #1 } + \__stex_symdecl_get_symbol_from_cs: }{ % argument is a string % is it a command name? @@ -2031,7 +2374,7 @@ \exp_args:Nx \cs_if_eq:NNTF { \tl_head:N \l_tmpa_tl } \stex_invoke_symbol:n { - \exp_args:No \__stex_symdecl_get_symbol_from_cs:n { \use:c { #1 } } + \__stex_symdecl_get_symbol_from_cs: }{ \__stex_symdecl_get_symbol_from_string:n { #1 } } @@ -2059,28 +2402,52 @@ \cs_new_protected:Nn \__stex_symdecl_get_symbol_from_string:n { \tl_set:Nn \l_tmpa_tl { - \msg_set:nnn{stex}{error/unknownsymbol}{ - No~symbol~#1~found! - } - \msg_error:nn{stex}{error/unknownsymbol} + \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 } - \stex_all_symbols:n { - \str_if_eq:eeT { \l_tmpa_str }{ \str_range:nnn {##1}{-\l_tmpa_int}{-1}}{ - \seq_map_break:n{\seq_map_break:n{ - \tl_set:Nn \l_tmpa_tl { - \str_set:Nn \l_stex_get_symbol_uri_str { ##1 } + %\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:n { +\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 { @@ -2097,7 +2464,6 @@ } } \keys_define:nn { stex / notation } { - lang .tl_set_x:N = \l__stex_notation_lang_str , variant .tl_set_x:N = \l__stex_notation_variant_str , prec .str_set_x:N = \l__stex_notation_prec_str , op .tl_set:N = \l__stex_notation_op_tl , @@ -2108,7 +2474,6 @@ } \cs_new_protected:Nn \_stex_notation_args:n { - \str_clear:N \l__stex_notation_lang_str \str_clear:N \l__stex_notation_variant_str \str_clear:N \l__stex_notation_prec_str \tl_clear:N \l__stex_notation_op_tl @@ -2125,26 +2490,28 @@ \IfBooleanTF#1{ \stex_setnotation:n {\l_stex_get_symbol_uri_str} }{} - \stex_smsmode_do: + \stex_smsmode_do:\ignorespacesandpars } - \stex_notation_do:nnnn + \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 \c_hash_str \l__stex_notation_lang_str } + { \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 \stex_symbol_after_invocation_tl +\tl_new:N \STEXInternalSymbolAfterInvokationTL -\cs_new_protected:Nn \stex_notation_do:nnnn { - \let\l_stex_current_symbol_str\relax +\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 \__stex_notation_suffix_str { #3 } + \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 { @@ -2195,10 +2562,10 @@ \int_compare:nNnTF \l__stex_notation_arity_str = 0 { \exp_args:NNe \cs_set:Npn \l_stex_notation_macrocode_cs { - \_stex_term_math_oms:nnnn { \l_stex_current_symbol_str } - { \__stex_notation_suffix_str } + \STEXInternalTermMathOMSiiii { \STEXInternalCurrentSymbolStr } + { \l__stex_notation_suffix_str } { \l__stex_notation_opprec_tl } - { \exp_not:n { #4 } } + { \exp_not:n { #5 } } } \l_stex_notation_after_do_tl }{ @@ -2207,10 +2574,10 @@ { \cs_generate_from_arg_count:NNnn \l_stex_notation_macrocode_cs \cs_set:Npn \l__stex_notation_arity_str } { { - \_stex_term_math_omb:nnnn { \l_stex_current_symbol_str } - { \__stex_notation_suffix_str } + \STEXInternalTermMathOMBiiii { \STEXInternalCurrentSymbolStr } + { \l__stex_notation_suffix_str } { \l__stex_notation_opprec_tl } - { \exp_not:n { #4 } } + { \exp_not:n { #5 } } }} }{ \str_if_in:NnTF \l__stex_notation_args_str B { @@ -2218,20 +2585,20 @@ { \cs_generate_from_arg_count:NNnn \l_stex_notation_macrocode_cs \cs_set:Npn \l__stex_notation_arity_str } { { - \_stex_term_math_omb:nnnn { \l_stex_current_symbol_str } - { \__stex_notation_suffix_str } + \STEXInternalTermMathOMBiiii { \STEXInternalCurrentSymbolStr } + { \l__stex_notation_suffix_str } { \l__stex_notation_opprec_tl } - { \exp_not:n { #4 } } + { \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 } { { - \_stex_term_math_oma:nnnn { \l_stex_current_symbol_str } - { \__stex_notation_suffix_str } + \STEXInternalTermMathOMAiiii { \STEXInternalCurrentSymbolStr } + { \l__stex_notation_suffix_str } { \l__stex_notation_opprec_tl } - { \exp_not:n { #4 } } + { \exp_not:n { #5 } } } } } } @@ -2250,16 +2617,16 @@ \str_set:Nx \l_tmpa_str { \str_head:N \l__stex_notation_remaining_args_str } \str_set:Nx \l__stex_notation_remaining_args_str { \str_tail:N \l__stex_notation_remaining_args_str } \str_if_eq:VnTF \l_tmpa_str a { - \__stex_notation_argument_assoc:n + \__stex_notation_argument_assoc:nn{a} }{ \str_if_eq:VnTF \l_tmpa_str B { - \__stex_notation_argument_assoc:n + \__stex_notation_argument_assoc:nn{B} }{ - \seq_pop_left:NN \l__stex_notation_remaining_precs_seq \l_tmpa_str + \seq_pop_left:NN \l__stex_notation_remaining_precs_seq \l_tmpb_str \tl_put_right:Nx \l_stex_notation_dummyargs_tl { - { \_stex_term_math_arg:nnn - { \int_use:N \l__stex_notation_currarg_int } - { \l_tmpa_str } + { \STEXInternalTermMathArgiii + { \l_tmpa_str\int_use:N \l__stex_notation_currarg_int } + { \l_tmpb_str } { ####\int_use:N \l__stex_notation_currarg_int } } } @@ -2268,11 +2635,11 @@ } } } -\cs_new_protected:Nn \__stex_notation_argument_assoc:n { +\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}{ - #1 + #2 } \int_zero:N \l_tmpa_int \tl_clear:N \l_tmpa_tl @@ -2281,7 +2648,7 @@ \tl_put_right:Nx \l_tmpa_tl { \str_if_eq:nnTF {##1}{a}{ {} }{ \str_if_eq:nnTF {##1}{B}{ {} }{ - {\_stex_term_arg:nn{\int_use:N \l_tmpa_int}{################ \int_use:N \l_tmpa_int}} + {\_stex_term_arg:nn{##1\int_use:N \l_tmpa_int}{################ \int_use:N \l_tmpa_int}} } } } @@ -2301,184 +2668,133 @@ \seq_pop_left:NN \l__stex_notation_remaining_precs_seq \l_tmpa_str \tl_put_right:Nx \l_stex_notation_dummyargs_tl { { - \_stex_term_math_assoc_arg:nnnn - { \int_use:N \l__stex_notation_currarg_int } + \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_final: { - \exp_args:Nne \use:nn - { - \cs_generate_from_arg_count:cNnn { - stex_notation_ \l_stex_get_symbol_uri_str \c_hash_str - \__stex_notation_suffix_str - _cs - } - \cs_set:Npn \l__stex_notation_arity_str } { { - \exp_after:wN \exp_after:wN \exp_after:wN - \exp_not:n \exp_after:wN \exp_after:wN \exp_after:wN - { \exp_after:wN \l_stex_notation_macrocode_cs \l_stex_notation_dummyargs_tl \stex_symbol_after_invocation_tl} - } } - - \tl_if_empty:NF \l__stex_notation_op_tl { - \cs_set:cpx { - stex_op_notation_ \l_stex_get_symbol_uri_str \c_hash_str - \__stex_notation_suffix_str - _cs - } { - \_stex_term_oms:nnn { - \l_stex_get_symbol_uri_str \c_hash_str \__stex_notation_suffix_str - }{ - \l_stex_get_symbol_uri_str - }{ \comp{ \exp_args:No \exp_not:n { \l__stex_notation_op_tl } } } - } +\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} } + } +} - \exp_args:Ne - \stex_add_to_current_module:n { - \cs_generate_from_arg_count:cNnn { - stex_notation_ \l_stex_get_symbol_uri_str \c_hash_str - \__stex_notation_suffix_str - _cs - } \cs_set:Npn {\l__stex_notation_arity_str} { +\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 \stex_symbol_after_invocation_tl} - } - \tl_if_empty:NF \l__stex_notation_op_tl { - \cs_set:cpn { - stex_op_notation_\l_stex_get_symbol_uri_str \c_hash_str - \__stex_notation_suffix_str - _cs - } { - \_stex_term_oms:nnn { - \l_stex_get_symbol_uri_str\c_hash_str \__stex_notation_suffix_str - }{ - \l_stex_get_symbol_uri_str - }{ \comp{ \exp_args:No \exp_not:n { \l__stex_notation_op_tl } } } + { \exp_after:wN \l_stex_notation_macrocode_cs \l_stex_notation_dummyargs_tl \STEXInternalSymbolAfterInvokationTL} } - } + {\exp_args:No \exp_not:n \l__stex_notation_op_tl } } - %\exp_args:Nx - % \stex_do_up_to_module:n { - \seq_put_right:cx { - l_stex_symdecl_ \l_stex_get_symbol_uri_str - _notations - } { - \__stex_notation_suffix_str - } - % } \stex_debug:nn{symbols}{ - Notation~\__stex_notation_suffix_str + 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 - \__stex_notation_suffix_str + \l__stex_notation_suffix_str _cs } } - - \exp_args:Ne - \stex_add_to_current_module:n { - \seq_put_right:cn { - l_stex_symdecl_\l_stex_get_symbol_uri_str - _notations - } { \__stex_notation_suffix_str } - } - - \stex_if_smsmode:F { - % HTML annotations - \stex_if_do_html:T { - \stex_annotate_invisible:nnn { notation } - { \l_stex_get_symbol_uri_str } { - \stex_annotate_invisible:nnn { notationfragment } - { \__stex_notation_suffix_str }{} - \stex_annotate_invisible:nnn { precedence } - { \l__stex_notation_prec_str }{} - - \int_zero:N \l_tmpa_int - \str_set_eq:NN \l__stex_notation_remaining_args_str \l__stex_notation_args_str - \tl_clear:N \l_tmpa_tl - \int_step_inline:nn { \l__stex_notation_arity_str }{ - \int_incr:N \l_tmpa_int - \str_set:Nx \l_tmpb_str { \str_head:N \l__stex_notation_remaining_args_str } - \str_set:Nx \l__stex_notation_remaining_args_str { \str_tail:N \l__stex_notation_remaining_args_str } - \str_if_eq:VnTF \l_tmpb_str a { + \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 { - \c_hash_str \c_hash_str \int_use:N \l_tmpa_int a , - \c_hash_str \c_hash_str \int_use:N \l_tmpa_int b + \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 { - \c_hash_str \c_hash_str \int_use:N \l_tmpa_int a , - \c_hash_str \c_hash_str \int_use:N \l_tmpa_int b - } } - }{ - \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { - \c_hash_str \c_hash_str \int_use:N \l_tmpa_int - } } - } + \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 \l_stex_current_symbol_str {\l_stex_get_symbol_uri_str } - $ \exp_args:Nno \use:nn { \use:c { - stex_notation_ \l_stex_current_symbol_str - \c_hash_str \__stex_notation_suffix_str _cs - } } { \l_tmpa_tl } $ + } + \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 } { - lang .tl_set_x:N = \l__stex_notation_lang_str , variant .tl_set_x:N = \l__stex_notation_variant_str , unknown .code:n = \str_set:Nx \l__stex_notation_variant_str \l_keys_key_str } \cs_new_protected:Nn \_stex_setnotation_args:n { - \str_clear:N \l__stex_notation_lang_str + % \str_clear:N \l__stex_notation_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 \c_hash_str \l__stex_notation_lang_str }{ - \exp_args:Nnx \seq_remove_all:cn { l_stex_symdecl_#1 _notations } - { \l__stex_notation_variant_str \c_hash_str \l__stex_notation_lang_str } - \exp_args:Nnx \seq_remove_all:cn { l_stex_symdecl_#1 _notations } - { \c_hash_str } - \exp_args:Nnx \seq_put_left:cn { l_stex_symdecl_#1 _notations } - { \l__stex_notation_variant_str \c_hash_str \l__stex_notation_lang_str } - \exp_args:Nx \stex_add_to_current_module:n { - \exp_args:Nnx \seq_remove_all:cn { l_stex_symdecl_#1 _notations } - { \l__stex_notation_variant_str \c_hash_str \l__stex_notation_lang_str } - \exp_args:Nnx \seq_put_left:cn { l_stex_symdecl_#1 _notations } - { \l__stex_notation_variant_str \c_hash_str \l__stex_notation_lang_str } - \exp_args:Nnx \seq_remove_all:cn { l_stex_symdecl_#1 _notations } - { \c_hash_str } - } + { \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 \c_hash_str \l__stex_notation_lang_str}~for~ + {\l__stex_notation_variant_str }~for~ #1 \\ \expandafter\meaning\csname l_stex_symdecl_#1 _notations\endcsname } }{ - % todo throw error + \msg_error:nnxx{stex}{unknownnotation}{\l__stex_notation_variant_str}{#1} } } @@ -2486,7 +2802,7 @@ \stex_get_symbol:n { #1 } \_stex_setnotation_args:n { #2 } \stex_setnotation:n{\l_stex_get_symbol_uri_str} - \stex_smsmode_do: + \stex_smsmode_do:\ignorespacesandpars } \cs_new_protected:Nn \stex_copy_notations:nn { @@ -2496,9 +2812,10 @@ } \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} } + \tl_put_right:Nn \l_tmpa_tl { {######## ##1} } } - \seq_map_inline:cn {l_stex_symdecl_#2_notations}{ + \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 @@ -2506,15 +2823,30 @@ \exp_after:wN \l_tmpa_cs \l_tmpa_tl } } - \exp_args:Nx - \stex_do_up_to_module:n { - \seq_put_right:cn{l_stex_symdecl_#1_notations}{##1} - \cs_generate_from_arg_count:cNnn { - stex_notation_ #1 \c_hash_str ##1 _cs - } \cs_set:Npn { \prop_item:cn {l_stex_symdecl_#2_prop}{ arity } }{ - \exp_after:wN\exp_not:n\exp_after:wN{\l_tmpa_tl} + + \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 } } @@ -2524,10 +2856,7 @@ \stex_get_symbol:n { #2 } \exp_args:Noo \stex_copy_notations:nn \l_tmpa_str \l_stex_get_symbol_uri_str - \exp_args:Nx \stex_add_import_to_current_module:n{ - \stex_copy_notations:nn {\l_tmpa_str} {\l_stex_get_symbol_uri_str} - } - \stex_smsmode_do: + \stex_smsmode_do:\ignorespacesandpars } \keys_define:nn { stex / symdef } { @@ -2536,8 +2865,9 @@ 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 , + % 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 = @@ -2551,10 +2881,11 @@ \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_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 @@ -2568,15 +2899,16 @@ \stex_symdecl_do:n { #1 } \tl_set:Nn \l_stex_notation_after_do_tl { \__stex_notation_final: - \stex_smsmode_do: + \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:nnnn + \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 \c_hash_str \l__stex_notation_lang_str } + { \l__stex_notation_variant_str } + { \l__stex_notation_prec_str} } \stex_deactivate_macro:Nn \symdef {module~environments} @@ -2587,6 +2919,7 @@ 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}}, @@ -2600,6 +2933,7 @@ \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 @@ -2665,11 +2999,7 @@ \tl_if_empty:NF \l__stex_variables_op_tl { \cs_set:cpx { stex_var_op_notation_ \l__stex_variables_name_str _cs - } { - \_stex_term_omv:nn { - var://\l__stex_variables_name_str - }{ \comp{ \exp_args:No \exp_not:n { \l__stex_variables_op_tl } } } - } + } { \exp_not:N\comp{ \exp_args:No \exp_not:n { \l__stex_variables_op_tl } } } } \tl_set:Nn \l_stex_notation_after_do_tl { @@ -2679,14 +3009,14 @@ } {{ \exp_after:wN \exp_after:wN \exp_after:wN \exp_not:n \exp_after:wN \exp_after:wN \exp_after:wN - { \exp_after:wN \l_stex_notation_macrocode_cs \l_stex_notation_dummyargs_tl \stex_symbol_after_invocation_tl} + { \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{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}{} @@ -2695,6 +3025,9 @@ \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 @@ -2704,36 +3037,44 @@ \str_set:Nx \l__stex_variables_remaining_args_str { \str_tail:N \l__stex_variables_remaining_args_str } \str_if_eq:VnTF \l_tmpb_str a { \tl_set:Nx \l_tmpa_tl { \l_tmpa_tl { - \c_hash_str \c_hash_str \int_use:N \l_tmpa_int a , - \c_hash_str \c_hash_str \int_use:N \l_tmpa_int b + \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 { - \c_hash_str \c_hash_str \int_use:N \l_tmpa_int a , - \c_hash_str \c_hash_str \int_use:N \l_tmpa_int b + \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 { - \c_hash_str \c_hash_str \int_use:N \l_tmpa_int + \stex_annotate:nnn{argmarker}{\int_use:N \l_tmpa_int}{} } } } } } \stex_annotate_invisible:nnn { notationcomp }{}{ - \str_set:Nx \l_stex_current_symbol_str {var://\l__stex_variables_name_str } + \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:nnnn { \l__stex_variables_args_str } { \prop_item:Nn \l_tmpa_prop { arity } } {} + \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_variables_reset:N { +\cs_new:Nn \_stex_reset:N { \tl_if_exist:NTF #1 { \def \exp_not:N #1 { \exp_args:No \exp_not:n #1 } }{ @@ -2745,13 +3086,13 @@ \clist_set:Nx \l__stex_variables_names { \tl_to_str:n {#1} } \exp_args:Nnx \use:nn { % TODO - \stex_annotate_invisible:nnn {vardecls}{\clist_use:Nn\l__stex_variables_names,}{ + \stex_annotate_invisible:nnn {vardecl}{\clist_use:Nn\l__stex_variables_names,}{ #2 } }{ - \__stex_variables_reset:N \varnot - \__stex_variables_reset:N \vartype - \__stex_variables_reset:N \vardefi + \_stex_reset:N \varnot + \_stex_reset:N \vartype + \_stex_reset:N \vardefi } } @@ -2770,8 +3111,140 @@ \str_set:Nn \l_tmpa_str { #1 } } \_stex_term_omv:nn { - var://\l_tmpa_str - }{ \comp{ #2 } } + 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 } @@ -2788,36 +3261,22 @@ Symbol~#1~has~no~operator~notation~for~notation~#2 } \msg_new:nnn{stex}{error/notallowed}{ - Symbol~invocation~#1~not~allowed~in~notation~component~of~#2 + Symbol~invokation~#1~not~allowed~in~notation~component~of~#2 } - -\keys_define:nn { stex / terms } { - lang .tl_set_x:N = \l__stex_terms_lang_str , - variant .tl_set_x:N = \l__stex_terms_variant_str , - unknown .code:n = \str_set:Nx - \l__stex_terms_variant_str \l_keys_key_str +\msg_new:nnn{stex}{error/doubleargument}{ + Argument~#1~of~symbol~#2~already~assigned } - -\cs_new_protected:Nn \__stex_terms_args:n { - \str_clear:N \l__stex_terms_lang_str - \str_clear:N \l__stex_terms_variant_str - - \keys_set:nn { stex / terms } { #1 } +\msg_new:nnn{stex}{error/overarity}{ + Argument~#1~invalid~for~symbol~#2~with~arity~#3 } -\cs_new:Nn \__stex_terms_reset:N { - \tl_if_exist:NTF #1 { - \def \exp_not:N #1 { \exp_args:No \exp_not:n #1 } - }{ - \let \exp_not:N #1 \exp_not:N \undefined - } -} -\bool_new:N \l__stex_terms_allow_semantic_bool -\bool_set_true:N \l__stex_terms_allow_semantic_bool +\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 { - \bool_if:NTF \l__stex_terms_allow_semantic_bool { + \ifvmode\indent\fi + \bool_if:NTF \l_stex_allow_semantic_bool { \str_if_eq:eeF { \prop_item:cn { l_stex_symdecl_#1_prop @@ -2835,7 +3294,7 @@ \exp_after:wN \__stex_terms_invoke_text:n \fi: { #1 } }{ - \msg_error:nnxx{stex}{error/notallowed}{#1}{\l_stex_current_symbol_str} + \msg_error:nnxx{stex}{error/notallowed}{#1}{\STEXInternalCurrentSymbolStr} } } @@ -2878,38 +3337,49 @@ \cs_new_protected:Nn \__stex_terms_invoke_op_custom:nn { \exp_args:Nnx \use:nn { - \str_set:Nn \l_stex_current_symbol_str { #1 } - \bool_set_false:N \l__stex_terms_allow_semantic_bool - \_stex_term_oms:nnn {#1 \c_hash_str\c_hash_str}{#1}{ + \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_terms_reset:N \l_stex_current_symbol_str - \bool_set_true:N \l__stex_terms_allow_semantic_bool + \_stex_reset:N \comp + \_stex_reset:N \STEXInternalCurrentSymbolStr + \bool_set_true:N \l_stex_allow_semantic_bool } } -\cs_new_protected:Nn \__stex_terms_find_notation:nn { - \str_set:Nn \l_stex_current_symbol_str { #1 } +\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} } { - \bool_lazy_all:nTF { - {\str_if_empty_p:N \l__stex_terms_variant_str} - {\str_if_empty_p:N \l__stex_terms_lang_str} - }{ - \seq_get_left:cN {l_stex_symdecl_#1_notations}\l__stex_terms_variant_str + \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_terms_variant_str \c_hash_str \l__stex_terms_lang_str + \l_stex_notation_variant_str }{ - \str_set:Nx \l__stex_terms_variant_str { \l__stex_terms_variant_str \c_hash_str \l__stex_terms_lang_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_terms_variant_str \c_hash_str \l__stex_terms_lang_str + ~\l_stex_notation_variant_str } } } @@ -2917,43 +3387,80 @@ } \cs_new_protected:Npn \__stex_terms_invoke_op_notation:nw #1 [#2] { - \__stex_terms_find_notation:nn { #1 }{ #2 } - \bool_set_false:N \l__stex_terms_allow_semantic_bool - \cs_if_exist:cTF { - stex_op_notation_ #1 \c_hash_str \l__stex_terms_variant_str _cs - }{ - \use:c{stex_op_notation_ #1 \c_hash_str \l__stex_terms_variant_str _cs} + \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} + } + } }{ - \msg_error:nnxx{stex}{error/noop}{#1}{\l__stex_terms_variant_str} + \_stex_reset:N \comp + \_stex_reset:N \STEXInternalCurrentSymbolStr + \bool_set_true:N \l_stex_allow_semantic_bool } - \bool_set_true:N \l__stex_terms_allow_semantic_bool } \cs_new_protected:Npn \__stex_terms_invoke_notation:nw #1 [#2] { - \__stex_terms_find_notation:nn { #1 }{ #2 } + \stex_find_notation:nn { #1 }{ #2 } \cs_if_exist:cTF { - stex_notation_ #1 \c_hash_str \l__stex_terms_variant_str _cs + stex_notation_ #1 \c_hash_str \l_stex_notation_variant_str _cs }{ - \tl_set:Nx \stex_symbol_after_invocation_tl { - \__stex_terms_reset:N \stex_symbol_after_invocation_tl - \__stex_terms_reset:N \l_stex_current_symbol_str - \bool_set_true:N \l__stex_terms_allow_semantic_bool - } - \bool_set_false:N \l__stex_terms_allow_semantic_bool - \use:c{stex_notation_ #1 \c_hash_str \l__stex_terms_variant_str _cs} + \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_terms_variant_str + ~\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 { - \bool_set_false:N \l__stex_terms_allow_semantic_bool - \str_set:Nn \l_stex_current_symbol_str { #1 } + \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 { @@ -2962,24 +3469,25 @@ \prop_put:Nno \l__stex_terms_custom_args_prop {args} \l_tmpa_str \tl_set:Nn \arg { \__stex_terms_arg: } \str_if_empty:NTF \l_tmpa_str { - \_stex_term_oms:nnn {#1}{#1}{#2} + \_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}{#2} + \_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}{#2} + \_stex_term_ombind:nnn {#1}{#1\c_hash_str CUSTOM-\l_tmpa_str}{\ignorespaces#2} }{ - \_stex_term_oma:nnn {#1}{#1}{#2} + \_stex_term_oma:nnn {#1}{#1\c_hash_str CUSTOM-\l_tmpa_str}{\ignorespaces#2} } } } % TODO check that all arguments exist }{ - \__stex_terms_reset:N \l_stex_current_symbol_str - \__stex_terms_reset:N \arg - \__stex_terms_reset:N \l__stex_terms_custom_args_prop - \bool_set_true:N \l__stex_terms_allow_semantic_bool + \_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 } } @@ -2996,40 +3504,136 @@ } }{ \int_set:Nn \l_tmpa_int { #2 } - \exp_args:NNx \prop_if_in:NnT \l__stex_terms_custom_args_prop {\int_use:N \l_tmpa_int} { - % TODO throw error - } } \str_set:Nx \l_tmpa_str {\prop_item:Nn \l__stex_terms_custom_args_prop {args} } \int_compare:nNnT \l_tmpa_int > {\str_count:N \l_tmpa_str} { - % TODO throw error + \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 { - \exp_args:No \_stex_term_arg:nn {\l_stex_current_symbol_str}{#3} + \stex_annotate_invisible:n { %TODO + \exp_args:No \_stex_term_arg:nn {\l_tmpa_str\int_use:N \l_tmpa_int}{\ignorespaces#3} } - }{ - \exp_args:No \_stex_term_arg:nn {\l_stex_current_symbol_str}{#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 { - \exp_args:Nnx \use:nn { - \bool_set_true:N \l__stex_terms_allow_semantic_bool - \stex_annotate:nnn{ arg }{ #1 }{ #2 } - }{ - \bool_set_false:N \l__stex_terms_allow_semantic_bool - } + \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:Nn \_stex_term_math_arg:nnn { +\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 @@ -3089,170 +3693,42 @@ } \cs_new_protected:Nn \_stex_term_oms:nnn { \stex_annotate:nnn{ OMID }{ #2 }{ - \stex_highlight_term:nn { #1 } { #3 } + #3 } } -\cs_new_protected:Nn \_stex_term_math_oms:nnnn { +\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{ OMID }{ #1 }{ - \stex_highlight_term:nn { #1 } { #2 } + \stex_annotate:nnn{ OMV }{ #1 }{ + #2 } } \cs_new_protected:Nn \_stex_term_oma:nnn { \stex_annotate:nnn{ OMA }{ #2 }{ - \stex_highlight_term:nn { #1 } { #3 } + #3 } } -\cs_new_protected:Nn \_stex_term_math_oma:nnnn { +\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 }{ - \stex_highlight_term:nn { #1 } { #3 } + #3 } } -\cs_new_protected:Nn \_stex_term_math_omb:nnnn { +\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_protected:Nn \_stex_term_math_assoc_arg:nnnn { - % TODO sequences - \clist_set:Nn \l_tmpa_clist{ #3 } - \int_compare:nNnTF { \clist_count:N \l_tmpa_clist } < 2 { - \tl_set:Nn \l_tmpa_tl { #3 } - }{ - \cs_set:Npn \l_tmpa_cs ##1 ##2 { #4 } - \clist_reverse:N \l_tmpa_clist - \clist_pop:NN \l_tmpa_clist \l_tmpa_tl - - \clist_map_inline:Nn \l_tmpa_clist { - \exp_args:NNNo \exp_args:NNo \tl_set:No \l_tmpa_tl { - \exp_args:Nno - \l_tmpa_cs { ##1 } \l_tmpa_tl - } - } - } - \exp_args:Nnno - \_stex_term_math_arg:nnn{#1}{#2}\l_tmpa_tl -} -\cs_new_protected:Nn \stex_term_custom:nn { - \str_set:Nn \l__stex_terms_custom_uri { #1 } - \str_set:Nn \l_tmpa_str { #2 } - \tl_clear:N \l_tmpa_tl - \int_zero:N \l_tmpa_int - \int_set:Nn \l_tmpb_int { \str_count:N \l_tmpa_str } - \__stex_terms_custom_loop: -} -\cs_new_protected:Nn \__stex_terms_custom_loop: { - \bool_set_false:N \l_tmpa_bool - \bool_while_do:nn { - \str_if_eq_p:ee X { - \str_item:Nn \l_tmpa_str { \l_tmpa_int + 1 } - } - }{ - \int_incr:N \l_tmpa_int - } - - \peek_charcode:NTF [ { - % notation/text component - \__stex_terms_custom_component:w - } { - \int_compare:nNnTF \l_tmpa_int = \l_tmpb_int { - % all arguments read => finish - \__stex_terms_custom_final: - } { - % arguments missing - \peek_charcode_remove:NTF * { - % invisible, specific argument position or both - \peek_charcode:NTF [ { - % visible specific argument position - \__stex_terms_custom_arg:wn - } { - % invisible - \peek_charcode_remove:NTF * { - % invisible specific argument position - \__stex_terms_custom_arg_inv:wn - } { - % invisible next argument - \__stex_terms_custom_arg_inv:wn [ \l_tmpa_int + 1 ] - } - } - } { - % next normal argument - \__stex_terms_custom_arg:wn [ \l_tmpa_int + 1 ] - } - } - } -} -\cs_new_protected:Npn \__stex_terms_custom_arg_inv:wn [ #1 ] #2 { - \bool_set_true:N \l_tmpa_bool - \__stex_terms_custom_arg:wn [ #1 ] { #2 } -} -\cs_new_protected:Npn \__stex_terms_custom_arg:wn [ #1 ] #2 { - \str_set:Nx \l_tmpb_str { - \str_item:Nn \l_tmpa_str { #1 } - } - \str_case:VnTF \l_tmpb_str { - { X } { - \msg_error:nnx{stex}{error/notationarg}{\l__stex_terms_custom_uri} - } - { i } { \__stex_terms_custom_set_X:n { #1 } } - { b } { \__stex_terms_custom_set_X:n { #1 } } - { a } { \__stex_terms_custom_set_X:n { #1 } } % TODO ? - { B } { \__stex_terms_custom_set_X:n { #1 } } % TODO ? - }{}{ - \msg_error:nnx{stex}{error/notationarg}{\l__stex_terms_custom_uri} - } - - \bool_if:nTF \l_tmpa_bool { - \tl_put_right:Nx \l_tmpa_tl { - \stex_annotate_invisible:n { - \_stex_term_arg:nn { \int_eval:n { #1 } } - \exp_not:n { { #2 } } - } - } - } { - \tl_put_right:Nx \l_tmpa_tl { - \_stex_term_arg:nn { \int_eval:n { #1 } } - \exp_not:n { { #2 } } - } - } - - \__stex_terms_custom_loop: -} -\cs_new_protected:Nn \__stex_terms_custom_set_X:n { - \str_set:Nx \l_tmpa_str { - \str_range:Nnn \l_tmpa_str 1 { #1 - 1 } - X - \str_range:Nnn \l_tmpa_str { #1 + 1 } { -1 } - } -} -\cs_new_protected:Npn \__stex_terms_custom_component:w [ #1 ] { - \tl_put_right:Nn \l_tmpa_tl { \comp{ #1 } } - \__stex_terms_custom_loop: -} -\cs_new_protected:Nn \__stex_terms_custom_final: { - \int_compare:nNnTF \l_tmpb_int = 0 { - \exp_args:Nnno \_stex_term_oms:nnn - }{ - \str_if_in:NnTF \l_tmpa_str {b} { - \exp_args:Nnno \_stex_term_ombind:nnn - } { - \exp_args:Nnno \_stex_term_oma:nnn - } - } - { \l__stex_terms_custom_uri } { \l__stex_terms_custom_uri } { \l_tmpa_tl } -} \cs_new:Nn \stex_capitalize:n { \uppercase{#1} } \keys_define:nn { stex / symname } { @@ -3295,7 +3771,7 @@ \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 }!{ + \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: @@ -3311,38 +3787,34 @@ \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 }!{ + \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: } - -\str_new:N \l_stex_current_symbol_str -\cs_new_protected:Nn \stex_highlight_term:nn { - \exp_args:Nnx - \use:nn { - \str_set:Nx \l_stex_current_symbol_str { #1 } - #2 - } { - \str_set:Nx \exp_not:N \l_stex_current_symbol_str - { \l_stex_current_symbol_str } +\cs_new_protected: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:Nn \stex_unhighlight_term:n { - #1 %\iffalse{{\fi}} #1 {{\iffalse}}\fi -} -\cs_new_protected:Npn \comp #1 { - \str_if_empty:NF \l_stex_current_symbol_str { - \rustex_if:TF { - \stex_annotate:nnn { comp }{ \l_stex_current_symbol_str }{ #1 } +\cs_new_protected:Npn \_varcomp #1 { + \str_if_empty:NF \STEXInternalCurrentSymbolStr { + \stex_html_backend:TF { + \stex_annotate:nnn { varcomp }{ \STEXInternalCurrentSymbolStr }{ #1 } }{ - \exp_args:Nnx \compemph@uri { #1 } { \l_stex_current_symbol_str } + \exp_args:Nnx \varemph@uri { #1 } { \STEXInternalCurrentSymbolStr } } } } +\def\comp{\_comp} + \cs_new_protected:Npn \compemph@uri #1 #2 { \compemph{ #1 } } @@ -3364,7 +3836,15 @@ } \cs_new_protected:Npn \symrefemph #1 { - \textbf{#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 @@ -3413,36 +3893,68 @@ } \cs_new_protected:Nn \__stex_variables_invoke_text:n { - %TODO + \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 [ { - \__stex_variables_invoke_op_custom:nw - }{ % TODO throw error + }{ + \__stex_variables_invoke_op_custom:nn } }{ \__stex_variables_invoke_op:n { #1 } } }{ \peek_charcode_remove:NTF * { - \__stex_variables_invoke_text:n { #1 } + \__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 }{ - \use:c{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 + } }{ - \msg_error:nnxx{stex}{error/noop}{variable~#1}{} + \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}{} + } } } @@ -3450,13 +3962,82 @@ \cs_if_exist:cTF { stex_var_notation_#1_cs }{ - \str_set:Nn \l_stex_current_symbol_str { #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 + } + \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 %%%%%%%%%%%%% @@ -3467,9 +4048,28 @@ Symbol~#1~not~assigned~in~interpretmodule~#2 } -\cs_new_protected:Nn \stex_get_symbol_in_copymodule:n { +\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 { - \__stex_features_get_symbol_from_cs:n { #1 } + \tl_set:Nn \l_tmpa_tl { #1 } + \__stex_copymodule_get_symbol_from_cs: }{ % argument is a string % is it a command name? @@ -3480,34 +4080,31 @@ \exp_args:Nx \cs_if_eq:NNTF { \tl_head:N \l_tmpa_tl } \stex_invoke_symbol:n { - \exp_args:No \__stex_features_get_symbol_from_cs:n { \use:c { #1 } } + \__stex_copymodule_get_symbol_from_cs:n{ #2 } }{ - \__stex_features_get_symbol_from_string:n { #1 } + \__stex_copymodule_get_symbol_from_string:nn { #1 }{ #2 } } } { - \__stex_features_get_symbol_from_string:n { #1 } + \__stex_copymodule_get_symbol_from_string:nn { #1 }{ #2 } } }{ % argument is not a command name - \__stex_features_get_symbol_from_string:n { #1 } + \__stex_copymodule_get_symbol_from_string:nn { #1 }{ #2 } % \l_stex_all_symbols_seq } } } -\cs_new_protected:Nn \__stex_features_get_symbol_from_string:n { +\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_set:nnn{stex}{error/unknownsymbol}{ - No~symbol~#1~found! - } - \msg_error:nn{stex}{error/unknownsymbol} + \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 \l__stex_features_copymodule_fields_seq { + \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 } @@ -3517,7 +4114,6 @@ \str_set:Nn \l_stex_get_symbol_uri_str { ##1 } - \__stex_features_get_symbol_check: } } } @@ -3526,14 +4122,14 @@ } } -\cs_new_protected:Nn \__stex_features_get_symbol_from_cs:n { +\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_features_get_symbol_check: + \__stex_copymodule_get_symbol_check:n { #1 } }{ % TODO % tail is not a single group @@ -3544,166 +4140,163 @@ } } -\cs_new_protected:Nn \__stex_features_get_symbol_check: { - \exp_args:NNno \seq_set_split:Nnn \l_tmpa_seq {?} \l_stex_get_symbol_uri_str - \int_compare:nNnTF {\seq_count:N \l_tmpa_seq} = 3 { - \seq_pop_right:NN \l_tmpa_seq \l_tmpb_str - \str_set:Nx \l_tmpa_str {\seq_use:Nn \l_tmpa_seq ?} - \seq_if_in:NoF \l__stex_features_copymodule_modules_seq \l_tmpa_str { - \msg_error:nnxx{stex}{error/copymodule/notallowed}{\l_stex_get_symbol_uri_str}{ - \l_stex_current_copymodule_name_str\\Allowed:~\seq_use:Nn \l__stex_features_copymodule_modules_seq {,~} - } - } - }{ +\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}{ - \l_stex_current_copymodule_name_str~(inexplicably) + :~\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_features_copymodule_modules_seq \l_stex_collect_imports_seq - \seq_clear:N \l__stex_features_copymodule_fields_seq - \seq_map_inline:Nn \l__stex_features_copymodule_modules_seq { + \seq_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_features_copymodule_fields_seq { + \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 + includes = \l_tmpa_seq %, + % fields = \l_tmpa_seq } \stex_debug:nn{copymodule}{#4~for~module~{\l_stex_import_ns_str ?\l_stex_import_name_str} as~\l_stex_current_module_str?\l_stex_current_copymodule_name_str} - \stex_debug:nn{copymodule}{modules:\seq_use:Nn \l__stex_features_copymodule_modules_seq {,~}} - \stex_debug:nn{copymodule}{fields:\seq_use:Nn \l__stex_features_copymodule_fields_seq {,~}} - \stex_if_smsmode:F { + \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{from}{\l_stex_import_ns_str ?\l_stex_import_name_str}{} + \stex_annotate_invisible:nnn{domain}{\l_stex_import_ns_str ?\l_stex_import_name_str}{} } - \bool_set_eq:NN \l__stex_features_oldhtml_bool \_stex_html_do_output_bool - \bool_set_false:N \_stex_html_do_output_bool } + \cs_new_protected:Nn \stex_copymodule_end:n { + % apply to every field \def \l_tmpa_cs ##1 ##2 {#1} - \bool_set_eq:NN \_stex_html_do_output_bool \l__stex_features_oldhtml_bool - \tl_clear:N \l_tmpa_tl - \tl_clear:N \l_tmpb_tl - \prop_get:NnN \l_stex_current_copymodule_prop {fields} \l_tmpa_seq - \seq_map_inline:Nn \l__stex_features_copymodule_modules_seq { + + \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 \l_tmpc_tl + + \tl_clear:N \__stex_copymodule_curr_symbol_tl % <- wrap in current symbol html \l_tmpa_cs{##1}{####1} - \str_if_exist:cTF {l__stex_features_copymodule_##1?####1_name_str} { - \tl_put_right:Nx \l_tmpa_tl { - \prop_set_from_keyval:cn { - l_stex_symdecl_\l_stex_current_module_str ? \use:c{l__stex_features_copymodule_##1?####1_name_str}_prop - }{ - \exp_after:wN \prop_to_keyval:N \csname - l_stex_symdecl_\l_stex_current_module_str ? \use:c{l__stex_features_copymodule_##1?####1_name_str}_prop - \endcsname - } - \seq_clear:c { - l_stex_symdecl_ - \l_stex_current_module_str ? \use:c{l__stex_features_copymodule_##1?####1_name_str} - _notations + + \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}}{} } } - \tl_put_right:Nx \l_tmpc_tl { - \stex_copy_notations:nn {\l_stex_current_module_str ? \use:c{l__stex_features_copymodule_##1?####1_name_str}}{##1?####1} - \stex_annotate_invisible:nnn{alias}{\use:c{l__stex_features_copymodule_##1?####1_name_str}}{} - } - \seq_put_right:Nx \l_tmpa_seq {\l_stex_current_module_str ? \use:c{l__stex_features_copymodule_##1?####1_name_str}} - \str_if_exist:cT {l__stex_features_copymodule_##1?####1_macroname_str} { - \tl_put_right:Nx \l_tmpc_tl { - \stex_annotate_invisible:nnn{macroname}{\use:c{l__stex_features_copymodule_##1?####1_macroname_str}}{} - } - \tl_put_right:Nx \l_tmpa_tl { - \tl_set:cx {\use:c{l__stex_features_copymodule_##1?####1_macroname_str}}{ - \stex_invoke_symbol:n { - \l_stex_current_module_str ? \use:c{l__stex_features_copymodule_##1?####1_name_str} - } - } + }{ + \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}$ } } - }{ - \tl_put_right:Nx \l_tmpc_tl { - \stex_copy_notations:nn {\l_stex_current_module_str ? \l_stex_current_copymodule_name_str / ####1 }{##1?####1} + \prop_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 } - \prop_set_eq:Nc \l_tmpa_prop {l_stex_symdecl_ ##1?####1 _prop} - \prop_put:Nnx \l_tmpa_prop { name }{ \l_stex_current_copymodule_name_str / ####1 } - \prop_put:Nnx \l_tmpa_prop { module }{ \l_stex_current_module_str } - \tl_put_right:Nx \l_tmpa_tl { - \prop_set_from_keyval:cn { - l_stex_symdecl_\l_stex_current_module_str ? \l_stex_current_copymodule_name_str / ####1_prop - }{ - \prop_to_keyval:N \l_tmpa_prop - } - \seq_clear:c { - l_stex_symdecl_ - \l_stex_current_module_str ? \l_stex_current_copymodule_name_str / ####1 - _notations + } + + \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}}{} } } - \seq_put_right:Nx \l_tmpa_seq {\l_stex_current_module_str ? \l_stex_current_copymodule_name_str / ####1 } - \str_if_exist:cT {l__stex_features_copymodule_##1?####1_macroname_str} { - \tl_put_right:Nx \l_tmpc_tl { - \stex_annotate_invisible:nnn{macroname}{\use:c{l__stex_features_copymodule_##1?####1_macroname_str}}{} - } - \tl_put_right:Nx \l_tmpa_tl { - \tl_set:cx {\use:c{l__stex_features_copymodule_##1?####1_macroname_str}}{ - \stex_invoke_symbol:n { - \l_stex_current_module_str ? \l_stex_current_copymodule_name_str / ####1 - } + \tl_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 } } } } - \tl_if_exist:cT {l__stex_features_copymodule_##1?####1_def_tl}{ - \tl_put_right:Nx \l_tmpc_tl { - \stex_annotate_invisible:nnn{definiens}{}{$\use:c{l__stex_features_copymodule_##1?####1_def_tl}$} - } + + \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 \l_tmpb_tl { - \stex_annotate:nnn{assignment} {##1?####1} { \l_tmpc_tl } + + \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} \l_tmpa_seq - \tl_put_left:Nx \l_tmpa_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 } } - \exp_args:No \stex_add_to_current_module:n \l_tmpa_tl - \stex_debug:nn{copymodule}{result:\meaning \l_tmpa_tl} - \exp_args:Nx \stex_do_up_to_module:n { - \exp_args:No \exp_not:n \l_tmpa_tl + + \seq_gput_right:cx{c_stex_module_\l_stex_current_module_str _copymodules}{ + \l_stex_current_module_str?\l_stex_current_copymodule_name_str } - \l_tmpb_tl - \stex_if_smsmode:F { + + \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 }{ structure } + \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} @@ -3716,7 +4309,7 @@ } \NewDocumentEnvironment {interpretmodule} { O{} m m}{ - \stex_copymodule_start:nnnn { #1 }{ #2 }{ #3 }{ realization } + \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} @@ -3727,63 +4320,153 @@ }{ \stex_copymodule_end:n { \tl_if_exist:cF { - l__stex_features_copymodule_##1?##2_def_tl + l__stex_copymodule_copymodule_##1?##2_def_tl }{ - \msg_error:nnxx{stex}{error/interpretmodule/nodefiniens}{ - ##1?##2 - }{\l_stex_current_copymodule_name_str} + \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} + } } } } -\NewDocumentCommand \donotcopy { O{} m}{ +\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 } - \stex_collect_imports:n {\l_stex_import_ns_str ?\l_stex_import_name_str } - \seq_map_inline:Nn \l_stex_collect_imports_seq { - \seq_remove_all:Nn \l__stex_features_copymodule_modules_seq { ##1 } + \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}{ - \seq_remove_all:Nn \l__stex_features_copymodule_fields_seq { ##1 ? ####1 } - \bool_lazy_any_p:nT { - { \cs_if_exist_p:c {l__stex_features_copymodule_##1?####1_name_str}} - { \cs_if_exist_p:c {l__stex_features_copymodule_##1?####1_macroname_str}} - { \cs_if_exist_p:c {l__stex_features_copymodule_##1?####1_def_tl}} - }{ - % TODO throw error + \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} + } + }} } } } - - \prop_get:NnN \l_stex_current_copymodule_prop { includes } \l_tmpa_seq - \seq_put_right:Nx \l_tmpa_seq {\l_stex_import_ns_str ?\l_stex_import_name_str } - \prop_put:Nnx \l_stex_current_copymodule_prop {includes} \l_tmpa_seq + \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_copymodule:n {#1} + \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_features_copymodule_\l_stex_get_symbol_uri_str _def_tl}{#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_features_renamedecl_args:n { +\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_features_renamedecl_args:n { #1 } - \stex_get_symbol_in_copymodule:n {#2} + \__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_features_copymodule_\l_stex_get_symbol_uri_str _macroname_str}{#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_features_copymodule_\l_stex_get_symbol_uri_str _name_str}{\l_stex_renamedecl_name_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 @@ -3801,43 +4484,22 @@ \l_stex_current_module_str ? \l_stex_renamedecl_name_str _prop }{ module }{ \l_stex_current_module_str } - \exp_args:NNx \seq_put_left:Nn \l__stex_features_copymodule_fields_seq { + \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} -\seq_new:N \l_stex_implicit_morphisms_seq -\NewDocumentCommand \implicitmorphism { O{} m m}{ - \stex_import_module_uri:nn { #1 } { #2 } - \stex_debug:nn{implicits}{ - Implicit~morphism:~ - \l_stex_module_ns_str ? \l__stex_features_name_str - } - \exp_args:NNx \seq_if_in:NnT \l_stex_all_modules_seq { - \l_stex_module_ns_str ? \l__stex_features_name_str - }{ - \msg_error:nnn{stex}{error/conflictingmodules}{ - \l_stex_module_ns_str ? \l__stex_features_name_str - } - } - - % TODO - - \seq_put_right:Nx \l_stex_implicit_morphisms_seq { - \l_stex_module_ns_str ? \l__stex_features_name_str - } -} - -\NewDocumentEnvironment{structural@feature}{ m m m }{ +\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:\\ @@ -3847,240 +4509,498 @@ \msg_error:nn{stex}{error/nomodule} } - \str_set:Nx \l_stex_module_name_str { - \prop_item:Nn \l_stex_current_module_prop - { name } / #2 - feature - } - - \str_set:Nx \l_stex_module_ns_str { - \prop_item:Nn \l_stex_current_module_prop - { ns } - } + \str_set_eq:NN \l_stex_feature_parent_str \l_stex_current_module_str - \str_clear:N \l_tmpa_str - \seq_clear:N \l_tmpa_seq - \tl_clear:N \l_tmpa_tl - \exp_args:NNx \prop_set_from_keyval:Nn \l_stex_current_module_prop { - origname = #2, - name = \l_stex_module_name_str , - ns = \l_stex_module_ns_str , - imports = \exp_not:o { \l_tmpa_seq } , - constants = \exp_not:o { \l_tmpa_seq } , - content = \exp_not:o { \l_tmpa_tl } , - file = \exp_not:o { \g_stex_currentfile_seq } , - lang = \l_stex_module_lang_str , - sig = \l_tmpa_str , - meta = \l_tmpa_str , - feature = #1 , - } + \stex_module_setup:nn{meta=NONE}{#2 - #1} - \stex_if_smsmode:F { - \begin{stex_annotate_env}{ feature:#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_set:Nx \l_tmpa_str { - c_stex_feature_ - \prop_item:Nn \l_stex_current_module_prop { ns } ? - \prop_item:Nn \l_stex_current_module_prop { name } - _prop + \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 } - \prop_gset_eq:cN { \l_tmpa_str } \l_stex_current_module_prop - \prop_gset_eq:NN \g_stex_last_feature_prop \l_stex_current_module_prop - \stex_if_smsmode:F { + \stex_if_do_html:T { \end{stex_annotate_env} } } - - -\prop_new:N \l_stex_all_structures_prop +\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_features_structure_name_str , + name .str_set_x:N = \l__stex_structures_name_str , } -\cs_new_protected:Nn \__stex_features_structure_args:n { - \str_clear:N \l__stex_features_structure_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}{ O{} m }{ - \__stex_features_structure_args:n { #1 } - \str_if_empty:NT \l__stex_features_structure_name_str { - \str_set:Nx \l__stex_features_structure_name_str { #2 } +\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}{ structure } - { \l__stex_features_structure_name_str }{} - \seq_clear:N \l_tmpa_seq - \prop_put:Nno \l_stex_current_module_prop { fields } \l_tmpa_seq - \stex_smsmode_do: + \begin{structural_feature_module}{ structure } + { \l__stex_structures_name_str }{} + \stex_smsmode_do: }{ - \prop_get:NnN \l_stex_current_module_prop { constants } \l_tmpa_seq - \prop_get:NnN \l_stex_current_module_prop { fields } \l_tmpb_seq - \str_set:Nx \l_tmpa_str { - \prop_item:Nn \l_stex_current_module_prop { ns } ? - \prop_item:Nn \l_stex_current_module_prop { name } + \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 } } - \seq_map_inline:Nn \l_tmpa_seq { - \exp_args:NNx \seq_put_right:Nn \l_tmpb_seq { \l_tmpa_str ? ##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} } - \prop_put:Nno \l_stex_current_module_prop { fields } { \l_tmpb_seq } - \exp_args:Nnx - \AddToHookNext { env / mathstructure / after }{ - \symdecl{ #2 }[type = \exp_not:N\collection,def={\STEXsymbol{module-type}{ - \_stex_term_math_oms:nnnn { \l_tmpa_str }{}{0}{} - }}, name = \prop_item:Nn \l_stex_current_module_prop { origname }] - \STEXexport { - \prop_put:Nno \exp_not:N \l_stex_all_structures_prop - {\prop_item:Nn \l_stex_current_module_prop { origname }} - {\l_tmpa_str} - \prop_put:Nno \exp_not:N \l_stex_all_structures_prop - {#2}{\l_tmpa_str} - } - } - - \end{structural@feature} - % \g_stex_last_feature_prop -} -\seq_new:N \l__stex_features_structure_field_seq -\str_new:N \l__stex_features_structure_field_str -\str_new:N \l__stex_features_structure_def_tl -\prop_new:N \l__stex_features_structure_prop -\NewDocumentCommand \instantiate { m O{} m }{ - \prop_get:NnN \l_stex_all_structures_prop {#1} \l_tmpa_str - \prop_set_eq:Nc \l__stex_features_structure_prop { - c_stex_feature_\l_tmpa_str _prop - } - \seq_set_from_clist:Nn \l__stex_features_structure_field_seq { #2 } - \seq_map_inline:Nn \l__stex_features_structure_field_seq { - \seq_set_split:Nnn \l_tmpa_seq{=}{ ##1 } - \int_compare:nNnTF {\seq_count:N \l_tmpa_seq} > 1 { - \seq_get_left:NN \l_tmpa_seq \l_tmpa_tl - \exp_args:NNno \seq_set_split:Nnn \l_tmpb_seq - {!} \l_tmpa_tl - \int_compare:nNnTF {\seq_count:N \l_tmpb_seq} > 1 { - \str_set:Nx \l__stex_features_structure_field_str {\seq_item:Nn \l_tmpb_seq 1} - \seq_get_right:NN \l_tmpb_seq \l_tmpb_tl - \seq_get_right:NN \l_tmpa_seq \l_tmpa_tl - }{ - \str_set:Nx \l__stex_features_structure_field_str \l_tmpa_tl - \seq_get_right:NN \l_tmpa_seq \l_tmpa_tl - \exp_args:NNno \seq_set_split:Nnn \l_tmpb_seq{!} - \l_tmpa_tl - \int_compare:nNnTF {\seq_count:N \l_tmpb_seq} > 1 { - \seq_get_left:NN \l_tmpb_seq \l_tmpa_tl - \seq_get_right:NN \l_tmpb_seq \l_tmpb_tl + } +} + +\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: }{ - \tl_clear:N \l_tmpb_tl + \__stex_structures_get_from_string:n { #1 } } - } - }{ - \seq_set_split:Nnn \l_tmpa_seq{!}{ ##1 } - \int_compare:nNnTF {\seq_count:N \l_tmpa_seq} > 1 { - \str_set:Nx \l__stex_features_structure_field_str {\seq_item:Nn \l_tmpa_seq 1} - \seq_get_right:NN \l_tmpa_seq \l_tmpb_tl - \tl_clear:N \l_tmpa_tl }{ - % TODO throw error + \__stex_structures_get_from_string:n { #1 } } + }{ + \__stex_structures_get_from_string:n { #1 } } - % \l_tmpa_str: name - % \l_tmpa_tl: definiens - % \l_tmpb_tl: notation - \tl_if_empty:NT \l__stex_features_structure_field_str { - % TODO throw error + } +} + +\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} + } + }} + } + } } - \str_clear:N \l_tmpb_str + } + \l_tmpa_tl +} - \prop_get:NnN \l__stex_features_structure_prop { fields } \l_tmpa_seq - \seq_map_inline:Nn \l_tmpa_seq { - \seq_set_split:Nnn \l_tmpb_seq ? { ####1 } - \seq_get_right:NN \l_tmpb_seq \l_tmpb_str - \str_if_eq:NNT \l__stex_features_structure_field_str \l_tmpb_str { - \seq_map_break:n { - \str_set:Nn \l_tmpb_str { ####1 } +\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 } } - \prop_get:cnN { l_stex_symdecl_ \l_tmpb_str _prop } {args} - \l_tmpb_str - \tl_if_empty:NTF \l_tmpb_tl { - \tl_if_empty:NF \l_tmpa_tl { - \exp_args:Nx \use:n { - \symdecl{#3/\l__stex_features_structure_field_str}[args=\l_tmpb_str,def={\exp_args:No\exp_not:n{\l_tmpa_tl}}] + \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} } - }{ - \tl_if_empty:NTF \l_tmpa_tl { - \exp_args:Nx \use:n { - \symdef{#3/\l__stex_features_structure_field_str}[args=\l_tmpb_str]\exp_after:wN\exp_not:n\exp_after:wN{\l_tmpb_tl} + + \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} } - }{ - \exp_args:Nx \use:n { - \symdef{#3/\l__stex_features_structure_field_str}[args=\l_tmpb_str,def={\exp_args:No\exp_not:n{\l_tmpa_tl}}] - \exp_after:wN\exp_not:n\exp_after:wN{\l_tmpb_tl} + \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 } } +} - \tl_clear:N \l__stex_features_structure_def_tl +\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} + } +} - \prop_get:NnN \l__stex_features_structure_prop { fields } \l_tmpa_seq - \seq_map_inline:Nn \l_tmpa_seq { - \seq_set_split:Nnn \l_tmpb_seq ? { ##1 } - \seq_get_right:NN \l_tmpb_seq \l_tmpa_str - \exp_args:Nx \use:n { - \tl_put_right:Nn \exp_not:N \l__stex_features_structure_def_tl { +\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}} + } + } - \prop_if_exist:cF { - l_stex_symdecl_ - \prop_item:Nn \l_stex_current_module_prop {ns} ? - \prop_item:Nn \l_stex_current_module_prop {name} ? - #3/\l_tmpa_str - _prop - }{ - \prop_get:cnN { l_stex_symdecl_ ##1 _prop } {args} - \l_tmpb_str - \exp_args:Nx \use:n { - \symdecl{#3/\l_tmpa_str}[args=\l_tmpb_str] + \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 +} - \symdecl*{#3}[type={\STEXsymbol{module-type}{ - \_stex_term_math_oms:nnnn { - \prop_item:Nn \l__stex_features_structure_prop {ns} ? - \prop_item:Nn \l__stex_features_structure_prop {name} - }{}{0}{} - }}] +\cs_new_protected:Nn \stex_invoke_instance:n { + \peek_charcode_remove:NTF ! { + \stex_invoke_symbol:n{#1} + }{ + \_stex_invoke_instance:nn {#1} + } +} - % TODO: -> sms file +\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} + } +} - \tl_set:cx{ #3 }{ - \stex_invoke_structure:nnn { - \prop_item:Nn \l_stex_current_module_prop {ns} ? - \prop_item:Nn \l_stex_current_module_prop {name} ? #3 - } { - \prop_item:Nn \l__stex_features_structure_prop {ns} ? - \prop_item:Nn \l__stex_features_structure_prop {name} +\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 } } - \stex_smsmode_do: +} + +\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_features_structure_prop { + \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_features_structure_prop { fields } \l_tmpa_seq + \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 @@ -4135,7 +5055,7 @@ } % TODO root - \rustex_if:TF { + \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 } @@ -4151,13 +5071,15 @@ \str_set:Nx \l_tmpa_str { \prop_item:cn { l_stex_symdecl_ \l_stex_get_symbol_uri_str _prop } { name } } - \exp_args:NNno \str_replace_all:Nnn \l_tmpa_str {-} {~} - \rustex_if:TF { - \stex_annotate:nnn { definiendum } { \l_stex_get_symbol_uri_str } { - \l_tmpa_str\l__stex_statements_definiendum_post_tl + \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 } + } } { - \defemph@uri { + \exp_args:Nnx \defemph@uri { \l_tmpa_str\l__stex_statements_definiendum_post_tl } { \l_stex_get_symbol_uri_str } } @@ -4172,12 +5094,14 @@ } \exp_args:NNno \str_replace_all:Nnn \l_tmpa_str {-} {~} \stex_ref_new_sym_target:n \l_stex_get_symbol_uri_str - \rustex_if:TF { - \stex_annotate:nnn { definiendum } { \l_stex_get_symbol_uri_str } { - \l_tmpa_str\l__stex_statements_definiendum_post_tl - } + \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 + } + } } { - \defemph@uri { + \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 } } @@ -4185,18 +5109,51 @@ \stex_deactivate_macro:Nn \Definame {definition~environments} \NewDocumentCommand \premise { m }{ - \stex_annotate:nnn{ premise }{}{ #1 } + \noindent\stex_annotate:nnn{ premise }{}{\ignorespaces #1 } } \NewDocumentCommand \conclusion { m }{ - \stex_annotate:nnn{ conclusion }{}{ #1 } + \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 \definiens { m }{ - \stex_annotate:nnn{ definiens }{}{ #1 } + +\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 }{ @@ -4222,20 +5179,25 @@ \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_tmpa_seq + \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_tmpa_seq { + \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_tmpa_seq {,}} + \begin{stex_annotate_env}{definition}{\seq_use:Nn \l_tmpb_seq {,}} \str_if_empty:NF \sdefinitiontype { - \stex_annotate_invisible:nnn{type}{\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 @@ -4253,7 +5215,9 @@ \stex_ref_new_doc_target:n \sdefinitionid \stex_smsmode_do: }{ - \str_if_empty:NF \sdefinitionname { \stex_symdecl_do:nn{}{\sdefinitionname} } + \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 @@ -4271,11 +5235,11 @@ } } \cs_new_protected:Nn \__stex_statements_sdefinition_start: { - \par\noindent\titleemph{Definition\tl_if_empty:NF \sdefinitiontitle { + \stex_par:\noindent\titleemph{Definition\tl_if_empty:NF \sdefinitiontitle { ~(\sdefinitiontitle) }~} } -\cs_new_protected:Nn \__stex_statements_sdefinition_end: {\par\medskip} +\cs_new_protected:Nn \__stex_statements_sdefinition_end: {\stex_par:\medskip} \newcommand\stexpatchdefinition[3][] { \str_set:Nx \l_tmpa_str{ #1 } @@ -4308,26 +5272,31 @@ \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_if_smsmode:TF{\stex_suppress_html:n { \str_if_empty:NF \sdefinitionname { \stex_symdecl_do:nn{}{\sdefinitionname} } - }{ - \seq_clear:N \l_tmpa_seq + }}{ + \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_tmpa_seq { + \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_tmpa_seq {,}}{ + \stex_annotate:nnn{definition}{\seq_use:Nn \l_tmpb_seq {,}}{ \str_if_empty:NF \sdefinitiontype { - \stex_annotate_invisible:nnn{type}{\sdefinitiontype}{} + \stex_annotate_invisible:nnn{typestrings}{\sdefinitiontype}{} } #2 - \str_if_empty:NF \sdefinitionname { \stex_symdecl_do:nn{}{\sdefinitionname} } + \str_if_empty:NF \sdefinitionname { + \stex_suppress_html:n{\stex_symdecl_do:nn{}{\sdefinitionname}} + \stex_annotate_invisible:nnn{statementname}{\sdefinitionname}{} + } } } \endgroup @@ -4355,21 +5324,25 @@ \__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_tmpa_seq + \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_tmpa_seq { + \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_tmpa_seq {,}} + \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 { @@ -4393,7 +5366,7 @@ \stex_smsmode_do: }{ \str_if_empty:NF \sassertionname { - \stex_symdecl_do:nn{}{\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 { @@ -4414,11 +5387,11 @@ } \cs_new_protected:Nn \__stex_statements_sassertion_start: { - \par\noindent\titleemph{Assertion~\tl_if_empty:NF \sassertiontitle { + \stex_par:\noindent\titleemph{Assertion~\tl_if_empty:NF \sassertiontitle { (\sassertiontitle) }~} } -\cs_new_protected:Nn \__stex_statements_sassertion_end: {\par\medskip} +\cs_new_protected:Nn \__stex_statements_sassertion_end: {\stex_par:\medskip} \newcommand\stexpatchassertion[3][] { \str_set:Nx \l_tmpa_str{ #1 } @@ -4447,6 +5420,7 @@ \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 { @@ -4458,28 +5432,29 @@ \stex_if_smsmode:TF{ \str_if_empty:NF \sassertionname { - \stex_symdecl_do:nn{}{\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_tmpa_seq + \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_tmpa_seq { + \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_tmpa_seq {,}}{ + \stex_annotate:nnn{assertion}{\seq_use:Nn \l_tmpb_seq {,}}{ \str_if_empty:NF \sassertiontype { - \stex_annotate_invisible:nnn{type}{\sassertiontype}{} + \stex_annotate_invisible:nnn{typestrings}{\sassertiontype}{} } #2 \str_if_empty:NF \sassertionname { - \stex_symdecl_do:nn{}{\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}{} } } } @@ -4491,11 +5466,13 @@ 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 } @@ -4506,19 +5483,22 @@ \stex_reactivate_macro:N \premise \stex_reactivate_macro:N \conclusion \stex_if_smsmode:F { - \seq_clear:N \l_tmpa_seq + \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_tmpa_seq { + \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_tmpa_seq {,}} + \begin{stex_annotate_env}{example}{\seq_use:Nn \l_tmpb_seq {,}} \str_if_empty:NF \sexampletype { - \stex_annotate_invisible:nnn{type}{\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 @@ -4538,7 +5518,9 @@ } \stex_smsmode_do: }{ - \str_if_empty:NF \sexamplename { \stex_symdecl_do:nn{}{\sexamplename} } + \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 @@ -4557,11 +5539,11 @@ } \cs_new_protected:Nn \__stex_statements_sexample_start: { - \par\noindent\titleemph{Example~\tl_if_empty:NF \sexampletitle { + \stex_par:\noindent\titleemph{Example~\tl_if_empty:NF \sexampletitle { (\sexampletitle) }~} } -\cs_new_protected:Nn \__stex_statements_sexample_end: {\par\medskip} +\cs_new_protected:Nn \__stex_statements_sexample_end: {\stex_par:\medskip} \newcommand\stexpatchexample[3][] { \str_set:Nx \l_tmpa_str{ #1 } @@ -4595,24 +5577,29 @@ \stex_ref_new_doc_target:n \sexampleid } \stex_if_smsmode:TF{ - \str_if_empty:NF \sexamplename { \stex_symdecl_do:nn{}{\examplename} } + \str_if_empty:NF \sexamplename { + \stex_suppress_html:n{\stex_symdecl_do:nn{}{\examplename}} + } }{ - \seq_clear:N \l_tmpa_seq + \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_tmpa_seq { + \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_tmpa_seq {,}}{ + \stex_annotate:nnn{example}{\seq_use:Nn \l_tmpb_seq {,}}{ \str_if_empty:NF \sexampletype { - \stex_annotate_invisible:nnn{type}{\sexampletype}{} + \stex_annotate_invisible:nnn{typestrings}{\sexampletype}{} } #2 - \str_if_empty:NF \sexamplename { \stex_symdecl_do:nn{}{\sexamplename} } + \str_if_empty:NF \sexamplename { + \stex_suppress_html:n{\stex_symdecl_do:nn{}{\sexamplename}} + \stex_annotate_invisible:nnn{statementname}{\sexamplename}{} + } } } \endgroup @@ -4626,7 +5613,8 @@ from .tl_set:N = \sparagraphfrom , to .tl_set:N = \sparagraphto , start .tl_set:N = \l_stex_sparagraph_start_tl , - name .str_set:N = \sparagraphname + name .str_set:N = \sparagraphname , + imports .tl_set:N = \l__stex_statements_sparagraph_imports_tl } \cs_new_protected:Nn \stex_sparagraph_args:n { @@ -4634,6 +5622,7 @@ \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 @@ -4651,19 +5640,19 @@ } \@in@omtexttrue \stex_if_smsmode:F { - \seq_clear:N \l_tmpa_seq + \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_tmpa_seq { + \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_tmpa_seq {,}} + \begin{stex_annotate_env}{paragraph}{\seq_use:Nn \l_tmpb_seq {,}} \str_if_empty:NF \sparagraphtype { - \stex_annotate_invisible:nnn{type}{\sparagraphtype}{} + \stex_annotate_invisible:nnn{typestrings}{\sparagraphtype}{} } \str_if_empty:NF \sparagraphfrom { \stex_annotate_invisible:nnn{from}{\sparagraphfrom}{} @@ -4671,6 +5660,9 @@ \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 { @@ -4678,6 +5670,7 @@ \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: }{ @@ -4685,6 +5678,14 @@ } } \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}}{ @@ -4709,7 +5710,7 @@ \ignorespacesandpars }{ \str_if_empty:NF \sparagraphname { - \stex_symdecl_do:nn{}{\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 { @@ -4730,7 +5731,7 @@ } \cs_new_protected:Nn \__stex_statements_sparagraph_start: { - \par\noindent\tl_if_empty:NTF \l_stex_sparagraph_start_tl { + \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}:~ } @@ -4738,7 +5739,7 @@ \titleemph{\l_stex_sparagraph_start_tl}~ } } -\cs_new_protected:Nn \__stex_statements_sparagraph_end: {\par\medskip} +\cs_new_protected:Nn \__stex_statements_sparagraph_end: {\stex_par:\medskip} \newcommand\stexpatchparagraph[3][] { \str_set:Nx \l_tmpa_str{ #1 } @@ -4785,23 +5786,23 @@ } \stex_if_smsmode:TF{ \str_if_empty:NF \sparagraphname { - \stex_symdecl_do:nn{}{\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_tmpa_seq + \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_tmpa_seq { + \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_tmpa_seq {,}}{ + \stex_annotate:nnn{paragraph}{\seq_use:Nn \l_tmpb_seq {,}}{ \str_if_empty:NF \sparagraphtype { - \stex_annotate_invisible:nnn{type}{\sparagraphtype}{} + \stex_annotate_invisible:nnn{typestrings}{\sparagraphtype}{} } \str_if_empty:NF \sparagraphfrom { \stex_annotate_invisible:nnn{from}{\sparagraphfrom}{} @@ -4810,11 +5811,12 @@ \stex_annotate_invisible:nnn{to}{\sparagraphto}{} } \str_if_empty:NF \sparagraphname { - \stex_symdecl_do:nn{}{\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_tmpa_seq { + \clist_map_inline:Nn \l_tmpb_seq { \stex_ref_new_sym_target:n {##1} } } @@ -5146,7 +6148,7 @@ } \cs_new_protected:Nn \__stex_sproof_sproof_end: {\sproofend} -\newcommand\stexpatchsproof[3][] { +\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 } @@ -5173,6 +6175,17 @@ } }{ \@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 }{ @@ -5187,17 +6200,6 @@ \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} } @@ -5215,7 +6217,7 @@ \end{stex_annotate_env} } } -\newenvironment{sproofcomment}[1][]{ +\newenvironment{spfcomment}[1][]{ \__stex_sproof_spf_args:n{#1} \clist_set:No \l_tmpa_clist \spftype \tl_set:Nn \l_tmpa_tl { @@ -5358,23 +6360,13 @@ premises .tl_set:N = \l__stex_sproof_just_premises_tl, args .tl_set:N = \l__stex_sproof_just_args_tl } -\newenvironment{justification}[1][]{}{} +\newcommand\spfjust[1][]{} \newcommand\stex_proof_premise:[2][]{#2} \newcommand\justarg[2][]{#2} -%%%%%%%%%%%%% others.dtx %%%%%%%%%%%%% - - % None -\NewDocumentCommand \MSC {m} { - % TODO -} -\@ifpackageloaded{tikzinput}{ - \RequirePackage{stex-tikzinput} -}{} - %%%%%%%%%%%%% metatheory.dtx %%%%%%%%%%%%% -\str_const:Nn \c_stex_metatheory_ns_str {http://mathhub.info/sTeX} +\str_const:Nn \c_stex_metatheory_ns_str {http://mathhub.info/sTeX/meta} \begingroup \stex_module_setup:nn{ ns=\c_stex_metatheory_ns_str, @@ -5387,15 +6379,21 @@ \csname stex_suppress_html:n\endcsname{ % is-a (a:A, a \in A, a is an A, etc.) \symdecl{isa}[args=ai] - \notation{isa}[typed]{#1 \comp{:} #2}{##1 \comp, ##2} + \notation{isa}[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] + \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} - \notation{bind}[depfun]{\comp( #1 \comp{)\;\to\;} #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} @@ -5416,23 +6414,34 @@ % function/operator application \symdecl{apply}[args=ia] - \notation{apply}[prec=0;0x\infprec,parens]{#1 \comp( #2 \comp)}{##1 \comp, ##2} + \notation{apply}[prec=0;0x\infprec,parens,op=\cdot(\cdot)]{#1 \comp( #2 \comp)}{##1 \comp, ##2} \notation{apply}[prec=0;0x\infprec,lambda]{#1 \; #2 }{##1 \; ##2} - % ``type'' of all collections (sets,classes,types,kinds) - \symdecl{collection} - \notation{collection}[U]{\comp{\mathcal{U}}} - \notation{collection}[set]{\comp{\textsf{Set}}} - % collection of propositions/booleans/truth values \symdecl{prop}[name=proposition] \notation{prop}[prop]{\comp{{\rm prop}}} \notation{prop}[BOOL]{\comp{{\rm BOOL}}} + \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}} @@ -5440,6 +6449,9 @@ \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} @@ -5448,25 +6460,62 @@ % structures \symdecl*{module-type}[args=1] - \notation{module-type}{\mathtt{MOD} #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{ - \let\nappa\apply \def\nappli#1#2#3#4{\apply{#1}{\naseqli{#2}{#3}{#4}}} \def\nappui#1#2#3#4{\apply{#1}{\nasequi{#2}{#3}{#4}}} \def\livar{\csname sequence-index\endcsname[li]} \def\uivar{\csname sequence-index\endcsname[ui]} \def\naseqli#1#2#3{\aseqfromto{\livar{#1}{#2}}{\livar{#1}{#3}}} \def\nasequi#1#2#3{\aseqfromto{\uivar{#1}{#2}}{\uivar{#1}{#3}}} - \def\nappe#1#2#3{\apply{#1}{\aseqfromto{#2}{#3}}} } \__stex_modules_end_module: \endgroup +%%%%%%%%%%%%% 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'. |