equal
deleted
inserted
replaced
14 structure Counter: COUNTER = |
14 structure Counter: COUNTER = |
15 struct |
15 struct |
16 |
16 |
17 fun make () = |
17 fun make () = |
18 let |
18 let |
19 val counter = Synchronized.var "counter" (0: int); |
19 val counter = Synchronized.var "counter" 0; |
20 fun next () = |
20 fun next () = |
21 Synchronized.change_result counter |
21 Synchronized.change_result counter |
22 (fn i => |
22 (fn i => |
23 let val j = i + (1: int) |
23 let val j = i + (if Thread_Data.is_virtual then 3 else 2) |
24 in (j, j) end); |
24 in (j, j) end); |
25 in next end; |
25 in next end; |
26 |
26 |
27 end; |
27 end; |
28 |
|