src/Pure/Concurrent/counter.ML
changeset 62920 a5853334c179
parent 52537 4b5941730bd8
child 68804 cbde6e3b132b
equal deleted inserted replaced
62919:9eb0359d6a77 62920:a5853334c179
    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