From c6e641ffb3195827acbb2787bb202824fef0cfa6 Mon Sep 17 00:00:00 2001
From: Adam Chlipala <adam@chlipala.net>
Date: Mon, 9 Dec 2013 15:47:14 -0500
Subject: Rename <activeHead> to <script> and make it work properly

---
 doc/manual.tex | 8 ++++++++
 1 file changed, 8 insertions(+)

(limited to 'doc')
diff --git a/doc/manual.tex b/doc/manual.tex
index ac12c3b7..db1bfe1c 100644
--- a/doc/manual.tex
+++ b/doc/manual.tex
@@ -2103,6 +2103,14 @@ $$\begin{array}{l}
   \mt{val} \; \mt{stopPropagation} : \mt{transaction} \; \mt{unit}
 \end{array}$$
 
+Finally, here is an HTML tag to leave a marker in the \cd{<head>} of a document asking for some side-effecting code to be run.  This pattern is \emph{much} less common in Ur/Web applications than in normal HTML/JavaScript applications; see Section \ref{signals} for the more idiomatic, functional way of manipulating the visible page.
+
+$$\begin{array}{l}
+  \mt{val} \; \mt{script} : \mt{unit} \to \mt{tag} \; [\mt{Code} = \mt{transaction} \; \mt{unit}] \; \mt{head} \; [] \; [] \; []
+\end{array}$$
+
+Note that the Ur/Web version of \cd{<script>} is used like \cd{<script code=\{...\}/>}, rather than \cd{<script>...</script>}.
+
 \subsubsection{Node IDs}
 
 There is an abstract type of node IDs that may be assigned to \cd{id} attributes of most HTML tags.
-- 
cgit v1.2.3

