summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/stex/source/stex/modules.dtx
diff options
context:
space:
mode:
Diffstat (limited to 'macros/latex/contrib/stex/source/stex/modules.dtx')
-rw-r--r--macros/latex/contrib/stex/source/stex/modules.dtx824
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