Small fixes on formal spec overview/examples

- Removes a link next to `[1]`. The link is also in the footnote so it's
  not strictly necessary, and adding a link right next to `[1]` makes
  `[]` disappear, so it appears as just `1`, which isn't probably what
  the author intended.
- Both of `throw/catch x` and `throw/catch $x` are being used. Unified
  them into `throw/catch $x`.
- Fixed a location of `$label2` in a test.

Author: aheejin

proposals/exception-handling/Exceptions-formal-examples.md

@@ -20,7 +20,7 @@ Note that the block contexts and throw contexts given for the reductions are the
 
 The only example with an almost full reduction trace, and all new instructions. Such explicit reduction steps are only shown in Example 4 and Example 5, to highlight the reduction step of the administrative `delegate`.
 
-In the following reduction, we don't show the first 4 steps, which just reduce the several `try`s and the `throw x` to their respective administrative instructions. The type of the tag `$x` here is `[]→[]`.
+In the following reduction, we don't show the first 4 steps, which just reduce the several `try`s and the `throw $x` to their respective administrative instructions. The type of the tag `$x` here is `[]→[]`.
 
 ```
 (tag $x)
@@ -153,11 +153,11 @@ Use the trivial throw context `T` again, this time to match the throw to the `ca
 Location of a rethrown exception. Let `x, y, z` be tag indices of tags with type `[t_x]→[]`, `[t_y]→[]`, and `[t_z]→[]` respectively. Let `val_p : t_p` for every `p` among `x, y, z`.
 
 ```
-try
+try $label2
   val_x
-  throw x
-catch x
-  try $label2
+  throw $x
+catch $x
+  try
     val_y
     throw y
   catch_all
@@ -177,8 +177,8 @@ Folded it looks as follows.
 (try
   (do
     val_x
-    (throw x))
-  (catch x  ;; <--- (rethrow 2) targets this catch.
+    (throw $x))
+  (catch $x  ;; <--- (rethrow 2) targets this catch.
     (try
       (do
         val_y
@@ -222,7 +222,7 @@ This reduces to `val_x (throw a_x)`, throwing to the caller.
 (func
   try $label0
     rethrow $label0 ;; cannot be done, because it's not within catch below
-  catch x
+  catch $x
   end)
 ```
 
@@ -237,7 +237,7 @@ This is a validation error (no catch block at given rethrow depth).
 ```
 (try $l
   (do
-    (throw x))
+    (throw $x))
   (delegate $l))
 ```
 
@@ -252,17 +252,17 @@ try $label1
   try
     try $label0
       try
-        throw x
+        throw $x
       delegate $label0 ;; delegate 0
     delegate $label1 ;; delegate 1
   catch_all
   end
-catch x
+catch $x
   instr*
 end
 ```
 
-In folded form and reduced to the point `throw x` is called, this is:
+In folded form and reduced to the point `throw $x` is called, this is:
 
 ```
 (label_0{}
@@ -295,7 +295,7 @@ The `delegate{ 1 }` reduces using the trivial throw context and the block contex
   (catch_0{ a_x instr* }
     (throw a_x) end) end)
 ```
-The thrown exception is (eventually) caught by the outer try's `catch x`, so the above reduces to the following.
+The thrown exception is (eventually) caught by the outer try's `catch $x`, so the above reduces to the following.
 
 ```
 (label_0 {}
@@ -310,7 +310,7 @@ The thrown exception is (eventually) caught by the outer try's `catch x`, so the
 ```
 try (result i32)
   try $label0
-    throw x
+    throw $x
   catch_all
     try
       throw y
@@ -328,7 +328,7 @@ In folded form this is:
   (do
     (try
       (do
-        (throw x))
+        (throw $x))
       (catch_all
         (try
           (do

proposals/exception-handling/Exceptions-formal-overview.md

@@ -185,7 +185,7 @@ label_m{} B^l[ delegate{l} T[val^n (throw a)] end ] end
   ↪ val^n (throw a)
 ```
 
-Note that the last reduction step above is similar to the reduction of `br l` [1](https://webassembly.github.io/spec/core/exec/instructions.html#xref-syntax-instructions-syntax-instr-control-mathsf-br-l), if we look at the entire `delegate{l}...end` as the `br l`, but also doing a throw after it breaks.
+Note that the last reduction step above is similar to the reduction of `br l` [1], if we look at the entire `delegate{l}...end` as the `br l`, but also doing a throw after it breaks.
 
 There is a subtle difference though. The instruction `br l` searches for the `l+1`th surrounding block and breaks out after that block. Because `delegate{l}` is always wrapped in its own `label_n{} ... end` [2], with the same lookup as for `br l` we end up breaking inside the `l+1`th surrounding block, and throwing there. So if that `l+1`th surrounding block is a try, we end up throwing in its "try code", and thus correctly getting delegated to that try's catches.