equal
deleted
inserted
replaced
19 |
19 |
20 text \<open> |
20 text \<open> |
21 |
21 |
22 Now the call |
22 Now the call |
23 |
23 |
24 @{ML_response_fake_both [display,gray] "ackermann (4, 12)" "\<dots>"} |
24 @{ML_matchresult_fake_both [display,gray] "ackermann (4, 12)" "\<dots>"} |
25 |
25 |
26 takes a bit of time before it finishes. To avoid this, the call can be encapsulated |
26 takes a bit of time before it finishes. To avoid this, the call can be encapsulated |
27 in a time limit of five seconds. For this you have to write |
27 in a time limit of five seconds. For this you have to write |
28 |
28 |
29 @{ML_response_fake_both [display,gray] |
29 @{ML_matchresult_fake_both [display,gray] |
30 "Timeout.apply (Time.fromSeconds 5) ackermann (4, 12) |
30 "Timeout.apply (Time.fromSeconds 5) ackermann (4, 12) |
31 handle TIMEOUT => ~1" |
31 handle TIMEOUT => ~1" |
32 "~1"} |
32 "~1"} |
33 |
33 |
34 where \<open>TimeOut\<close> is the exception raised when the time limit |
34 where \<open>TimeOut\<close> is the exception raised when the time limit |
38 or later, because this version of PolyML has the infrastructure for multithreaded |
38 or later, because this version of PolyML has the infrastructure for multithreaded |
39 programming on which @{ML "apply" in Timeout} relies. |
39 programming on which @{ML "apply" in Timeout} relies. |
40 |
40 |
41 \begin{readmore} |
41 \begin{readmore} |
42 The function @{ML "apply" in Timeout} is defined in the structure |
42 The function @{ML "apply" in Timeout} is defined in the structure |
43 @{ML_struct Timeout} which can be found in the file |
43 @{ML_structure Timeout} which can be found in the file |
44 @{ML_file "Pure/concurrent/timeout.ML"}. |
44 @{ML_file "Pure/concurrent/timeout.ML"}. |
45 \end{readmore} |
45 \end{readmore} |
46 |
46 |
47 |
47 |
48 \<close> |
48 \<close> |