equal
deleted
inserted
replaced
13 3.3, instead of 3.1. This is the "-old-syntax" variant (Java-like) as |
13 3.3, instead of 3.1. This is the "-old-syntax" variant (Java-like) as |
14 before, not "-new-syntax" (Python-like). Minor INCOMPATIBILITY. |
14 before, not "-new-syntax" (Python-like). Minor INCOMPATIBILITY. |
15 |
15 |
16 |
16 |
17 *** ML *** |
17 *** ML *** |
|
18 |
|
19 * ML antiquotation "try" provides variants of exception handling that |
|
20 avoids accidental capture of physical interrupts (which could affect ML |
|
21 semantics in unpredictable ways): |
|
22 |
|
23 \<^try>\<open>EXPR catch HANDLER\<close> |
|
24 \<^try>\<open>EXPR finally HANDLER\<close> |
|
25 \<^try>\<open>EXPR\<close> |
|
26 |
|
27 See also the implementations Isabelle_Thread.try_catch / try_finally / |
|
28 try. The HANDLER always runs as uninterruptible, but the EXPR uses the |
|
29 the current thread attributes (normally interruptible). Various examples |
|
30 occur in the Isabelle sources (.ML and .thy files). |
18 |
31 |
19 * Isabelle/ML explicitly rejects 'handle' with catch-all patterns. |
32 * Isabelle/ML explicitly rejects 'handle' with catch-all patterns. |
20 INCOMPATIBILITY, better use \<^try>\<open>...\<close> with 'catch' or 'finally', or |
33 INCOMPATIBILITY, better use \<^try>\<open>...\<close> with 'catch' or 'finally', or |
21 as last resort declare [[ML_catch_all]] within the theory context. |
34 as last resort declare [[ML_catch_all]] within the theory context. |
22 |
35 |