1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
|
\begin{sfragment}{The \texttt{smodule}-Environment}
\begin{environment}{smodule}
A new module is declared using the basic syntax
\begin{center}
\stexcode"\begin{smodule}[options]{ModuleName}...\end{smodule}".
\end{center}
A module is required to declare any new formal content such as symbols or
notations (but not variables, which may be introduced anywhere).
The |smodule|-environment takes several keyword arguments, all of which are
optional:
\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}
\end{environment}
\begin{mmtbox}
An \sTeX module corresponds to an \mmt/\omdoc \emph{theory}.
As such it gets assigned a module URI (\emph{universal resource identifier})
of the form |<namespace>?<module-name>|.
\end{mmtbox}
By default, opening a module will produce no output whatsoever,
e.g.:
\stexexample{%
\begin{smodule}[title={This is Some Module}]{SomeModule}
Hello World
\end{smodule}
}
\begin{function}{\stexpatchmodule}
We can customize this behavior either for all modules or
only for modules with a specific |type| using the command
\stexcode"\stexpatchmodule[optional-type]{begin-code}{end-code}".
Some optional parameters are then available in |\smodule*|-macros,
specifically |\smoduletitle|, |\smoduletype| and |\smoduleid|.
\end{function}
For example:
\stexexample{%
\stexpatchmodule[display]
{\textbf{Module (\smoduletitle)}\par}
{\par\noindent\textbf{End of Module (\smoduletitle)}}
\begin{smodule}[type=display,title={Some New Module}]{SomeModule2}
Hello World
\end{smodule}
}
\end{sfragment}
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "../stex-manual"
%%% End:
% LocalWords: srccite mmtbox stexexample stexpatchmodule smoduletitle smoduleid
% LocalWords: display,title
|