Update formal spec to (partially) implement the 3rd EH proposal

document/core/exec/runtime.rst

@@ -683,7 +683,7 @@ In order to be able to break jumping over exception handlers and caught exceptio
 
 .. math::
    \begin{array}{llll}
-   \production{(block contexts)} & \XC^{k} &::=& \handler~\XB^k~\END \\
+   \production{(control contexts)} & \XC^{k} &::=& \handler~\XB^k~\END \\
    & & | & \CAUGHTadm~\{\tagaddr~\val^\ast\}~\XB^k~\END \\
    \production{(block contexts)} & \XB^0 &::=& \dots ~|~  \val^\ast~\XC^0~\instr^\ast\\
    \production{(block contexts)} & \XB^{k+1} &::=& \dots ~|~ \val^\ast~\XC^{k+1}~\instr^\ast \\
@@ -726,7 +726,8 @@ Throw contexts allow matching the program context around a throw instruction up
    Contrary to block contexts, throw contexts don't skip over handlers.
 
    Since handlers are not included above, there is always a unique maximal throw context to match the reduction rules.
-   This basically means that :math:`\CAUGHTadm {\dots} instr^\ast \END` is not a potential catching block for exceptions thrown by :math:`\instr^\ast`, since these are instructions in the scope of a |CATCH| or a |CATCHALL|.
+
+   |CAUGHTadm| blocks do not represent active handlers. Instead, they delimit the continuation of a handler that has already been selected. Their sole purpose is to record the exception that has been caught, such that |RETHROW| can access it inside such a block.
 
 .. note::
    For example, catching a simple :ref:`throw <exec-throw>` in a :ref:`try block <exec-try-catch>` would be as follows.
@@ -750,10 +751,12 @@ Throw contexts allow matching the program context around a throw instruction up
       \stepto & \val^m & \\
       \end{array}
 
-   When a throw occurs, we pop the values :math:`val^m:[t^m]` and append them to the tag address :math:`a` into
-   a |CAUGHTadm| instruction. We then search for the maximal surrounding throw context `T`, which means we pop
-   any other values, labels, frames, and |CAUGHTadm| instructions, until we find an exception handler
-   (corresponding to a try block) that :ref:`handles the exception <syntax-handler>`.
+
+
+   When a throw of the form :math:`val^m (throw a)` occurs, we search for the maximal surrounding throw context :math:`T`,
+   which means we pop any other values, labels, frames, and |CAUGHTadm| instructions surrounding the throw :math:`val^m (throw a)`,
+   until we find an exception handler (corresponding to a try block) that :ref:`handles the exception <syntax-handler>`.
+   We then append the values :math:`val^m:[t^m]` to the tag address :math:`a` into a new |CAUGHTadm| instruction which we push on the stack.
 
    In other words, when a throw occurs, normal execution halts and exceptional execution begins, until the throw
    is the continuation (i.e., in the place of a :math:`\_`) of a throw context in a catching try block.

document/core/text/instructions.rst

@@ -941,8 +941,8 @@ Such a folded instruction can appear anywhere a regular instruction can.
        \quad\equiv \\ &\qquad
          \text{try}~~\Tlabel~~\Tblocktype~~\Tinstr_1^\ast
        &\hspace{-5ex} (\text{catch}~~x{:}\Ttagidx_I~~\Tinstr_2^\ast)^\ast~~(\text{catch\_all}~~\Tinstr_3^\ast)^?~~\text{end} \\ &
-      \text{(}~\text{try}~~\Tlabel~~\Tblocktype
-       &\hspace{-15ex} \text{(}~\text{delegate}~~l{:}\Tlabelidx~~\Tinstr^\ast~~\text{)}~\text{)}
+     \text{(}~\text{try}~~\Tlabel~~\Tblocktype~~\text{(}~\text{do} &\hspace{-8ex} \Tinstr^\ast~\text{)}~~
+       \text{(}~\text{delegate}~~l{:}\Tlabelidx~~\text{)}~\text{)}
        \quad\equiv \\ &\qquad
          \text{try}~~\Tlabel~~\Tblocktype~~\Tinstr^\ast &\hspace{-5ex} \text{delegate}~~l{:}\Tlabelidx \\
    \end{array}

document/core/util/macros.def

@@ -909,11 +909,11 @@
 .. |CLABELS| mathdef:: \xref{valid/conventions}{context}{\K{labels}}
 .. |CRETURN| mathdef:: \xref{valid/conventions}{context}{\K{return}}
 .. |CREFS| mathdef:: \xref{valid/conventions}{context}{\K{refs}}
-.. |LCATCH| mathdef:: \xref{valid/conventions}{valid-labeltype}{\mathrel{\K{catch}}}
+.. |LCATCH| mathdef:: \xref{valid/conventions}{context}{\mathrel{\K{catch}}}
 
 .. Contexts, non-terminals
 
-.. |labeltype| mathdef:: \xref{valid/conventions}{valid-labeltype}{\mathrel{\X{labeltype}}}
+.. |labeltype| mathdef:: \xref{valid/conventions}{context}{\mathrel{\X{labeltype}}}
 
 
 .. Judgments