diff options
Diffstat (limited to 'macros/latex/contrib/stex/source/stex/modules.dtx')
-rw-r--r-- | macros/latex/contrib/stex/source/stex/modules.dtx | 824 |
1 files changed, 824 insertions, 0 deletions
diff --git a/macros/latex/contrib/stex/source/stex/modules.dtx b/macros/latex/contrib/stex/source/stex/modules.dtx new file mode 100644 index 0000000000..f345e3066b --- /dev/null +++ b/macros/latex/contrib/stex/source/stex/modules.dtx @@ -0,0 +1,824 @@ +% \iffalse meta-comment +% An Infrastructure for Semantic Macros and Module Scoping +% Copyright (c) 2019 Michael Kohlhase, all rights reserved +% this file is released under the +% LaTeX Project Public License (LPPL) +% +% The original of this file is in the public repository at +% http://github.com/sLaTeX/sTeX/ +% +% TODO update copyright +% +%<*driver> +\providecommand\bibfolder{../../lib/bib} +\input{../../doc/docheader} + +\begin{document} + \DocInput{\jobname.dtx} +\end{document} +%</driver> +% \fi +% +% \title{ \sTeX-Modules +% \thanks{Version {\fileversion} (last revised {\filedate})} +% } +% +% \author{Michael Kohlhase, Dennis Müller\\ +% FAU Erlangen-Nürnberg\\ +% \url{http://kwarc.info/} +% } +% +% \maketitle +% +%\ifinfulldoc\else +% This is the documentation for the \pkg{stex-modules} package. +% For a more high-level introduction, +% see \href{\basedocurl/manual.pdf}{the \sTeX Manual} or the +% \href{\basedocurl/stex.pdf}{full \sTeX documentation}.\fi +% +% +% \begin{documentation}\label{pkg:modules:doc} +% +% This sub package contains code related to Modules +% +% \ifinfulldoc\else +% \input{../../doc/packages/modules} +% \fi +% +% \section{Macros and Environments}\label{pkg:modules:doc:macros} +% +% The content of a module with uri \meta{<URI>} is stored in four +% macros. All modifications of these macros are global: +% \begin{variable}{\c_stex_module_<URI>_prop} +% A property list with the following fields: +% \begin{itemize} +% \item[|name|] The \emph{name} of the module, +% \item[|ns|] the \emph{namespace} in field |ns|, +% \item[|file|] the \emph{file} containing the module, +% as a sequence of path fragments +% \item[|lang|] the module's \emph{language}, +% \item[|sig|] the language of the signature module, if the +% current file is a translation from some other language, +% \item[|deprecate|] if this module is deprecated, the module +% that replaces it, +% \item[|meta|] the metatheory of the module. +% \end{itemize} +% \end{variable} +% +% \begin{variable}{\c_stex_module_<URI>_code} +% The code to execute when this module is activated (i.e. imported), +% e.g. to set all the semantic macros, notations, etc. +% \end{variable} +% +% \begin{variable}{\c_stex_module_<URI>_constants} +% The names of all constants declared in the module +% \end{variable} +% +% \begin{variable}{\c_stex_module_<URI>_constants} +% The full URIs of all modules imported in this module +% \end{variable} +% +% \begin{variable}{\l_stex_current_module_str} +% \cs{l_stex_current_module_str} always +% contains the URI of the current module (if existent). +% \end{variable} +% +% \begin{variable}{\l_stex_all_modules_seq} +% Stores full URIs for all modules currently in scope. +% \end{variable} +% +% \begin{function}[pTF]{\stex_if_in_module:} +% Conditional for whether we are currently in a module +% \end{function} +% +% \begin{function}[pTF]{\stex_if_module_exists:n} +% Conditional for whether a module with the provided URI +% is already known. +% \end{function} +% +% \begin{function}{\stex_add_to_current_module:n,\STEXexport} +% Adds the provided tokens to the |_code| control sequence of the +% current module. +% +% \cs{stex_add_to_current_module:n} is used internally, +% \cs{STEXexport} is intended for users and additionally executes +% the provided code immediately. +% \end{function} +% +% \begin{function}{\stex_add_constant_to_current_module:n} +% Adds the declaration with the provided name to the |_constants| +% control sequence of the current module. +% \end{function} +% +% \begin{function}{\stex_add_import_to_current_module:n} +% Adds the module with the provided full URI to the |_imports| +% control sequence of the current module. +% \end{function} +% +% \begin{function}{\stex_collect_imports:n} +% Iterates over all imports of the provided (full URI of a) module +% and stores them as a topologically sorted list -- including +% the provided module as the last element -- in +% |\l_stex_collect_imports_seq| +% \end{function} +% +% \begin{function}{\stex_do_up_to_module:n} +% Code that is \emph{exported} from module (such as symbol declarations) +% should be local \emph{to the current module}. For that reason, ideally +% all symbol declarations and similar commands should be called directly +% in the module environment, however, that is not always feasible, e.g. +% in structural features or |sparapraph|s. \cs{stex_do_up_to_module} +% therefore executes the provided code repeatedly in an \cs{aftergroup} +% up until the group level is equal to that of the innermost smodule environment. +% \end{function} +% +% \begin{function}{\stex_modules_current_namespace:} +% Computes the current namespace as follows: +% +% If the current file is |.../source/sub/file.tex| in some archive +% with namespace |http://some.namespace/foo|, then the namespace of +% is |http://some.namespace/foo/sub/file|. Otherwise, the namespace +% is the absolute file path of the current file (i.e. starting with |file:///|). +% +% The result is stored in |\l_stex_modules_ns_str|. Additionally, the sub path +% relative to the current repository is stored in |\l_stex_modules_subpath_str|. +% \end{function} +% +% \subsection{The \texttt{smodule} environment} +% +% \begin{environment}{module} +% \begin{syntax} \cs{begin}|{module}[|\meta{options}|]|\Arg{name}\end{syntax} +% +% Opens a new module with name \meta{name}. Options are: +% \begin{itemize} +% \item[|title|] (\meta{token list}) to display in customizations. +% \item[|type|] (\meta{string}$\ast$) for use in customizations. +% \item[|deprecate|] (\meta{module}) if set, will throw a warning +% when loaded, urging to use \meta{module} instead. +% \item[|id|] (\meta{string}) for cross-referencing. +% \item[|ns|] (\meta{URI}) the namespace to use. \emph{Should not be used, +% unless you know precisely what you're doing}. If not explicitly set, is +% computed using \cs{stex_modules_current_namespace:}. +% \item[|lang|] (\meta{language}) if not set, computed from the current file name (e.g. |foo.en.tex|). +% \item[|sig|] (\meta{language}) if the current file is a translation of a file with the same base name +% but a different language suffix, setting |sig=<lang>| will preload the module +% from that language file. This helps ensuring that the (formal) content of both modules +% is (almost) identical across languages and avoids duplication. +% \item[|creators|] (\meta{string}$\ast$) names of the creators. +% \item[|contributors|] (\meta{string}$\ast$) names of contributors. +% \item[|srccite|] (\meta{string}) a source citation for the content of this module. +% \end{itemize} +% +% \begin{function}{\stex_module_setup:nn} +% \begin{syntax}\cs{stex_module_setup:nn}\Arg{params}\Arg{name}\end{syntax} +% Sets up a new module with name \meta{name} and optional parameters +% \meta{params}. In particular, sets +% \cs{l_stex_current_module_str} appropriately. +% \end{function} +% +% \end{environment} +% +% \begin{function}{\stexpatchmodule} +% \begin{syntax} \cs{stexpatchmodule} [\meta{type}] \Arg{begincode} \Arg{endcode} \end{syntax} +% Customizes the presentation for those |smodule|-environments +% with |type=|\meta{type}, or all others if no \meta{type} is given. +% \end{function} +% +% \begin{function}{\STEXModule} +% \begin{syntax} \cs{STEXModule} \Arg{fragment} \end{syntax} +% Attempts to find a module whose URI ends with \meta{fragment} +% in the current scope and passes the full URI on to +% \cs{stex_invoke_module:n}. +% \end{function} +% +% \begin{function}{\stex_invoke_module:n} +% Invoked by \cs{STEXModule}. Needs to be followed either +% by |!\macro| or |?|\Arg{symbolname}. In the first case, +% it stores the full URI in \cs{macro}; in the second +% case, it invokes the symbol \meta{symbolname} in the +% selected module. +% \end{function} +% +% \begin{function}{\stex_activate_module:n} +% Activate the module with the provided URI; i.e. executes +% all macro code of the module's |_code|-macro (does +% nothing if the module is already activated in the current +% context) and adds the module to \cs{l_stex_all_modules_seq}. +% \end{function} +% +% \end{documentation} +% +% \begin{implementation}\label{pkg:modules:impl} +% +% \section{\sTeX-Modules Implementation} +% +% \begin{macrocode} +%<*package> + +%%%%%%%%%%%%% modules.dtx %%%%%%%%%%%%% + +%<@@=stex_modules> +% \end{macrocode} +% +% Warnings and error messages +% +% \begin{macrocode} +\msg_new:nnn{stex}{error/unknownmodule}{ + No~module~#1~found +} +\msg_new:nnn{stex}{error/syntax}{ + Syntax~error:~#1 +} +\msg_new:nnn{stex}{error/siglanguage}{ + Module~#1~declares~signature~#2,~but~does~not~ + declare~its~language +} +\msg_new:nnn{stex}{warning/deprecated}{ + #1~is~deprecated;~please~use~#2~instead! +} + +\msg_new:nnn{stex}{error/conflictingmodules}{ + Conflicting~imports~for~module~#1 +} +% \end{macrocode} +% +% +% \begin{variable}{\l_stex_current_module_str} +% The current module: +% \begin{macrocode} +\str_new:N \l_stex_current_module_str +% \end{macrocode} +% \end{variable} +% +% \begin{variable}{\l_stex_all_modules_seq} +% Stores all available modules +% \begin{macrocode} +\seq_new:N \l_stex_all_modules_seq +% \end{macrocode} +% \end{variable} +% +% \begin{macro}[pTF]{\stex_if_in_module:} +% \begin{macrocode} +\prg_new_conditional:Nnn \stex_if_in_module: {p, T, F, TF} { + \str_if_empty:NTF \l_stex_current_module_str + \prg_return_false: \prg_return_true: +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}[pTF]{\stex_if_module_exists:n} +% \begin{macrocode} +\prg_new_conditional:Nnn \stex_if_module_exists:n {p, T, F, TF} { + \prop_if_exist:cTF { c_stex_module_#1_prop } + \prg_return_true: \prg_return_false: +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\stex_add_to_current_module:n,\STEXexport} +% +% Only allowed within modules: +% +% \begin{macrocode} +\cs_new_protected:Nn \stex_add_to_current_module:n { + \tl_gput_right:cn {c_stex_module_\l_stex_current_module_str _code} { #1 } +} +\cs_new_protected:Npn \STEXexport { + \begingroup + \newlinechar=-1\relax + \endlinechar=-1\relax + %\catcode`\ = 9\relax + \expandafter\endgroup\_@@_export:n +} +\cs_new_protected:Nn \_@@_export:n { + \ignorespaces #1 + \stex_add_to_current_module:n { \ignorespaces #1 } + \stex_smsmode_do: +} +\stex_deactivate_macro:Nn \STEXexport {module~environments} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\stex_add_constant_to_current_module:n} +% \begin{macrocode} +\cs_new_protected:Nn \stex_add_constant_to_current_module:n { + \str_set:Nx \l_tmpa_str { #1 } + \seq_gput_right:co {c_stex_module_\l_stex_current_module_str _constants} { \l_tmpa_str } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\stex_add_import_to_current_module:n} +% \begin{macrocode} +\cs_new_protected:Nn \stex_add_import_to_current_module:n { + \str_set:Nx \l_tmpa_str { #1 } + \exp_args:Nno + \seq_if_in:cnF{c_stex_module_\l_stex_current_module_str _imports}\l_tmpa_str{ + \seq_gput_right:co{c_stex_module_\l_stex_current_module_str _imports}\l_tmpa_str + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\stex_collect_imports:n} +% \begin{macrocode} +\cs_new_protected:Nn \stex_collect_imports:n { + \seq_clear:N \l_stex_collect_imports_seq + \_@@_collect_imports:n {#1} +} +\cs_new_protected:Nn \_@@_collect_imports:n { + \seq_map_inline:cn {c_stex_module_#1_imports} { + \seq_if_in:NnF \l_stex_collect_imports_seq { ##1 } { + \_@@_collect_imports:n { ##1 } + } + } + \seq_if_in:NnF \l_stex_collect_imports_seq { #1 } { + \seq_put_right:Nx \l_stex_collect_imports_seq { #1 } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\stex_do_up_to_module:n} +% \begin{macrocode} +\int_new:N \l_@@_group_depth_int +\tl_new:N \l_@@_aftergroup_tl +\cs_new_protected:Nn \stex_do_up_to_module:n { + \int_compare:nNnTF \l_@@_group_depth_int = \currentgrouplevel { + #1 + }{ + #1 + \expandafter \tl_gset:Nn \expandafter \l_@@_aftergroup_tl \expandafter { \l_@@_aftergroup_tl #1 } + \aftergroup\_@@_aftergroup_do: + } +} +\cs_new_protected:Nn \_@@_aftergroup_do: { + \int_compare:nNnTF \l_@@_group_depth_int = \currentgrouplevel { + \l_@@_aftergroup_tl + \tl_clear:N \l_@@_aftergroup_tl + }{ + \l_@@_aftergroup_tl + \aftergroup\_@@_aftergroup_do: + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\stex_modules_compute_namespace:nN} +% Computes the appropriate namespace from the top-level namespace +% of a repository (|#1|) and a file path +% (|#2|). +% +% +% \begin{macrocode} + +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\stex_modules_current_namespace:} +% +% Computes the current namespace based on the current +% MathHub repository (if existent) and the current file. +% +% \begin{macrocode} +\str_new:N \l_stex_modules_ns_str +\str_new:N \l_stex_modules_subpath_str +\cs_new_protected:Nn \_@@_compute_namespace:nN { + \str_set:Nx \l_tmpa_str { #1 } + \seq_set_eq:NN \l_tmpa_seq #2 + % split off file extension + \seq_pop_right:NN \l_tmpa_seq \l_tmpb_str + \exp_args:NNno \seq_set_split:Nnn \l_tmpb_seq . \l_tmpb_str + \seq_get_left:NN \l_tmpb_seq \l_tmpb_str + \seq_put_right:No \l_tmpa_seq \l_tmpb_str + + \bool_set_true:N \l_tmpa_bool + \bool_while_do:Nn \l_tmpa_bool { + \seq_pop_left:NN \l_tmpa_seq \l_tmpb_str + \exp_args:No \str_case:nnTF { \l_tmpb_str } { + {source} { \bool_set_false:N \l_tmpa_bool } + }{}{ + \seq_if_empty:NT \l_tmpa_seq { + \bool_set_false:N \l_tmpa_bool + } + } + } + + \stex_path_to_string:NN \l_tmpa_seq \l_stex_modules_subpath_str + \str_if_empty:NTF \l_stex_modules_subpath_str { + \str_set_eq:NN \l_stex_modules_ns_str \l_tmpa_str + }{ + \str_set:Nx \l_stex_modules_ns_str { + \l_tmpa_str/\l_stex_modules_subpath_str + } + } +} + +\cs_new_protected:Nn \stex_modules_current_namespace: { + \str_clear:N \l_stex_modules_subpath_str + \prop_if_exist:NTF \l_stex_current_repository_prop { + \prop_get:NnN \l_stex_current_repository_prop { ns } \l_tmpa_str + \_@@_compute_namespace:nN \l_tmpa_str \g_stex_currentfile_seq + }{ + % split off file extension + \seq_set_eq:NN \l_tmpa_seq \g_stex_currentfile_seq + \seq_pop_right:NN \l_tmpa_seq \l_tmpb_str + \exp_args:NNno \seq_set_split:Nnn \l_tmpb_seq . \l_tmpb_str + \seq_get_left:NN \l_tmpb_seq \l_tmpb_str + \seq_put_right:No \l_tmpa_seq \l_tmpb_str + \str_set:Nx \l_stex_modules_ns_str { + file:/\stex_path_to_string:N \l_tmpa_seq + } + } +} +% \end{macrocode} +% \end{macro} +% +% \subsubsection{The \texttt{smodule} environment} +% +% |smodule| arguments: +% +% \begin{macrocode} +\keys_define:nn { stex / module } { + title .tl_set:N = \smoduletitle , + type .str_set_x:N = \smoduletype , + id .str_set_x:N = \smoduleid , + deprecate .str_set_x:N = \l_stex_module_deprecate_str , + ns .str_set_x:N = \l_stex_module_ns_str , + lang .str_set_x:N = \l_stex_module_lang_str , + sig .str_set_x:N = \l_stex_module_sig_str , + creators .str_set_x:N = \l_stex_module_creators_str , + contributors .str_set_x:N = \l_stex_module_contributors_str , + meta .str_set_x:N = \l_stex_module_meta_str , + srccite .str_set_x:N = \l_stex_module_srccite_str +} + +\cs_new_protected:Nn \_@@_args:n { + \str_clear:N \smoduletitle + \str_clear:N \smoduletype + \str_clear:N \smoduleid + \str_clear:N \l_stex_module_ns_str + \str_clear:N \l_stex_module_deprecate_str + \str_clear:N \l_stex_module_lang_str + \str_clear:N \l_stex_module_sig_str + \str_clear:N \l_stex_module_creators_str + \str_clear:N \l_stex_module_contributors_str + \str_clear:N \l_stex_module_meta_str + \str_clear:N \l_stex_module_srccite_str + \keys_set:nn { stex / module } { #1 } +} + +% module parameters here? In the body? + +% \end{macrocode} +% +% \begin{macro}{\stex_module_setup:nn} +% Sets up a new module property list: +% \begin{macrocode} +\cs_new_protected:Nn \stex_module_setup:nn { + \str_set:Nx \l_stex_module_name_str { #2 } + \_@@_args:n { #1 } +% \end{macrocode} +% +% First, we set up the name and namespace of the module. +% +% Are we in a nested module? +% +% \begin{macrocode} + \stex_if_in_module:TF { + % Nested module + \prop_get:cnN {c_stex_module_\l_stex_current_module_str _prop} + { ns } \l_stex_module_ns_str + \str_set:Nx \l_stex_module_name_str { + \prop_item:cn {c_stex_module_\l_stex_current_module_str _prop} + { name } / \l_stex_module_name_str + } + }{ + % not nested: + \str_if_empty:NT \l_stex_module_ns_str { + \stex_modules_current_namespace: + \str_set_eq:NN \l_stex_module_ns_str \l_stex_modules_ns_str + \exp_args:NNNo \seq_set_split:Nnn \l_tmpa_seq + / {\l_stex_module_ns_str} + \seq_pop_right:NN \l_tmpa_seq \l_tmpa_str + \str_if_eq:NNT \l_tmpa_str \l_stex_module_name_str { + \str_set:Nx \l_stex_module_ns_str { + \stex_path_to_string:N \l_tmpa_seq + } + } + } + } +% \end{macrocode} +% +% Next, we determine the language of the module: +% +% \begin{macrocode} + \str_if_empty:NT \l_stex_module_lang_str { + \seq_get_right:NN \g_stex_currentfile_seq \l_tmpa_str + \seq_set_split:NnV \l_tmpa_seq . \l_tmpa_str + \seq_pop_right:NN \l_tmpa_seq \l_tmpa_str % .tex + \seq_pop_left:NN \l_tmpa_seq \l_tmpa_str % <filename> + \seq_if_empty:NF \l_tmpa_seq { %remaining element should be language + \stex_debug:nn{modules} {Language~\l_stex_module_lang_str~ + inferred~from~file~name} + \seq_pop_left:NN \l_tmpa_seq \l_stex_module_lang_str + } + } + + \stex_if_smsmode:F { \str_if_empty:NF \l_stex_module_lang_str { + \prop_get:NVNTF \c_stex_languages_prop \l_stex_module_lang_str + \l_tmpa_str { + \ltx@ifpackageloaded{babel}{ + \exp_args:Nx \selectlanguage { \l_tmpa_str } + }{} + } { + \msg_error:nnx{stex}{error/unknownlanguage}{\l_tmpa_str} + } + }} +% \end{macrocode} +% +% We check if we need to extend a signature module, and set +% \cs{l_stex_current_module_prop} accordingly: +% +% \begin{macrocode} + \str_if_empty:NTF \l_stex_module_sig_str { + \exp_args:Nnx \prop_gset_from_keyval:cn { + c_stex_module_\l_stex_module_ns_str?\l_stex_module_name_str _prop + } { + name = \l_stex_module_name_str , + ns = \l_stex_module_ns_str , + file = \exp_not:o { \g_stex_currentfile_seq } , + lang = \l_stex_module_lang_str , + sig = \l_stex_module_sig_str , + deprecate = \l_stex_module_deprecate_str , + meta = \l_stex_module_meta_str + } + \seq_clear:c {c_stex_module_\l_stex_module_ns_str?\l_stex_module_name_str _imports} + \seq_clear:c {c_stex_module_\l_stex_module_ns_str?\l_stex_module_name_str _constants} + \tl_clear:c {c_stex_module_\l_stex_module_ns_str?\l_stex_module_name_str _code} + \str_set:Nx\l_stex_current_module_str{\l_stex_module_ns_str?\l_stex_module_name_str} +% \end{macrocode} +% +% We load the metatheory: +% +% \begin{macrocode} + \str_if_empty:NT \l_stex_module_meta_str { + \str_set:Nx \l_stex_module_meta_str { + \c_stex_metatheory_ns_str ? Metatheory + } + } + \str_if_eq:VnF \l_stex_module_meta_str {NONE} { + \bool_set_true:N \l_stex_in_meta_bool + \exp_args:Nx \stex_add_to_current_module:n { + \bool_set_true:N \l_stex_in_meta_bool + \stex_activate_module:n {\l_stex_module_meta_str} + \bool_set_false:N \l_stex_in_meta_bool + } + \stex_activate_module:n {\l_stex_module_meta_str} + \bool_set_false:N \l_stex_in_meta_bool + } + }{ + \str_if_empty:NT \l_stex_module_lang_str { + \msg_error:nnxx{stex}{error/siglanguage}{ + \l_stex_module_ns_str?\l_stex_module_name_str + }{\l_stex_module_sig_str} + } + + \seq_set_eq:NN \l_tmpa_seq \g_stex_currentfile_seq + \seq_pop_right:NN \l_tmpa_seq \l_tmpa_str + \seq_set_split:NnV \l_tmpb_seq . \l_tmpa_str + \seq_pop_right:NN \l_tmpb_seq \l_tmpa_str % .tex + \seq_pop_left:NN \l_tmpb_seq \l_tmpa_str % <filename> + \str_set:Nx \l_tmpa_str { + \stex_path_to_string:N \l_tmpa_seq / + \l_tmpa_str . \l_stex_module_sig_str .tex + } + \IfFileExists \l_tmpa_str { + \exp_args:No \stex_file_in_smsmode:nn { \l_tmpa_str } { + \str_clear:N \l_stex_current_module_str + \seq_clear:N \l_stex_all_modules_seq + \stex_debug:nn{modules}{Loading~signature~\l_tmpa_str} + } + }{ + \msg_error:nnx{stex}{error/unknownmodule}{for~signature~\l_tmpa_str} + } + \stex_if_smsmode:F { + \stex_activate_module:n { + \l_stex_module_ns_str ? \l_stex_module_name_str + } + } + \str_set:Nx\l_stex_current_module_str{\l_stex_module_ns_str?\l_stex_module_name_str} + } + \str_if_empty:NF \l_stex_module_deprecate_str { + \msg_warning:nnxx{stex}{warning/deprecated}{ + Module~\l_stex_current_module_str + }{ + \l_stex_module_deprecate_str + } + } + \seq_put_right:Nx \l_stex_all_modules_seq { + \l_stex_module_ns_str ? \l_stex_module_name_str + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{environment}{smodule} +% +% The |module| environment. +% +% \begin{macro}{\_@@_begin_module:} +% +% implements |\begin{smodule}| +% +% \begin{macrocode} +\cs_new_protected:Nn \_@@_begin_module: { + \stex_reactivate_macro:N \STEXexport + \stex_reactivate_macro:N \importmodule + \stex_reactivate_macro:N \symdecl + \stex_reactivate_macro:N \notation + \stex_reactivate_macro:N \symdef + + \stex_debug:nn{modules}{ + New~module:\\ + Namespace:~\l_stex_module_ns_str\\ + Name:~\l_stex_module_name_str\\ + Language:~\l_stex_module_lang_str\\ + Signature:~\l_stex_module_sig_str\\ + Metatheory:~\l_stex_module_meta_str\\ + File:~\stex_path_to_string:N \g_stex_currentfile_seq + } + + \stex_if_smsmode:F{ + \begin{stex_annotate_env} {theory} { + \l_stex_module_ns_str ? \l_stex_module_name_str + } + + \stex_annotate_invisible:nnn{header}{} { + \stex_annotate:nnn{language}{ \l_stex_module_lang_str }{} + \stex_annotate:nnn{signature}{ \l_stex_module_sig_str }{} + \str_if_eq:VnF \l_stex_module_meta_str {NONE} { + \stex_annotate:nnn{metatheory}{ \l_stex_module_meta_str }{} + } + \str_if_empty:NF \smoduletype { + \stex_annotate:nnn{type}{\smoduletype}{} + } + } + } + \int_set:Nn \l_@@_group_depth_int {\currentgrouplevel} + % TODO: Inherit metatheory for nested modules? +} +\iffalse \end{stex_annotate_env} \fi %^^A make syntax highlighting work again +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\_@@_end_module:} +% +% implements |\end{module}| +% +% \begin{macrocode} +\cs_new_protected:Nn \_@@_end_module: { + \stex_debug:nn{modules}{Closing~module~\prop_item:cn {c_stex_module_\l_stex_current_module_str _prop} { name }} +} +% \end{macrocode} +% \end{macro} +% +% The core environment +% +% \begin{macrocode} +\iffalse \begin{stex_annotate_env} \fi %^^A make syntax highlighting work again +\NewDocumentEnvironment { smodule } { O{} m } { + \stex_module_setup:nn{#1}{#2} + \par + \stex_if_smsmode:F{ + \tl_clear:N \l_tmpa_tl + \clist_map_inline:Nn \smoduletype { + \tl_if_exist:cT {_@@_smodule_##1_start:}{ + \tl_set:Nn \l_tmpa_tl {\use:c{_@@_smodule_##1_start:}} + } + } + \tl_if_empty:NTF \l_tmpa_tl { + \_@@_smodule_start: + }{ + \l_tmpa_tl + } + } + \_@@_begin_module: + \str_if_empty:NF \smoduleid { + \stex_ref_new_doc_target:n \smoduleid + } + \stex_smsmode_do: +} { + \_@@_end_module: + \stex_if_smsmode:F { + \end{stex_annotate_env} + \clist_set:No \l_tmpa_clist \smoduletype + \tl_clear:N \l_tmpa_tl + \clist_map_inline:Nn \l_tmpa_clist { + \tl_if_exist:cT {_@@_smodule_##1_end:}{ + \tl_set:Nn \l_tmpa_tl {\use:c{_@@_smodule_##1_end:}} + } + } + \tl_if_empty:NTF \l_tmpa_tl { + \_@@_smodule_end: + }{ + \l_tmpa_tl + } + } +} +% \end{macrocode} +% \end{environment} +% +% \begin{macro}{\stexpatchmodule} +% \begin{macrocode} +\cs_new_protected:Nn \_@@_smodule_start: {} +\cs_new_protected:Nn \_@@_smodule_end: {} + +\newcommand\stexpatchmodule[3][] { + \str_set:Nx \l_tmpa_str{ #1 } + \str_if_empty:NTF \l_tmpa_str { + \tl_set:Nn \_@@_smodule_start: { #2 } + \tl_set:Nn \_@@_smodule_end: { #3 } + }{ + \exp_after:wN \tl_set:Nn \csname _@@_smodule_#1_start:\endcsname{ #2 } + \exp_after:wN \tl_set:Nn \csname _@@_smodule_#1_end:\endcsname{ #3 } + } +} +% \end{macrocode} +% \end{macro} +% +% \subsubsection{Invoking modules} +% +% \begin{macro}{\STEXModule,\stex_invoke_module:n} +% \begin{macrocode} +\NewDocumentCommand \STEXModule { m } { + \exp_args:NNx \str_set:Nn \l_tmpa_str { #1 } + \int_set:Nn \l_tmpa_int { \str_count:N \l_tmpa_str } + \tl_set:Nn \l_tmpa_tl { + \msg_error:nnx{stex}{error/unknownmodule}{#1} + } + \seq_map_inline:Nn \l_stex_all_modules_seq { + \str_set:Nn \l_tmpb_str { ##1 } + \str_if_eq:eeT { \l_tmpa_str } { + \str_range:Nnn \l_tmpb_str { -\l_tmpa_int } { -1 } + } { + \seq_map_break:n { + \tl_set:Nn \l_tmpa_tl { + \stex_invoke_module:n { ##1 } + } + } + } + } + \l_tmpa_tl +} + +\cs_new_protected:Nn \stex_invoke_module:n { + \stex_debug:nn{modules}{Invoking~module~#1} + \peek_charcode_remove:NTF ! { + \_@@_invoke_uri:nN { #1 } + } { + \peek_charcode_remove:NTF ? { + \_@@_invoke_symbol:nn { #1 } + } { + \msg_error:nnx{stex}{error/syntax}{ + ?~or~!~expected~after~ + \c_backslash_str STEXModule{#1} + } + } + } +} + +\cs_new_protected:Nn \_@@_invoke_uri:nN { + \str_set:Nn #2 { #1 } +} + +\cs_new_protected:Nn \_@@_invoke_symbol:nn { + \stex_invoke_symbol:n{#1?#2} +} +% \end{macrocode} +% \end{macro} +% +% \begin{macro}{\stex_activate_module:n} +% \begin{macrocode} +\bool_new:N \l_stex_in_meta_bool +\bool_set_false:N \l_stex_in_meta_bool +\cs_new_protected:Nn \stex_activate_module:n { + \stex_debug:nn{modules}{Activating~module~#1} + \seq_if_in:NnT \l_stex_implicit_morphisms_seq { #1 }{ + \msg_error:nnn{stex}{error/conflictingmodules}{ #1 } + } + \exp_args:NNx \seq_if_in:NnF \l_stex_all_modules_seq { #1 } { + \seq_put_right:Nx \l_stex_all_modules_seq { #1 } + \use:c{ c_stex_module_#1_code } + } +} +% \end{macrocode} +% \end{macro} +% +% \begin{macrocode} +%</package> +% \end{macrocode} +% +% \end{implementation} +% +% \PrintIndex |