summaryrefslogtreecommitdiff
path: root/doc
diff options
context:
space:
mode:
authorGravatar Adam Chlipala <adam@chlipala.net>2010-12-16 10:23:37 -0500
committerGravatar Adam Chlipala <adam@chlipala.net>2010-12-16 10:23:37 -0500
commitb064753122a284177a8ac0bad7b0f75bc300eb39 (patch)
tree959c7f1d847fcdd654f99f5b2ca61406455aba89 /doc
parent6219b399b733fd772fbcc25bd52c4f7e50060728 (diff)
Clarify that you aren't supposed to be able to create new XML tags
Diffstat (limited to 'doc')
-rw-r--r--doc/manual.tex2
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/manual.tex b/doc/manual.tex
index 2509439a..03219a4e 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -1863,7 +1863,7 @@ $$\begin{array}{l}
\hspace{.1in} \Rightarrow \mt{xml} \; \mt{ctx} \; \mt{use_1} \; \mt{bind} \to \mt{xml} \; \mt{ctx} \; (\mt{use_1} \rc \mt{use_2}) \; \mt{bind}
\end{array}$$
-We will not list here the different HTML tags and related functions from the standard library. They should be easy enough to understand from the code in \texttt{basis.urs}. The set of tags in the library is not yet claimed to be complete for HTML standards.
+We will not list here the different HTML tags and related functions from the standard library. They should be easy enough to understand from the code in \texttt{basis.urs}. The set of tags in the library is not yet claimed to be complete for HTML standards. Also note that there is currently no way for the programmer to add his own tags. It \emph{is} possible to add new tags directly to \texttt{basis.urs}, but this should only be done as a prelude to suggesting a patch to the main distribution.
One last useful function is for aborting any page generation, returning some XML as an error message. This function takes the place of some uses of a general exception mechanism.
$$\begin{array}{l}