equal
deleted
inserted
replaced
31 @{ML_response [display,gray] |
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 TimeLimit.TimeOut => ~1" |
33 handle TimeLimit.TimeOut => ~1" |
34 "~1"} |
34 "~1"} |
35 |
35 |
36 where @{ML_text TimeOut} is the exception raised when the time limit |
36 where @{text TimeOut} is the exception raised when the time limit |
37 is reached. |
37 is reached. |
38 |
38 |
39 Note that @{ML "timeLimit" in TimeLimit} is only meaningful when you use PolyML, |
39 Note that @{ML "timeLimit" in TimeLimit} is only meaningful when you use PolyML, |
40 because PolyML has a rich infrastructure for multithreading programming on |
40 because PolyML has a rich infrastructure for multithreading programming on |
41 which @{ML "timeLimit" in TimeLimit} relies. |
41 which @{ML "timeLimit" in TimeLimit} relies. |