Add exceptional return to func_invoke in embedding doc

document/core/Makefile

@@ -136,13 +136,13 @@ singlehtml:
 bikeshed:
 	$(SPHINXBUILD) -b singlehtml -c util/bikeshed \
 		$(ALLSPHINXOPTS) $(BUILDDIR)/bikeshed_singlehtml
-	python util/bikeshed_fixup.py $(BUILDDIR)/bikeshed_singlehtml/index.html \
+	python3 util/bikeshed_fixup.py $(BUILDDIR)/bikeshed_singlehtml/index.html \
 		>$(BUILDDIR)/bikeshed_singlehtml/index_fixed.html
 	mkdir -p $(BUILDDIR)/bikeshed_mathjax/
 	bikeshed spec index.bs $(BUILDDIR)/bikeshed_mathjax/index.html
 	mkdir -p $(BUILDDIR)/html/bikeshed/
 	(cd util/katex/ && yarn && yarn build && npm install --only=prod)
-	python util/mathjax2katex.py $(BUILDDIR)/bikeshed_mathjax/index.html \
+	python3 util/mathjax2katex.py $(BUILDDIR)/bikeshed_mathjax/index.html \
 		>$(BUILDDIR)/html/bikeshed/index.html
 	mkdir -p $(BUILDDIR)/html/bikeshed/katex/dist/
 	cp -r util/katex/dist/* $(BUILDDIR)/html/bikeshed/katex/dist/

document/core/appendix/embedding.rst

@@ -26,8 +26,17 @@ For numeric parameters, notation like :math:`n:\u32` is used to specify a symbol
 
 .. _embed-error:
 
-Errors
-~~~~~~
+Exceptions and Errors
+~~~~~~~~~~~~~~~~~~~~~
+
+Invoke operations may throw or propagate exceptions, indicated by an auxiliary syntactic class:
+
+.. math::
+   \begin{array}{llll}
+   \production{exception} & \exception &::=& \ETHROW ~ \tagaddr ~ val^\ast \\
+   \end{array}
+
+The tag instance :math:`tagaddr` identifies the :ref:`type <syntax-tagtype>` of exception thrown. The values :math:`val^\ast` are the exception's payload; their types match the tag type's parameters.
 
 Failure of an interface operation is indicated by an auxiliary syntactic class:
 
@@ -43,6 +52,8 @@ In addition to the error conditions specified explicitly in this section, implem
    Implementations can refine it to carry suitable classifications and diagnostic messages.
 
 
+
+
 Pre- and Post-Conditions
 ~~~~~~~~~~~~~~~~~~~~~~~~
 
@@ -293,21 +304,24 @@ Functions
 .. index:: invocation, value, result
 .. _embed-func-invoke:
 
-:math:`\F{func\_invoke}(\store, \funcaddr, \val^\ast) : (\store, \val^\ast ~|~ \error)`
-........................................................................................
+:math:`\F{func\_invoke}(\store, \funcaddr, \val^\ast) : (\store, \val^\ast ~|~ \exception ~|~ \error)`
+......................................................................................................
 
 1. Try :ref:`invoking <exec-invocation>` the function :math:`\funcaddr` in :math:`\store` with :ref:`values <syntax-val>` :math:`\val^\ast` as arguments:
 
   a. If it succeeds with :ref:`values <syntax-val>` :math:`{\val'}^\ast` as results, then let :math:`\X{result}` be :math:`{\val'}^\ast`.
 
-  b. Else it has trapped, hence let :math:`\X{result}` be :math:`\ERROR`.
+  b. Else if the outcome is an exception with :ref:`tag <syntax-tagaddr>` :math:`\tagaddr` and payload :ref:`values <syntax-val>` :math:`{\val'}^\ast`,  let :math:`\X{result}` be :math:`\ETHROW~\tagaddr~{\val'}^\ast`.
+
+  c. Else it has trapped, hence let :math:`\X{result}` be :math:`\ERROR`.
 
 2. Return the new store paired with :math:`\X{result}`.
 
 .. math::
    ~ \\
    \begin{array}{lclll}
    \F{func\_invoke}(S, a, v^\ast) &=& (S', {v'}^\ast) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; {v'}^\ast) \\
+   \F{func\_invoke}(S, a, v^\ast) &=& (S', \ETHROW~a'~{v'}^\ast) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \XT[(\THROWadm~a')]) \\
    \F{func\_invoke}(S, a, v^\ast) &=& (S', \ERROR) && (\iff \invoke(S, a, v^\ast) \stepto^\ast S'; F; \TRAP) \\
    \end{array}
 

document/core/util/macros.def

@@ -1323,3 +1323,5 @@
 
 .. |error| mathdef:: \xref{appendix/embedding}{embed-error}{\X{error}}
 .. |ERROR| mathdef:: \xref{appendix/embedding}{embed-error}{\K{error}}
+.. |exception| mathdef:: \xref{appendix/embedding}{embed-error}{\X{exception}}
+.. |ETHROW| mathdef:: \xref{appendix/embedding}{embed-error}{\K{THROW}}