summaryrefslogtreecommitdiff
path: root/macros/latex/contrib/stex/doc/packages/stex-modules.tex
diff options
context:
space:
mode:
Diffstat (limited to 'macros/latex/contrib/stex/doc/packages/stex-modules.tex')
-rw-r--r--macros/latex/contrib/stex/doc/packages/stex-modules.tex74
1 files changed, 73 insertions, 1 deletions
diff --git a/macros/latex/contrib/stex/doc/packages/stex-modules.tex b/macros/latex/contrib/stex/doc/packages/stex-modules.tex
index c067f28a1c..424c2200e8 100644
--- a/macros/latex/contrib/stex/doc/packages/stex-modules.tex
+++ b/macros/latex/contrib/stex/doc/packages/stex-modules.tex
@@ -1 +1,73 @@
-\textcolor{red}{TODO: modules documentation} \ No newline at end of file
+\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