equal
deleted
inserted
replaced
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, |
39 because PolyML has the infrastructure for multithreading programming on |
39 because PolyML has the infrastructure for multithreaded programming on |
40 which @{ML "timeLimit" in TimeLimit} relies. |
40 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 |