25 @{ML_response_fake [display,gray] "ackermann (4, 12)" "\<dots>"} |
25 @{ML_response_fake [display,gray] "ackermann (4, 12)" "\<dots>"} |
26 |
26 |
27 takes a bit of time before it finishes. To avoid this, the call can be encapsulated |
27 takes a bit of time before it finishes. To avoid this, the call can be encapsulated |
28 in a time limit of five seconds. For this you have to write |
28 in a time limit of five seconds. For this you have to write |
29 |
29 |
30 @{ML_response [display,gray] |
30 @{ML_response_fake_both [display,gray] |
31 "TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) |
31 "TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) |
32 handle TimeLimit.TimeOut => ~1" |
32 handle TimeLimit.TimeOut => ~1" |
33 "~1"} |
33 "~1"} |
34 |
34 |
35 where @{text TimeOut} is the exception raised when the time limit |
35 where @{text TimeOut} is the exception raised when the time limit |
36 is reached. |
36 is reached. |
37 |
37 |
38 Note that @{ML "timeLimit" in TimeLimit} is only meaningful when you use PolyML, |
38 Note that @{ML "timeLimit" in TimeLimit} is only meaningful when you use PolyML 5.2.1 |
39 because PolyML has the infrastructure for multithreaded programming on |
39 or later, because this version of PolyML has the infrastructure for multithreaded |
40 which @{ML "timeLimit" in TimeLimit} relies. |
40 programming on which @{ML "timeLimit" in TimeLimit} relies. |
41 |
41 |
42 \begin{readmore} |
42 \begin{readmore} |
43 The function @{ML "timeLimit" in TimeLimit} is defined in the structure |
43 The function @{ML "timeLimit" in TimeLimit} is defined in the structure |
44 @{ML_struct TimeLimit} which can be found in the file |
44 @{ML_struct TimeLimit} which can be found in the file |
45 @{ML_file "Pure/ML-Systems/multithreading_polyml.ML"}. |
45 @{ML_file "Pure/ML-Systems/multithreading_polyml.ML"}. |