equal
deleted
inserted
replaced
21 |
21 |
22 text {* |
22 text {* |
23 |
23 |
24 Now the call |
24 Now the call |
25 |
25 |
26 @{ML_response_fake [display] "ackermann (4, 12)" "\<dots>"} |
26 @{ML_response_fake [display,gray] "ackermann (4, 12)" "\<dots>"} |
27 |
27 |
28 takes a bit of time before it finishes. To avoid this, the call can be encapsulated |
28 takes a bit of time before it finishes. To avoid this, the call can be encapsulated |
29 in a time limit of five seconds. For this you have to write: |
29 in a time limit of five seconds. For this you have to write: |
30 |
30 |
31 @{ML_response [display] |
31 @{ML_response [display,gray] |
32 "TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) |
32 "TimeLimit.timeLimit (Time.fromSeconds 5) ackermann (4, 12) |
33 handle TimeOut => ~1" |
33 handle TimeOut => ~1" |
34 "~1"} |
34 "~1"} |
35 |
35 |
36 where @{ML_text TimeOut} is the exception raised when the time limit |
36 where @{ML_text TimeOut} is the exception raised when the time limit |