fix throwref execution semantics

document/core/exec/instructions.rst

@@ -2757,75 +2757,75 @@ Control Instructions
 :math:`\THROWREF`
 .................
 
-1. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
-
-2. Assert: due to :ref:`validation <valid-throw_ref>`, a :ref:`reference <syntax-ref>` is on the top of the stack.
+1. Assert: due to :ref:`validation <valid-throw_ref>`, a :ref:`reference <syntax-ref>` is on the top of the stack.
 
-3. Pop the reference :math:`\reff` from the stack.
+2. Pop the reference :math:`\reff` from the stack.
 
-4. If :math:`\reff` is :math:`\REFNULL~\X{ht}`, then:
+3. If :math:`\reff` is :math:`\REFNULL~\X{ht}`, then:
 
    a. Trap.
 
-5. Assert: due to :ref:`validation <valid-throw_ref>`, :math:`\reff` is an :ref:`exception reference <syntax-ref.exn-addr>`.
+4. Assert: due to :ref:`validation <valid-throw_ref>`, :math:`\reff` is an :ref:`exception reference <syntax-ref.exn-addr>`.
 
-6. Let :math:`\REFEXNADDR~\X{ea}` be :math:`\reff`.
+5. Let :math:`\REFEXNADDR~\X{ea}` be :math:`\reff`.
 
-7. Assert: due to :ref:`validation <valid-throw_ref>`, :math:`S.\SEXNS[\X{ea}]` exists.
+6. Assert: due to :ref:`validation <valid-throw_ref>`, :math:`S.\SEXNS[\X{ea}]` exists.
 
-8. Let :math:`\X{exn}` be the :ref:`exception instance <syntax-exninst>` :math:`S.\SEXNS[\X{ea}]`.
+7. Let :math:`\X{exn}` be the :ref:`exception instance <syntax-exninst>` :math:`S.\SEXNS[\X{ea}]`.
 
-9. Let :math:`a` be the :ref:`tag address <syntax-tagaddr>` :math:`\X{exn}.\EITAG`.
+8. Let :math:`a` be the :ref:`tag address <syntax-tagaddr>` :math:`\X{exn}.\EITAG`.
 
-10. While the stack is not empty and the top of the stack is not an :ref:`exception handler <syntax-handler>`, do:
+9. While the stack is not empty and the top of the stack is not an :ref:`exception handler <syntax-handler>`, do:
 
    a. Pop the top element from the stack.
 
-11. Assert: the stack is now either empty, or there is an exception handler on the top of the stack.
+10. Assert: the stack is now either empty, or there is an exception handler on the top of the stack.
 
-12. If the stack is empty, then:
+11. If the stack is empty, then:
 
    a. Return the exception :math:`(\REFEXNADDR~a)` as a :ref:`result <syntax-result>`.
 
-13. Assert: there is an :ref:`exception handler <syntax-handler>` on the top of the stack.
+12. Assert: there is an :ref:`exception handler <syntax-handler>` on the top of the stack.
 
-14. Pop the exception handler  :math:`\HANDLER_n\{\catch^\ast\}` from the stack.
+13. Pop the exception handler  :math:`\HANDLER_n\{\catch^\ast\}` from the stack.
 
-15. If :math:`\catch^\ast` is empty, then:
+14. If :math:`\catch^\ast` is empty, then:
 
     a. Push the exception reference :math:`\REFEXNADDR~\X{ea}` back to the stack.
 
     b. Execute the instruction |THROWREF| again.
 
-16. Else:
+15. Else:
+
+    a. Let :math:`F` be the :ref:`current <exec-notation-textual>` :ref:`frame <syntax-frame>`.
 
-    a. Let :math:`\catch_1` be the first :ref:`catch clause <syntax-catch>` in :math:`\catch^\ast` and :math:`{\catch'}^\ast` the remaining clauses.
+    b. Let :math:`\catch_1` be the first :ref:`catch clause <syntax-catch>` in :math:`\catch^\ast` and :math:`{\catch'}^\ast` the remaining clauses.
 
-    b. If :math:`\catch_1` is of the form :math:`\CATCH~x~l` and the :ref:`tag address <syntax-tagaddr>` :math:`a` equals :math:`F.\AMODULE.\MITAGS[x]`, then:
+    c. If :math:`\catch_1` is of the form :math:`\CATCH~x~l` and the :ref:`tag address <syntax-tagaddr>` :math:`a` equals :math:`F.\AMODULE.\MITAGS[x]`, then:
 
        i. Push the values :math:`\X{exn}.\EIFIELDS` to the stack.
 
        ii. Execute the instruction :math:`\BR~l`.
 
-    c. Else if :math:`\catch_1` is of the form :math:`\CATCHREF~x~l` and the :ref:`tag address <syntax-tagaddr>` :math:`a` equals :math:`F.\AMODULE.\MITAGS[x]`, then:
+    d. Else if :math:`\catch_1` is of the form :math:`\CATCHREF~x~l` and the :ref:`tag address <syntax-tagaddr>` :math:`a` equals :math:`F.\AMODULE.\MITAGS[x]`, then:
 
        i. Push the values :math:`\X{exn}.\EIFIELDS` to the stack.
 
        ii. Push the exception reference :math:`\REFEXNADDR~\X{ea}` to the stack.
 
        iii. Execute the instruction :math:`\BR~l`.
 
-    d. Else if :math:`\catch_1` is of the form :math:`\CATCHALL~l`, then:
+    e. Else if :math:`\catch_1` is of the form :math:`\CATCHALL~l`, then:
 
        i. Execute the instruction :math:`\BR~l`.
 
-    e. Else if :math:`\catch_1` is of the form :math:`\CATCHALLREF~l`, then:
+    f. Else if :math:`\catch_1` is of the form :math:`\CATCHALLREF~l`, then:
 
        i. Push the exception reference :math:`\REFEXNADDR~\X{ea}` to the stack.
 
        ii. Execute the instruction :math:`\BR~l`.
 
-    f. Else:
+    g. Else:
 
        1. Push the modified handler  :math:`\HANDLER_n\{{\catch'}^\ast\}` back to the stack.