summaryrefslogtreecommitdiff
path: root/Master/texmf-dist/doc/latex/stex
diff options
context:
space:
mode:
authorKarl Berry <karl@freefriends.org>2022-05-24 20:23:29 +0000
committerKarl Berry <karl@freefriends.org>2022-05-24 20:23:29 +0000
commitd1a45dc92e84130c08386511a72d4ba1bc95b1b9 (patch)
tree0b41d5e406b7fb349d9c8a6fe3e05e255e2b92a9 /Master/texmf-dist/doc/latex/stex
parent36e380761892b6ddfed9ad4e5cd585a8b3ae17cc (diff)
stex (24may22)
git-svn-id: svn://tug.org/texlive/trunk@63390 c570f23f-e606-0410-a88d-b1316a301751
Diffstat (limited to 'Master/texmf-dist/doc/latex/stex')
-rw-r--r--Master/texmf-dist/doc/latex/stex/README.md52
-rw-r--r--Master/texmf-dist/doc/latex/stex/packages/stex-basics.tex35
-rw-r--r--Master/texmf-dist/doc/latex/stex/packages/stex-document-structure.tex156
-rw-r--r--Master/texmf-dist/doc/latex/stex/packages/stex-features.tex277
-rw-r--r--Master/texmf-dist/doc/latex/stex/packages/stex-hwexam.tex85
-rw-r--r--Master/texmf-dist/doc/latex/stex/packages/stex-inheritance.tex132
-rw-r--r--Master/texmf-dist/doc/latex/stex/packages/stex-mathhub.tex166
-rw-r--r--Master/texmf-dist/doc/latex/stex/packages/stex-metatheory.tex31
-rw-r--r--Master/texmf-dist/doc/latex/stex/packages/stex-modules.tex74
-rw-r--r--Master/texmf-dist/doc/latex/stex/packages/stex-problem.tex152
-rw-r--r--Master/texmf-dist/doc/latex/stex/packages/stex-proofs.tex215
-rw-r--r--Master/texmf-dist/doc/latex/stex/packages/stex-references.tex9
-rw-r--r--Master/texmf-dist/doc/latex/stex/packages/stex-slides.tex213
-rw-r--r--Master/texmf-dist/doc/latex/stex/packages/stex-statements.tex146
-rw-r--r--Master/texmf-dist/doc/latex/stex/packages/stex-symbols.tex588
-rw-r--r--Master/texmf-dist/doc/latex/stex/packages/stex-terms.tex178
-rw-r--r--Master/texmf-dist/doc/latex/stex/packages/stex-tikzinput.tex62
-rw-r--r--Master/texmf-dist/doc/latex/stex/stex-abstract.tex24
-rw-r--r--Master/texmf-dist/doc/latex/stex/stex-doc.pdfbin1467004 -> 1645539 bytes
-rw-r--r--Master/texmf-dist/doc/latex/stex/stex-doc.tex13
-rw-r--r--Master/texmf-dist/doc/latex/stex/stex-docheader.tex520
-rw-r--r--Master/texmf-dist/doc/latex/stex/stex-manual.pdfbin670569 -> 983933 bytes
-rw-r--r--Master/texmf-dist/doc/latex/stex/stex-manual.tex972
-rw-r--r--Master/texmf-dist/doc/latex/stex/stex-tutorial.tex354
24 files changed, 3521 insertions, 933 deletions
diff --git a/Master/texmf-dist/doc/latex/stex/README.md b/Master/texmf-dist/doc/latex/stex/README.md
index 13caa1f7342..b5eed1a41fa 100644
--- a/Master/texmf-dist/doc/latex/stex/README.md
+++ b/Master/texmf-dist/doc/latex/stex/README.md
@@ -3,8 +3,13 @@ sTeX: An Infrastructure for Semantic Preloading of LaTeX Documents
![CI Status](https://github.com/slatex/sTeX/workflows/CI/badge.svg)
This repository contains the sTeX package collection, a version of TeX/LaTeX that allows
-to markup TeX/LaTeX documents semantically without leaving the document format,
-essentially turning it into a document format for mathematical knowledge management (MKM).
+to markup TeX/LaTeX documents semantically without leaving the document format.
+
+Running `pdflatex` over sTeX-annotated documents formats them into normal-looking PDF. But
+sTeX also comes with a [conversion pipeline](https://github.com/slatex/RusTeX) into
+semantically annotated HTML5, which can host semantic added-value services that make the
+documents active (i.e. interactive and user-adaptive) and essentially turning LaTeX into a
+document format for (mathematical) knowledge management (MKM).
## Copyright & License
@@ -12,12 +17,41 @@ Copyright (c) 2022 Michael Kohlhase
The package is distributed under the terms of the LaTeX Project Public License (LPPL)
## Maintainers
-Michael Kohlhase, Dennis Müller, FAU Erlangen-Nürnberg.
+[Michael Kohlhase](https://kwarc.info/kohlhase), [Dennis Müller](https://kwarc.info/people/dmueller), FAU Erlangen-Nürnberg.
## Documentation
-See the
-[documentation of the sTeX package](https://github.com/slatex/sTeX/blob/main/doc/stex-doc.pdf)
-for details.
+The [sTeX manual ](https://github.com/slatex/sTeX/blob/main/doc/stex-manual.pdf) gives a
+general introduction and motivation. The
+[sTeX package documentation](https://github.com/slatex/sTeX/blob/main/doc/stex-doc.pdf)
+gives the details of the implementation. A complete list of sTeX-related publications can
+be found [here](https://kwarc.github.io/bibs/sTeX/).
+
+## sTeX Corpus & Best Practices
+
+sTeX comes with a large corpus of pre-annotated materials that act as evaluation grounds
+and regression tests for the sTeX functionality and best practices that are publicly
+available.
+* [HelloWorld](https://gl.mathhub.info/HelloWorld) a collection of simple hello world
+ examples the show off the best practices of sTeX annotation.
+* [SMGLoM](https://gl.mathhub.info/smglom), the Semantic, Multilingual Glossary of
+ Mathematics (and similar disciplines). SMGloM provides a large set of definitions and
+ well-designed semantic macros for core mathematical (and computation) concepts and
+ objects. This resource greatly facilitates "getting off the ground" in semantic
+ annotation.
+* [MiKoMH](https://gl.mathhub.info/MiKoMH) a set of semantically annotated courses in
+ computer science and (symbolic) AI (ca. 5000 pages of slides and notes). Ca. 3000
+ problem/solutions exist are only available upon request.
+* [sTeX3 Labs](https://gl.mathhub.info/sTeX) a set of experimental re-formalizations of
+ (mostly) [SMGLoM](https://gl.mathhub.info/smglom) material to fully take advantage of
+ the sTeX3 functionality and the
+ [rusTeX](https://github.com/slatex/RusTeX)/[MMT](https://uniformal.github.io) pipeline
+ and knowledge managemen facilities.
+
+All of these are hosted on [MathHub](https://mathhub.info), an experimental portal for the
+management of active mathematical documents and flexiformal mathematics. The organization
+of the material into "mathematical archives" (GIT repositories with a particular
+standardized structure on [a GitLab repository management server](https://gl.mathhub.info)
+greatly enhances modularization and the provision of added value services.
## Setup
@@ -31,10 +65,10 @@ Then update your `TEXINPUTS` environment variable, e.g. by placing the followin
export TEXINPUTS="$(TEXINPUTS):<sTeXDIR>//:
```
-Similarly, set your `MATHHUB` environment variable to where you intend to keep your sTeX archives. For details, see the documentation linked above.
+Similarly, set your `MATHHUB` environment variable to where you intend to keep your sTeX
+archives. For details, see the documentation linked above. For a LaTeX IDE, update the directory path where `pdflatex` looks for paths.
-For a LaTeX IDE, update the directory path where `pdflatex` looks for paths.
-For larger documents it may be necessary to enlarge the internal memory allocation of the TEX/LATEX executables. This can be done by adding the following configurations in `texmf.cnf` (or changing them, if they already exist).
+For larger documents it may (rarely) be necessary to enlarge the internal memory allocation of the TEX/LATEX executables. This can be done by adding the following configurations in `texmf.cnf` (or changing them, if they already exist).
```
param_size = 20000 % simultaneous macro parameters, also applies to MP
nest_size = 1000 % simultaneous semantic levels (e.g., groups)
diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-basics.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-basics.tex
index daa6d6418d2..f766b9b22f1 100644
--- a/Master/texmf-dist/doc/latex/stex/packages/stex-basics.tex
+++ b/Master/texmf-dist/doc/latex/stex/packages/stex-basics.tex
@@ -1,3 +1,9 @@
+We can use \sTeX by simply including the package with |\usepackage{stex}|,
+or -- primarily for individual fragments to be included in other
+documents -- by using the \sTeX document class with |\documentclass{stex}|
+which combines the \pkg{standalone} document class with the \pkg{stex}
+package.
+
Both the \pkg{stex} package and document class offer the following
options:
@@ -5,12 +11,31 @@ options:
\item[\texttt{lang}] (\meta{language}$\ast$) Languages
to load with the \pkg{babel} package.
\item[\texttt{mathhub}] (\meta{directory}) MathHub folder
- to search for repositories.
- \item[\texttt{sms}] (\meta{boolean}) use \emph{persisted}
- mode (not yet implemented).
+ to search for repositories -- this is not necessary if the
+ |MATHHUB| system variable is set.
+ \item[\texttt{writesms}] (\meta{boolean}) with this package
+ option, \sTeX will write the contents of all external
+ modules imported via \stexcode"\importmodule" or \stexcode"\usemodule"
+ into a file \stexcode"\jobname.sms" (analogously to
+ the table of contents \stexcode".toc"-file).
+ \item[\texttt{usems}] (\meta{boolean}) subsequently tells
+ \sTeX to read the generated sms-file at the beginning of the
+ document. This allows for e.g. collaborating on documents
+ without all authors having to have all used archives and
+ modules available -- one author can load the modules
+ with \texttt{writesms}, and the rest can use the
+ the modules with \texttt{usesms}. Furthermore, the sms
+ file can be submitted alongside a \texttt{tex}-file,
+ effectively making it ``standalone''.
\item[\texttt{image}] (\meta{boolean}) passed on to
\pkg{tikzinput}.
\item[\texttt{debug}] (\meta{log-prefix}$\ast$) Logs debugging
information with the given prefixes to the terminal,
- or all if |all| is given.
-\end{description} \ No newline at end of file
+ or all if |all| is given. Largely irrelevant for the
+ majority of users.
+\end{description}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "../stex-manual"
+%%% End:
diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-document-structure.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-document-structure.tex
index 1c8fe97dac2..f8d570ea5e0 100644
--- a/Master/texmf-dist/doc/latex/stex/packages/stex-document-structure.tex
+++ b/Master/texmf-dist/doc/latex/stex/packages/stex-document-structure.tex
@@ -1 +1,155 @@
-\textcolor{red}{TODO: document-structure documentation} \ No newline at end of file
+The \pkg{document-structure} package supplies an infrastructure for writing {\omdoc} documents in {\LaTeX}.
+This includes a simple structure sharing mechanism for \sTeX that allows to to move from
+a copy-and-paste document development model to a copy-and-reference model, which
+conserves space and simplifies document management. The augmented structure can be used
+by MKM systems for added-value services, either directly from the \sTeX sources, or
+after translation.
+
+
+ The \pkg{document-structure} package supplies macros and environments that allow to label document
+ fragments and to reference them later in the same document or in other documents. In
+ essence, this enhances the document-as-trees model to
+ documents-as-directed-acyclic-graphs (DAG) model. This structure can be used by MKM
+ systems for added-value services, either directly from the \sTeX sources, or after
+ translation. Currently, trans-document referencing provided by this package can only be
+ used in the \sTeX collection.
+
+ DAG models of documents allow to replace the ``Copy and Paste'' in the source document
+ with a label-and-reference model where document are shared in the document source and the
+ formatter does the copying during document formatting/presentation.
+
+The \pkg{document-structure} package accepts the following options:
+\begin{center}
+ \begin{tabular}{|l|p{10cm}|}\hline
+ \texttt{class=\meta{name}} & load \meta{name}|.cls| instead of |article.cls|\\\hline
+ \texttt{topsect=\meta{sect}} & The top-level sectioning level; the default for
+ \meta{sect} is \texttt{section}\\\hline
+ \end{tabular}
+\end{center}
+
+\begin{environment}{sfragment}
+ The structure of the document is given by nested |sfragment| environments. In the
+ {\LaTeX} route, the |sfragment| environment is flexibly mapped to sectioning commands,
+ inducing the proper sectioning level from the nesting of |sfragment|
+ environments. Correspondingly, the |sfragment| environment takes an optional key/value
+ argument for metadata followed by a regular argument for the (section) title of the
+ sfragment. The optional metadata argument has the keys |id| for an identifier,
+ |creators| and |contributors| for the Dublin Core metadata~\cite{DCMI:dmt03}. The option
+ |short| allows to give a short title for the generated section. If the title contains
+ semantic macros, they need to be protected by |\protect|\ednote{MK: still?}, and we need
+ to give the |loadmodules| key it needs no value. For instance we would have
+\begin{latexcode}
+\begin{smodule}{foo}
+ \symdef{bar}{B^a_r}
+ ...
+ \begin{sfragment}[id=sec.barderiv,loadmodules]
+ {Introducing $\protect\bar$ Derivations}
+\end{latexcode}
+
+\sTeX automatically computes the sectioning level, from the nesting of |sfragment|
+environments.
+\end{environment}
+
+But sometimes, we want to skip levels (e.g. to use a |\subsection*| as an introduction for
+a chapter).
+
+\begin{environment}{blindfragment}
+ Therefore the \pkg{document-structure} package provides a variant |blindfragment| that
+ does not produce markup, but increments the sectioning level and logically groups
+ document parts that belong together, but where traditional document markup relies on
+ convention rather than explicit markup. The |blindfragment| environment is useful
+ e.g. for creating frontmatter at the correct level. The example below shows a typical
+ setup for the outer document structure of a book with parts and chapters.
+
+\begin{latexcode}
+\begin{document}
+\begin{blindfragment}
+\begin{blindfragment}
+\begin{frontmatter}
+\maketitle\newpage
+\begin{sfragment}{Preface}
+... <<preface>> ...
+\end{sfragment}
+\clearpage\setcounter{tocdepth}{4}\tableofcontents\clearpage
+\end{frontmatter}
+\end{blindfragment}
+... <<introductory remarks>> ...
+\end{blindfragment}
+\begin{sfragment}{Introduction}
+... <<intro>> ...
+\end{sfragment}
+... <<more chapters>> ...
+\bibliographystyle{alpha}\bibliography{kwarc}
+\end{document}
+\end{latexcode}
+
+Here we use two levels of |blindfragment|:
+\begin{itemize}
+\item The outer one groups the introductory parts of the book (which we assume to have a
+ sectioning hierarchy topping at the part level). This |blindfragment| makes sure that
+ the introductory remarks become a ``chapter'' instead of a ``part''.
+\item The inner one groups the frontmatter\footnote{We shied away from redefining the
+ |frontmatter| to induce a blindfragment, but this may be the ``right'' way to go in
+ the future.} and makes the preface of the book a section-level construct.\ednote{MK:
+ We need a substitute for the ``Note that here the |display=flow| on the |sfragment|
+ environment prevents numbering as is traditional for prefaces.''}
+\end{itemize}
+\end{environment}
+
+\begin{function}{\skipfragment}
+ The |\skipfragment| ``skips an |sfragment|'', i.e. it just steps the respective sectioning
+ counter. This macro is useful, when we want to keep two documents in sync structurally,
+ so that section numbers match up: Any section that is left out in one becomes a
+ |\skipfragment|.
+\end{function}
+
+\begin{function}{\currentsectionlevel,\CurrentSectionLevel}
+ The |\currentsectionlevel| macro supplies the name of the current sectioning level,
+ e.g. ``chapter'', or ``subsection''. |\CurrentSectionLevel| is the capitalized
+ variant. They are useful to write something like ``In this |\currentsectionlevel|, we
+ will\ldots'' in an |sfragment| environment, where we do not know which sectioning level we
+ will end up.
+\end{function}
+
+\begin{function}{\prematurestop,\afterprematurestop}
+ For prematurely stopping the formatting of a document, \sTeX provides the
+ |\prematurestop| macro. It can be used everywhere in a document and ignores all input
+ after that -- backing out of the |sfragment| environment as needed. After that -- and
+ before the implicit |\end{document}| it calls the internal |\afterprematurestop|, which
+ can be customized to do additional cleanup or e.g. print the bibliography.
+
+ |\prematurestop| is useful when one has a driver file, e.g. for a course taught multiple
+ years and wants to generate course notes up to the current point in the lecture. Instead
+ of commenting out the remaining parts, one can just move the |\prematurestop| macro.
+ This is especially useful, if we need the rest of the file for processing, e.g. to
+ generate a theory graph of the whole course with the already-covered parts marked up as
+ an overview over the progress; see |import_graph.py| from the |lmhtools|
+ utilities~\cite{lmhtools:github:on}.
+\end{function}
+
+Text fragments and modules can be made more re-usable by the use of global variables. For
+instance, the admin section of a course can be made course-independent (and therefore
+re-usable) by using variables (actually token registers) |courseAcronym| and |courseTitle|
+instead of the text itself. The variables can then be set in the \sTeX preamble of the
+course notes file.
+
+\begin{function}{\setSGvar,\useSGvar}
+ |\setSGvar{|\meta{vname}|}{|\meta{text}|}| to set the global variable \meta{vname} to
+ \meta{text} and |\useSGvar{|\meta{vname}|}| to reference it.
+\end{function}
+
+\begin{function}{\ifSGvar}
+ With|\ifSGvar| we can test for the contents of a global variable: the macro call
+ |\ifSGvar{|\meta{vname}|}{|\meta{val}|}{|\meta{ctext}|}| tests the content of the global
+ variable \meta{vname}, only if (after expansion) it is equal to \meta{val}, the
+ conditional text \meta{ctext} is formatted.
+\end{function}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "../stex-manual"
+%%% End:
+
+% LocalWords: article.cls topsect DCMI:dmt03 loadmodules lmhtools
+% LocalWords: prematurestop afterprematurestop import_graph.py STRlabel STRcopy vname
+% LocalWords: STRsemantics setSGvar ifSGvar ctext
diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-features.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-features.tex
index e70bbaa0e84..b5ce5906d15 100644
--- a/Master/texmf-dist/doc/latex/stex/packages/stex-features.tex
+++ b/Master/texmf-dist/doc/latex/stex/packages/stex-features.tex
@@ -1,18 +1,173 @@
+\begin{sfragment}{The \texttt{mathstructure} Environment}
+\begin{smodule}[ns=https://github.com/slatex/sTeX/doc]{MathStructures}
+ A common occurence in mathematics is bundling several
+ interrelated ``declarations'' together into \emph{structures}.
+ For example:
+ \begin{itemize}
+ \item A \emph{monoid} is a structure $\mathstruct{M,\circ,e}$
+ with $\circ:M\times M\to M$ and $e\in M$ such that...
+ \item A \emph{topological space} is a structure
+ $\mathstruct{X,\mathcal T}$ where $X$ is a set and
+ $\mathcal T$ is a topology on $X$
+ \item A \emph{partial order} is a structure $\mathstruct{S,\leq}$
+ where $\leq$ is a binary relation on $S$ such that...
+ \end{itemize}
+
+ This phenomenon is important and common enough to warrant special
+ support, in particular because it requires being able
+ to \emph{instantiate} such structures (or, rather,
+ structure \emph{signatures}) in order to talk about (concrete
+ or variable) \emph{particular} monoids, topological spaces,
+ partial orders etc.
+
+ \begin{environment}{mathstructure}
+ The \stexcode"mathstructure" environment allows us to do
+ exactly that. It behaves exactly like the
+ \stexcode"smodule" environment, but is itself only allowed
+ inside an \stexcode"smodule" environment, and allows
+ for instantiation later on.
+ \end{environment}
+
+ How this works is again best demonstrated by example:
+ \symdef{funtype}[args=ai]{#1 \comp\to #2}{##1 \comp\times ##2}
+ \symdef{fun}[args=bi]{#1 \comp\mapsto #2}
+ \symdef{set}{\comp{\texttt{Set}}}
+
+ \stexexample{%
+\begin{mathstructure}{monoid}
+ \symdef{universe}[type=\set]{\comp{U}}
+ \symdef{op}[
+ args=2,
+ type=\funtype{\universe,\universe}{\universe},
+ op=\circ
+ ]{#1 \comp{\circ} #2}
+ \symdef{unit}[type=\universe]{\comp{e}}
+\end{mathstructure}
+
+A \symname{monoid} is...
+ }
+ Note that the \stexcode"\symname{monoid}" is appropriately
+ highlighted and (depending on your pdf viewer)
+ shows a URI on hovering -- implying that the \stexcode"mathstructure"
+ environment has generated a \emph{symbol} |monoid| for us.
+ It has not generated a semantic macro though, since
+ we can not use the |monoid|-symbol \emph{directly}. Instead,
+ we can instantiate it, for example for integers:
+
+ \stexexample{%
+\symdef{Int}[type=\set]{\comp{\mathbb Z}}
+\symdef{addition}[
+ type=\funtype{\Int,\Int}{\Int},
+ args=2,
+ op=+
+]{##1 \comp{+} ##2}
+\symdef{zero}[type=\Int]{\comp{0}}
+
+$\mathstruct{\Int,\addition!,\zero}$ is a \symname{monoid}.
+ }
+
+ So far, we have not actually instantiated |monoid|, but now
+ that we have all the symbols to do so, we can:
+
+ \stexexample{%
+\instantiate{intmonoid}{monoid}{\mathbb{Z}_{+,0}}[
+ universe = Int ,
+ op = addition ,
+ unit = zero
+]
+
+$\intmonoid{universe}$, $\intmonoid{unit}$ and $\intmonoid{op}{a}{b}$.
+
+Also: $\intmonoid!$
+ }
+ \begin{function}{\instantiate}
+ So summarizing:
+ \stexcode"\instantiate" takes four arguments: The
+ (macro-)name of the instance, a key-value pair assigning
+ declarations in the corresponding \stexcode"mathstructure"
+ to symbols currently in scope, the name of the \stexcode"mathstructure"
+ to instantiate, and lastly a notation for the instance itself.
+
+ It then generates a semantic macro that takes as argument
+ the name of a declaration in the instantiated \stexcode"mathstructure"
+ and resolves it to the corresponding instance of that particular declaration.
+ \end{function}
+
+ \begin{mmtbox}
+ \stexcode"\instantiate" and \stexcode"mathstructure" make use of the
+ \emph{Theories-as-Types} paradigm (see \cite{MueRabKoh:tat18}):
+
+ \stexcode"mathstructure{<name>}" simply creates a nested theory with name
+ |<name>-structure|. The \emph{constant} |<name>| is defined as
+ |Mod(<name>-structure)| -- a \emph{dependent record type with manifest fields},
+ the fields of which are generated from (and correspond to) the constants in
+ |<name>-structure|.
+
+ \stexcode"\instantiate" generates a constant whose definiens is a record term of
+ type |Mod(<name>-structure)|, with the fields assigned based on the respective
+ key-value-list.
+ \end{mmtbox}
+
+ Notably, \stexcode"\instantiate" throws an error if not \emph{every}
+ declaration in the instantiated \stexcode"mathstructure" is being assigned.
+
+ You might consequently ask what the usefulness of \stexcode"mathstructure"
+ even is.
+
+ \begin{function}{\varinstantiate}
+ The answer is that we can also instantiate a
+ \stexcode"mathstructure" with a \emph{variable}.
+ The syntax of \stexcode"\varianstantiate" is equivalent
+ to that of \stexcode"\instantiate", but all of the key-value-pairs
+ are optional, and if not explicitly assigned (to a symbol \emph{or}
+ a variable declared with \stexcode"\vardef") inherit their notation
+ from the one in the \stexcode"mathstructure" environment.
+ \end{function}
+
+ This allows us to do things like:
+
+ \stexexample{%
+\varinstantiate{varM}{monoid}{M}
+
+A \symname{monoid} is a structure
+$\varM!:=\mathstruct{\varM{universe},\varM{op}!,\varM{unit}}$
+such that
+$\varM{op}!:\funtype{\varM{universe},\varM{universe}}{\varM{universe}}$ ...
+}
+
+and
+
+\stexexample{%
+ \varinstantiate{varMb}{monoid}{M_2}[universe = Int]
+
+ Let $\varMb!:=\mathstruct{\varMb{universe},\varMb{op}!,\varMb{unit}}$
+be a \symname{monoid} on $\Int$ ...
+ }
+
+ We will return to these two example later, when we also know
+ how to handle the \emph{axioms} of a monoid.
+\end{smodule}
+\end{sfragment}
+
+\begin{sfragment}{The \texttt{copymodule} Environment}
+
+ \textcolor{red}{TODO: explain}
+
Given modules:
-\stexexample{
- \begin{smodule}{magma}
- \symdef{universe}{\comp{\mathcal U}}
- \symdef{operation}[args=2,op=\circ]{#1 \comp\circ #2}
- \end{smodule}
- \begin{smodule}{monoid}
- \importmodule{magma}
- \symdef{unit}{\comp e}
- \end{smodule}
- \begin{smodule}{group}
- \importmodule{monoid}
- \symdef{inverse}[args=1]{{#1}^{\comp{-1}}}
- \end{smodule}
+\stexexample{%
+\begin{smodule}{magma}
+ \symdef{universe}{\comp{\mathcal U}}
+ \symdef{operation}[args=2,op=\circ]{#1 \comp\circ #2}
+\end{smodule}
+\begin{smodule}{monoid}
+ \importmodule{magma}
+ \symdef{unit}{\comp e}
+\end{smodule}
+\begin{smodule}{group}
+ \importmodule{monoid}
+ \symdef{inverse}[args=1]{{#1}^{\comp{-1}}}
+\end{smodule}
}
We can form a module for \emph{rings} by ``cloning''
@@ -20,48 +175,64 @@ an instance of |group| (for addition) and |monoid| (for multiplication),
respectively, and ``glueing them together'' to ensure they share the
same universe:
-\stexexample{
- \begin{smodule}{ring}
- \begin{copymodule}{group}{addition}
- \renamedecl[name=universe]{universe}{runiverse}
- \renamedecl[name=plus]{operation}{rplus}
- \renamedecl[name=zero]{unit}{rzero}
- \renamedecl[name=uminus]{inverse}{ruminus}
- \end{copymodule}
- \notation*{rplus}[plus,op=+,prec=60]{#1 \comp+ #2}
- %\setnotation{rplus}{plus}
- \notation*{rzero}[zero]{\comp0}
- %\setnotation{rzero}{zero}
- \notation*{ruminus}[uminus,op=-]{\comp- #1}
- %\setnotation{ruminus}{uminus}
- \begin{copymodule}{monoid}{multiplication}
- \assign{universe}{\runiverse}
- \renamedecl[name=times]{operation}{rtimes}
- \renamedecl[name=one]{unit}{rone}
- \end{copymodule}
- \notation*{rtimes}[cdot,op=\cdot,prec=50]{#1 \comp\cdot #2}
- %\setnotation{rtimes}{cdot}
- \notation*{rone}[one]{\comp1}
- %\setnotation{rone}{one}
- Test: $\rtimes a{\rplus c{\rtimes de}}$
- \end{smodule}
+\stexexample{%
+\begin{smodule}{ring}
+ \begin{copymodule}{group}{addition}
+ \renamedecl[name=universe]{universe}{runiverse}
+ \renamedecl[name=plus]{operation}{rplus}
+ \renamedecl[name=zero]{unit}{rzero}
+ \renamedecl[name=uminus]{inverse}{ruminus}
+ \end{copymodule}
+ \notation*{rplus}[plus,op=+,prec=60]{#1 \comp+ #2}
+%\setnotation{rplus}{plus}
+ \notation*{rzero}[zero]{\comp0}
+%\setnotation{rzero}{zero}
+ \notation*{ruminus}[uminus,op=-]{\comp- #1}
+%\setnotation{ruminus}{uminus}
+ \begin{copymodule}{monoid}{multiplication}
+ \assign{universe}{\runiverse}
+ \renamedecl[name=times]{operation}{rtimes}
+ \renamedecl[name=one]{unit}{rone}
+ \end{copymodule}
+ \notation*{rtimes}[cdot,op=\cdot,prec=50]{#1 \comp\cdot #2}
+%\setnotation{rtimes}{cdot}
+ \notation*{rone}[one]{\comp1}
+%\setnotation{rone}{one}
+ Test: $\rtimes a{\rplus c{\rtimes de}}$
+\end{smodule}
}
\textcolor{red}{TODO: explain donotclone}
+
+\end{sfragment}
+
+\begin{sfragment}{The \texttt{interpretmodule} Environment}
+
+ \textcolor{red}{TODO: explain}
+
+\stexexample{%
+\begin{smodule}{int}
+ \symdef{Integers}{\comp{\mathbb Z}}
+ \symdef{plus}[args=2,op=+]{#1 \comp+ #2}
+ \symdef{zero}{\comp0}
+ \symdef{uminus}[args=1,op=-]{\comp-#1}
+
+ \begin{interpretmodule}{group}{intisgroup}
+ \assign{universe}{\Integers}
+ \assign{operation}{\plus!}
+ \assign{unit}{\zero}
+ \assign{inverse}{\uminus!}
+ \end{interpretmodule}
+\end{smodule}
+}
+
+\end{sfragment}
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "../stex-manual"
+%%% End:
-\stexexample{
- \begin{smodule}{int}
- \symdef{Integers}{\comp{\mathbb Z}}
- \symdef{plus}[args=2,op=+]{#1 \comp+ #2}
- \symdef{zero}{\comp0}
- \symdef{uminus}[args=1,op=-]{\comp-#1}
-
- \begin{interpretmodule}{group}{intisgroup}
- \assign{universe}{\Integers}
- \assign{operation}{\plus!}
- \assign{unit}{\zero}
- \assign{inverse}{\uminus!}
- \end{interpretmodule}
- \end{smodule}
-} \ No newline at end of file
+% LocalWords: circ,e intmonoid MueRabKoh:tat18 varinstantiate 2,op runiverse rplus prec
+% LocalWords: rzero uminus ruminus plus,op uminus,op rtimes cdot,op cdot,prec 1,op
+% LocalWords: donotclone intisgroup
diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-hwexam.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-hwexam.tex
index 5f1758b0150..5aced96e664 100644
--- a/Master/texmf-dist/doc/latex/stex/packages/stex-hwexam.tex
+++ b/Master/texmf-dist/doc/latex/stex/packages/stex-hwexam.tex
@@ -1 +1,84 @@
-\textcolor{red}{TODO: hwexam documentation} \ No newline at end of file
+
+The \pkg{hwexam} package and class supplies an infrastructure that allows to format
+nice-looking assignment sheets by simply including problems from problem files marked up
+with the \pkg{roblem} package. It is designed to be compatible with |problems.sty|, and
+inherits some of the functionality.
+
+\begin{variable}{solutions,notes,hints,gnotes,pts,min}
+ The \pkg{wexam} package and class take the options |solutions|, |notes|, |hints|,
+ |gnotes|, |pts|, |min|, and |boxed| that are just passed on to the \pkg{problems}
+ package (cf. its documentation for a description of the intended behavior).
+\end{variable}
+
+This package supplies the \DescribeEnv{assignment}|assignment| environment that groups
+problems into assignment sheets. It takes an optional KeyVal argument with the keys
+\DescribeMacro{number}|number| (for the assignment number; if none is given, 1 is
+assumed as the default or --- in multi-assignment documents --- the ordinal of the
+|assignment| environment), \DescribeMacro{title}|title| (for the assignment title; this
+is referenced in the title of the assignment sheet), \DescribeMacro{type}|type| (for the
+assignment type; e.g. ``quiz'', or ``homework''), \DescribeMacro{given}|given| (for the
+date the assignment was given), and \DescribeMacro{due}|due| (for the date the
+assignment is due).
+
+Furthermore, the \pkg{hwexam} package takes the option
+\DescribeMacro{multiple}|multiple| that allows to combine multiple assignment sheets
+into a compound document (the assignment sheets are treated as section, there is a table
+of contents, etc.).
+
+Finally, there is the option \DescribeMacro{test}|test| that modifies the behavior to
+facilitate formatting tests. Only in |test| mode, the macros |\testspace|,
+|\testnewpage|, and |\testemptypage| have an effect: they generate space for the
+students to solve the given problems. Thus they can be left in the {\LaTeX} source.
+
+\DescribeMacro{\testspace}|\testspace| takes an argument that expands to a dimension,
+and leaves vertical space accordingly. \DescribeMacro{\testnewpage}|\testnewpage| makes
+a new page in |test| mode, and \DescribeMacro{\testemptypage}|\testemptypage| generates
+an empty page with the cautionary message that this page was intentionally left empty.
+
+Finally, the \DescribeEnv{testheading}|\testheading| takes an optional keyword argument
+where the keys \DescribeMacro{duration}|duration| specifies a string that specifies the
+duration of the test, \DescribeMacro{min}|min| specifies the equivalent in number of
+minutes, and \DescribeMacro{reqpts}|reqpts| the points that are required for a perfect
+grade.
+
+\begin{latexcode}
+\title{320101 General Computer Science (Fall 2010)}
+\begin{testheading}[duration=one hour,min=60,reqpts=27]
+ Good luck to all students!
+\end{testheading}
+\end{latexcode}
+
+Will result in
+\begin{center}
+ \begin{minipage}{.9\textwidth}
+\makeatletter
+\@problem{1.1}{4}{10}
+\@problem{2.1}{4}{8}
+\@problem{2.2}{6}{10}
+\@problem{2.3}{6}{10}
+\@problem{3.1}{4}{8}
+\@problem{3.2}{4}{8}
+\@problem{3.3}{2}{4}
+\makeatother
+\title{320101 General Computer Science (Fall 2010)}
+\begin{testheading}[duration=one hour,min=60,reqpts=27]
+ good luck
+\end{testheading}
+\end{minipage}
+\end{center}
+\ednote{MK: The first three ``problems'' come from the stex examples above, how do we get rid
+ of this?}
+
+\begin{function}{\inputassignment}
+ The |\inputassignment| macro can be used to input an assignment from another file. It
+ takes an optional KeyVal argument and a second argument which is a path to the file
+ containing the problem (the macro assumes that there is only one |assignment|
+ environment in the included file). The keys |number|, |title|, |type|, |given|, and
+ |due| are just as for the |assignment| environment and (if given) overwrite the ones
+ specified in the |assignment| environment in the included file.
+\end{function}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "../stex-manual"
+%%% End:
diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-inheritance.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-inheritance.tex
index 41631f94d27..be7c4e68ec0 100644
--- a/Master/texmf-dist/doc/latex/stex/packages/stex-inheritance.tex
+++ b/Master/texmf-dist/doc/latex/stex/packages/stex-inheritance.tex
@@ -1 +1,131 @@
-\textcolor{red}{TODO: inheritance documentation} \ No newline at end of file
+\begin{sfragment}{Simple Inheritance and Namespaces}
+
+ \begin{function}{\importmodule,\usemodule}
+ \stexcode"\importmodule[Some/Archive]{path?ModuleName}" is only allowed within an
+ \stexcode"smodule"-environment and makes the symbols declared in |ModuleName|
+ available therein. Additionally the symbols of |ModuleName| will be exported if the
+ current module is imported somewhere else via \stexcode"\importmodule".
+
+ \stexcode"\usemodule" behaves the same way, but without exporting the content of the
+ used module.
+ \end{function}
+
+ It is worth going into some detail how exactly \stexcode"\importmodule"
+ and \stexcode"\usemodule" resolve their arguments to find
+ the desired module -- which is closely related to the
+ \emph{namespace} generated for a module, that is used to generate
+ its URI.
+
+ \begin{dangerbox}
+ Ideally, \sTeX would use arbitrary URIs for modules, with no
+ forced relationships between the \emph{logical} namespace
+ of a module and the \emph{physical} location of the file
+ declaring the module -- like \mmt does things.
+
+ Unfortunately, \TeX\ only provides very restricted access to
+ the file system, so we are forced to generate namespaces
+ systematically in such a way that they reflect the physical
+ location of the associated files, so that \sTeX can resolve
+ them accordingly. Largely, users need not concern themselves
+ with namespaces at all, but for completenesses sake, we describe
+ how they are constructed:
+
+ \begin{itemize}
+ \item If \stexcode"\begin{smodule}{Foo}"
+ \iffalse\end{smodule}\fi occurs in a file
+ |/path/to/file/Foo[.|\meta{lang}|].tex| which does not belong
+ to an archive, the namespace is |file://path/to/file|.
+ \item If the same statement occurs in a file
+ |/path/to/file/bar[.|\meta{lang}|].tex|, the namespace is
+ |file://path/to/file/bar|.
+ \end{itemize}
+
+ In other words: outside of archives, the namespace corresponds to
+ the file URI with the filename dropped iff it is equal to the
+ module name, and ignoring the (optional) language suffix.
+
+ If the current file is in an archive, the procedure is the same
+ except that the initial segment of the file path up to the archive's
+ |source|-folder is replaced by the archive's namespace URI.
+\end{dangerbox}
+
+\begin{dangerbox}
+ Conversely, here is how namespaces/URIs and file paths are computed
+ in import statements, examplary \stexcode"\importmodule":
+
+ \begin{itemize}
+ \item \stexcode"\importmodule{Foo}" outside of an archive refers
+ to module |Foo| in the current namespace. Consequently, |Foo|
+ must have been declared earlier in the same document or, if not,
+ in a file |Foo[.|\meta{lang}|].tex| in the same directory.
+ \item The same statement \emph{within} an archive refers to either
+ the module |Foo| declared earlier in the same document, or
+ otherwise to the module |Foo| in the archive's top-level namespace.
+ In the latter case, is has to be declared in a file |Foo[.|\meta{lang}|].tex|
+ directly in the archive's |source|-folder.
+ \item Similarly, in \stexcode"\importmodule{some/path?Foo}" the path
+ |some/path| refers to either the sub-directory and relative
+ namespace path of the current directory and namespace outside of an archive,
+ or relative to the current archive's top-level namespace and |source|-folder,
+ respectively.
+
+ The module |Foo| must either be declared in the file
+ \meta{top-directory}|/some/path/Foo[.|\meta{lang}|].tex|, or in
+ \meta{top-directory}|/some/path[.|\meta{lang}|].tex| (which are
+ checked in that order).
+ \item Similarly, \stexcode"\importmodule[Some/Archive]{some/path?Foo}"
+ is resolved like the previous cases, but relative to the archive
+ |Some/Archive| in the mathhub-directory.
+ \item Finally, \stexcode"\importmodule{full://uri?Foo}" naturally refers to the
+ module |Foo| in the namespace |full://uri|. Since the file this module
+ is declared in can not be determined directly from the URI, the module
+ must be in memory already, e.g. by being referenced earlier in the
+ same document.
+
+ Since this is less compatible with a modular development, using full
+ URIs directly is strongly discouraged, unless the module is delared in
+ the current file directly.
+ \end{itemize}
+
+ \end{dangerbox}
+
+ \begin{function}{\STEXexport}
+ \stexcode"\importmodule" and \stexcode"\usemodule" import all symbols, notations,
+ semantic macros and (recursively) \stexcode"\importmodule"s. If you want to
+ additionally export e.g. convenience macros and other (\sTeX) code from a module, you
+ can use the command \stexcode"\STEXexport{<code>}" in your module. Then |<code>| is
+ executed (both immediately and) every time the current module is opened via
+ \stexcode"\importmodule" or \stexcode"\usemodule".
+ \end{function}
+
+ \begin{dangerbox}
+ For persistency reasons, everything in an \stexcode"\STEXexport"
+ is digested by \TeX in the \LaTeX3-category code scheme.
+ This means that the characters \stexcode"_" and \stexcode":"
+ are considered \emph{letters} and valid parts of
+ control sequence names, and space characters are ignored entirely.
+ For spaces, use the character \stexcode"~" instead, and
+ keep in mind, that if you want to use subscripts, you
+ should use \stexcode"\c_math_subscript_token" instead
+ of \stexcode"_"!
+
+
+ Also note, that \stexcode"\newcommand" defines macros \emph{globally}
+ and throws an error if the macro already exists,
+ potentially leading to low-level \LaTeX\xspace errors if
+ we put a \stexcode"\newcommand" in an \stexcode"\STEXexport"
+ and the |<code>| is executed more than once in a document
+ -- which can happen easily.
+
+ A safer alternative is to use macro definition principles,
+ that are safe to use even if the macro being defined already
+ exists, and ideally are local to the current \TeX\xspace group,
+ such as \stexcode"\def" or \stexcode"\let".
+ \end{dangerbox}
+
+\end{sfragment}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "../stex-manual"
+%%% End:
diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-mathhub.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-mathhub.tex
index 4b05134e70d..fb872acfbad 100644
--- a/Master/texmf-dist/doc/latex/stex/packages/stex-mathhub.tex
+++ b/Master/texmf-dist/doc/latex/stex/packages/stex-mathhub.tex
@@ -1,5 +1,6 @@
\begin{sfragment}{The Local MathHub-Directory}
- |\usemodule|, |\importmodule|, |\inputref| etc. allow for
+ \stexcode"\usemodule", \stexcode"\importmodule",
+ \stexcode"\inputref" etc. allow for
including content modularly without having to specify absolute
paths, which would differ between users and machines. Instead,
\sTeX uses \emph{archives} that determine the global
@@ -7,30 +8,30 @@
for \sTeX to find content referenced via such URIs.
All \sTeX archives need to exist in the local |MathHub|-directory.
- \sTeX knows where this folder is via one of three means:
+ \sTeX knows where this folder is via one of four means:
\begin{enumerate}
- \item If the \sTeX package is loaded with the option
- |mathhub=/path/to/mathhub|, then \sTeX will consider
- |/path/to/mathhub| as the local |MathHub|-directory.
- \item If the |mathhub| package option is \emph{not}
- set, but the macro |\mathhub| exists when the
- \sTeX-package is loaded, then this macro is
- assumed to point to the local |MathHub|-directory; i.e.
- |\def\mathhub{/path/to/mathhub}\usepackage{stex}|
- will set the |MathHub|-directory as |path/to/mathhub|.
- \item Otherwise, \sTeX will attempt to retrieve the
- system variable |MATHHUB|, assuming it will
- point to the local |MathHub|-directory. Since this
- variant needs setting up only \emph{once} and is
- machine-specific (rather than defined in tex code),
- it is compatible with collaborating and sharing tex
- content, and hence recommended.
+ \item If the \sTeX package is loaded with the option |mathhub=/path/to/mathhub|, then
+ \sTeX will consider |/path/to/mathhub| as the local |MathHub|-directory.
+ \item If the |mathhub| package option is \emph{not} set, but the macro |\mathhub|
+ exists when the \sTeX-package is loaded, then this macro is assumed to point to the
+ local |MathHub|-directory; i.e.
+ \stexcode"\def\mathhub{/path/to/mathhub}\usepackage{stex}" will set the
+ |MathHub|-directory as |path/to/mathhub|.
+ \item Otherwise, \sTeX will attempt to retrieve the system variable |MATHHUB|,
+ assuming it will point to the local |MathHub|-directory. Since this variant needs
+ setting up only \emph{once} and is machine-specific (rather than defined in tex
+ code), it is compatible with collaborating and sharing tex content, and hence
+ recommended.
+ \item Finally, if all else fails, \sTeX will look for a file
+ |~/.stex/mathhub.path|. If this file exists, \sTeX will assume that it contains the
+ path to the local |MathHub|-directory. This method is recommended on systems where
+ it is difficult to set environment variables.
\end{enumerate}
\end{sfragment}
\begin{sfragment}{The Structure of \sTeX Archives}
- An \sTeX archive |group/name| needs to be stored in the
+ An \sTeX archive |group/name| is stored in the
directory |/path/to/mathhub/group/name|; e.g. assuming your
local |MathHub|-directory is set as |/user/foo/MathHub|, then
in order for the |smglom/calculus|-archive to be found by the
@@ -43,19 +44,41 @@
|MANIFEST.MF|, the content of which we will consider shortly
\end{itemize}
An additional |lib|-directory is optional, and is where \sTeX will
- look for files included via |\libinput|.
+ look for files included via \stexcode"\libinput".
Additionally a \emph{group} of archives |group/name| may have
an additional archive |group/meta-inf|. If this |meta-inf|-archive
- has a |/lib|-subdirectory, it too will be searched by |\libinput|
+ has a |/lib|-subdirectory, it too will be searched by \stexcode"\libinput"
from all tex files in any archive in the |group/*|-group.
+
+ \paragraph{} We recommend the following additional directory structure in the
+ |source|-folder of an \sTeX archive:
+ \begin{itemize}
+ \item |/source/mod/| -- individual \sTeX modules, containing
+ symbol declarations, notations, and
+ \stexcode"\begin{sparagraph}[type=symdoc,for=...]"
+ environments for ``encyclopaedic'' symbol documentations
+ \iffalse\end{sparagraph}\fi
+ \item |/source/def/| -- definitions
+ \item |/source/ex/| -- examples
+ \item |/source/thm/| -- theorems, lemmata and proofs; preferably
+ proofs in separate files to allow for multiple proofs for the
+ same statement
+ \item |/source/snip/| -- individual text snippets such as remarks,
+ explanations etc.
+ \item |/source/frag/| -- individual document fragments,
+ ideally only \stexcode"\inputref"ing snippets, definitions,
+ examples etc. in some desirable order
+ \item |/source/tikz/| -- tikz images, as individual |.tex|-files
+ \item |/source/PIC/| -- image files.
+ \end{itemize}
+
\end{sfragment}
\begin{sfragment}{MANIFEST.MF-Files}
- The |MANIFEST.MF| in the |META-INF|-directory consists of
- key-value-pairs, instructing \sTeX (and associated software)
- of various properties of an archive. For example,
- the |MANIFEST.MF| of the |smglom/calculus|-archive looks like this:
+ The |MANIFEST.MF| in the |META-INF|-directory consists of key-value-pairs, informing
+ \sTeX (and associated software) of various properties of an archive. For example, the
+ |MANIFEST.MF| of the |smglom/calculus|-archive looks like this:
\begin{framed}
\begin{verbatim}
@@ -86,4 +109,95 @@
e.g. for |lmh install|.
\end{itemize}
-\end{sfragment} \ No newline at end of file
+\end{sfragment}
+
+\begin{sfragment}{Using Files in \sTeX Archives Directly}
+ Several macros provided by \sTeX allow for directly including
+ files in repositories. These are:
+ \begin{function}{\mhinput}
+ \stexcode"\mhinput[Some/Archive]{some/file}" directly
+ inputs the file |some/file| in the |source|-folder of
+ |Some/Archive|.
+ \end{function}
+ \begin{function}{\inputref}
+ \stexcode"\inputref[Some/Archive]{some/file}" behaves like \stexcode"\mhinput", but
+ wraps the input in a |\begingroup ... \endgroup|. When converting to |xhtml|, the
+ file is not input at all, and instead an |html|-annotation is inserted that
+ references the file, e.g. for lazy loading.
+
+ In the majority of practical cases \stexcode"\inputref" is likely to be preferred
+ over \stexcode"\mhinput" because it leads to less duplication in the generated
+ |xhtml|.
+ \end{function}
+ \begin{function}{\ifinput}
+ Both \stexcode"\mhinput" and \stexcode"\inputref"
+ set \stexcode"\ifinput" to ``true'' during input. This allows
+ for selectively including e.g. bibliographies only if the
+ current file is not being currently included in a larger document.
+ \end{function}
+ \begin{function}{\addmhbibresource}
+ \stexcode"\addmhbibresource[Some/Archive]{some/file}" searches for a file like
+ \stexcode"\mhinput" does, but calls |\addbibresource| to the result and looks for
+ the file in the archive root directory directly, rather than the |source|
+ directory. Typical invocations are
+ \begin{itemize}
+ \item |\addmhbibresource{lib/refs.bib}|, which specifies a bibliography in the |lib|
+ folder in the local archive or
+ \item |\addmhbibresource[HW/meta-inf]{lib/refs.bib}| in another.
+ \end{itemize}
+ \end{function}
+ \begin{function}{\libinput}
+ \stexcode"\libinput{some/file}"
+ searches for a file |some/file| in
+ \begin{itemize}
+ \item the |lib|-directory of the current archive, and
+ \item the |lib|-directory of a |meta-inf|-archive in
+ (any of) the archive groups containing the current archive
+ \end{itemize}
+ and include all found files in reverse order;
+ e.g. \stexcode"\libinput{preamble}" in a |.tex|-file in
+ |smglom/calculus| will \emph{first} input |.../smglom/meta-inf/lib/preamble.tex|
+ and then |../smglom/calculus/lib/preamble.tex|.
+
+ \stexcode|\libinput| will throw an error if \emph{no} candidate for |some/file|
+ is found.
+ \end{function}
+ \begin{function}{\libusepackage}
+ \stexcode"\libusepackage[package-options]{some/file}" searches for a file
+ |some/file.sty| in the same way that \stexcode"\libinput" does, but will
+ call\\
+ |\usepackage[package-options]{path/to/some/file}| instead of |\input|.
+
+ \stexcode|\libusepackage| throws an error if not \emph{exactly one} candidate for
+ |some/file| is found.
+ \end{function}
+
+ \begin{remark}
+ A good practice is to have individual \sTeX fragments
+ follow basically this document frame:
+ \begin{latexcode}[gobble=12]
+ \documentclass{stex}
+ \libinput{preamble}
+ \begin{document}
+ ...
+ \ifinputref \else \libinput{postamble} \fi
+ \end{document}
+ \end{latexcode}
+ Then the |preamble.tex| files can take care of loading the generally required
+ packages, setting presentation customizations etc. (per archive or archive group
+ or both), and |postamble.tex| can e.g. print the bibliography, index etc.
+
+ \stexcode|\libusepackage| is particularly useful in |preamble.tex| when we want to
+ use custom packages that are not part of {\TeX}Live. In this case we commit the
+ respective packages in one of the |lib| folders and use \stexcode|\libusepackage|
+ to load them.
+ \end{remark}
+\end{sfragment}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "../stex-manual"
+%%% End:
+
+%%% LocalWords: mathhub symdoc,for lmh subdirs arithmetics,smglom sets,smglom mv,smglom
+%%% LocalWords: linear-algebra,smglom
diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-metatheory.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-metatheory.tex
index 1585ba504c8..4feb646eb9f 100644
--- a/Master/texmf-dist/doc/latex/stex/packages/stex-metatheory.tex
+++ b/Master/texmf-dist/doc/latex/stex/packages/stex-metatheory.tex
@@ -1 +1,30 @@
-\textcolor{red}{TODO: metatheory documentation} \ No newline at end of file
+The \pkg{stex-metatheory} package contains \sTeX symbols so ubiquitous, that it is
+virtually impossible to describe any flexiformal content without them, or that are
+required to annotate even the most primitive symbols with meaningful
+(foundation-independent) ``type''-annotations, or required for basic structuring
+principles (theorems, definitions). As such, it serves as the default meta theory for any
+\sTeX module.
+
+We can also see the \pkg{stex-metatheory} as a foundation of mathematics in the sense of
+\cite{rabe:future:15}, albeit an informal one (the ones discussed there are all formal
+foundations). The state of the \pkg{stex-metatheory} is necessarily incomplete, and will
+stay so for a long while: It arises as a collection of empirically useful symbols that are
+collected as more and more mathematics are encoded in \sTeX and are classified as
+foundational.
+
+Formal foundations should ideally instantiate these symbols with their formal counterparts,
+e.g. |isa| corresponds to a typing operation in typed setting, or the $\in$-operator in
+set-theoretic contexts; |bind| corresponds to a universal quantifier in ($n$th-order)
+logic, or a $\Pi$ in dependent type theories.
+
+We make this theory part of the \sTeX collection due to the obiquity
+of the symbols involved. Note however, that the metatheory is
+for all practical purposes a ``normal'' \sTeX module, and the
+symbols contained ``normal'' \sTeX symbols.
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "../stex-manual"
+%%% End:
+
+% LocalWords: stex-metatheory th-order
diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-modules.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-modules.tex
index c067f28a1c3..424c2200e85 100644
--- a/Master/texmf-dist/doc/latex/stex/packages/stex-modules.tex
+++ b/Master/texmf-dist/doc/latex/stex/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
diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-problem.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-problem.tex
index 1ce5aaa3a23..a90c36412d0 100644
--- a/Master/texmf-dist/doc/latex/stex/packages/stex-problem.tex
+++ b/Master/texmf-dist/doc/latex/stex/packages/stex-problem.tex
@@ -1 +1,151 @@
-\textcolor{red}{TODO: problem documentation} \ No newline at end of file
+The \pkg{problem} package supplies an infrastructure that allows specify problem. Problems
+are text fragments that come with auxiliary functions: hints, notes, and
+solutions\footnote{for the moment multiple choice problems are not supported, but may
+ well be in a future version}. Furthermore, we can specify how long the solution to a
+given problem is estimated to take and how many points will be awarded for a perfect
+solution.
+
+Finally, the \pkg{problem} package facilitates the management of problems in small files,
+so that problems can be re-used in multiple environment.
+
+\begin{function}{solutions,notes,hints,gnotes,pts,min,boxed,test}
+ The \pkg{problem} package takes the options |solutions| (should solutions be output?),
+ |notes| (should the problem notes be presented?), |hints| (do we give the hints?),
+ |gnotes| (do we show grading notes?), |pts| (do we display the points awarded for
+ solving the problem?), |min| (do we display the estimated minutes for problem
+ soling). If theses are specified, then the corresponding auxiliary parts of the problems
+ are output, otherwise, they remain invisible.
+
+ The |boxed| option specifies that problems should be formatted in framed boxes so that
+ they are more visible in the text. Finally, the |test| option signifies that we are in a
+ test situation, so this option does not show the solutions (of course), but leaves space
+ for the students to solve them.
+\end{function}
+
+\begin{environment}{problem}
+ The main environment provided by the \pkg{problem}package is (surprise surprise) the
+ |problem| environment. It is used to mark up problems and exercises. The environment
+ takes an optional KeyVal argument with the keys |id| as an identifier that can be
+ reference later, |pts| for the points to be gained from this exercise in homework or
+ quiz situations, |min| for the estimated minutes needed to solve the problem, and
+ finally |title| for an informative title of the problem.
+\end{environment}
+
+\stexexample{%
+\documentclass{article}
+\usepackage[solutions,hints,pts,min]{problem}
+\begin{document}
+ \begin{sproblem}[id=elefants,pts=10,min=2,title=Fitting Elefants]
+ How many Elefants can you fit into a Volkswagen beetle?
+ \begin{hint}
+ Think positively, this is simple!
+ \end{hint}
+ \begin{exnote}
+ Justify your answer
+ \end{exnote}
+\begin{solution}[for=elefants,height=3cm]
+ Four, two in the front seats, and two in the back.
+ \begin{gnote}
+ if they do not give the justification deduct 5 pts
+ \end{gnote}
+\end{solution}
+\end{sproblem}
+\end{document}
+}
+
+\begin{environment}{solution}
+ The |solution| environment can be to specify a solution to a problem. If the package
+ option |solutions| is set or |\solutionstrue| is set in the text, then the solution will
+ be presented in the output. The |solution| environment takes an optional KeyVal argument
+ with the keys |id| for an identifier that can be reference |for| to specify which
+ problem this is a solution for, and |height| that allows to specify the amount of space
+ to be left in test situations (i.e. if the |test| option is set in the |\usepackage|
+ statement).
+\end{environment}
+
+\begin{environment}{hint,exnote,gnote}
+ The |hint| and |exnote| environments can be used in a |problem| environment to give
+ hints and to make notes that elaborate certain aspects of the problem. The |gnote|
+ (grading notes) environment can be used to document situtations that may arise in
+ grading.
+\end{environment}
+
+\begin{function}{\startsolutions,\stopsolutions}
+ Sometimes we would like to locally override the |solutions| option we have given to the
+ package. To turn on solutions we use the |\startsolutions|, to turn them off,
+ |\stopsolutions|. These two can be used at any point in the documents.
+\end{function}
+
+\begin{function}{\ifsolutions}
+ Also, sometimes, we want content (e.g. in an exam with master solutions) conditional on
+ whether solutions are shown. This can be done with the |\ifsolutions| conditional.
+\end{function}
+
+\begin{environment}{mcb}
+ Multiple choice blocks can be formatted using the |mcb| environment, in which single
+ choices are marked up with |\mcc| macro.
+\end{environment}
+
+\begin{function}{\mcc}
+ |\mcc[|\meta{keyvals}|]{|\meta{text}|}| takes an optional key/value argument
+ \meta{keyvals} for choice metadata and a required argument \meta{text} for the proposed
+ answer text. The following keys are supported
+ \begin{itemize}
+ \item |T| for true answers, |F| for false ones,
+ \item |Ttext| the verdict for true answers, |Ftext| for false ones, and
+ \item |feedback| for a short feedback text given to the student.
+ \end{itemize}
+\end{function}
+
+If we start the solutions, then we get
+
+\stexexample{%
+\startsolutions
+\begin{sproblem}[title=Functions,name=functions1]
+ What is the keyword to introduce a function definition in python?
+ \begin{mcb}
+ \mcc[T]{def}
+ \mcc[F,feedback=that is for C and C++]{function}
+ \mcc[F,feedback=that is for Standard ML]{fun}
+ \mcc[F,Ftext=Nooooooooo,feedback=that is for Java]{public static void}
+ \end{mcb}
+\end{sproblem}
+}
+without solutions (that is what the students see during the exam/quiz)\ednote{MK: that did
+not work!}
+\stexexample{%
+\stopsolutions
+\begin{sproblem}[title=Functions,name=functions1]
+ What is the keyword to introduce a function definition in python?
+ \begin{mcb}
+ \mcc[T]{def}
+ \mcc[F,feedback=that is for C and C++]{function}
+ \mcc[F,feedback=that is for Standard ML]{fun}
+ \mcc[F,Ftext=Nooooooooo,feedback=that is for Java]{public static void}
+ \end{mcb}
+\end{sproblem}
+}
+
+\begin{function}{\includeproblem}
+ The |\includeproblem| macro can be used to include a problem from another file. It takes
+ an optional KeyVal argument and a second argument which is a path to the file containing
+ the problem (the macro assumes that there is only one problem in the include file). The
+ keys |title|, |min|, and |pts| specify the problem title, the estimated minutes for
+ solving the problem and the points to be gained, and their values (if given) overwrite
+ the ones specified in the |problem| environment in the included file.
+\end{function}
+
+The sum of the points and estimated minutes (that we specified in the |pts| and |min| keys
+to the |problem| environment or the |\includeproblem| macro) to the log file and the
+screen after each run. This is useful in preparing exams, where we want to make sure that
+the students can indeed solve the problems in an allotted time period.
+
+The |\min| and |\pts| macros allow to specify (i.e. to print to the margin) the
+distribution of time and reward to parts of a problem, if the |pts| and |pts| options are
+set. This allows to give students hints about the estimated time and the points to be
+awarded.
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "../stex-manual"
+%%% End:
diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-proofs.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-proofs.tex
index 0523c65948d..d06db1282f5 100644
--- a/Master/texmf-dist/doc/latex/stex/packages/stex-proofs.tex
+++ b/Master/texmf-dist/doc/latex/stex/packages/stex-proofs.tex
@@ -1 +1,214 @@
-\textcolor{red}{TODO: sproofs documentation} \ No newline at end of file
+The \pkg{stex-proof} package supplies macros and environment that allow to annotate the
+structure of mathematical proofs in \sTeX document. This structure can be used by MKM
+systems for added-value services, either directly from the \sTeX sources, or after
+translation.
+
+We will go over the general intuition by way of a running example:
+
+\begin{latexcode}
+\begin{sproof}[id=simple-proof]
+ {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$}
+ \begin{spfcases}{For the induction we have to consider three cases:}
+ \begin{spfcase}{$n=1$}
+ \begin{spfstep}[type=inline] then we compute $1=1^2$\end{spfstep}
+ \end{spfcase}
+ \begin{spfcase}{$n=2$}
+ \begin{spfcomment}[type=inline]
+ This case is not really necessary, but we do it for the
+ fun of it (and to get more intuition).
+ \end{spfcomment}
+ \begin{spfstep}[type=inline] We compute $1+3=2^{2}=4$.\end{spfstep}
+ \end{spfcase}
+ \begin{spfcase}{$n>1$}
+ \begin{spfstep}[type=assumption,id=ind-hyp]
+ Now, we assume that the assertion is true for a certain $k\geq 1$,
+ i.e. $\sum_{i=1}^k{(2i-1)}=k^{2}$.
+ \end{spfstep}
+ \begin{spfcomment}
+ We have to show that we can derive the assertion for $n=k+1$ from
+ this assumption, i.e. $\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$.
+ \end{spfcomment}
+ \begin{spfstep}
+ We obtain $\sum_{i=1}^{k+1}{2i-1}=\sum_{i=1}^k{2i-1}+2(k+1)-1$
+ \spfjust[method=arith:split-sum]{by splitting the sum}.
+ \end{spfstep}
+ \begin{spfstep}
+ Thus we have $\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1$
+ \spfjust[method=fertilize]{by inductive hypothesis}.
+ \end{spfstep}
+ \begin{spfstep}[type=conclusion]
+ We can \spfjust[method=simplify]{simplify} the right-hand side to
+ ${k+1}^2$, which proves the assertion.
+ \end{spfstep}
+ \end{spfcase}
+ \begin{spfstep}[type=conclusion]
+ We have considered all the cases, so we have proven the assertion.
+ \end{spfstep}
+ \end{spfcases}
+\end{sproof}
+\end{latexcode}
+
+This yields the following result:
+
+\begin{mdframed}
+ \begin{sproof}[id=simple-proof]
+ {We prove that $\sum_{i=1}^n{2i-1}=n^{2}$ by induction over $n$}
+ \begin{spfcases}{For the induction we have to consider the following cases:}
+ \begin{spfcase}{$n=1$}
+ \begin{spfstep}[type=inline] then we compute $1=1^2$\end{spfstep}
+ \end{spfcase}
+ \begin{spfcase}{$n=2$}
+ \begin{spfcomment}[type=inline]
+ This case is not really necessary, but we do it for the fun
+ of it (and to get more intuition).
+ \end{spfcomment}
+ \begin{spfstep}[type=inline]
+ We compute $1+3=2^{2}=4$
+ \end{spfstep}
+ \end{spfcase}
+ \begin{spfcase}{$n>1$}
+ \begin{spfstep}[type=hypothesis,id=ind-hyp]
+ Now, we assume that the assertion is true for a certain $k\geq 1$, i.e.
+ $\sum_{i=1}^k{(2i-1)}=k^{2}$.
+ \end{spfstep}
+ \begin{spfcomment}
+ We have to show that we can derive the assertion for $n=k+1$ from this
+ assumption, i.e. $\sum_{i=1}^{k+1}{(2i-1)}=(k+1)^{2}$.
+ \end{spfcomment}
+ \begin{spfstep}[id=splitit]
+ We obtain $\sum_{i=1}^{k+1}{(2i-1)}=\sum_{i=1}^k{(2i-1)}+2(k+1)-1$
+ \spfjust[method=arith:split-sum]{by splitting the sum}.
+ \end{spfstep}
+ \begin{spfstep}[id=byindhyp]
+ Thus we have $\sum_{i=1}^{k+1}{(2i-1)}=k^2+2k+1$
+ \spfjust[method=fertilize]{by \premise[ind-hyp]{inductive hypothesis}}.
+ \end{spfstep}
+ \begin{spfstep}[type=conclusion]
+ We can \spfjust[method=simplify-eq]{simplify the \justarg[rhs]{right-hand side}} to
+ $(k+1)^2$, which proves the assertion.
+ \end{spfstep}
+ \end{spfcase}
+ \begin{spfstep}[type=conclusion]
+ We have considered all the cases, so we have proven the assertion.
+ \end{spfstep}
+ \end{spfcases}
+\end{sproof}
+\end{mdframed}
+
+\begin{environment}{sproof}
+ The |sproof| environment is the main container for proofs. It takes an optional |KeyVal|
+ argument that allows to specify the |id| (identifier) and |for| (for which assertion is
+ this a proof) keys. The regular argument of the |proof| environment contains an
+ introductory comment, that may be used to announce the proof style. The |proof|
+ environment contains a sequence of |spfstep|, |spfcomment|, and |spfcases| environments
+ that are used to markup the proof steps.
+\end{environment}
+
+\begin{function}{\spfidea}
+ The |\spfidea| macro allows to give a one-paragraph description of the proof idea.
+\end{function}
+
+\begin{function}{\spfsketch}
+ For one-line proof sketches, we use the |\spfsketch| macro, which takes the same
+ optional argument as |sproof| and another one: a natural language text that sketches
+ the proof.
+\end{function}
+
+\begin{environment}{spfstep}
+ Regular proof steps are marked up with the |step| environment, which takes an optional
+ |KeyVal| argument for annotations. A proof step usually contains a local assertion
+ (the text of the step) together with some kind of evidence that this can be derived
+ from already established assertions.
+\end{environment}
+
+\begin{function}{\spfjust}
+ This evidence is marked up with the |\spfjust| macro in the \pkg{stex-proofs}
+ package. This environment totally invisible to the formatted result; it wraps the text
+ in the proof step that corresponds to the evidence. The environment takes an optional
+ |KeyVal| argument, which can have the |method| key, whose value is the name of a proof
+ method (this will only need to mean something to the application that consumes the
+ semantic annotations). Furthermore, the justification can contain ``premises''
+ (specifications to assertions that were used justify the step) and ``arguments''
+ (other information taken into account by the proof method).
+\end{function}
+
+\begin{function}{\premise}
+ The |\premise| macro allows to mark up part of the text as reference to an assertion
+ that is used in the argumentation. In the running example we have used the |\premise|
+ macro to identify the inductive hypothesis.
+\end{function}
+
+\begin{function}{\justarg}
+ The |\justarg| macro is very similar to |\premise| with the difference that it is used
+ to mark up arguments to the proof method. Therefore the content of the first argument
+ is interpreted as a mathematical object rather than as an identifier as in the case of
+ |\premise|. In our example, we specified that the simplification should take place on
+ the right hand side of the equation. Other examples include proof methods that
+ instantiate. Here we would indicate the substituted object in a |\justarg| macro.
+\end{function}
+
+Note that both |\premise| and |\justarg| can be used with an empty second argument to
+mark up premises and arguments that are not explicitly mentioned in the text.
+
+\begin{environment}{subproof}
+ The |spfcases| environment is used to mark up a subproof. This environment takes an
+ optional |KeyVal| argument for semantic annotations and a second argument that allows
+ to specify an introductory comment (just like in the |proof| environment). The
+ |method| key can be used to give the name of the proof method
+ executed to make this subproof.
+\end{environment}
+
+\begin{environment}{spfcases}
+ The |spfcases| environment is used to mark up a proof by cases. Technically it is a
+ variant of the |subproof| where the |method| is |by-cases|. Its contents are |spfcase|
+ environments that mark up the cases one by one.
+\end{environment}
+
+\begin{environment}{spfcase}
+ The content of a |spfcases| environment are a sequence of case proofs marked up in the
+ |spfcase| environment, which takes an optional |KeyVal| argument for semantic
+ annotations. The second argument is used to specify the the description of the case
+ under consideration. The content of a |spfcase| environment is the same as that of a
+ |sproof|, i.e. |spfstep|s, |spfcomment|s, and |spfcases| environments.
+\end{environment}
+
+\begin{function}{\spfcasesketch}
+ |\spfcasesketch| is a variant of the |spfcase| environment that takes the same
+ arguments, but instead of the |spfstep|s in the body uses a third argument for a proof
+ sketch.
+\end{function}
+
+\begin{environment}{spfcomment}
+ The |spfcomment| environment is much like a |step|, only that it does not have an
+ object-level assertion of its own. Rather than asserting some fact that is relevant
+ for the proof, it is used to explain where the proof is going, what we are attempting
+ to to, or what we have achieved so far. As such, it cannot be the target of a
+ |\premise|.
+\end{environment}
+
+\begin{function}{\sproofend}
+ Traditionally, the end of a mathematical proof is marked with a little box at the end of
+ the last line of the proof (if there is space and on the end of the next line if there
+ isn't), like so:\sproofend
+
+ The \pkg{stex-proofs} package provides the |\sproofend| macro for this.
+\end{function}
+
+\begin{variable}{\sProofEndSymbol}
+ If a different symbol for the proof end is to be used (e.g. {\sl{q.e.d}}), then this can
+ be obtained by specifying it using the |\sProofEndSymbol| configuration macro (e.g. by
+ specifying |\sProofEndSymbol{q.e.d}|).
+\end{variable}
+
+Some of the proof structuring macros above will insert proof end symbols for sub-proofs,
+in most cases, this is desirable to make the proof structure explicit, but sometimes this
+wastes space (especially, if a proof ends in a case analysis which will supply its own
+proof end marker). To suppress it locally, just set |proofend={}| in them or use use
+|\sProofEndSymbol{}|.
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "../stex-manual"
+%%% End:
+
+% LocalWords: hypothesis,id geq splitit arith:split-sum byindhyp rhs proofend
diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-references.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-references.tex
index bf8a8ed66c0..11de003e9be 100644
--- a/Master/texmf-dist/doc/latex/stex/packages/stex-references.tex
+++ b/Master/texmf-dist/doc/latex/stex/packages/stex-references.tex
@@ -1 +1,8 @@
-\textcolor{red}{TODO: references documentation} \ No newline at end of file
+\begin{sfragment}[id=sec.references]{Referencing Symbols and Statements}
+\textcolor{red}{TODO: references documentation}
+\end{sfragment}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "../stex-manual"
+%%% End:
diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-slides.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-slides.tex
index 1f9d0c989d6..a900c1fcbb8 100644
--- a/Master/texmf-dist/doc/latex/stex/packages/stex-slides.tex
+++ b/Master/texmf-dist/doc/latex/stex/packages/stex-slides.tex
@@ -1 +1,212 @@
-\textcolor{red}{TODO: notesslides documentation} \ No newline at end of file
+The \pkg{notesslides} document class is derived from |beamer.cls|~\cite{beamerclass:on},
+it adds a ``notes version'' for course notes that is more suited to printing than the one
+supplied by |beamer.cls|.
+
+The \pkg{notesslides} class takes the notion of a slide frame from Till Tantau's excellent
+\pkg{beamer} class and adapts its notion of frames for use in the \sTeX and \omdoc. To
+support semantic course notes, it extends the notion of mixing frames and explanatory
+text, but rather than treating the frames as images (or integrating their contents into
+the flowing text), the \pkg{notesslides} package displays the slides as such in the course
+notes to give students a visual anchor into the slide presentation in the course (and to
+distinguish the different writing styles in slides and course notes).
+
+In practice we want to generate two documents from the same source: the slides for
+presentation in the lecture and the course notes as a narrative document for home
+study. To achieve this, the \pkg{notesslides} class has two modes: \emph{slides mode} and
+\emph{notes mode} which are determined by the package option.
+
+
+\begin{variable}{slides,notes,sectocframes,frameimages,fiboxed}
+ The \pkg{notesslides} class takes a variety of class options:
+ \begin{itemize}
+ \item The options |slides| and |notes| switch between slides mode and notes mode (see
+ Section~\ref{sec:user:notesslides}).
+ \item If the option |sectocframes| is given, then for the |sfragment|s, special frames
+ with the |sfragment| title (and number) are generated.
+ \item If the option |frameimages| is set, then slide mode also shows the
+ |\frameimage|-generated frames (see section~\ref{sec:user:frameimage}). If also the
+ |fiboxed| option is given, the slides are surrounded by a box.
+ \end{itemize}
+\end{variable}
+
+\begin{environment}{frame,note}
+ Slides are represented with the |frame| environment just like in the \pkg{beamer} class,
+ see~\cite{Tantau:ugbc} for details. The \pkg{notesslides} class adds the |note|
+ environment for encapsulating the course note fragments.\footnote{MK: it would be very
+ nice, if we did not need this environment, and this should be possible in principle,
+ but not without intensive LaTeX trickery. Hints to the author are welcome.}
+\end{environment}
+
+\begin{dangerbox}
+ Note that it is essential to start and end the |notes| environment at the start of the
+ line -- in particular, there may not be leading blanks -- else {\LaTeX} becomes confused
+ and throws error messages that are difficult to decipher.
+\end{dangerbox}
+
+By interleaving the |frame| and |note| environments, we can build course notes as shown
+here:
+
+\begin{latexcode}
+\ifnotes\maketitle\else
+\frame[noframenumbering]\maketitle\fi
+
+\begin{note}
+ We start this course with ...
+\end{note}
+
+\begin{frame}
+ \frametitle{The first slide}
+ ...
+\end{frame}
+\begin{note}
+ ... and more explanatory text
+\end{note}
+
+\begin{frame}
+ \frametitle{The second slide}
+ ...
+\end{frame}
+...
+\end{latexcode}
+
+\begin{function}{\ifnotes}
+ Note the use of the |\ifnotes| conditional, which allows different treatment between
+ |notes| and |slides| mode -- manually setting |\notestrue| or |\notesfalse| is strongly
+ discouraged however.
+\end{function}
+
+\begin{dangerbox}
+ We need to give the title frame the |noframenumbering| option so that the frame
+ numbering is kept in sync between the slides and the course notes.
+\end{dangerbox}
+
+\begin{dangerbox}
+ The \pkg{beamer} class recommends not to use the |allowframebreaks| option on frames
+ (even though it is very convenient). This holds even more in the |notesslides| case: At
+ least in conjunction with |\newpage|, frame numbering behaves funnily (we have tried to
+ fix this, but who knows).
+\end{dangerbox}
+
+\begin{function}{\inputref*}
+ If we want to transclude a the contents of a file as a note, we can use a new variant
+ |\inputref*| of the |\inputref| macro: |\inputref*{foo}| is equivalent to
+ |\begin{note}\inputref{foo}\end{note}|.
+\end{function}
+
+\begin{environment}{nparagraph, nparagraph, ndefinition, nexample, nsproof, nassertion}
+ There are some environments that tend to occur at the top-level of |note|
+ environments. We make convenience versions of these: e.g. the |nparagraph| environment
+ is just an |sparagraph| inside a |note| environment (but looks nicer in the source,
+ since it avoids one level of source indenting). Similarly, we have the |nfragment|,
+ |ndefinition|, |nexample|, |nsproof|, and |nassertion| environments.
+\end{environment}
+
+\begin{function} {\setslidelogo}
+ The default logo provided by the \pkg{notesslides} package is the {\sTeX} logo it can be
+ customized using |\setslidelogo{|\meta{logo name}|}|.
+\end{function}
+
+\begin{function}{\setsource}
+ The default footer line of the \pkg{notesslides} package mentions copyright and
+ licensing. In the \pkg{beamer} class, |\source| stores the author's name as the
+ copyright holder . By default it is \emph{Michael Kohlhase} in the \pkg{notesslides}
+ package since he is the main user and designer of this
+ package. |\setsource{|\meta{name}|}| can change the writer's name.
+\end{function}
+
+\begin{function}{\setlicensing}
+ For licensing, we use the Creative Commons Attribuition-ShareAlike license by default to
+ strengthen the public domain. If package |hyperref| is loaded, then we can attach a
+ hyperlink to the license logo. |\setlicensing[|\meta{url}|]{|\meta{logo name}|}| is used
+ for customization, where \meta{url} is optional.
+\end{function}
+
+Sometimes, we want to integrate slides as images after all -- e.g. because we already
+have a PowerPoint presentation, to which we want to add \sTeX notes.
+
+\begin{function}{\frameimage,\mhframeimage}
+ In this case we can use |\frameimage[|\meta{opt}|]{|\meta{path}|}|, where \meta{opt} are
+ the options of |\includegraphics| from the \pkg{graphicx} package~\cite{CarRah:tpp99}
+ and \meta{path} is the file path (extension can be left off like in
+ |\includegraphics|). We have added the |label| key that allows to give a frame label
+ that can be referenced like a regular |beamer| frame.
+
+The |\mhframeimage| macro is a variant of |\frameimage| with repository support. Instead
+of writing
+\begin{latexcode}
+\frameimage{\MathHub{fooMH/bar/source/baz/foobar}}
+\end{latexcode}
+ we can simply write (assuming that |\MathHub| is defined as above)
+\begin{latexcode}
+\mhframeimage[fooMH/bar]{baz/foobar}
+\end{latexcode}
+ Note that the |\mhframeimage| form is more semantic, which allows more advanced document
+management features in \textsf{MathHub}.
+\end{function}
+
+If |baz/foobar| is the ``current module'', i.e. if we are on the \textsf{MathHub} path
+\ldots|MathHub/fooMH/bar|\ldots, then stating the repository in the first optional
+argument is redundant, so we can just use
+\begin{latexcode}
+\mhframeimage{baz/foobar}
+\end{latexcode}
+
+\begin{function}{\textwarning}
+ The |\textwarning| macro generates a warning sign: \textwarning
+\end{function}
+
+In course notes, we sometimes want to point to an ``excursion'' -- material that is either
+presupposed or tangential to the course at the moment -- e.g. in an appendix. The typical
+setup is the following:
+
+\begin{latexcode}
+\excursion{founif}{../ex/founif}{We will cover first-order unification in}
+...
+\begin{appendix}\printexcursions\end{appendix}
+\end{latexcode}
+
+\begin{function}{\excursion}
+ The |\excursion{|\meta{ref}|}{|\meta{path}|}{|\meta{text}|}| is syntactic sugar for
+
+\begin{latexcode}
+\begin{nparagraph}[title=Excursion]
+ \activateexcursion{founif}{../ex/founif}
+ We will cover first-order unification in \sref{founif}.
+\end{nparagraph}
+\end{latexcode}
+\end{function}
+
+\begin{function}{\activateexcursion,\printexcursion,\excursionref}
+ Here |\activateexcursion{|\meta{path}|}| augments the |\printexcursions| macro by a call
+ |\inputref{|\meta{path}|}|. In this way, the |\printexcursions| macro (usually in the
+ appendix) will collect up all excursions that are specified in the main text.
+
+ Sometimes, we want to reference -- in an excursion -- part of another. We can use
+ |\excursionref{|\meta{label}|}| for that.
+\end{function}
+
+\begin{function}{\excursiongroup}
+ Finally, we usually want to put the excursions into an |sfragment| environment and add
+ an introduction, therefore we provide the a variant of the |\printexcursions| macro:
+ |\excursiongroup[id=|\meta{id}|,intro=|\meta{path}|]| is equivalent to
+\begin{latexcode}
+\begin{note}
+\begin{sfragment}[id=<id>]{Excursions}
+ \inputref{<path>}
+ \printexcursions
+\end{sfragment}
+\end{note}
+\end{latexcode}
+\end{function}
+
+\begin{dangerbox}
+ When option |book| which uses |\pagestyle{headings}| is given and semantic macros are
+ given in the |sfragment| titles, then they sometimes are not defined by the time the
+ heading is formatted. Need to look into how the headings are made. This is a problem of
+ the underlying \pkg{document-structure} package.
+\end{dangerbox}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "../stex-manual"
+%%% End:
diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-statements.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-statements.tex
index aa9f5f76abf..6a2478fa7d1 100644
--- a/Master/texmf-dist/doc/latex/stex/packages/stex-statements.tex
+++ b/Master/texmf-dist/doc/latex/stex/packages/stex-statements.tex
@@ -1 +1,145 @@
-\textcolor{red}{TODO: statements documentation} \ No newline at end of file
+\begin{sfragment}{Definitions, Theorems, Examples, Paragraphs}
+\begin{smodule}{Statements}
+ As mentioned earlier, we can semantically mark-up
+ \emph{statements} such as definitions, theorems, lemmata, examples, etc.
+
+ The corresponding environments for that are:
+ \begin{itemize}
+ \item \stexcode"sdefinition" for definitions,
+ \item \stexcode"sassertion" for assertions, i.e.
+ propositions that are declared to be \emph{true},
+ such as theorems, lemmata, axioms,
+ \item \stexcode"sexample" for examples and counterexamples, and
+ \item \stexcode"sparagraph" for ``other'' semantic paragraphs,
+ such as comments, remarks, conjectures, etc.
+ \end{itemize}
+
+ The \emph{presentation} of these environments can be customized
+ to use e.g. predefined |theorem|-environments, see \sref{sec.customhighlight}
+ for details.
+
+ All of these environments take optional arguments in the form of
+ |key=value|-pairs. Common to all of them are the keys |id=| (for cross-referencing,
+ see \sref{sec.references}), |type=| for customization (see \sref{sec.customhighlight})
+ and additional information (e.g. definition principles, ``difficulty'' etc), as well
+ as |title=| (for giving the paragraph a title), and finally |for=|.
+
+ The |for=| key expects a comma-separated list of existing
+ symbols, allowing for e.g. things like
+ \symdef{addition}[args=a,prec=100]{#1}{##1 \comp+ ##2}
+ \symdef{multiplication}[args=a,prec=50]{#1}{##1 \comp\cdot ##2}
+ \stexexample{%
+\begin{sexample}[
+ id=additionandmultiplication.ex,
+ for={addition,multiplication},
+ type={trivial,boring},
+ title={An Example}
+]
+ $\addition{2,3}$ is $5$, $\multiplication{2,3}$ is $6$.
+\end{sexample}
+ }
+
+ \begin{function}{\definiendum,\definame,\Definame}
+ \stexcode"sdefinition" (and \stexcode"sparagraph" with
+ |type=symdoc|) introduce three new macros:
+ \stexcode"definiendum" behaves like \stexcode"symref"
+ (and \stexcode"definame"/\stexcode"Definame"
+ like \stexcode"symname"/\stexcode"Symname", respectively),
+ but highlights the referenced symbol as \emph{being defined}
+ in the current definition.
+ \end{function}
+
+ \begin{mmtbox}
+ The special |type=symdoc| for \stexcode"sparagraph" is intended to be used for
+ ``informal definitions'', or encyclopedia-style descriptions for symbols.
+
+ The \mmt system can use those (in lieu of an actual \stexcode"sdefinition" in scope)
+ to present to users, e.g. when hovering over symbols.
+ \end{mmtbox}
+
+ \begin{function}{\definiens}
+ Additionally, \stexcode"sdefinition" (and \stexcode"sparagraph" with
+ |type=symdoc|) introduces \stexcode"\definiens[<optional symbolname>]{<code>}"
+ which marks up |<code>| as being the explicit \emph{definiens}
+ of |<optional symbolname>| (in case |for=| has multiple symbols).
+ \end{function}
+
+ All four statement environments -- i.e. \stexcode|sdefinition|,
+ \stexcode|sassertion|, \stexcode|sexample|, and \stexcode|sparagraph| -- also take an
+ optional parameter |name=| -- if this one is given a value, the environment will
+ generate a \emph{symbol} by that name (but with no semantic macro). Not only does this
+ allow for \stexcode"\symref" et al, it allows us to resume our earlier example for
+ monoids much more nicely:\ednote{MK: we should reference the example explicitly here.}
+
+ \symdef{set}{\comp{\texttt{Set}}}
+ \symdef{equal}[args=2]{#1 \comp= #2}
+ \symdef{inset}[args=2]{#1 \comp\in #2}
+ \symdef{funtype}[args=ai]{#1 \comp\to #2}{##1 \comp\times ##2}
+
+ \stexexample{%
+\begin{mathstructure}{monoid}
+ \symdef{universe}[type=\set]{\comp{U}}
+ \symdef{op}[
+ args=2,
+ type=\funtype{\universe,\universe}{\universe},
+ op=\circ
+ ]{#1 \comp{\circ} #2}
+ \symdef{unit}[type=\universe]{\comp{e}}
+
+ \begin{sparagraph}[type=symdoc,for=monoid]
+ A \definame{monoid} is a structure
+ $\mathstruct{\universe,\op!,\unit}$
+ where $\op!:\funtype{\universe}{\universe}$ and
+ $\inset{\unit}{\universe}$ such that
+
+ \begin{sassertion}[name=associative,
+ type=axiom,
+ title=Associativity]
+ $\op!$ is associative
+ \end{sassertion}
+ \begin{sassertion}[name=isunit,
+ type=axiom,
+ title=Unit]
+ $\equal{\op{\svar{x}}{\unit}}{\svar{x}}$
+ for all $\inset{\svar{x}}{\universe}$
+ \end{sassertion}
+ \end{sparagraph}
+\end{mathstructure}
+
+An example for a \symname{monoid} is...
+ }
+
+ The main difference to before\ednote{MK: reference} is that the two
+ \stexcode|sassertion|s now have |name=| attributes. Thus the \stexcode"mathstructure"
+ \symname{monoid} now contains two additional symbols, namely the axioms for
+ associativity and that $e$ is a unit. Note that both symbols do not represent the mere
+ \emph{propositions} that e.g. $\circ$ is associative, but \emph{the assertion that it
+ is actually true} that $\circ$ is associative.
+
+ If we now want to instantiate |monoid| (unless with a variable,
+ of course), we also need to assign |associative| and |neutral|
+ to analogous assertions. So the earlier example
+ \begin{latexcode}[gobble=8]
+ \instantiate{intmonoid}{monoid}{\mathbb{Z}_{+,0}}[
+ universe = Int ,
+ op = addition ,
+ unit = zero
+ ]
+ \end{latexcode}
+ ...will not work anymore. We now need to give assertions that
+ |addition| is associative and that |zero| is a unit with respect
+ to addition.\footnote{Of course, \sTeX can not check that
+ the assertions are the ``correct'' ones -- but if
+ the assertions (both in |monoid| as well as those for addition and
+ zero) are properly marked up, \mmt can. \textcolor{red}{TODO: should}}
+
+\end{smodule}
+\end{sfragment}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "../stex-manual"
+%%% End:
+
+% LocalWords: sec.customhighlight a,prec additionandmultiplication.ex trivial,boring
+% LocalWords: addition,multiplication symdoc symdoc,for isunit
diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-symbols.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-symbols.tex
index 50b450a248f..e7bafeda6b6 100644
--- a/Master/texmf-dist/doc/latex/stex/packages/stex-symbols.tex
+++ b/Master/texmf-dist/doc/latex/stex/packages/stex-symbols.tex
@@ -1 +1,587 @@
-\textcolor{red}{TODO: symbols documentation} \ No newline at end of file
+\begin{smodule}[ns=https://github.com/slatex/sTeX/doc]{SymbolsAndNotations}
+\begin{sfragment}{Declaring New Symbols and Notations}
+ Inside an \stexcode"smodule" environment, we can declare new \sTeX symbols.
+
+\begin{function}{\symdecl}
+ The most basic command for doing so is using \stexcode"\symdecl{symbolname}". This
+ introduces a new symbol with name |symbolname|, arity $0$ and semantic macro
+ \stexcode"\symbolname".
+
+ The starred variant \stexcode"\symdecl*{symbolname}" will declare a symbol, but not
+ introduce a semantic macro. If we don't want to supply a notation (for example to
+ introduce concepts like ``abelian'', which is not something that has a notation), the
+ starred variant is likely to be what we want.
+\end{function}
+\begin{mmtbox}
+ \stexcode"\symdecl" introduces a new \omdoc/\mmt constant in the current module
+ (=\omdoc/\mmt theory). Correspondingly, they get assigned the URI
+ |<module-URI>?<constant-name>|.
+\end{mmtbox}
+
+Without a semantic macro or a notation, the only meaningful way to reference a symbol is
+via \stexcode"\symref",\stexcode"\symname" etc.
+
+\stexexample{%
+\symdecl*{foo}
+Given a \symname{foo}, we can...
+}
+
+Obviously, most semantic macros should take actual \emph{arguments}, implying that the
+symbol we introduce is an \emph{operator} or \emph{function}. We can let
+\stexcode"\symdecl" know the \emph{arity} (i.e. number of arguments) of a symbol like
+this:
+
+\stexexample{%
+\symdecl{binarysymbol}[args=2]
+\symref{binarysymbol}{this} is a symbol taking two arguments.
+}
+
+So far we have gained exactly \ldots nothing by adding the arity information: we cannot do
+anything with the arguments in the text.
+
+We will now see what we can gain with more machinery.
+
+\begin{function}{\notation}
+ We probably want to supply a notation as well, in which case we can finally actually use
+ the semantic macro in math mode. We can do so using the \stexcode"\notation" command,
+ like this:
+
+\stexexample{%
+\notation{binarysymbol}{\text{First: }#1\text{; Second: }#2}
+$\binarysymbol{a}{b}$ }
+\end{function}
+
+\begin{mmtbox}
+ Applications of semantic macros, such as \stexcode"\binarysymbol{a}{b}" are translated
+ to \mmt/\omdoc as |OMA|-terms with head |<OMS name="...?binarysymbol"/>|.
+
+ Semantic macros with no arguments correspond to |OMS| directly.
+\end{mmtbox}
+
+\begin{function}{\comp}
+ For many semantic services e.g. semantic highlighting or \defemph{wikification} (linking
+ user-visible notation components to the definition of the respective symbol they come
+ from), we need to specify the notation components. Unfortunately, there is currently no
+ way the \sTeX engine can infer this by itself, so we have to specify it manually in the
+ notation specification. We can do so with the \stexcode"\comp" command.
+\end{function}
+
+We can introduce a new notation |highlight| for \stexcode"\binarysymbol" that fixes this
+flaw, which we can subsequently use with \stexcode"\binarysymbol[highlight]":
+
+\stexexample{%
+\notation{binarysymbol}[highlight]
+ {\comp{\text{First: }}#1\comp{\text{; Second: }}#2}
+$\binarysymbol[highlight]{a}{b}$
+}
+
+\begin{dangerbox}
+ Ideally, \stexcode"\comp" would not be necessary: Everything in a notation that is
+ \emph{not} an argument should be a notation component. Unfortunately, it is
+ computationally expensive to determine where an argument begins and ends, and the
+ argument markers |#n| may themselves be nested in other macro applications or
+ \TeX\xspace groups, making it ultimately almost impossible to determine them
+ automatically while also remaining compatible with arbitrary highlighting customizations
+ (such as tooltips, hyperlinks, colors) that users might employ, and that are ultimately
+ invoked by \stexcode"\comp".
+\end{dangerbox}
+
+\begin{dangerbox}
+ Note that it is required that
+ \begin{enumerate}
+ \item the argument markers |#n| never occur inside a \stexcode"\comp", and
+ \item no semantic arguments may ever occur inside a notation.
+ \end{enumerate}
+ Both criteria are not just required for technical reasons, but conceptionally
+ meaningful:
+
+ The underlying principle is that the arguments to a semantic macro represent
+ \emph{arguments to the mathematical operation} represented by a symbol. For example, a
+ semantic macro \stexcode"\addition{a}{b}" taking two arguments would represent \emph{the
+ actual addition of (mathematical objects) $a$ and $b$}. It should therefore be
+ impossible for $a$ or $b$ to be part of a notation component of \stexcode"\addition".
+
+ Similarly, a semantic macro can not conceptually be part of the notation of
+ \stexcode"\addition", since a semantic macro represents a \emph{distinct mathematical
+ concept} with \emph{its own semantics}, whereas notations are syntactic
+ representations of the very symbol to which the notation belongs.
+
+ If you want an argument to a semantic macro to be a purely syntactic parameter, then you
+ are likely somewhat confused with respect to the distinction between the precise
+ \emph{syntax} and \emph{semantics} of the symbol you are trying to declare (which
+ happens quite often even to experienced \sTeX users), and might want to give those
+ another thought - quite likely, the macro you aim to implement does not actually
+ represent a semantically meaningful mathematical concept, and you will want to use
+ \stexcode"\def" and similar native \LaTeX\xspace macro definitions rather than semantic
+ macros.
+\end{dangerbox}
+
+\begin{function}{\symdef}
+ In the vast majority of cases where a symbol declaration should come with a semantic
+ macro, we will want to supply a notation immediately. For that reason, the
+ \stexcode"\symdef" command combines the functionality of both \stexcode"\symdecl" and
+ \stexcode"\notation" with the optional arguments of both:
+\end{function}
+
+\stexexample{%
+\symdef{newbinarysymbol}[hl,args=2]
+ {\comp{\text{1.: }}#1\comp{\text{; 2.: }}#2}
+$\newbinarysymbol{a}{b}$
+}
+
+We just declared a new symbol |newbinarysymbol| with |args=2| and immediately provided it
+with a notation with identifier |hl|. Since |hl| is the \emph{first} (and so far, only)
+notation supplied for |newbinarysymbol|, using \stexcode"\newbinarysymbol" without
+optional argument defaults to this notation.\bigskip
+
+But one man's meat is another man's poison: it is very subjective what the ``default
+notation'' of an operator should be. Different communities have different practices. For
+instance, the complex unit is written as $i$ in Mathematics and as $j$ in electrical
+engineering. So to allow modular specification and facilitate re-use of document fragments
+\sTeX allows to re-set notation defaults.
+
+\begin{function}{\setnotation}
+ The first notation provided will stay the default notation unless explicitly changed --
+ this is enabled by the \stexcode"\setnotation" command:
+ \stexcode"\setnotation{symbolname}{notation-id}" sets the default notation of
+ \stexcode"\symbolname" to |notation-id|, i.e. henceforth, \stexcode"\symbolname" behaves
+ like \stexcode"\symbolname[notation-id]" from now on.
+\end{function}
+
+Often, a default notation is set right after the corresponding notation is introduced --
+the starred version \stexcode"\notation*" for that reason introduces a new notation and
+immediately sets it to be the new default notation. So expressed differently, the
+\emph{first} \stexcode"\notation" for a symbol behaves exactly like \stexcode"\notation*",
+and \stexcode"\notation*{foo}[bar]{...}" behaves exactly like
+\stexcode"\notation{foo}[bar]{...}\setnotation{foo}{bar}".
+
+\begin{function}{\textsymdecl}
+ In the less mathematical settings where we want a symbol and
+ semantic macro for some concept with a notation \emph{beyond}
+ its mere name, but which should also be available in \TeX's text
+ mode, the command \stexcode"\textsymdecl" is useful.
+ For example, we can declare a symbol \stexcode"openmath"
+ with the notation \stexcode"\textsc{OpenMath}" using
+ \textsymdecl{openmath}[name=OpenMath]{\textsc{OpenMath}}
+ \stexcode"\textsymdecl{openmath}[name=OpenMath]{\textsc{OpenMath}}".
+ The \stexcode"\openmath" yields \openmath both in text and math
+ mode.
+\end{function}
+
+\begin{sfragment}{Operator Notations}
+ Once we have a semantic macro with arguments, such as \stexcode"\newbinarysymbol", the
+ semantic macro represents the \emph{application} of the symbol to a list of
+ arguments. What if we want to refer to the operator \emph{itself}, though?
+
+ We can do so by supplying the \stexcode"\notation" (or \stexcode"\symdef") with an
+ \emph{operator notation}, indicated with the optional argument |op=|. We can then
+ invoke the operator notation using \stexcode"\symbolname![notation-identifier]". Since
+ operator notations never take arguments, we do not need to use \stexcode"\comp" in it,
+ the whole notation is wrapped in a \stexcode"\comp" automatically:
+
+ \stexexample{%
+ \notation{newbinarysymbol}[ab, op={\text{a:}\cdot\text{; b:}\cdot}]
+ {\comp{\text{a:}}#1\comp{\text{; b:}}#2} \symname{newbinarysymbol} is also
+ occasionally written $\newbinarysymbol![ab]$
+ }
+
+ \begin{mmtbox}
+ \stexcode"\symbolname!" is translated to \omdoc/\mmt as |<OMS name="...?symbolname"/>|
+ directly.
+ \end{mmtbox}
+
+\end{sfragment}
+\end{sfragment}
+
+\begin{sfragment}{Argument Modes}
+ The notations so far used \emph{simple} arguments which we call \emph{mode}-|i|
+ arguments. Declaring a new symbol with \stexcode"\symdecl{foo}[args=3]" is equivalent to
+ writing \stexcode"\symdecl{foo}[args=iii]", indicating that the semantic macro takes
+ three mode-|i| arguments. However, there are three more argument modes which we will
+ investigate now, namely mode-|b|, mode-|a| and mode-|B| arguments.
+
+\begin{sfragment}{Mode-\texttt b Arguments}
+
+A mode-|b| argument represents a \emph{variable} that is \emph{bound} by the symbol in
+its application, making the symbol a \emph{binding operator}. Typical examples of
+binding operators are e.g. sums $\sum$, products $\prod$, integrals $\int$, quantifiers
+like $\forall$ and $\exists$, that $\lambda$-operator, etc.
+
+\begin{mmtbox}
+ Mode-|b| arguments behave exactly like mode-|i| arguments within \TeX, but applications
+ of binding operators, i.e. symbols with mode-|b| arguments, are translated to
+ |OMBIND|-terms in \omdoc/\mmt, rather than |OMA|.
+\end{mmtbox}
+
+For example, we can implement a summation operator binding an index variable and taking
+lower and upper index bounds and the expression to sum over like this:
+
+\stexexample{%
+\symdef{summation}[args=biii]
+ {\mathop{\comp{\sum}}_{#1\comp{=}#2}^{#3}#4}
+ $\summation{\svar{x}}{1}{\svar{n}}{\svar{x}}^2$
+}
+
+where the variable $\svar{x}$ is now \emph{bound} by the \stexcode"\summation"-symbol in
+the expression.
+\end{sfragment}
+
+\begin{sfragment}{Mode-\texttt a Arguments}
+ Mode-|a| arguments represent a \emph{flexary argument sequence}, i.e. a sequence of
+ arguments of arbitrary length. Formally, operators that take arbitrarily many arguments
+ don't ``exist'', but in informal mathematics, they are ubiquitous. Mode-|a| arguments
+ allow us to write e.g. \stexcode"\addition{a,b,c,d,e}" rather than having to write
+ something like \stexcode"\addition{a}{\addition{b}{\addition{c}{\addition{d}{e}}}}"!
+
+ \stexcode"\notation" (and consequently \stexcode"\symdef", too) take one additional
+ argument for each mode-|a| argument that indicates how to ``accumulate'' a
+ comma-separated sequence of arguments. This is best demonstrated on an example.
+
+ Let's say we want an operator representing quantification over an ascending chain of
+ elements in some set, i.e. \stexcode"\ascendingchain{S}{a,b,c,d,e}{t}" should yield
+ $\forall a{<_S}b{<_S}c{<_S}d{<_S}e.\,t$. The ``base''-notation for this operator is
+ simply\\ \stexcode"{\comp{\forall} #2\comp{.\,}#3}", where |#2| represents the full
+ notation fragment \emph{accumulated} from |{a,b,c,d,e}|.
+
+ The \emph{additional} argument to \stexcode"\notation" (or \stexcode"\symdef") takes the
+ same arguments as the base notation and two \emph{additional} arguments |##1| and |##2|
+ representing successive pairs in the mode-|a| argument, and accumulates them into |#2|,
+ i.e. to produce $a<_Sb<_Sc<_Sd<_Se$, we do \stexcode"{##1 \comp{<}_{#1} ##2}":
+
+ \stexexample{%
+\symdef{ascendingchain}[args=iai]
+ {\comp{\forall} #2\comp{.\,}#3}
+ {##1 \comp{<}_{#1} ##2}
+
+Tadaa: $\ascendingchain{S}{a,b,c,d,e}{t}$
+}
+
+If this seems overkill, keep in mind that you will rarely need the single-hash arguments
+|#1|,|#2| etc. in the |a|-notation-argument. For a much more representative and simpler
+example, we can introduce flexary addition via:
+\stexexample{%
+ \symdef{addition}[args=a]{#1}{##1 \comp{+} ##2}
+
+Tadaa: $\addition{a,b,c,d,e}$
+}
+
+\begin{sfragment}{The \texttt{assoc}-key}
+ We mentioned earlier that ``formally'', flexary arguments don't really
+ ``exist''. Indeed, formally, addition is usually defined as a binary operation,
+ quantifiers bind a single variable etc.
+
+ Consequently, we can tell \sTeX (or, rather, \mmt/\omdoc) how to ``resolve'' flexary
+ arguments by providing \stexcode"\symdecl" or \stexcode"\symdef" with an optional
+ |assoc|-argument, as in \stexcode"\symdecl{addition}[args=a,assoc=bin]". The possible
+ values for the |assoc|-key are:
+ \begin{itemize}
+ \item[|bin|:] A binary, associative argument, e.g. as in \stexcode"\addition"
+ \item[|binl|:] A binary, left-associative argument, e.g.
+ $a^{\scriptstyle b^{\scriptstyle c^d}}$, which stands for $((a^b)^c)^d$
+ \item[|binr|:] A binary, right-associative argument, e.g. as in $A\to B\to C\to D$,
+ which stands for $A \to (B \to (C \to D))$
+ \item[|pre|:] Successively prefixed, e.g. as in $\forall x,y,z.\,P$, which stands for
+ $\forall x.\, \forall y.\, \forall z.\,P$
+ \item[|conj|:] Conjunctive, e.g. as in $a=b=c=d$ or $a,b,c,d\in A$, which stand for
+ $a=d\wedge b=d\wedge c=d$ and $a\in A\wedge b\in A \wedge c\in A\wedge d\in A$,
+ respectively
+ \item[|pwconj|:] Pairwise conjunctive, e.g. as in $a\neq b\neq c\neq d$, which stands
+ for $a\neq b\wedge a\neq c\wedge a\neq d\wedge b\neq c\wedge b\neq d\wedge c\neq d$
+ \end{itemize}
+ As before, at the PDF level, this annotation is invisible (and without effect), but at
+ the level of the generated OMDoc/MMT this leads to more semantical expressions.
+\end{sfragment}
+\end{sfragment}
+
+\begin{sfragment}{Mode-\texttt B Arguments}
+ Finally, mode-|B| arguments simply combine the functionality of both |a| and |b| -
+ i.e. they represent an arbitrarily long sequence of variables to be bound, e.g. for
+ implementing quantifiers:
+
+ \stexexample{%
+\symdef{quantforall}[args=Bi]
+ {\comp{\forall}#1\comp{.}#2}
+ {##1\comp,##2}
+
+$\quantforall{\svar{x},\svar{y},\svar{z}}{P}$
+}
+\end{sfragment}
+\end{sfragment}
+
+\begin{sfragment}{Type and Definiens Components}
+ \stexcode"\symdecl" and \stexcode"\symdef" take two more optional arguments. \TeX\xspace
+ largely ignores them (except for special situations we will talk about later), but \mmt
+ can pick up on them for additional services. These are the |type| and |def| keys, which
+ expect expressions in math-mode (ideally using semantic macros, of course!)
+
+ \begin{mmtbox}
+ The |type| and |def| keys correspond to the |type| and |definiens| components of
+ \omdoc/\mmt constants.
+
+ Correspondingly, the name ``type'' should be taken with a grain of salt, since
+ \omdoc/\mmt -- being foundation-independent -- does not a priori implement a fixed
+ typing system.
+ \end{mmtbox}
+
+ \symdef{funtype}[args=ai]{#1 \comp\to #2}{##1 \comp\times ##2}
+ \symdef{fun}[args=bi]{#1 \comp\mapsto #2}
+ \symdef{set}{\comp{\texttt{Set}}}
+
+ The |type|-key allows us to provide additional information
+ (given the necessary \sTeX symbols), e.g. for
+ addition on natural numbers:
+
+ \stexexample{%
+\symdef{Nat}[type=\set]{\comp{\mathbb N}}
+\symdef{addition}[
+ type=\funtype{\Nat,\Nat}{\Nat},
+ op=+,
+ args=a
+]{#1}{##1 \comp+ ##2}
+
+\symname{addition} is an operation $\funtype{\Nat,\Nat}{\Nat}$
+}
+
+The |def|-key allows for declaring symbols as abbreviations:
+\stexexample{%
+\symdef{successor}[
+ type=\funtype{\Nat}{\Nat},
+ def=\fun{\svar{x}}{\addition{\svar{x},1}},
+ op=\mathtt{succ},
+ args=1
+]{\comp{\mathtt{succ(}#1\comp{)}}}
+
+The \symname{successor} operation $\funtype{\Nat}{\Nat}$
+is defined as $\fun{\svar{x}}{\addition{\svar{x},1}}$
+}
+\end{sfragment}
+
+\begin{sfragment}{Precedences and Automated Bracketing}
+ Having done \stexcode"\addition", the obvious next thing to implement is
+ \stexcode"\multiplication". This is straight-forward in theory:
+
+ \stexexample{%
+\symdef{multiplication}[
+ type=\funtype{\Nat,\Nat}{\Nat},
+ op=\cdot,
+ args=a
+]{#1}{##1 \comp\cdot ##2}
+
+\symname{multiplication} is an operation $\funtype{\Nat,\Nat}{\Nat}$
+}
+
+However, if we \emph{combine} \stexcode"\addition" and \stexcode"\multiplication", we
+notice a problem:
+
+\stexexample{%
+$\addition{a,\multiplication{b,\addition{c,\multiplication{d,e}}}}$
+}
+
+We all know that $\multiplication!$ binds stronger than $\addition!$, so the output
+$\addition{a,\multiplication{b,\addition{c,\multiplication{d,e}}}}$ does not actually
+reflect the term we wrote. We can of course insert parentheses manually
+
+\stexexample{%
+$\addition{a,\multiplication{b,(\addition{c,\multiplication{d,e}})}}$
+}
+but we can also do better by supplying \emph{precedences} and
+have \sTeX insert parentheses automatically.
+
+For that purpose, \stexcode"\notation" (and hence \stexcode"\symdef") take an optional
+argument |prec=<opprec>;<argprec1>x...x<argprec n>|.
+
+We will investigate the precise meaning of |<opprec>| and the |<argprec>|s shortly -- in
+the vast majority of cases, it is perfectly sufficient to think of |prec=| taking a single
+number and having that be \emph{the} precedence of the notation, where lower precedences
+(somewhat counterintuitively) bind stronger than higher precedences. So fixing our
+notations for \stexcode"\addition" and \stexcode"\multiplication", we get:
+
+\stexexample{%
+\notation{multiplication}[
+ op=\cdot,
+ prec=50
+]{#1}{##1 \comp\cdot ##2}
+\notation{addition}[
+ op=+,
+ prec=100
+]{#1}{##1 \comp+ ##2}
+
+$\addition{a,\multiplication{b,\addition{c,\multiplication{d,e}}}}$
+}
+
+Note that the precise numbers used for precedences are pretty arbitrary - what matters is
+which precedences are higher than which other precedences when used in conjunction.
+\begin{variable}{\infprec,\neginfprec}
+ It is occasionally useful to have ``infinitely'' high or low precedences to enforce or
+ forbid automated bracketing entirely -- for those purposes, \stexcode"\infprec" and
+ \stexcode"\neginfprec" exist (which are implemented as the maximal and minimal integer
+ values accordingly).
+\end{variable}
+
+\begin{dangerbox}
+ More precisely, each notation takes
+ \begin{enumerate}
+ \item One \emph{operator precedence} and
+ \item one \emph{argument precedence} for each argument.
+ \end{enumerate}
+ By default, all precedences are $0$, unless the symbol takes no argument, in which case
+ the operator precedence is \stexcode"\neginfprec" (negative infinity). If we only
+ provide a single number, this is taken as both the operator precedence and all argument
+ precedences.
+
+ \sTeX decides whether to insert parentheses by comparing operator precedences to a
+ \emph{downward precedence} $p_d$ with initial value \stexcode"\infprec". When
+ encountering a semantic macro, \sTeX takes the operator precedence $p_{op}$ of the
+ notation used and checks whether $p_{op}>p_d$. If so, \sTeX insert parentheses.
+
+ When \sTeX steps into an argument of a semantic macro, it sets $p_d$ to the respective
+ argument precedence of the notation used.
+
+ In the example above:
+ \begin{enumerate}
+ \item \sTeX starts out with $p_d=$\stexcode"\infprec".
+ \item \sTeX encounters \stexcode"\addition" with $p_{op}=100$. Since
+ $100\not>$\stexcode"\infprec", it inserts no parentheses.
+ \item Next, \sTeX encounters the two arguments for \stexcode"\addition". Both have no
+ specifically provided argument precedence, so \sTeX uses $p_d=p_{op}=100$ for both and
+ recurses.
+ \item Next, \sTeX encounters \stexcode"\multiplication{b,...}", whose notation has
+ $p_{op}=50$.
+ \item We compare to the current downward precedence $p_d$ set by \stexcode"\addition",
+ arriving at $p_{op}=50\not>100=p_d$, so \sTeX again inserts no parentheses.
+ \item Since the notation of \stexcode"\multiplication" has no explicitly set argument
+ precedences, \sTeX uses the operator precedence for all arguments of
+ \stexcode"\multiplication", hence sets $p_d=p_{op}=50$ and recurses.
+ \item Next, \sTeX encounters the inner \stexcode"\addition{c,...}" whose notation has
+ $p_{op}=100$.
+ \item We compare to the current downward precedence $p_d$ set by
+ \stexcode"\multiplication", arriving at $p_{op}=100>50=p_d$ -- which finally prompts
+ \sTeX to insert parentheses, and we proceed as before.
+ \end{enumerate}
+\end{dangerbox}
+\end{sfragment}
+
+\begin{sfragment}{Variables}
+ All symbol and notation declarations require a module with which they are associated,
+ hence the commands \stexcode"\symdecl", \stexcode"\notation", \stexcode"\symdef"
+ etc. are disabled outside of |smodule|-environments.
+
+ Variables are different -- variables are allowed everywhere, are not exported when the
+ current module (if one exists) is imported (via \stexcode"\importmodule" or
+ \stexcode"\usemodule") and (also unlike symbol declarations) ``disappear'' at the end of
+ the current \TeX\xspace group.
+
+ \begin{function}{\svar}
+ So far, we have always used variables using \stexcode"\svar{n}", which marks-up $n$ as
+ a variable with name |n|. More generally, \stexcode"\svar[foo]{<texcode>}" marks-up
+ the arbitrary |<texcode>| as representing a variable with name |foo|.
+ \end{function}
+
+ Of course, this makes it difficult to reuse variables, or introduce ``functional''
+ variables with arities $>0$, or provide them with a type or definiens.
+
+ \begin{function}{\vardef}
+ For that, we can use the \stexcode"\vardef" command. Its syntax is largely the same as
+ that of \stexcode"\symdef", but unlike symbols, variables have only one notation
+ (\textcolor{red}{TODO: so far?}), hence there is only \stexcode"\vardef" and no
+ \stexcode"\vardecl".
+ \end{function}
+
+\stexexample{%
+\vardef{varf}[
+ name=f,
+ type=\funtype{\Nat}{\Nat},
+ op=f,
+ args=1,
+ prec=0;\neginfprec
+]{\comp{f}#1}
+\vardef{varn}[name=n,type=\Nat]{\comp{n}}
+\vardef{varx}[name=x,type=\Nat]{\comp{x}}
+
+Given a function $\varf!:\funtype{\Nat}{\Nat}$,
+by $\addition{\varf!,\varn}$ we mean the function
+$\fun{\varx}{\varf{\addition{\varx,\varn}}}$
+}
+
+(of course, ``lifting'' addition in the way described in the previous example is an
+operation that deserves its own symbol rather than abusing \stexcode"\addition",
+but... well.)
+
+\textcolor{red}{TODO: bind=forall/exists}
+\end{sfragment}
+
+\begin{sfragment}{Variable Sequences}
+ Variable \emph{sequences} occur quite frequently in informal mathematics, hence they
+ deserve special support. Variable sequences behave like variables in that they disappear
+ at the end of the current \TeX\xspace group and are not exported from modules, but their
+ declaration is quite different.
+
+ \begin{function}{\varseq}
+ A variable sequence is introduced via the command \stexcode"\varseq", which takes the
+ usual optional arguments |name| and |type|. It then takes a starting index, an end
+ index and a \emph{notation} for the individual elements of the sequence parametric in
+ an index. Note that both the starting as well as the ending index may be variables.
+ \end{function}
+
+ This is best shown by example:
+ \stexexample{%
+\vardef{varn}[name=n,type=\Nat]{\comp{n}}
+\varseq{seqa}[name=a,type=\Nat]{1}{\varn}{\comp{a}_{#1}}
+
+The $i$th index of $\seqa!$ is $\seqa{i}$.
+}
+
+Note that the syntax |\seqa!| now automatically generates a presentation based on the
+starting and ending index.
+
+\textcolor{red}{TODO: more notations for invoking sequences}.
+
+\vardef{varn}[name=n,type=\Nat]{\comp{n}}
+\varseq{seqa}[name=a]{1}{\varn}{\comp{a}_{#1}}
+
+Notably, variable sequences are nicely compatible with |a|-type arguments, so we can do
+the following:
+
+\stexexample{%
+$\addition{\seqa}$
+}
+
+Sequences can be \emph{multidimensional} using the |args|-key, in which case the
+notation's arity increases and starting and ending indices have to be provided as a
+comma-separated list:
+
+\stexexample{%
+\vardef{varm}[name=m,type=\Nat]{\comp{m}}
+\varseq{seqa}[
+ name=a,
+ args=2,
+ type=\Nat,
+]{1,1}{\varn,\varm}{\comp{a}_{#1}^{#2}}
+
+$\seqa!$ and $\addition{\seqa}$
+}
+\vardef{varm}[name=m,type=\Nat]{\comp{m}}
+
+We can also explicitly provide a ``middle'' segment to be used, like such:
+
+\stexexample{%
+\varseq{seqa}[
+ name=a,
+ type=\Nat,
+ args=2,
+ mid={\comp{a}_{\varn}^1,\comp{a}_1^2,\ellipses,\comp{a}_{1}^{\varm}}
+]{1,1}{\varn,\varm}{\comp{a}_{#1}^{#2}}
+
+$\seqa!$ and $\addition{\seqa}$
+}
+\end{sfragment}
+\end{smodule}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "../stex-manual"
+%%% End:
+
+% LocalWords: binarysymbol newbinarysymbol hl,args a,b,c,d,e ascendingchain assoc binl
+% LocalWords: a,assoc binr x,y,z conj a,b,c,d pwconj funtype succ prec opprec argprec1
+% LocalWords: argprec texcode varf varn n,type varx x,type varseq seqa a,type th m,type
diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-terms.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-terms.tex
index cc67ce0c7fc..759b3f5fdd8 100644
--- a/Master/texmf-dist/doc/latex/stex/packages/stex-terms.tex
+++ b/Master/texmf-dist/doc/latex/stex/packages/stex-terms.tex
@@ -1 +1,177 @@
-\textcolor{red}{TODO: terms documentation} \ No newline at end of file
+\begin{smodule}{SymbolsInText}
+ \symdef{set}{\comp{\texttt{Set}}}
+
+ Given a symbol declaration \stexcode"\symdecl{symbolname}",
+ we obtain a semantic macro \stexcode"\symbolname".
+ We can use this semantic macro in math mode to use its notation(s),
+ and we can use \stexcode"\symbolname!"
+ in math mode to use its operator notation(s).
+ What else can we do?
+
+\begin{sfragment}{\texttt{\textbackslash symref} and its variants}
+
+ \begin{function}{\symref,\symname}
+ We have already seen \stexcode"\symname" and
+ \stexcode"\symref", the latter being the more general.
+
+ \stexcode"\symref{<symbolname>}{<code>}" marks-up |<code>|
+ as referencing |<symbolname>|. Since quite often, the |<code>|
+ should be (a variant of) the name of the symbol anyway,
+ we also have \stexcode"\symname{<symbolname>}".
+ \end{function}
+
+ Note that \stexcode"\symname" uses the \emph{name}
+ of a symbol, not its macroname. More precisely,
+ \stexcode"\symname" will insert the name of the symbol
+ with ``|-|'' replaced by spaces.
+ If a symbol does not have
+ an explicit |name=| given, the two are equal -- but
+ for \stexcode"\symname" it often makes sense to make the
+ two explicitly distinct. For example:
+ \stexexample{%
+\symdef{Nat}[
+ name=natural-number,
+ type=\set
+]{\comp{\mathbb{N}}}
+
+A \symname{Nat} is...
+ }
+
+ \stexcode"\symname" takes two additional optional
+ arguments, |pre=| and |post=| that get prepended or appended
+ respectively to the symbol name.
+
+ \begin{function}{\Symname}
+ Additionally, \stexcode"\Symname" behaves exactly
+ like \stexcode"\symname", but will capitalize the first
+ letter of the name:
+ \end{function}
+ \stexexample{%
+\Symname[post=s]{Nat} are...
+ }
+
+ \begin{dangerbox}
+ This is as good a place as any other to explain how
+ \sTeX resolves a string |symbolname| to an actual symbol.
+
+ If \stexcode"\symbolname" is a semantic macro, then
+ \sTeX has no trouble resolving |symbolname| to the full
+ URI of the symbol that is being invoked.
+
+ However, especially in \stexcode"\symname" (or if a symbol
+ was introduced using \stexcode"\symdecl*" without
+ generating a semantic macro), we might
+ prefer to use the \emph{name} of a symbol directly for
+ readability -- e.g. we would want to write
+ \stexcode"A \symname{natural-number} is..." rather than
+ \stexcode"A \symname{Nat} is...". \sTeX attempts to handle
+ this case thusly:
+
+ If |string| does \emph{not} correspond to a semantic
+ macro \stexcode"\string" and does \emph{not}
+ contain a |?|, then \sTeX checks
+ all symbols currently in scope until it finds one,
+ whose name is |string|. If |string| is of the
+ form |pre?name|, \sTeX first looks through all modules
+ currently in scope, whose full URI ends with |pre|,
+ and then looks for a symbol with name |name| in those.
+ This allows
+ for disambiguating more precisely, e.g. by
+ saying \stexcode"\symname{Integers?addition}"
+ or \stexcode"\symname{RealNumbers?addition}" in the
+ case where several |addition|s are in scope.
+ \end{dangerbox}
+\end{sfragment}
+
+\symdef{addition}[op=+,prec=100,args=2]{#1 \comp+ #2}
+\symdef{multiplication}[op=\cdot,prec=50,args=a]{#1}{##1 \comp\cdot ##2}
+
+\begin{sfragment}{Marking Up Text and On-the-Fly Notations}
+ We can also use semantic macros outside of text mode though,
+ which allows us to annotate arbitrary text fragments.
+
+ Let us assume again, that we have
+ \stexcode"\symdef{addition}[args=2]{#1 \comp+ #2}". Then we
+ can do
+ \stexexample{%
+\addition{\comp{The sum of} \arg{$\svar{n}$} \comp{ and }\arg{$\svar{m}$}}
+is...
+ }
+ ...which marks up the text fragment as representing
+ an \emph{application} of the |addition|-symbol to two
+ argument $\svar{n}$ and $\svar{m}$.
+
+ \begin{mmtbox}
+ As expected, the above example is translated to \omdoc/\mmt
+ as an |OMA| with |<OMS name="...?addition"/>| as head and
+ |<OMV name="n"/>| and |<OMV name="m"/>| as arguments.
+ \end{mmtbox}
+
+ \begin{dangerbox}
+ Note the difference in treating ``arguments'' between math mode and text mode. In
+ math mode the (in this case two) tokens/groups following the \stexcode|\addition|
+ macro are treated as arguments to the addition function, whereas in text mode the
+ group following \stexcode|\addition| is taken to be the ad-hoc presentation. We
+ drill in on this now.
+ \end{dangerbox}
+
+ \begin{function}{\arg}
+ In text mode, every semantic macro takes exactly one
+ argument, namely the text-fragment to be annotated.
+ The \stexcode"\arg" command is only valid within the
+ argument to a semantic macro and marks up the
+ \emph{individual arguments} for the symbol.
+ \end{function}
+
+ We can also use semantic macros in text mode to invoke
+ an operator itself instead of its application, with the
+ usual syntax using |!|:
+ \stexexample{%
+\addition!{Addition} is...
+ }
+
+ Indeed, \stexcode"\symbolname!{<code>}" is exactly equivalent to
+ \stexcode"\symref{symbolname}{<code>}" (the latter is in fact implemented in terms of
+ the former).
+
+ \stexcode"\arg" also allows us to switch the order of arguments
+ around and ``hide'' arguments: For example, \stexcode"\arg[3]{<code>}"
+ signifies that |<code>| represents the \emph{third}
+ argument to the current operator, and \stexcode"\arg*[i]{<code>}"
+ signifies that |<code>| represents the $i$th argument, but it
+ should not produce any output (it is exported in the |xhtml|
+ however, so that \mmt and other systems can pick up on it).\ednote{MK: I do not
+ understand why we have to/want to give the second arg*; I think this must be
+ elaborated on.}
+ \stexexample{%
+\addition{\comp{adding}
+ \arg[2]{$\svar{k}$}
+ \arg*{$\addition{\svar{n}}{\svar{m}}$}} yields...
+ }
+ Note that since the second \stexcode"\arg" has no explicit argument
+ number, it automatically represents the first not-yet-given
+ argument -- i.e. in this case the first one.\ednote{MK: I do not understand this at
+ all. }
+
+ \paragraph{} The same syntax can be used in math mod as well. This allows us to
+ spontaneously introduce new notations on the fly. We can activate it using the starred
+ variants of semantic macros:
+
+ \stexexample{%
+Given $\addition{\svar{n}}{\svar{m}}$, then
+$\addition*{
+ \arg*{\addition{\svar{n}}{\svar{m}}}
+ \comp{+}
+ \arg{\svar{k}}
+}$ yields...
+ }
+
+\end{sfragment}
+\end{smodule}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "../stex-manual"
+%%% End:
+
+% LocalWords: prec cdot,prec 50,args th
diff --git a/Master/texmf-dist/doc/latex/stex/packages/stex-tikzinput.tex b/Master/texmf-dist/doc/latex/stex/packages/stex-tikzinput.tex
index fb7d0c1e5b2..ac321f129cd 100644
--- a/Master/texmf-dist/doc/latex/stex/packages/stex-tikzinput.tex
+++ b/Master/texmf-dist/doc/latex/stex/packages/stex-tikzinput.tex
@@ -1 +1,61 @@
-\textcolor{red}{TODO: tikzinput documentation} \ No newline at end of file
+\begin{function}{image}
+ The behavior of the \pkg{ikzinput} package is determined by whether the |image| option
+ is given. If it is not, then the \pkg{tikz} package is loaded, all other options are
+ passed on to it and |\tikzinput{|\meta{file}|}| inputs the TIKZ file \meta{file}|.tex|;
+ if not, only the \pkg{graphicx} package is loaded and |\tikzinput{|\meta{file}|}| loads
+ an image file \meta{file}|.|\meta{ext} generated from \meta{file}|.tex|.
+\end{function}
+
+The selective input functionality of the \pkg{tikzinput} package assumes that the TIKZ
+pictures are externalized into a standalone picture file, such as the following one
+
+\begin{latexcode}
+\documentclass{standalone}
+\usepackage{tikz}
+\usetikzpackage{...}
+\begin{document}
+ \begin{tikzpicture}
+ ...
+ \end{tikzpicture}
+\end{document}
+\end{latexcode}
+
+ The \pkg{standalone} class is a minimal {\LaTeX} class that when loaded in a document
+ that uses the \pkg{standalone} package: the preamble and the |documenat| environment
+ are disregarded during loading, so they do not pose any problems. In effect, an
+ |\input| of the file above only sees the |tikzpicture| environment, but the file itself
+ is standalone in the sense that we can run {\LaTeX} over it separately, e.g. for
+ generating an image file from it.
+
+\begin{function}{\tikzinput,\ctikzinput}
+ This is exactly where the \pkg{tikzinput} package comes in: it supplies the |\tikzinput|
+ macro, which -- depending on the |image| option -- either directly inputs the TIKZ
+ picture (source) or tries to load an image file generated from it.
+
+ Concretely, if the |image| option is not set for the \pkg{tikzinput} package, then
+ |\tikzinput[|\meta{opt}|]{|\meta{file}|}| disregards the optional argument \meta{opt}
+ and inputs \meta{file}|.tex| via |\input| and resizes it to as specified in the |width|
+ and |height| keys. If it is, |\tikzinput[|\meta{opt}|]{|\meta{file}|}| expands to
+ |\includegraphics[|\meta{opt}|]{|\meta{file}|}|.
+
+ |\ctizkinput| is a version of |\tikzinput| that is centered.
+\end{function}
+
+\begin{function}{\mhtikzinput,\cmhtikzinput}
+ |\mhtizkinput| is a variant of |\tikzinput| that treats its file path argument as a
+ relative path in a math archive in analogy to \stexcode|\inputref|. To give the archive
+ path, we use the |mhrepos=| key. Again, |\cmhtizkinput| is a version of |\mhtikzinput|
+ that is centered.
+\end{function}
+
+\begin{function}{\libusetikzlibrary}
+ Sometimes, we want to supply archive-specific TIKZ libraries in the |lib| folder of the
+ archive or the |meta-inf/lib| of the archive group. Then we need an analogon to
+ \stexcode|\libinput| for \stexcode|\usetikzlibrary|. The \pkg{stex-tikzinput} package
+ provides the \stexcode|libusetikzlibrary| for this purpose.
+\end{function}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "../stex-manual"
+%%% End:
diff --git a/Master/texmf-dist/doc/latex/stex/stex-abstract.tex b/Master/texmf-dist/doc/latex/stex/stex-abstract.tex
index 445bbf064aa..f342bbf9075 100644
--- a/Master/texmf-dist/doc/latex/stex/stex-abstract.tex
+++ b/Master/texmf-dist/doc/latex/stex/stex-abstract.tex
@@ -1,10 +1,26 @@
\begin{abstract}
- \sTeX is a collection of {\LaTeX} package that allow to markup documents semantically without leaving the document format, essentially turning {\LaTeX} into a document format for mathematical knowledge management (MKM).
+ \sTeX is a collection of {\LaTeX} packages that allow to markup documents semantically
+ without leaving the document format.
+
+ Running `pdflatex` over sTeX-annotated documents formats them into normal-looking
+ PDF. But sTeX also comes with a conversion pipeline into semantically annotated HTML5,
+ which can host semantic added-value services that make the documents active
+ (i.e. interactive and user-adaptive) and essentially turning {\LaTeX} into a document
+ format for (mathematical) knowledge management (MKM).
\sTeX augments {\LaTeX} with
\begin{itemize}
- \item \emph{Semantic macros} that denote and distinguish between mathematical concepts, operators, etc. independent of their notational presentation,
- \item A powerful \emph{module system} that allows for authoring and importing individual fragments containing document text and/or semantic macros, independent of -- and without hard coding -- directory paths relative to the current document,
- \item A mechanism for exporting \sTeX documents to (modular) XHTML, preserving all the semantic information for semantically informed knowledge management services.
+ \item \emph{semantic macros} that denote and distinguish between mathematical concepts,
+ operators, etc. independent of their notational presentation,
+ \item a powerful \emph{module system} that allows for authoring and importing individual
+ fragments containing document text and/or semantic macros, independent of -- and
+ without hard coding -- directory paths relative to the current document, and
+ \item a mechanism for exporting \sTeX documents to (modular) XHTML, preserving all the
+ semantic information for semantically informed knowledge management services.
\end{itemize}
\end{abstract}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "stex-manual"
+%%% End:
diff --git a/Master/texmf-dist/doc/latex/stex/stex-doc.pdf b/Master/texmf-dist/doc/latex/stex/stex-doc.pdf
index 7499111fa86..0d0a36720cb 100644
--- a/Master/texmf-dist/doc/latex/stex/stex-doc.pdf
+++ b/Master/texmf-dist/doc/latex/stex/stex-doc.pdf
Binary files differ
diff --git a/Master/texmf-dist/doc/latex/stex/stex-doc.tex b/Master/texmf-dist/doc/latex/stex/stex-doc.tex
index d2e82390837..7a98ff49c2b 100644
--- a/Master/texmf-dist/doc/latex/stex/stex-doc.tex
+++ b/Master/texmf-dist/doc/latex/stex/stex-doc.tex
@@ -1,4 +1,4 @@
-\def\bibfolder{../lib/bib}
+\def\bibfolder#1{../lib/bib/#1}
\input{stex-docheader}
\infulldoctrue
@@ -7,14 +7,13 @@
\clist_gput_right:Nn \g_docinput_clist
{ #1 }
}
-\bool_set_true:N \stex_dtx_tests_bool
\ExplSyntaxOff
\expandafter\newif\csname if@infulldoc\expandafter\endcsname\csname @infulldoctrue\endcsname
\begin{document}
\title{
- The {\stex{3}} Package
+ The {\stex{3}} Package Collection
\thanks{Version {\fileversion} (last revised {\filedate})}
}
\author{Michael Kohlhase, Dennis Müller\\
@@ -207,4 +206,12 @@
\DocInputAgain
+\begin{sfragment}{References}\ednote{we need an un-numbered version {sfragment*}}
+ \printbibliography[heading=none]
+\end{sfragment}
\end{document}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
diff --git a/Master/texmf-dist/doc/latex/stex/stex-docheader.tex b/Master/texmf-dist/doc/latex/stex/stex-docheader.tex
index d0f13e90b33..d16b19703bd 100644
--- a/Master/texmf-dist/doc/latex/stex/stex-docheader.tex
+++ b/Master/texmf-dist/doc/latex/stex/stex-docheader.tex
@@ -7,14 +7,15 @@
\RequirePackage{tikzinput}
\usetikzlibrary{fit}
-\usepackage[debug=all,lang=en, mathhub=./tests]{stex}
+% \usepackage[debug=all,lang=en, mathhub=./tests]{stex}
+\usepackage[lang=en, mathhub=./tests]{stex}
\usepackage{url,array,float,textcomp}
\usepackage[show]{ed}
\usepackage[hyperref=auto,style=alphabetic]{biblatex}
-\addbibresource{\bibfolder/kwarcpubs.bib}
-\addbibresource{\bibfolder/extpubs.bib}
-\addbibresource{\bibfolder/kwarccrossrefs.bib}
-\addbibresource{\bibfolder/extcrossrefs.bib}
+\addbibresource{\bibfolder{kwarcpubs.bib}}
+\addbibresource{\bibfolder{extpubs.bib}}
+\addbibresource{\bibfolder{kwarccrossrefs.bib}}
+\addbibresource{\bibfolder{extcrossrefs.bib}}
\usepackage{amssymb}
\usepackage{amsfonts}
\usepackage{xspace}
@@ -26,73 +27,121 @@
\floatname{exfig}{Example}
\usepackage{listings}
-
-\ExplSyntaxOn
-
-\keys_define:nn { stex-tests } {
- do .bool_set:N = \stex_dtx_tests_bool
-}
-
-\ProcessKeysOptions { stex-tests }
-
-\prg_new_conditional:Nnn \stex_indtx: { T } {
- \bool_if:NTF \stex_dtx_tests_bool
- \prg_return_true: \prg_return_false:
+\usepackage{lststex}
+
+\lstdefinelanguage{sTeX}{
+ sensitive=true,
+ numbers=left,
+ numbersep=3pt,
+ xleftmargin=3pt,
+ alsodigit={\$},
+ %gobble=4,
+ alsoletter={\\},
+ %moredelim = [s][\itshape]{$}{$},
+ %moredelim = [s][\itshape\bfseries]{\\[}{\\]},
+ classoffset=0,keywordstyle=\bfseries,morekeywords={
+ \\begin,\\end,\\ExplSyntaxOn,\\ExplSyntaxOff,\\documentclass,
+ \\usepackage,\\def,\\[,\\],\\else,\\fi,$\iffalse$\fi,
+ \\newcommand, \\renewcommand, \\let
+ },
+ classoffset=1,keywordstyle=\itshape\color{OliveGreen},morekeywords={
+ \\defeq,\\geometricSeries,\\infinitesum,\\realdivide,
+ \\realpower,
+ \\symbolname,\\binarysymbol,\\newbinarysymbol,\\addition,
+ \\summation,\\ascendingchain,\\quantforall,\\set,\\funtype,
+ \\Nat,\\successor,\\multiplication,\\Int,\\zero,\\uminus,
+ \\intmonoid
+ },
+ classoffset=2,keywordstyle=\color{blue},morekeywords={
+ \\symdecl,\\symdef,\\notation,\\vardef,\\varseq,\\instantiate,
+ \\varinstantiate, \\renamedecl, \\assign, \\setnotation,
+ \\STEXexport
+ },
+ classoffset=3,keywordstyle=\color{BurntOrange},morekeywords={
+ \\importmodule,\\usemodule,\\libinput,\\inputref,\\mhinput,
+ \\libusepackage,\\addmhbibresource,\\ifinputref
+ },
+ classoffset=4,keywordstyle=\color{Purple},morekeywords={
+ \\definiendum,\\definame,\\symref,\\symname,\\comp,
+ \\compemph,\\definiens,\\svar,\\infprec,\\neginfprec,\\ellipses,
+ \\Symname,\\arg
+ },
+ classoffset=5,keywordstyle=\color{magenta},morekeywords={
+ smodule,sdefinition,sassertion,sparagraph,sexample,
+ sproof,subproof,spfcases,spfcase,spfstep,spfcomment,
+ \\spfidea,\\spfsketch,\\spfcasesketch,\\sproofend,
+ \\spfjust,\\premise,\\justarg,
+ copymodule,interpretmodule,mathstructure,sexample
+ },
+ classoffset=6,keywordstyle=\color{cyan},morekeywords={
+ sfragment,blindfragment,\\skipfragment,
+ \\currentsectionlevel,\\Currentsectionlevel
+ \\prematurestop,\\afterprematurestop,
+ \\setSGvar,\\useSGvar,\\ifSGvar
+ },
+ classoffset=7,keywordstyle=\color{brown},morekeywords={
+ frame,note,\\ifnotes,\\setslidelogo,\\setsource,\\setlicensing
+ slides,notes,sectocframes,frameimages,fiboxed,
+ nparagraph, nparagraph, ndefinition, nexample, nsproof, nassertion,
+ \\frameimage,\\mhframeimage,\\textwarning,
+ \\activateexcursion,\\printexcursion,\\excursionref,\\excursiongroup
+ },
+ classoffset=8,keywordstyle=\color{red},morekeywords={
+ frame,note
+ }
}
-\ExplSyntaxOff
-
-\lstdefinestyle{mylatex}{
- keywordstyle=\color{BurntOrange}
-}
-\lstdefinelanguage{mylatex}{
- emphstyle=\underbar,
- alsodigit={:},
- %alsoletter={_},
- alsoletter={\\}
- sensitive=true,
- classoffset=0,keywordstyle=\bfseries,
- morekeywords={\\begin,\\end,\\ExplSyntaxOn,\\ExplSyntaxOff},
- classoffset=1,keywordstyle=\color{blue},
- morekeywords={
- \\symdecl,
- \\symdef,
- \\notation,
- \\abbrdef,
- \\importmodule,
- \\usemodule,
- \\STEXwithbrackets,
- \\symref
- },
- classoffset=2,keywordstyle=\color{Purple},
- morekeywords={
- \\stex_path_from_string:Nn,
- \\stex_path_to_string:NN,
- \\stex_path_to_string:N,
- \\stex_require_repository:n,
- \\stex_modules_current_namespace:,
- \\stex_debug:n,
- \\stex_set_current_repository:n,
- \\stex_file_in_smsmode:nn,
- \\stex_get_symbol:n,
- },
- classoffset=3,keywordstyle=\color{SkyBlue},
- morekeywords={
- \\l_stex_modules_ns_str,
- \\g_stex_currentfile_seq,
- \\l_stex_current_module_prop,
- \\l_stex_get_symbol_uri_str,
- }
- classoffset=0,
-%^^A morecomment=[l][\color{Gray}]{//},
-%^^A morecomment=[s][\color{Gray}]{/*}{*/},
- morecomment=[s][\color{Green}]{$}{$},,
- morecomment=[s][\color{OliveGreen}]{\\[}{\\]},
+%\lstdefinestyle{mylatex}{
+% keywordstyle=\color{BurntOrange}
+%}
+%\lstdefinelanguage{mylatex}{
+% emphstyle=\underbar,
+% alsodigit={:},
+% %alsoletter={_},
+% alsoletter={\\}
+% sensitive=true,
+% classoffset=0,keywordstyle=\bfseries,
+% morekeywords={\\begin,\\end,\\ExplSyntaxOn,\\ExplSyntaxOff},
+% classoffset=1,keywordstyle=\color{blue},
+% morekeywords={
+% \\symdecl,
+% \\symdef,
+% \\notation,
+% \\abbrdef,
+% \\importmodule,
+% \\usemodule,
+% \\STEXwithbrackets,
+% \\symref
+% },
+% classoffset=2,keywordstyle=\color{Purple},
+% morekeywords={
+% \\stex_path_from_string:Nn,
+% \\stex_path_to_string:NN,
+% \\stex_path_to_string:N,
+% \\stex_require_repository:n,
+% \\stex_modules_current_namespace:,
+% \\stex_debug:n,
+% \\stex_set_current_repository:n,
+% \\stex_file_in_smsmode:nn,
+% \\stex_get_symbol:n,
+% },
+% classoffset=3,keywordstyle=\color{SkyBlue},
+% morekeywords={
+% \\l_stex_module_ns_str,
+% \\g_stex_currentfile_seq,
+% \\l_stex_current_module_prop,
+% \\l_stex_get_symbol_uri_str,
+% }
+% classoffset=0,
+%%^^A morecomment=[l][\color{Gray}]{//},
+%%^^A morecomment=[s][\color{Gray}]{/*}{*/},
+% morecomment=[s][\color{Green}]{$}{$},,
+% morecomment=[s][\color{OliveGreen}]{\\[}{\\]},
%^^A morestring=[b][\color{Purple}]\$,
-}
-\lstnewenvironment{latexcode}[1][language=mylatex]{\lstset{language=mylatex,basicstyle=\tiny,inputencoding=utf8,#1,alsoletter={\\,*},alsoother={\$}}}{}
-
+%}
+\lstnewenvironment{latexcode}[1][]{\lstset{language=sTeX,#1}}{}
+\def\stexcode{\lstinline[language=sTeX]}
\usepackage{mdframed,realboxes}
\usepackage[most]{tcolorbox}
@@ -103,13 +152,13 @@
\newenvironment{stextest@output}
{
- \begin{mdframed}[linewidth=1pt,backgroundcolor=white]\tiny
+ \begin{mdframed}[linewidth=1pt,backgroundcolor=white]\small
}
{\end{mdframed}}
\newenvironment{stextest@input}
{
- \begin{mdframed}[linewidth=1pt,backgroundcolor=lightgray]\tiny
+ \begin{mdframed}[linewidth=1pt,backgroundcolor=white]\small
}
{\end{mdframed}}
@@ -118,47 +167,49 @@
\newcount\test@counter\test@counter=0
\newcount\example@counter\example@counter=0
-\newenvironment{stextest@border}
-{
- \global\advance\test@counter by 1
- \newtcolorbox{stextestborderbox}{
- empty,
- title={Test \the\test@counter},
- attach boxed title to top left,
- minipage boxed title,
- boxed title style={empty,size=minimal,toprule=0pt,top=4pt,left=3mm,overlay={}},
- coltitle=red,fonttitle=\bfseries,
- before=\par\medskip\noindent,parbox=false,boxsep=0pt,left=3mm,right=0mm,top=2pt,breakable,pad at break=0mm,
- before upper=\csname @totalleftmargin\endcsname0pt,
- overlay unbroken={\draw[red,line width=2pt] ([xshift=-0pt]title.north west) -- ([xshift=-0pt]frame.south west); },
- overlay first={\draw[red,line width=2pt] ([xshift=-0pt]title.north west) -- ([xshift=-0pt]frame.south west); },
- overlay middle={\draw[red,line width=2pt] ([xshift=-0pt]frame.north west) -- ([xshift=-0pt]frame.south west); },
- overlay last={\draw[red,line width=2pt] ([xshift=-0pt]frame.north west) -- ([xshift=-0pt]frame.south west); },
- }
-%^^A\refstepcounter{remark}
-\begin{stextestborderbox}\small
+\newtcolorbox{exampleborderbox}{
+ empty,
+ title={Example \the\example@counter},
+ attach boxed title to top left,
+ minipage boxed title,
+ boxed title style={empty,size=minimal,toprule=0pt,top=1pt,left=3mm,overlay={}},
+ coltitle=blue,fonttitle=\bfseries,
+ parbox=false,boxsep=0pt,left=3mm,right=0mm,top=2pt,breakable,pad at break=0mm,
+ before upper=\csname @totalleftmargin\endcsname0pt,
+ overlay unbroken={\draw[blue,line width=2pt] ([xshift=-0pt]title.north west) -- ([xshift=-0pt]frame.south west); },
+ overlay first={\draw[blue,line width=2pt] ([xshift=-0pt]title.north west) -- ([xshift=-0pt]frame.south west); },
+ overlay middle={\draw[blue,line width=2pt] ([xshift=-0pt]frame.north west) -- ([xshift=-0pt]frame.south west); },
+ overlay last={\draw[blue,line width=2pt] ([xshift=-0pt]frame.north west) -- ([xshift=-0pt]frame.south west); },
+ outer arc=4pt
}
-{\end{stextestborderbox}}
+
+
+%\newtcolorbox{exampleborderbox}{
+% enhanced,
+% left=0pt,
+% title={Example \the\example@counter},
+% right=0pt,
+% top=8pt,
+% bottom=8pt,
+% colback=white,
+% colframe=blue,
+% width=\textwidth,
+% enlarge left by=0mm,
+% boxsep=5pt,
+% fontupper=\small,
+% arc=4pt,
+% outer arc=4pt,
+% leftupper=1.5cm,
+% fonttitle=\bfseries,
+% coltitle=blue,
+% boxed title style={empty,size=minimal,toprule=0pt,top=1pt,left=3mm,overlay={}},
+%}
\newenvironment{example@border}
{
\global\advance\example@counter by 1
- \newtcolorbox{exampleborderbox}{
- empty,
- title={Example \the\example@counter},
- attach boxed title to top left,
- minipage boxed title,
- boxed title style={empty,size=minimal,toprule=0pt,top=1pt,left=3mm,overlay={}},
- coltitle=blue,fonttitle=\bfseries,
- parbox=false,boxsep=0pt,left=3mm,right=0mm,top=2pt,breakable,pad at break=0mm,
- before upper=\csname @totalleftmargin\endcsname0pt,
- overlay unbroken={\draw[blue,line width=2pt] ([xshift=-0pt]title.north west) -- ([xshift=-0pt]frame.south west); },
- overlay first={\draw[blue,line width=2pt] ([xshift=-0pt]title.north west) -- ([xshift=-0pt]frame.south west); },
- overlay middle={\draw[blue,line width=2pt] ([xshift=-0pt]frame.north west) -- ([xshift=-0pt]frame.south west); },
- overlay last={\draw[blue,line width=2pt] ([xshift=-0pt]frame.north west) -- ([xshift=-0pt]frame.south west); },
- }
%^^A\refstepcounter{remark}
-\begin{exampleborderbox}\small
+\begin{exampleborderbox}
}
{\end{exampleborderbox}}
@@ -172,97 +223,134 @@
\ExplSyntaxOn
-\AddToHook{begindocument}{
- \stex_indtx:T {
- \newwrite\alltestsoutfile
- \immediate\openout\alltestsoutfile=alltests.tst
- }
-}
-
- \def\stextest{
- \begingroup
- \catcode`\\=12\relax
- \catcode`\#=12\relax
- \catcode`\&=12\relax
- \catcode`\$=12\relax
- \catcode`\^=12\relax
- \catcode`\_=12\relax
- \catcode`^^J=12\relax
- \endlinechar=`^^J
- \newlinechar=-1
+\def\stexexample{
+ \begingroup
+ \catcode`\\=12\relax
+ \catcode`\#=12\relax
+ \catcode`\&=12\relax
+ \catcode`\$=12\relax
+ \catcode`\^=12\relax
+ \catcode`\_=12\relax
+ \catcode`\ =12\relax
+ \catcode`^^J=12\relax
+ \endlinechar=`^^J
+ \newlinechar=-1
%^^A \everyeof{\noexpand}
- \test_a:n
- }
- \long\def \test_a:n #1 {
- \endgroup
- \stex_indtx:T {
- \immediate\write\alltestsoutfile{%
- ^^J\c_backslash_str stextest{\detokenize{^^J^^J#1^^J}}^^J
- }
+ \example_a:n
+}
+\long\def\example_a:n #1 {
+ \endgroup
+ \begin{example@border}
+ \immediate\openout\testoutfile=stextest.tex
+ \immediate\write\testoutfile{
+ \c_backslash_str begin{latexcode}
+ \detokenize{^^J}#1
+ \c_backslash_str end{latexcode}
}
- \begin{stextest@border}
- \immediate\openout\testoutfile=stextest.tst
- \immediate\write\testoutfile{
- \c_backslash_str begin{latexcode}
- \detokenize{^^J^^J#1^^J}
- \c_backslash_str end{latexcode}
- }
- \immediate\closeout\testoutfile
- \begin{stextest@input}
- \catcode`\#=12\relax
- \input{stextest.tst}
- \end{stextest@input}
- \immediate\openout\testoutfile=stextest.tst
- \immediate\write\testoutfile{\detokenize{#1}}
- \immediate\closeout\testoutfile
- \stex_indtx:T {
- \begin{stextest@output}
- \input{stextest.tst}
- \end{stextest@output}
- }
- \end{stextest@border}
- }
+ \immediate\closeout\testoutfile
+
+ Input:
+
+ \begin{stextest@input}
+ \catcode`\#=12\relax
+ \input{stextest.tex}
+ \end{stextest@input}
+ \immediate\openout\testoutfile=stextest.tex
+ \immediate\write\testoutfile{#1}
+ \immediate\closeout\testoutfile
+
+ Output:
+
+ \begin{stextest@output}
+ \input{stextest.tex}
+ \end{stextest@output}
+ \end{example@border}
+}
- \def\stexexample{
- \begingroup
- \catcode`\\=12\relax
- \catcode`\#=12\relax
- \catcode`\&=12\relax
- \catcode`\$=12\relax
- \catcode`\^=12\relax
- \catcode`\_=12\relax
- \catcode`^^J=12\relax
- \endlinechar=`^^J
- \newlinechar=-1
-%^^A \everyeof{\noexpand}
- \example_a:n
- }
- \long\def \example_a:n #1 {
- \endgroup
- \begin{example@border}
- \immediate\openout\testoutfile=stextest.tst
- \immediate\write\testoutfile{
- \c_backslash_str begin{latexcode}
- \detokenize{^^J}#1
- \c_backslash_str end{latexcode}
- }
- \immediate\closeout\testoutfile
- \begin{stextest@input}
- \catcode`\#=12\relax
- \input{stextest.tst}
- \end{stextest@input}
- \immediate\openout\testoutfile=stextest.tst
- \immediate\write\testoutfile{#1}
- \immediate\closeout\testoutfile
- \begin{stextest@output}
- \input{stextest.tst}
- \end{stextest@output}
- \end{example@border}
- }
+\ExplSyntaxOff
- \long\def\test#1{}
+\def\textwarning{\includegraphics[width=1.2em]{stex-dangerous-bend}\xspace}
+\newtcolorbox{dangerbox}{
+ breakable,
+ enhanced,
+ left=0pt,
+ right=0pt,
+ top=8pt,
+ bottom=8pt,
+ colback=white,
+ colframe=red,
+ width=\textwidth,
+ enlarge left by=0mm,
+ boxsep=5pt,
+ fontupper=\small,
+ arc=4pt,
+ outer arc=4pt,
+ leftupper=1.5cm,
+ overlay={
+ \node[anchor=west] at ([xshift=10pt]$(frame.north west)!0.5!(frame.south west)$)
+ {\includegraphics[width=1cm,height=1cm]{stex-dangerous-bend}};}
+}
-\ExplSyntaxOff
+\usetikzlibrary{decorations.pathmorphing,shapes,arrows,calc}
+% Taken from pgflibrarytikzmmt.code.tex
+\newcommand{\mmtarrowtip}{angle 45}
+\newcommand{\mmtarrowtipmonoright}{right hook}
+
+\tikzstyle{include}=[\mmtarrowtipmonoright-\mmtarrowtip,thick]
+\tikzstyle{morph}=[-\mmtarrowtip,thick]
+\tikzstyle{preview}=[decorate, decoration={coil,aspect=0,amplitude=1pt,
+ segment length=6pt,
+ pre=lineto,pre length=3pt,
+ post=lineto,post length=5pt}, thick]
+\tikzstyle{view}=[preview,-\mmtarrowtip]
+
+% TIKZ RULES
+\def\mmtlogo{
+\begin{tikzpicture}
+
+ % White Background (Margins are eyeballed)
+ % This is necessary because we paste white over arrows later.
+ % If somebody want's to do the full song and dance with
+ % interrupted arrows to get transparent background, be my guest.
+
+ \fill[white!] (-0.01,0.15) rectangle (1.11,-0.95);
+
+ % Arrows
+ \draw [blue, include] (0,0) -- (1.1,0);
+ \draw [green, morph] (0,-0.4) -- (1.1,-0.4);
+ \draw [red, view] (-0,-0.8) -- (1.1,-0.8);
+
+ % Cutout for letters
+ \fill[white] (0.33,0.1) rectangle (0.66,-0.9);
+
+ % Letters
+ \node at (0.18,0) (nodeM1) {\large M};
+ \node at (0.18,-0.4) (nodeM2) {\large M};
+ \node at (0.21,-0.8) (nodeT) {\large T};
+
+\end{tikzpicture}
+}
+
+\newtcolorbox{mmtbox}{
+ breakable,
+ enhanced,
+ left=0pt,
+ right=0pt,
+ top=8pt,
+ bottom=8pt,
+ colback=white,
+ colframe=green,
+ width=\textwidth,
+ enlarge left by=0mm,
+ boxsep=5pt,
+ fontupper=\small,
+ arc=4pt,
+ outer arc=4pt,
+ leftupper=1.5cm,
+ overlay={
+ \node[anchor=west] at ([xshift=10pt]$(frame.north west)!0.5!(frame.south west)$)
+ {\mmtlogo};}
+}
\MakeShortVerb{\|}
@@ -283,7 +371,7 @@
\def\atwintoo#1#2#3{{#1 #2 #3}\atwin{#1}{#2}{#3}}
\def\cT{\mathcal{T}}\def\cD{\mathcal{D}}
-\def\fileversion{3.0}
+\def\fileversion{3.1}
\def\filedate{\today}
\RequirePackage{pdfcomment}
@@ -322,7 +410,7 @@
\newif\ifinfulldoc\infulldocfalse
\makeatother
-\def\basedocurl{https://github.com/slatex/sTeX/blob/latex3/doc}
+\def\basedocurl{https://github.com/slatex/sTeX/blob/main/doc}
\newcounter{module}
\NewDocumentEnvironment {module}{}{
@@ -331,25 +419,31 @@
}{
}
-\stexpatchmodule{\begin{module}}{\end{module}}
-
-\def\compemph#1{\textcolor{blue}{#1}}
-\def\symrefemph#1{\textcolor{green}{#1}}
-
-\RequirePackage{pdfcomment}
-\makeatletter
-\protected\def\compemph@uri#1#2{%
- \pdftooltip{%
- \srefsymuri{#2}{\compemph{#1}}%
- }{%
- URI: \detokenize{#2}%
- }%
+\stexpatchmodule[visible]{\begin{module}}{\end{module}}
+
+\usepackage{stexthm}
+
+
+\newtcolorbox{remarkbox}[1][]{
+ empty,
+ title={Remark \theremark: #1},
+ attach boxed title to top left,
+ minipage boxed title,
+ boxed title style={empty,size=minimal,toprule=0pt,top=4pt,left=3mm,overlay={}},
+ fonttitle=\bfseries,coltitle=black,
+ before=\par\medskip\noindent,parbox=false,boxsep=0pt,left=3mm,right=0mm,top=2pt,breakable,pad at break=0mm,
+ before upper=\csname @totalleftmargin\endcsname0pt,
+ overlay unbroken={\draw[black,line width=2pt] ([xshift=-0pt]title.north west) -- ([xshift=-0pt]frame.south west); },
+ overlay first={\draw[black,line width=2pt] ([xshift=-0pt]title.north west) -- ([xshift=-0pt]frame.south west); },
+ overlay middle={\draw[black,line width=2pt] ([xshift=-0pt]frame.north west) -- ([xshift=-0pt]frame.south west); },
+ overlay last={\draw[black,line width=2pt] ([xshift=-0pt]frame.north west) -- ([xshift=-0pt]frame.south west); },
}
-\protected\def\symrefemph@uri#1#2{%
- \pdftooltip{%
- \srefsymuri{#2}{\symrefemph{#1}}%
- }{%
- URI: \detokenize{#2}%
- }%
+
+\renewenvironment{remark}[1][]{
+ \refstepcounter{remark}\begin{remarkbox}[#1]
+ \begin{mdframed}[linewidth=1pt,backgroundcolor=lightgray!33!white]
+}{
+\end{mdframed}\end{remarkbox}\endlist
}
-\makeatother \ No newline at end of file
+
+\usepackage{rustex}
diff --git a/Master/texmf-dist/doc/latex/stex/stex-manual.pdf b/Master/texmf-dist/doc/latex/stex/stex-manual.pdf
index 80b4154b9af..32c1e047ca5 100644
--- a/Master/texmf-dist/doc/latex/stex/stex-manual.pdf
+++ b/Master/texmf-dist/doc/latex/stex/stex-manual.pdf
Binary files differ
diff --git a/Master/texmf-dist/doc/latex/stex/stex-manual.tex b/Master/texmf-dist/doc/latex/stex/stex-manual.tex
index 92834af1c5e..31b9c4eaeb2 100644
--- a/Master/texmf-dist/doc/latex/stex/stex-manual.tex
+++ b/Master/texmf-dist/doc/latex/stex/stex-manual.tex
@@ -6,14 +6,12 @@
\csname if@infulldoc\endcsname\else
-\def\bibfolder{../lib/bib}
+\def\bibfolder#1{../lib/bib/#1}
\input{stex-docheader}
\infulldoctrue
-\csname bool_set_true:N\expandafter\endcsname\csname stex_dtx_tests_bool\endcsname
-
\begin{document}
\csname if@infulldoc\endcsname\else
\title{
@@ -33,7 +31,7 @@
associated software. It is primarily directed at end-users
who want to use \sTeX to author semantically
enriched documents. For the full documentation, see
- \href{\basedocurl/stex.pdf}{the \sTeX documentation}
+ \href{\basedocurl/stex-doc.pdf}{the \sTeX documentation}.
\makeatletter
\renewcommand\part{%
@@ -137,6 +135,19 @@
\long\def\ignore#1{}
+\begin{dangerbox}
+ Boxes like this one contain implementation details that are
+ mostly relevant for more advanced use cases, might be useful
+ to know when debugging, or might be good to know to better understand
+ how something works. They can easily be skipped on a first read.
+\end{dangerbox}
+
+\begin{mmtbox}
+ Boxes like this one explain how some \sTeX concept relates to the \mmt/\omdoc system,
+ philosophy or language; see \cite{uniformal:on,Kohlhase:OMDoc1.2} for introductions.
+\end{mmtbox}
+
+
\begin{sfragment}{What is \sTeX?}
Formal systems for mathematics (such as interactive theorem provers)
@@ -173,143 +184,98 @@ authoring workflows.
\paragraph{} The general \sTeX workflow combines functionalities
provided by several pieces of software:
\begin{itemize}
- \item The \sTeX package to use semantic annotations in
- {\LaTeX} documents,
- \item \RusTeX to convert |tex| sources to (semantically enriched)
- |xhtml|,
- \item The \mmt software, that extracts semantic information
- from the thus generated |xhtml| and provides semantically informed
- added value services.
+\item The \sTeX package collection to use semantic annotations in {\LaTeX} documents,
+\item \RusTeX \cite{RusTeX:on} to convert |tex| sources to (semantically enriched) |xhtml|,
+\item The \mmt system~\cite{uniformal:on}, that extracts semantic information from the
+ thus generated |xhtml| and provides semantically informed added value services.
+ Notably, \mmt integrates the \RusTeX system already.
\end{itemize}
-
-% ----------------------------
-
-\ignore{The objectives of this project will be achieved by developing a
-language and system
-that uses non-intrusive annotations
-to augment informal documents with semantic information
-(ranging from \textbf{fully formal} to \textbf{purely informal})
- without
-impacting linguistic presentation or document layout.
-That way, the system
-remains compatible with established publishing
-pipelines and practices, while additionally providing flexiformal
-information that
-enables formal knowledge management services, and hence produces
-\emph{rich active documents}, satisfying \textbf{R3}, \textbf{R4} and
-\textbf{R5}.
-In particular, it will avoid commitment to a fixed logical foundation.
-Instead, it will be designed as a modular pipeline of consecutive
-and compositional
-annotations, semantics extraction and translation steps, extensible
-via new structuring mechanisms (\textbf{R1}), library content
-(\textbf{R2}),
-NLP techniques, foundations, translation methods and
-end-user services.
-
-Naturally, the benefits of formal knowledge management services scale
-with the amount of mathematics involved. Consequently I will primarily
-focus on those
-STEM fields in which mathematical methods are most prominently
-used (e.g. mathematics, physics, computer science). Since in those fields
-\LaTeX~is the most commonly used scientific writing tool, I will also
-primarily focus on \LaTeX~as a development and evaluation target, but
-the system will be designed such that all components apart from
-the surface language will be integrable with other writing tools
-(e.g. WYSIWYG word processors).
-
-\paragraph{} The basic architecture of the proposed system is sketched in
-\autoref{fig:architecture}.
-\begin{figure}\centering
- \resizebox{0.95\textwidth}{!}{\tikzinput[]{diagram}}
- {\small (Note, that the syntax used
- in the box on the top right is prototypical and subject to change during the project.
- Details and open questions regarding the syntax are discussed here:
- \url{https://github.com/KWARC/FoMID/issues/1})}
- \caption{Basic Architecture of the Proposed System}\label{fig:architecture}
-\end{figure}
-A user can write their content using standard \LaTeX\ in an IDE;
-ideally using semantic annotations provided by \sTeX
-%and the library developed in \OBJref{smglom}
-(as in the upper right of
-\autoref{fig:architecture}), but not necessarily so.
-
-The document is converted to xhtml with \omdoc annotations
-using \LaTeX ML in the background,
-thus becoming actionable by the \mmt system. Both the source document
-as well as the generated xhtml/\omdoc are accessible to a natural language
-processing pripeline that can supply additional inferred semantic
-information or suggest annotations to the user, in the latter case
-augmenting the source document directly. This pipeline can use both
-classical NLP techniques using the GLIF system, as well as machine
-learning models such as \cite{own:fifom}.
-
-A semiformal fragment is converted
-into an appropriate syntax tree (possibly containing opaque
-informal nodes),
-thus becoming amenable
-to flexiformal knowledge management services. In a consecutive step
--- if sufficiently annotated --, these are
-additionally translated
-to a fully formal foundation, e.g. using the techniques from
-\cite{DMueller:phd:19,own:translations}, allowing
-more powerful services and conversion to established formal
-systems. All three representations
-are thus available from within the \mmt system for various
-knowledge management services, interfaces for which can be
-implemented in the IDE.
-
-Importantly, every non-trivial arrow in the figure is
-composable and extensible --
-translations to a foundation can be provided
-by supplying an appropriate formalization and alignment-based
-translations (or entirely new methods),
-services can be implemented generically using the \mmt API,
-NLP techniques can be implemented both inside and alongside of
-GLIF, and the concrete syntax within \sTeX can be extended
-by convenience macros in \LaTeX\ (enabling new
-structuring mechanisms as in \textbf{R1} via
-\mmt extensions, see
-\cite{MueRabRot:rslffml20}) as well as via additions to
-the library, which will be extensible both from within the IDE
-as well as on MathHub,
-remaining backwards compatible with existing content in a surface
-language. Additionally, sufficiently disambiguated
-statements can be translated to the syntax of
-external systems (such as interactive theorem prover systems
-or computer algebra systems),
-which can thus be integrated as additional services into the system.
-}
-
\end{sfragment}
\begin{sfragment}{Quickstart}
-
- \begin{sfragment}{Setup}
- \begin{sfragment}{The \sTeX IDE}
- TODO: VSCode Plugin
- \end{sfragment}
- \begin{sfragment}{Manual Setup}
- Foregoing on the \sTeX IDE, we will need several
- pieces of software; namely:
+
+ \begin{sfragment}{Setup}
+ There are two ways of using \sTeX: as a
+ \begin{enumerate}
+ \item way of writing {\LaTeX} more modularly (object-oriented Math) for creating PDF
+ documents or
+ \item foundation for authoring active documents in HTML5 instrumented with knowledge
+ management services.
+ \end{enumerate}
+ Both are legitimate and useful. The first requires a significantly smaller
+ tool-chain, so we describe it first. The second requires a much more substantial
+ (and experimental) toolchain of knowledge management systems. Both workflows profit
+ from an integrated development environment (IDE), which (also) automates setup as
+ far as possible (see \sref{sec.sTeX-IDE}).
+
+ \begin{sfragment}[id=sec.minimal-setup]{Minimal Setup for the PDF-only Workflow}
+ In the best of all worlds, there is no setup, as you already have a new version of
+ {\TeX}Live on your system as a {\LaTeX} enthusiast. If not now is the time to
+ install it; see \cite{TeXLive:on}. You can usually update {\TeX}Live via a package
+ manager or the {\TeX}Live manager \textbf{tlmgr}.
+
+ Alternatively, you can install \sTeX from CTAN, the Comprehensive {\TeX} Archive
+ Network; see \cite{stexCTAN:on} for details.
+ \end{sfragment}
+
+ \begin{sfragment}[id=sec.git-setup]{GIT-based Setup for the \sTeX Development Version}
+ If you want use the latest and greatest \sTeX packages
+ that have not even been released to CTAN,
+ then you can directly clone them from the \sTeX development
+ repository \cite{sTeX:github:on} by the following command-line instructions:
+\begin{lstlisting}[language=bash]
+ cd <stexdir>
+ git clone https://github.com/slatex/sTeX.git
+\end{lstlisting}
+ and keep it updated by pulling updates via \lstinline|git pull| in the cloned \sTeX
+ directory.
+ Then update your \lstinline|TEXINPUTS| environment variable, e.g. by placing the following line in your \lstinline|.bashrc|:
+\begin{lstlisting}[language=bash]
+export TEXINPUTS="$(TEXINPUTS):<sTeXDIR>//:"
+\end{lstlisting}
+ \end{sfragment}
+
+ \begin{sfragment}[id=sec.stex-archives]{\sTeX Archives (Manual Setup)}
+ Writing semantically annotated \sTeX becomes much easier, if we can use
+ well-designed libraries of already annotated content. \sTeX provides such
+ libraries as \sTeX archives -- i.e. GIT repositories at
+ \url{https://gl.mathhub.info} -- most prominently the SMGLoM libraries at
+ \url{https://gl.mathhub.info/smglom}.
+
+ To do so, we set up a \textbf{local MathHub} by creating a MathHub directory
+ \lstinline|<mhdir>|. Every \sTeX archive as an \textbf{archive path}
+ \lstinline|<apath>| and a name \lstinline|<archive>|. We can clone the \sTeX
+ archive by the following command-line instructions:
+\begin{lstlisting}[language=bash]
+ cd <mhdir>/<apath>
+ git clone https://gl.mathhub.info/smglom/<archive>.git
+\end{lstlisting}
+ Note that \sTeX archives often depend on other archives, thus you should be
+ prepared to clone these as well -- e.g. if \texttt{pdflatex} reports missing
+ files.
+ To make sure that \sTeX too knows where to find its archives, we need to set a global
+ system variable |MATHHUB|, that points to your local |MathHub|-directory (see
+ \sref{sec.stexarchives}).
+\begin{lstlisting}[language=bash]
+export MATHHUB="<mhdir>''
+\end{lstlisting}
+ \end{sfragment}
+
+ \begin{sfragment}[id=sec.sTeX-IDE]{The \sTeX IDE}
+ We are currently working on an \sTeX IDE as an \sTeX plugin for |VScode|;
+ see~\cite{sTeX-IDE:on}. It will feature a setup procedure that automates the setup
+ described above (and below). For additional functionality see the (now obsolete)
+ plugin for \sTeX1 \cite{stexls:on,stexls-vscode-plugin:on}.
+ \end{sfragment}
+
+ \begin{sfragment}{Manual Setup for Active Documents and Knowledge Management Services}
+ Foregoing on the \sTeX IDE, we will need several additional (on top of the minimal
+ setup above) pieces of software; namely:
\begin{itemize}
- \item \textbf{The \sTeX-Package} available
- \href{https://github.com/slatex/sTeX/blob/latex3/doc/stex.pdf}{here}%
- \ednote{For now, we require the \texttt{latex3}-branch}.
- Note, that the CTAN repository for \LaTeX{} packages
- may contain outdated versions of the \sTeX package, so
- make sure, that your |TEXMF| system variable is configured such
- that the packages available in the linked repository are prioritized
- over potential default packages that come with your \TeX{} distribution.
-
- %If you are only interested in using semantic macros in (ultimately)
- %|pdf|s generated by |pdflatex|, this is all you need.
-
\item \textbf{The \mmt System} available
- \href{https://github.com/uniformal/MMT/tree/sTeX}{here}%
- \ednote{For now, we require the \texttt{sTeX}-branch, requiring manually
- compiling the MMT sources}. We recommend following
+ \href{https://github.com/uniformal/MMT/tree/sTeX}{here}.
+ We recommend following
the setup routine documented
\href{https://uniformal.github.io//doc/setup/}{here}.
@@ -317,513 +283,305 @@ which can thus be integrated as additional services into the system.
a |MathHub|-directory on your local file system, where
the \mmt system will look for \sTeX/\mmt content archives.
- \item To make sure that \sTeX too knows where to find its
- archives, we need to set a global system variable |MATHHUB|,
- that points to your local |MathHub|-directory
- (see \sref{sec.stexarchives}).
- \item \textbf{\sTeX Archives} If we only care about {\LaTeX} and generating |pdf|s, we do not
- technically need \mmt at all; however, we still need the |MATHHUB|
- system variable to be set. Furthermore, \mmt can make downloading
- content archives we might want to use significantly easier, since
- it makes sure that all dependencies of (often highly interrelated)
- \sTeX archives are cloned as well.
-
- Once set up, we can run |mmt| in a shell and download an archive along with
- all of its dependencies like this: |lmh install <name-of-repository>|,
- or a whole \emph{group} of archives; for example,
- |lmh install smglom| will download all smglom archives.
- \item \textbf{\RusTeX} The \mmt system will also set up \RusTeX for you,
- which is used to generate (semantically annotated)
- |xhtml| from tex sources. In lieu of using \mmt, you
- can also download and use \RusTeX directly
+ \item \textbf{\sTeX Archives} If we only care about {\LaTeX} and generating
+ |pdf|s, we do not technically need \mmt at all; however, we still need the
+ |MATHHUB| system variable to be set. Furthermore, \mmt can make downloading
+ content archives we might want to use significantly easier, since it makes sure
+ that all dependencies of (often highly interrelated) \sTeX archives are cloned
+ as well.
+
+ Once set up, we can run |mmt| in a shell and download an archive along with all
+ of its dependencies like this: |lmh install <name-of-repository>|, or a whole
+ \emph{group} of archives; for example, |lmh install smglom| will download all
+ smglom archives.
+ \item \textbf{\RusTeX} The \mmt system will also set up \RusTeX for you, which is
+ used to generate (semantically annotated) |xhtml| from tex sources. In lieu of
+ using \mmt, you can also download and use \RusTeX directly
\href{https://github.com/slatex/RusTeX}{here}.
-
\end{itemize}
\end{sfragment}
- \end{sfragment}
- \begin{sfragment}{A First \sTeX Document}
- Having set everything up, we can write a first
- \sTeX document. As an example, we will use the
- |smglom/calculus| and |smglom/arithmetics| archives,
- which should be present in the designated |MathHub|-folder.
-
- The document we will consider is the following:
- \begin{framed}\begin{latexcode}
-\documentclass{article}
-\usepackage{stex}
-\usepackage{xcolor}
-\def\compemph#1{\textcolor{blue}{#1}}
+ \end{sfragment}
+
+ \input{stex-tutorial}
-\begin{document}
- \usemodule[smglom/calculus]{series}
- \usemodule[smglom/arithmetics]{realarith}
-
- The \symref{series}{series} $\infinitesum{n}{1}{
- \realdivide[frac]{1}{
- \realpower{2}{n}
- }
- }$ \symref{converges}{converges} towards $1$.
-
-\end{document}
- \end{latexcode}\end{framed}
-
- Compiling this document with |pdflatex| should yield
- the output
-
- \begin{framed}
- The \textbf{series}
- $\textcolor{blue}{\sum}_{n=1}^{\textcolor{blue}\infty} \frac{1}{2^n}$
- \textbf{converges} towards $1$.
- \end{framed}
-
- Note that the $\sum$ and $\infty$-symbols are highlighted in blue,
- and the words ``series'' and ``converges'' in bold.
- This signifies that these words and symbols
- reference \sTeX \emph{symbols}
- formally declared somewhere; associating their
- \emph{presentation} in the document with their (formal)
- definition - i.e. their semantics. The precise way
- in which they are highlighted (if at all) can of course
- be customized (see \ednote{somewhere later}).
-
- \begin{function}{\usemodule}
- The command |\usemodule[some/archive]{modulename}|
- finds some module in the appropriate archive -- in the first
- case (|\usemodule[smglom/calculus]{series}|), \sTeX
- looks for the archive |smglom/calculus| in our local
- MathHub-directory (see \sref{sec.stexarchives}), and
- in its source-folder for a file |series.tex|. Since no such
- file exists, and by default the document is assumed to be
- in \emph{english}, it picks the file |series.en.tex|, and
- indeed, in here we find a statement |\begin{smodule}{series}|.
- \iffalse\end{smodule}\fi
-
- \sTeX now reads this file and makes all semantic macros therein
- available to use, along with all its dependencies.
- This enables the usage of |\infinitesum| later on.
-
- Analogously, |\usemodule[smglom/arithmetics]{realarith}|
- opens the file |realarith.en.tex| in the |.../smglom/arithmetics/source|-folder
- and makes its contents available, e.g. |\realdivide| and |\realpower|.
- \end{function}
-
- \begin{function}{\symref,\symname}
- The command |\symref{symbolname}{text}| marks the |text|
- in the second argument as representing the |symbolname|
- in the first argument -- which is why the word ``series''
- is set in boldface. In the pdf, this is all that happens.
- In the |xhtml| (which we will investigate shortly) however,
- we will note that the word ``series'' is now annotated with the
- full URI of the symbol denoting the \emph{mathematical concept of
- a series}. In other words, the word is associated with an unambiguous
- semantics.
-
- Notably, in both cases above (\emph{series} and \emph{converges})
- the text that \emph{references} the symbol and the name of the symbol
- are identical. Since this occurs quite often, the shorthand
- |\symname{converges}| would have worked as well, where
- |\symname{foo-bar}| behaves exactly like |\symref{foo-bar}{foo bar}|
- - i.e. the text is simply the name of the symbol with ``|-|'' replaced by
- a space.
- \end{function}
-
- \begin{function}{\importmodule}
- If you investigated the contents of the imported modules
- (|realarith| and |series|) more closely, you'll note that
- none of them contain a symbol ``|converges|''. Yet, we
- can use |\symref| to refer to ``converges''. That is because
- the symbol |converges| is found in
- |smglom/calculus/source/sequenceConvergence.en.tex|, and
- |series.en.tex| contains the line
- |\importmodule{sequenceConvergence}|. The |\importmodule|-statement
- makes the module referenced available to all documents
- that include the current module. As such, a ``current module''
- has to exist for |\importmodule| to work, which is why the command
- is only allowed within a |module|-environment.
- \end{function}
-
- \textcolor{red}{TODO} explain |xhtml| conversion, MMT compilation
- (requires an archive...?).
-
- \end{sfragment}
\end{sfragment}
-\begin{sfragment}{Using \sTeX}
+\begin{sfragment}{Creating \sTeX Content}
+
\input{packages/stex-basics}
-
- \input{packages/stex-terms}
- \input{packages/stex-references}
-\end{sfragment}
+ \begin{sfragment}{How Knowledge is Organized in \sTeX}
+
+ \sTeX content is organized on multiple levels:
+ \begin{enumerate}
+ \item \sTeX \textbf{archives} (see \sref{sec.stexarchives})
+ contain individual |.tex|-files.
+ \item These may contain \sTeX \textbf{modules}, introduced via
+ \stexcode"\begin{smodule}{ModuleName}".\iffalse\end{smodule}\fi
+ \item Modules contain \sTeX \textbf{symbol declarations}, introduced via
+ \stexcode"\symdecl{symbolname}", \stexcode"\symdef{symbolname}" and some other
+ constructions. Most symbols have a \emph{notation} that can
+ be used via a \emph{semantic macro} \stexcode"\symbolname" generated
+ by symbol declarations.
+ \item \sTeX \textbf{expressions} finally are built up from
+ usages of semantic macros.
+ \end{enumerate}
+
+ \begin{mmtbox}
+ \begin{itemize}
+ \item \sTeX archives are simultaneously \mmt archives, and the same directory
+ structure is consequently used.
+ \item \sTeX modules correspond to \omdoc/\mmt \emph{theories}.
+ \stexcode"\importmodule"s (and similar constructions) induce \mmt |include|s and
+ other \emph{theory morphisms}, thus giving rise to a \emph{theory graph} in the
+ \omdoc sense~\cite{RabKoh:WSMSML13}.
+ \item Symbol declarations induce \omdoc/\mmt \emph{constants}, with optional
+ (formal) \emph{type} and \emph{definiens} components.
+ \item Finally, \sTeX expressions are converted to \omdoc/\mmt terms, which use the
+ abstract syntax (and XML encoding) of \openmath \cite{BusCapCar:2oms04}.
+ \end{itemize}
+ \end{mmtbox}
+ \end{sfragment}
-\begin{sfragment}[id=sec.stexarchives]{\sTeX Archives}
- \input{packages/stex-mathhub}
-\end{sfragment}
+ \begin{sfragment}[id=sec.stexarchives]{\sTeX Archives}
+ \input{packages/stex-mathhub}
+ \end{sfragment}
-\begin{sfragment}{Creating New Modules and Symbols}
- \textcolor{red}{TODO}
+ \begin{sfragment}[id=sec.decls]{Module, Symbol and Notation Declarations}
+ \input{packages/stex-modules}
+ \input{packages/stex-symbols}
+ \end{sfragment}
- \stexexample{
- \begin{smodule}{assoctest}
- \symdef{foo}[args=iia]{\comp{a:}#1\comp{;b:}#2\comp{;c:}#3}{\comp[#1\comp{;}##1\comp+##2\comp;#2\comp]}
- $\foo {w_1}{w_2}{x,y,z}$
- \end{smodule}
- }
-
- \input{packages/stex-modules}
+ \begin{sfragment}{Module Inheritance and Structures}
+ The \sTeX features for modular document management are inherited from the OMDoc/MMT
+ model that organizes knowledge into a graph, where the nodes are theories (called
+ modules in \sTeX) and the edges are truth-preserving mappings (called theory
+ morphismes in MMT). We have already seen modules/theories above.
+
+ Before we get into theory morphisms in \sTeX we will see a very simple application of
+ modules: managing multilinguality modularly.
+
+ \begin{sfragment}{Multilinguality and Translations}
+
+ If we load the \sTeX document class or package with the option |lang=<lang>|, \sTeX
+ will load the appropriate \pkg{babel} language for you -- e.g. |lang=de| will load
+ the babel language |ngerman|. Additionally, it makes \sTeX aware of the current
+ document being set in (in this example) \emph{german}. This matters for reasons
+ other than mere \pkg{babel}-purposes, though:
+
+ Every \emph{module} is assigned a language. If no \sTeX
+ package option is set that allows for inferring a language,
+ \sTeX will check whether the current file name ends in
+ e.g. |.en.tex| (or |.de.tex| or |.fr.tex|, or...) and
+ set the language accordingly. Alternatively, a language
+ can be explicitly assigned via
+ \stexcode"\begin{smodule}[lang=<language>]{Foo}".
+ \iffalse\end{smodule}\fi
- \input{packages/stex-symbols}
+ \begin{mmtbox}
+ Technically, each |smodule|-environment induces \emph{two}
+ \omdoc/\mmt theories:
+ \stexcode"\begin{smodule}[lang=<lang>]{Foo}"
+ \iffalse\end{smodule}\fi
+ generates a theory |some/namespace?Foo| that only contains
+ the ``formal'' part of the module -- i.e. exactly the
+ content that is exported when using \stexcode"\importmodule".
+
+ Additionally, \mmt generates a \emph{language theory}
+ |some/namespace/Foo?<lang>| that includes |some/namespace?Foo|
+ and contains all the other document content -- variable
+ declarations, includes for each \stexcode"\usemodule", etc.
+ \end{mmtbox}
+
+ Notably, the language suffix in a filename is ignored
+ for \stexcode"\usemodule", \stexcode"\importmodule"
+ and in generating/computing URIs for modules. This however
+ allows for providing \emph{translations} for modules
+ between languages without needing to duplicate content:
+
+ If a module |Foo| exists in e.g. english in a file |Foo.en.tex|,
+ we can provide a file |Foo.de.tex| right next to it, and write
+ \stexcode"\begin{smodule}[sig=en]{Foo}".
+ \iffalse\end{smodule}\fi
+ The |sig|-key then signifies, that the ``signature'' of the
+ module is contained in the \emph{english} version of the module,
+ which is immediately imported from there, just like
+ \stexcode"\importmodule" would.
+
+ Additionally to translating the informal content of a module
+ file to different languages, it also allows for customizing
+ notations between languages. For example,
+ the \emph{least common multiple} of two numbers is often
+ denoted as $\mathtt{lcm}(a,b)$ in english, but is
+ called \emph{kleinstes gemeinsames Vielfaches} in german
+ and consequently denoted as $\mathtt{kgV}(a,b)$ there.
+
+ We can therefore imagine a german version of an lcm-module
+ looking something like this:
+
+ \begin{latexcode}[gobble=8]
+ \begin{smodule}[sig=en]{lcm}
+ \notation*{lcm}[de]{\comp{\mathtt{kgV}}(#1,#2)}
+
+ Das \symref{lcm}{kleinste gemeinsame Vielfache}
+ $\lcm{a,b}$ von zwei Zahlen $a,b$ ist...
+ \end{smodule}
+ \end{latexcode}
+
+ If we now do \stexcode"\importmodule{lcm}"
+ (or \stexcode"\usemodule{lcm}") within a \emph{german} document,
+ it will also load the content of the german translation,
+ including the |de|-notation for \stexcode"\lcm".
- \input{packages/stex-inheritance}
+ \end{sfragment}
- \begin{sfragment}{Advanced Structuring Mechanisms}
+ \input{packages/stex-inheritance}
\input{packages/stex-features}
\end{sfragment}
+
\begin{sfragment}{Primitive Symbols (The \sTeX Metatheory)}
\input{packages/stex-metatheory}
\end{sfragment}
+
\end{sfragment}
-\begin{sfragment}{\sTeX Statements (Definitions, Theorems, Examples, ...)}
- \input{packages/stex-statements}
+\begin{sfragment}[id=sec.textsymbols]{Using \sTeX Symbols}
+ \input{packages/stex-terms}
+ \input{packages/stex-references}
+\end{sfragment}
+\begin{sfragment}{\sTeX Statements}
+ \input{packages/stex-statements}
\input{packages/stex-proofs}
\end{sfragment}
+\begin{sfragment}[id=sec.customhighlight]{Highlighting and Presentation Customizations}
+
+ The environments starting with |s| (i.e. \stexcode"smodule", \stexcode"sassertion",
+ \stexcode"sexample", \stexcode"sdefinition", \stexcode"sparagraph" and
+ \stexcode"sproof") by default produce no additional output whatsoever (except for the
+ environment content of course). Instead, the document that uses them (whether directly
+ or e.g. via \stexcode"\inputref") can decide how these environments are supposed to look
+ like.
+
+ The \pkg{stexthm} package defines some default customizations that can be used, but of
+ course many existing \LaTeX\xspace templates come with their own |definition|, |theorem|
+ and similar environments that authors are supposed (or even required) to use. Their
+ concrete syntax however is usually not compatible with all the additional arguments that
+ \sTeX allows for semantic information.
+
+ Therefore we introduced the separate environments \stexcode"sdefinition" etc. instead of
+ using \stexcode"definition" directly. We allow authors to specify how these environments
+ should be styled via the commands \stexcode"stexpatch*".
+
+ \begin{function}{\stexpatchmodule,\stexpatchdefinition,
+ \stexpatchassertion,\stexpatchexample,\stexpatchparagraph,
+ \stexpatchproof}
+ All of these commands take one optional and two proper arguments, i.e.\\
+ \stexcode"\stexpatch*[<type>]{<begin-code>}{<end-code>}".
+
+ After \stex reads and processes the optional arguments for these environments, (some
+ of) their values are stored in the macros \stexcode"\s*<field>"
+ (i.e. \stexcode"sexampleid", \stexcode"\sassertionname", etc.). It then checks for all
+ the values |<type>| in the |type=|-list, whether an \stexcode"\stexpatch*[<type>]" for
+ the current environment has been called. If it finds one, it uses the patches
+ |<begin-code>| and |<end-code>| to mark up the current environment. If no patch for
+ (any of) the type(s) is found, it checks whether and \stexcode"\stexpatch*" was called
+ without optional argument.
+ \end{function}
+
+ For example, if we want to use a predefined |theorem| environment for
+ \stexcode"sassertion"s with |type=theorem|, we can do
+\begin{latexcode}
+\stexpatchassertion[theorem]{\begin{theorem}}{\end{theorem}}
+\end{latexcode}
+ ...or, rather, since e.g. |theorem|-like environments defined using \pkg{amsthm} take an
+ optional title as argument, we can do:
+\begin{latexcode}
+\stexpatchassertion[theorem]
+ {\ifx\sassertiontitle\@empty
+ \begin{theorem}
+ \else
+ \begin{theorem}[\sassertiontitle]
+ \fi}
+ {\end{theorem}}
+\end{latexcode}
+
+ Or, if we want \emph{all kinds of} \stexcode"sdefinition"s to use a predefined
+ |definition|-environment irrespective of their |type=|, then we can issue the following
+ customization patch:
+\begin{latexcode}
+\stexpatchdefinition
+ {\ifx\sdefinitiontitle\@empty
+ \begin{definition}
+ \else
+ \begin{definition}[\sdefinitiontitle]
+ \fi}
+ {\end{definition}}
+\end{latexcode}
+
+ \begin{function}{\compemph,\varemph,\symrefemph,\defemph}
+ Apart from the environments, we can control how \sTeX highlights variables, notation
+ components, \stexcode"\symref"s and \stexcode"\definiendum"s, respectively.
+
+ To do so, we simply redefine these four macros. For example, to highlight notation
+ components (i.e. everything in a \stexcode"\comp") in blue, as in this document, we
+ can do \stexcode"\def\compemph#1{\textcolor{blue}{#1}}". By default, |\compemph| et
+ al do nothing.
+ \end{function}
+
+ \begin{function}{\compemph@uri,\varemph@uri,\symrefemph@uri,\defemph@uri}
+ For each of the four macros, there exists an additional macro that takes the full URI
+ of the relevant symbol currently being highlighted as a second argument. That allows
+ us to e.g. use pdf tooltips and links. For example, this document uses\Ednote{MK: why
+ |protected|, ... if we show that, then we should explain.}
+\begin{latexcode}
+\protected\def\symrefemph@uri#1#2{
+ \pdftooltip{
+ \srefsymuri{#2}{\symrefemph{#1}}
+ }{
+ URI:~\detokenize{#2}
+ }
+}
+\end{latexcode}
+ By default, |\compemph@uri| is simply defined as |\compemph{#1}| (analogously for the
+ other three commands).
+\end{function}
+\end{sfragment}
+
\begin{sfragment}{Additional Packages}
- \input{packages/stex-tikzinput}
+ \begin{sfragment}{Tikzinput: Treating TIKZ code as images}
+ \input{packages/stex-tikzinput}
+ \end{sfragment}
\begin{sfragment}{Modular Document Structuring}
\input{packages/stex-document-structure}
\end{sfragment}
\begin{sfragment}{Slides and Course Notes}
\input{packages/stex-slides}
\end{sfragment}
- \begin{sfragment}{Homework, Problems and Exams}
+ \begin{sfragment}{Representing Problems and Solutions}
\input{packages/stex-problem}
-
- \input{packages/stex-hwexam}
\end{sfragment}
-
+ \begin{sfragment}{Homeworks, Quizzes and Exams}
+ \input{packages/stex-hwexam}
+ \end{sfragment}
\end{sfragment}
-\chapter{Stuff}
-
-\section{Modules}
-
-
-\begin{function}{\sTeX , \stex}
- Both print this \stex logo.
-\end{function}
-
- \subsection{Semantic Macros and Notations}
-
- Semantic macros invoke a formally declared symbol.
-
- To declare a symbol (in a module), we use \cs{symdecl},
- which takes as argument the name of the corresponding
- semantic macro, e.g. |\symdecl{foo}| introduces the macro
- \cs{foo}. Additionally, \cs{symdecl} takes several options,
- the most important one being its arity. |foo| as declared above
- yields a \emph{constant} symbol. To introduce an \emph{operator}
- which takes arguments, we have to specify which arguments it takes.
-
- \begin{smodule}{SemanticMacrosExample}
- For example, to introduce binary multiplication,
- we can do |\symdecl{mult}[args=2]|. We can then supply
- the semantic macro with arbitrarily many notations, such as
- |\notation{mult}{#1 #2}|.
-
- \stexexample{
- \symdecl{mult}[args=2]
- \notation{mult}{#1 #2}
- $\mult{a}{b}$
-}
-
- Since usually, a freshly introduced symbol also comes with a
- notation from the start, the \cs{symdef} command combines
- \cs{symdecl} and \cs{notation}. So instead of the above,
- we could have also written
- \begin{center} |\symdef{mult}[args=2]{#1 #2}| \end{center}
-
- \symdecl{mult}[args=2]
- \notation{mult}{#1 #2}
-
- \notation{mult}[cdot]{#1 \comp{\cdot} #2}
- \notation{mult}[times]{#1 \comp{\times} #2}
- Adding more notations like
- |\notation{mult}[cdot]{#1 \comp{\cdot} #2}| or
- |\notation{mult}[times]{#1 \comp{\times} #2}|
- allows us to write |$\mult[cdot]{a}{b}$| and
- |$\mult[times]{a}{b}$|:
- \stexexample{
- \notation{mult}[cdot]{#1 \comp{\cdot} #2}
- \notation{mult}[times]{#1 \comp{\times} #2}
- $\mult[cdot]{a}{b}$ and $\mult[times]{a}{b}$
-}
- \notation{mult}[cdot]{#1 \comp{\cdot} #2}
- \notation{mult}[times]{#1 \comp{\times} #2}
-
- Not using an explicit option with a semantic macro yields
- the first declared notation, unless changed\ednote{TODO}.
-
- Outside of math mode, or by using the starred variant
- |\foo*|, allows to provide a custom notation, where
- notational (or textual) components can be given
- explicitly in square brackets.
- \stexexample{
- $\mult*{\arg{a}\comp{\ast}\arg{b}}$ is the
- \mult{\comp{product of} \arg{$a$} \comp{and} \arg{$b$}}
-}
-
- In custom mode, prefixing an argument with a star will not
- print that argument, but still export it to \omdoc:
- \stexexample{
- \mult{\comp{Multiplying} \arg*{$\mult{a}{b}$} again by \arg{$b$}} yields...
-}
- The syntax |*[|\meta{int}|]| allows switching
- the order of arguments. For example, given a 2-ary semantic
- macro |\forevery| with exemplary notation
- |\forall #1. #2|, we can write
- \stexexample{
- \symdecl{forevery}[args=2]
- \forevery{\arg[2]{The proposition $P$} \comp{holds for every} \arg[1]{$x\in A$}}
-}
-
- When using |*[|$n$|]|, after reading the provided ($n$th) argument,
- the ``argument counter'' automatically
- continues where we left off, so the |*[1]| in the above example
- can be omitted.
-
- For a macro with arity $>0$, we can refer to the operator
- \emph{itself} semantically by suffixing the semantic macro
- with an exclamation point |!| in either text or math mode.
- For that reason \cs{notation} (and thus \cs{symdef}) take an
- additional optional argument |op=|, which allows to assign
- a notation for the operator itself. e.g.
- \stexexample{
- \symdef{add}[args=2,op={+}]{#1 \comp+ #2}
- The operator $\add!$ adds two elements, as in $\add ab$.
- }
-
- |*| is composable with |!| for custom notations, as in:
-
- \stexexample{
- \mult!{\comp{Multiplication}} (denoted by $\mult!*{\comp\cdot}$) is defined by...
-}
-
- The macro \cs{comp} as used everywhere above is responsible
- for highlighting, linking, and tooltips, and should be wrapped
- around the notation (or text) components that should be treated
- accordingly. While it is attractive to just wrap a whole notation,
- this would also wrap around e.g. the arguments themselves, so
- instead, the user is tasked with marking the notation components
- themself.
-
- The precise behaviour of \cs{comp} is governed by
- the macro \cs{@comp}, which takes two arguments: The tex code
- of the text
- (unexpanded) to highlight, and the URI of the current symbol.
- \cs{@comp} can be safely redefined to customize the behaviour.
-
-
- The starred variant |\symdecl*{foo}| does not introduce a semantic
- macro, but still declares a corresponding symbol. |foo| (like
- any other symbol, for that matter) can
- then be accessed via \cs{STEXsymbol}|{foo}| or (if |foo| was declared
- in a module |Foo|) via \cs{STEXModule}|{Foo}?{foo}|.
-
- both \cs{STEXsymbol} and \cs{STEXModule} take any
- arbitrary ending segment of a full URI to determine
- which symbol or module is meant. e.g.
- \cs{STEXsymbol}|{Foo?foo}| is also valid, as are e.g.
- \cs{STEXModule}|{path?Foo}?{foo}| or
- \cs{STEXsymbol}|{path?Foo?foo}|
-
- There's also a convient shortcut \cs{symref}|{?foo}{some text}| for
- \cs{STEXsymbol}|{?foo}![some text]|.
-
- \end{smodule}
-
- \subsubsection{Other Argument Types}
-
- So far, we have stated the arity of a semantic macro directly.
- This works if we only have ``normal'' (or more precisely: |i|-type) arguments.
- To make use of other argument types, instead of providing the arity
- numerically, we can provide it as a sequence of characters representing
- the argument types -- e.g. instead of writing |args=2|, we
- can equivalently write |args=ii|, indicating that the macro
- takes two |i|-type arguments.
-
- Besides |i|-type arguments, \sTeX has two other types, which we will
- discuss now.
-
- The first are \emph{binding} (|b|-type) arguments, representing
- variables that are \emph{bound} by the operator. This is the
- case for example in the above \cs{forevery}-macro:
- The first argument is not actually an argument that the
- |forevery| ``function'' is ``applied'' to; rather, the first argument
- is a new variable (e.g. $x$) that is \emph{bound} in the subsequent
- argument. More accurately, the macro should therefore have been
- implemented thusly:
- \begin{center}|\symdef{forevery}[args=bi]{\forall #1.\; #2}|\end{center}
-
- \begin{smodule}{OtherArgs}
- |b|-type arguments are indistinguishable from |i|-type arguments
- within \sTeX, but are treated very differently in \omdoc and by \mmt.
- More interesting \emph{within} \sTeX are |a|-type arguments,
- which represent (associative) arguments of flexible arity, which are
- provided as comma-separated lists.
- This allows e.g. better representing the \cs{mult}-macro above:
-
- \stexexample{
- \symdef{mult}[args=a]{#1}{##1 \comp\cdot ##2}
- $\mult{a,b,c,{d^e},f}$
-}
- As the example above shows, notations get a little more complicated
- for associative arguments. For every |a|-type argument, the
- \cs{notation}-macro takes an additional argument that declares
- how individual entries in an |a|-type argument list are aggregated.
- The first notation argument then describes how the aggregated
- expression is combined into the full representation.
-
- For a more interesting example, consider a flexary operator
- for ordered sequences in ordered set, that taking
- arguments |{a,b,c}| and |\mathbb{R}| prints
- $a \leq b \leq c\in \mathbb R$. This operator takes
- two arguments (an |a|-type argument and an |i|-type argument),
- aggregates the individuals of the associative argument using |\leq|,
- and combines the result with |\in| and the second argument thusly:
-
- \stexexample{
- \symdef{numseq}[args=ai]{#1 \comp\in #2}{##1 \comp\leq ##2}
- $\numseq{a,b,c}{\mathbb R}$
-}
-
- Finally, |B|-type arguments combine the functionalities of |a|
- and |b|, i.e. they represent flexary binding operator arguments.
-
-\ednote{what about e.g. \detokenize{\int_x\int_y\int_z f dx dy dz}?}
-\ednote{``decompose'' a-type arguments into fixed-arity operators?}
-
- \end{smodule}
-
- \subsubsection{Precedences}
-
- Every notation has an (upwards) \emph{operator precedence} and
- for each argument a (downwards) \emph{argument precedence}
- used for automated bracketing. For example, a notation
- for a binary operator \cs{foo} could be declared like this:
- \begin{center} |\notation{foo}[prec=200;500x600]{#1 \comp{+} #2}| \end{center}
- assigning an operator precedence of 200, an argument precedence
- of 500 for the first argument, and an argument precedence of 600
- for the second argument.
-
- \sTeX insert brackets thusly: Upon encountering a semantic
- macro (such as \cs{foo}), its operator precedence (e.g. 200)
- is compared to the current downwards precedence (initially
- \cs{neginfprec}). If the operator precedence is \emph{larger}
- than the current downwards precedence, parentheses are inserted
- around the semantic macro.
-
- Notations for symbols of arity 0 have a default precedence of \cs{infprec},
- i.e. by default, parentheses are never inserted around constants.
- Notations for symbols with arity $>0$ have a default operator
- precedence of $0$.
- If no argument precedences are explicitly provided, then by
- default they are equal to the operator precedence.
-
- Consequently, if some operator $A$ should bind stronger than
- some operator $B$, then $A$s operator precedence should be
- smaller than $B$s argument precedences.
-
- For example:
- \begin{smodule}{NotationsEx}
- \symdecl{plus}[args=2]
- \symdecl{times}[args=2]
- \stexexample{
-\notation{plus}[prec=100]{#1 \comp{+} #2}
-\notation{times}[prec=50]{#1 \comp{\cdot} #2}
-$\plus{a}{\times{b}{c}}$ and $\times{a}{\plus{b}{c}}$
-}
-
-
- \end{smodule}
-
- \subsection{Archives and Imports}
-
- \subsubsection{Namespaces}
- Ideally, \sTeX would use arbitrary URIs for modules, with no
- forced relationships between the \emph{logical} namespace
- of a module and the \emph{physical} location of the file
- declaring the module -- like \mmt does things.
-
- Unfortunately, \TeX\ only provides very restricted access to
- the file system, so we are forced to generate namespaces
- systematically in such a way that they reflect the physical
- location of the associated files, so that \sTeX can resolve
- them accordingly. Largely, users need not concern themselves
- with namespaces at all, but for completenesses sake, we describe
- how they are constructed:
-
- \begin{itemize}
- \item If \cs{begin}|{module}{Foo}| occurs in a file
- |/path/to/file/Foo[.|\meta{lang}|].tex| which does not belong
- to an archive, the namespace is |file://path/to/file|.
- \item If the same statement occurs in a file
- |/path/to/file/bar[.|\meta{lang}|].tex|, the namespace is
- |file://path/to/file/bar|.
- \end{itemize}
-
- In other words: outside of archives, the namespace corresponds to
- the file URI with the filename dropped iff it is equal to the
- module name, and ignoring the (optional) language suffix^^A
- \footnote{which is internally attached to the module name instead,
- but a user need not worry about that.}.
-
- If the current file is in an archive, the procedure is the same
- except that the initial segment of the file path up to the archive's
- |source|-folder is replaced by the archive's namespace URI.
-
- \subsubsection{Paths in Import-Statements}
-
- Conversely, here is how namespaces/URIs and file paths are computed
- in import statements, examplary \cs{importmodule}:
-
- \begin{itemize}
- \item \cs{importmodule}|{Foo}| outside of an archive refers
- to module |Foo| in the current namespace. Consequently, |Foo|
- must have been declared earlier in the same document or, if not,
- in a file |Foo[.|\meta{lang}|].tex| in the same directory.
- \item The same statement \emph{within} an archive refers to either
- the module |Foo| declared earlier in the same document, or
- otherwise to the module |Foo| in the archive's top-level namespace.
- In the latter case, is has to be declared in a file |Foo[.|\meta{lang}|].tex|
- directly in the archive's |source|-folder.
- \item Similarly, in \cs{importmodule}|{some/path?Foo}| the path
- |some/path| refers to either the sub-directory and relative
- namespace path of the current directory and namespace outside of an archive,
- or relative to the current archive's top-level namespace and |source|-folder,
- respectively.
-
- The module |Foo| must either be declared in the file
- \meta{top-directory}|/some/path/Foo[.|\meta{lang}|].tex|, or in
- \meta{top-directory}|/some/path[.|\meta{lang}|].tex| (which are
- checked in that order).
- \item Similarly, \cs{importmodule}|[Some/Archive]{some/path?Foo}|
- is resolved like the previous cases, but relative to the archive
- |Some/Archive| in the mathhub-directory.
- \item Finally, \cs{importmodule}|{full://uri?Foo}| naturally refers to the
- module |Foo| in the namespace |full://uri|. Since the file this module
- is declared in can not be determined directly from the URI, the module
- must be in memory already, e.g. by being referenced earlier in the
- same document.
-
- Since this is less compatible with a modular development, using full
- URIs directly is discouraged.
-
- \end{itemize}
-
+\csname if@infulldoc\endcsname\else
+\newpage
+\printbibliography
+\end{document}
+\fi
-
-
-\csname if@infulldoc\endcsname\else\end{document}\fi
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: t
+%%% End:
+
+% LocalWords: stex-docheader infulldoctrue l@subsubsection toclevel@part ExplSyntaxOff
+% LocalWords: l_document_structure_section_level_int dangerbox mmtbox omdoc OBJref lmh
+% LocalWords: own:fifom MueRabRot:rslffml20 sec.stexarchives stex-mathhub ngerman a,b
+% LocalWords: Metatheory sec.customhighlight sproof stexthm xspace stexpatchmodule
+% LocalWords: stexpatchexample stexpatchparagraph sexampleid amsthm sassertiontitle
+% LocalWords: sdefinitiontitle compemph varemph srefsymuri stex-hwexam TeXLive:on tlmgr
+% LocalWords: stexls:on,stexls-vscode-plugin:on
diff --git a/Master/texmf-dist/doc/latex/stex/stex-tutorial.tex b/Master/texmf-dist/doc/latex/stex/stex-tutorial.tex
new file mode 100644
index 00000000000..dcd4c442e00
--- /dev/null
+++ b/Master/texmf-dist/doc/latex/stex/stex-tutorial.tex
@@ -0,0 +1,354 @@
+ \begin{sfragment}{A First \sTeX Document}
+ Having set everything up, we can write a first
+ \sTeX document. As an example, we will use the
+ |smglom/calculus| and |smglom/arithmetics| archives,
+ which should be present in the designated |MathHub|-folder,
+ and write a small fragment defining the \emph{geometric series}:
+
+ % \textcolor{red}{TODO: use some sTeX-archive instead of smglom,
+ % use a convergence-notion that includes the limit,
+ % mark-up the theorem properly}
+
+ \begin{framed}\begin{latexcode}[gobble=8]
+ \documentclass{article}
+ \usepackage{stex,xcolor,stexthm}
+
+ \begin{document}
+ \begin{smodule}{GeometricSeries}
+ \importmodule[smglom/calculus]{series}
+ \importmodule[smglom/arithmetics]{realarith}
+
+ \symdef{geometricSeries}[name=geometric-series]{\comp{S}}
+
+ \begin{sdefinition}[for=geometricSeries]
+ The \definame{geometricSeries} is the \symname{?series}
+ \[\defeq{\geometricSeries}{\definiens{
+ \infinitesum{\svar{n}}{1}{
+ \realdivide[frac]{1}{
+ \realpower{2}{\svar{n}}
+ }}
+ }}.\]
+ \end{sdefinition}
+
+ \begin{sassertion}[name=geometricSeriesConverges,type=theorem]
+ The \symname{geometricSeries} \symname{converges} towards $1$.
+ \end{sassertion}
+ \end{smodule}
+ \end{document}
+ \end{latexcode}\end{framed}
+
+ Compiling this document with |pdflatex| should yield
+ the output
+
+ \begin{mdframed}
+ \noindent\textbf{Definition 0.1. }\ The
+ \pdftooltip{\textcolor{blue}{\textbf{geometric series}}}{URI: file://your/file/name/here?GeometricSeries?geometric-series}
+ is the
+ \pdftooltip{\textcolor{blue}{series}}{URI: http://mathhub.info/smglom/calculus?series?series}
+ \[
+ \pdftooltip{\textcolor{blue}S}{URI: file://your/file/name/here?GeometricSeries?geometric-series}
+ \pdftooltip{\textcolor{blue}{:=}}{URI: http://mathhub.info/smglom/mv?defeq?definitional-equation}
+ \mathop{\pdftooltip{\textcolor{blue}{\sum}}{URI: http://mathhub.info/smglom/calculus?series?infinitesum}
+ }_{
+ \pdftooltip{\textcolor{gray}{n}}{Variable var://n}=1
+ }^{
+ \pdftooltip{\textcolor{blue}\infty}{URI: http://mathhub.info/smglom/calculus?series?infinitesum}
+ } \frac{1}{2^{\pdftooltip{\textcolor{gray}{n}}{Variable var://n}}}
+ .\]
+ \noindent\textbf{Theorem 0.2. }\ The
+ \pdftooltip{\textcolor{blue}{geometric series}}{URI: file://your/file/name/here?GeometricSeries?geometric-series}
+ \pdftooltip{\textcolor{blue}{converges}}{URI: http://mathhub.info/smglom/calculus?sequenceConvergence?converges} towards $1$.
+ \end{mdframed}
+
+ Move your cursor over the various highlighted parts of the document -- depending on
+ your pdf viewer, this should yield some interesting (but possibly for now cryptic)
+ information.
+
+ \begin{sparagraph}[type=remark]
+ Note that all of the highlighting, tooltips, coloring and the environment headers
+ come from \pkg{stexthm} -- by default, the amount of additional packages loaded
+ is kept to a minimum and all the presentations can be customized,
+ see \sref{sec.customhighlight}.
+ \end{sparagraph}
+
+ Let's investigate this document in detail to understand the respective parts of the
+ \sTeX markup infrastructure:\bigskip
+
+ \begin{environment}{smodule}
+ \begin{latexcode}[numbers=none,aboveskip=0pt,belowskip=0pt,gobble=8]
+ \begin{smodule}{GeometricSeries}
+ ...
+ \end{smodule}
+ \end{latexcode}
+ First, we open a new \emph{module} called |GeometricSeries|. The main purpose of
+ the |smodule| environment is to group the contents and associate it with a
+ \emph{globally unique} identifier (URI), which is computed from the name
+ |GeometricSeries| and the document context.
+
+ (Depending on your pdf viewer), the URI should pop up in a tooltip if you hover over
+ the word \pdftooltip{\textcolor{blue}{\textbf{geometric series}}}{URI:
+ file://your/file/name/here?GeometricSeries?geometric-series}.
+ \end{environment}\bigskip
+
+ \begin{function}{\importmodule}
+ \begin{latexcode}[numbers=none,aboveskip=0pt,belowskip=0pt,gobble=8]
+ \importmodule[smglom/calculus]{series}
+ \importmodule[smglom/arithmetics]{realarith}
+ \end{latexcode}
+ Next, we \emph{import} two modules -- |series| from the \sTeX archive
+ |smglom/calculus|, and |realarith| from the \sTeX archive |smglom/arithmetics|. If
+ we investigate these archives, we find the files |series.en.tex| and
+ |realarith.en.tex| (respectively) in their respective |source|-folders, which
+ contain the statements \stexcode"\begin{smodule}{series}" and
+ \stexcode"\begin{smodule}{realarith}" (respectively).
+ \iffalse\end{smodule}\end{smodule}\fi
+
+ The \stexcode"\importmodule"-statements make all \stex symbols and associated
+ semantic macros (e.g. \stexcode"\infinitesum", \stexcode"\realdivide",
+ \stexcode"\realpower") in the imported module available to the current module
+ |GeometricSeries|. The module |GeometricSeries| ``exports'' all of these symbols to
+ all modules imports it via an \stexcode"\importmodule{GeometricSeries}"
+ instruction. Additionally it exports the local symbol \stexcode"\geometricSeries".
+ \end{function}
+
+ \begin{function}{\usemodule}
+ If we only want to \emph{use} the content of some module |Foo|,
+ e.g. in remarks or examples, but none
+ of the symbols in our current module actually \emph{depend} on
+ the content of |Foo|, we can use \stexcode"\usemodule" instead -- like
+ \stexcode"\importmodule", this will make the module content available,
+ but will \emph{not} export it to other modules.
+ \end{function}\bigskip
+
+ \begin{function}{\symdef}
+ \begin{latexcode}[numbers=none,aboveskip=0pt,belowskip=0pt,gobble=6]
+ \symdef{GeometricSeries}[name=geometric-series]{\comp{S}}
+ \end{latexcode}
+ Next, we introduce a new \emph{symbol} with name
+ |geometric-series| and assign it the semantic macro
+ \stexcode"\geometricSeries".
+ \stexcode"\symdef" also immediately assigns this symbol a \emph{notation},
+ namely $S$.
+ \end{function}
+
+ \begin{function}{\comp}
+ The macro \stexcode"\comp" marks the $S$ in the notation as a
+ \emph{notational component}, as opposed to e.g. arguments
+ to \stexcode"\geometricSeries".
+ It is the notational components that get highlighted
+ and associated with the corresponding symbol (i.e. in this
+ case |geometricSeries|). Since \stexcode"\geometricSeries" takes
+ no arguments, we can wrap the whole notation in a \stexcode"\comp".
+ \end{function}\bigskip
+
+ \begin{latexcode}[numbers=none,aboveskip=0pt,belowskip=0pt,gobble=8]
+ \begin{sdefinition}[for=geometricSeries]
+ ...
+ \end{sdefinition}
+ \begin{sassertion}[name=geometricSeriesConverges,type=theorem]
+ ...
+ \end{sassertion}
+ \end{latexcode}
+ What follows are two \sTeX-\emph{statements} (e.g. definitions,
+ theorems, examples, proofs, ...). These are semantically marked-up
+ variants of the usual environments, which take additional optional
+ arguments (e.g. |for=|, |type=|, |name=|). Since many \LaTeX\xspace templates
+ predefine environments like |definition| or |theorem| with
+ different syntax, we use \stexcode"sdefinition",
+ \stexcode"sassertion", \stexcode"sexample"
+ etc. instead. You can customize these environments to e.g.
+ simply wrap around some predefined |theorem|-environment.
+ That way, we can still use \stexcode"sassertion" to provide semantic
+ information, while being fully compatible with (and using
+ the document presentation of) predefined environments.
+
+ In our case, the \pkg{stexthm}-package patches
+ e.g. \stexcode"\begin{sassertion}[type=theorem]" to use
+ a |theorem|-environment defined (as usual) using the \pkg{amsthm} package.
+ \bigskip \iffalse \end{sassertion}\fi
+
+ \begin{function}{\symname}
+ \begin{latexcode}[numbers=none,aboveskip=0pt,belowskip=0pt,gobble=6]
+ ... is the \symname{?series}
+ \end{latexcode}
+ The \stexcode"\symname"-command prints the name of a symbol,
+ highlights it (based on customizable settings)
+ and associates the text printed with the corresponding
+ symbol.
+
+ Note that the argument of \stexcode"\symref" can be
+ an imported symbol
+ (here the |series| symbol is imported from the |series| module). \sTeX tries to
+ determine the full symbol URI from the argument. If there are name clashes in or
+ with the imported symbols, the name of the exporting module can be prepended to the
+ symbol name before the |?| character.
+
+ If you hover over the word
+ \pdftooltip{\textcolor{blue}{series}}{URI: http://mathhub.info/smglom/calculus?series?series}
+ in the pdf output, you should see a tooltip showing the full URI
+ of the symbol used.
+ \end{function}
+ \begin{function}{\symref}
+ The \stexcode"\symname"-command is a special case of the more general
+ \stexcode"\symref"-command, which allows customizing the precise text associated
+ with a symbol. \stexcode"\symref" takes two arguments: the first ist the symbol
+ name (or macro name), and the second a variant verbalization of the symbol, e.g. an inflection
+ variant, a different language or a synonym. In our example
+ \stexcode"\symname{?series}" abbreviates \stexcode|\symref{?series}{series}|.
+
+ \end{function}
+ \begin{function}{\definame,\definiendum}
+ \begin{latexcode}[numbers=none,aboveskip=0pt,belowskip=0pt,gobble=6]
+ The \definame{geometricSeries} ...
+ \end{latexcode}
+ The \stexcode"sdefinition"-environment provides two additional
+ macros, \stexcode"\definame" and \stexcode"\definiendum" which behave
+ similarly to \stexcode"\symname" and \stexcode"\symref", but explicitly mark
+ the symbols as \emph{being defined} in this environment,
+ to allow for special highlighting.
+ \end{function}\bigskip
+
+ \begin{latexcode}[numbers=none,aboveskip=0pt,belowskip=0pt,gobble=8]
+ \[\defeq{\geometricSeries}{\definiens{
+ \infinitesum{\svar{n}}{1}{
+ \realdivide[frac]{1}{
+ \realpower{2}{\svar{n}}
+ }}
+ }}.\]
+ \end{latexcode}
+ The next snippet -- set in a math environment -- uses
+ several semantic macros imported from (or recursively via)
+ |series| and |realarithmetics|, such as \stexcode"\defeq",
+ \stexcode"\infinitesum",
+ etc. In math mode, using a semantic macro inserts its (default)
+ definition. A semantic macro can have several notations -- in
+ that case, we can explicitly choose a specific notation by
+ providing its identifier as an optional argument; e.g.
+ \stexcode"\realdivide[frac]{a}{b}" will use the explicit notation named |frac|
+ of the semantic macro \stexcode"\realdivide", which yields $\frac ab$
+ instead of $a/b$.
+ \begin{function}{\svar}
+ The \stexcode"\svar{n}" command marks up the |n| as a variable
+ with name |n| and notation |n|.
+ \end{function}
+ \begin{function}{\definiens}
+ The \stexcode"sdefinition"-environment additionally provides the
+ \stexcode"\definiens"-command, which allows for explicitly
+ marking up its argument as the \emph{definiens} of the
+ symbol currently being defined.
+ \end{function}
+
+ \begin{sfragment}{\omdoc/xhtml Conversion}
+ So, if we run |pdflatex| on our document, then \sTeX yields pretty colors and
+ tooltips\footnote{...and hyperlinks for symbols, and indices, and allows reusing
+ document fragments modularly, and...}. But \sTeX becomes a lot more powerful if
+ we additionally convert our document to |xhtml| while preserving all the \sTeX
+ markup in the result.
+
+ \textcolor{red}{TODO VSCode Plugin}
+
+ Using \rustex \cite{RusTeX:on}, we can convert the document to |xhtml|
+ using the command |rustex -i /path/to/file.tex -o /path/to/outfile.xhtml|.
+ Investigating the resulting file, we notice additional semantic
+ information resulting from our usage of semantic macros,
+ \stexcode"\symref" etc. Below is the (abbreviated) snippet inside
+ our \stexcode"\definiens" block:
+
+\begin{lstlisting}[escapechar=!,
+morekeywords={property,resource,stex:comp,stex:arg,stex:OMA,stex:OMV}]
+<mrow resource="" property="stex:definiens">
+ <mrow resource="...?series?infinitesum" property="stex:OMBIND">
+ <munderover displaystyle="true">
+ <mo resource="...?series?infinitesum" property="stex:comp">!$\Sigma$!</mo>
+ <mrow>
+ <mrow resource="1" property="stex:arg">
+ <mi resource="var://n" property="stex:OMV">n</mi>
+ </mrow>
+ <mo resource="...?series?infinitesum" property="stex:comp">=</mo>
+ <mi resource="2" property="stex:arg">1</mi>
+ </mrow>
+ <mi resource="...?series?infinitesum" property="stex:comp">!$\infty$!</mi>
+ </munderover>
+ <mrow resource="3" property="stex:arg">
+ <mfrac resource="...?realarith?division#frac#" property="stex:OMA">
+ <mi resource="1" property="stex:arg">1</mi>
+ <mrow resource="2" property="stex:arg">
+ <msup resource="...realarith?exponentiation" property="stex:OMA">
+ <mi resource="1" property="stex:arg">2</mi>
+ <mrow resource="2" property="stex:arg">
+ <mi resource="var://n" property="stex:OMV">n</mi>
+ </mrow>
+ </msup>
+ </mrow>
+ </mfrac>
+ </mrow>
+ </mrow>
+</mrow>
+ \end{lstlisting}
+ ...containing all the semantic information. The \mmt system
+ can extract from this the following \openmath snippet:
+
+ \begin{lstlisting}[escapechar=!]
+<OMBIND>
+ <OMID name="...?series?infinitesum"/>
+ <OMV name="n"/>
+ <OMLIT name="1"/>
+ <OMA>
+ <OMS name="...?realarith?division"/>
+ <OMLIT name="1"/>
+ <OMA>
+ <OMS name="...realarith?exponentiation"/>
+ <OMLIT name="2"/>
+ <OMV name="n"/>
+ </OMA>
+ </OMA>
+</OMBIND>
+ \end{lstlisting}
+ ...giving us the full semantics of the snippet, allowing for
+ a plurality of knowledge management services -- in particular
+ when serving the |xhtml|.
+
+ \begin{remark}
+ Note that the |html| when opened in a browser will
+ look slightly different than the |pdf| when it comes
+ to highlighting semantic content -- that is because
+ naturally |html| allows for much more powerful
+ features than |pdf| does. Consequently, the |html|
+ is intended to be served by a system like \mmt,
+ which can pick up on the semantic information and
+ offer much more powerful highlighting, linking
+ and similar features, and being customizable by
+ \emph{readers} rather than being prescribed by an author.
+
+ Additionally, not all browsers (most notably Chrome)
+ support \mathml natively, and might require
+ additional external JavaScript libraries such as
+ MathJax to render mathematical formulas properly.
+ \end{remark}
+ \end{sfragment}
+
+
+ \begin{sfragment}{\mmt/\omdoc Conversion}
+ Another way to convert our document to \emph{actual}
+ \mmt/\omdoc is to put it in an \sTeX \textbf{archive}
+ (see \sref{sec.stexarchives}) and have \mmt take care of
+ everything.
+
+ Assuming the above file is |source/demo.tex| in
+ an \sTeX archive |MyTest|, you can run \mmt and
+ do
+ |build MyTest stex-omdoc demo.tex| to convert the
+ document to both |xhtml| (which you will find in
+ |xhtml/demo.xhtml| in the archive) and formal
+ \mmt/\omdoc, which you can subsequently view in
+ the \mmt browser (see \url{https://uniformal.github.io//doc/applications/server.html#the-mmt-web-site}
+ for details).
+ \end{sfragment}
+\end{sfragment}
+
+%%% Local Variables:
+%%% mode: latex
+%%% TeX-master: "stex-manual"
+%%% End:
+
+% LocalWords: coloring sec.customhighlight realarith infinitesum realarithmetics