equal
deleted
inserted
replaced
1 (* Title: Pure/ML-Systems/multithreading_polyml.ML |
1 (* Title: Pure/ML-Systems/multithreading_polyml.ML |
2 Author: Makarius |
2 Author: Makarius |
3 |
3 |
4 Multithreading in Poly/ML 5.2 or later (cf. polyml/basis/Thread.sml). |
4 Multithreading in Poly/ML 5.2.1 or later (cf. polyml/basis/Thread.sml). |
5 *) |
5 *) |
6 |
6 |
7 signature MULTITHREADING_POLYML = |
7 signature MULTITHREADING_POLYML = |
8 sig |
8 sig |
9 val interruptible: ('a -> 'b) -> 'a -> 'b |
9 val interruptible: ('a -> 'b) -> 'a -> 'b |