src/Pure/General/timing.ML
changeset 67001 b34fbf33a7ea
parent 67000 1698e9ccef2d
child 67932 04352338f7f3
equal deleted inserted replaced
67000:1698e9ccef2d 67001:b34fbf33a7ea
    55     val real_time2 = Timer.checkRealTimer real_timer;
    55     val real_time2 = Timer.checkRealTimer real_timer;
    56     val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times;
    56     val {nongc = {sys, usr}, gc = {sys = gc_sys, usr = gc_usr}} = cpu_times;
    57     val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} =
    57     val {nongc = {sys = sys2, usr = usr2}, gc = {sys = gc_sys2, usr = gc_usr2}} =
    58       Timer.checkCPUTimes cpu_timer;
    58       Timer.checkCPUTimes cpu_timer;
    59 
    59 
    60     open Time;
       
    61     val elapsed = real_time2 - real_time;
    60     val elapsed = real_time2 - real_time;
    62     val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
    61     val gc = gc_usr2 - gc_usr + gc_sys2 - gc_sys;
    63     val cpu = usr2 - usr + sys2 - sys + gc;
    62     val cpu = usr2 - usr + sys2 - sys + gc;
    64   in {elapsed = elapsed, cpu = cpu, gc = gc} end;
    63   in {elapsed = elapsed, cpu = cpu, gc = gc} end;
    65 
    64