src/Pure/ML/ml_statistics.ML
changeset 72113 2d9e40cfe9af
parent 72111 b9ded33bd58c
child 72134 f40200b5bb3c
equal deleted inserted replaced
72112:3546dd4ade74 72113:2d9e40cfe9af
   130 end;
   130 end;
   131 
   131 
   132 
   132 
   133 (* monitor process *)
   133 (* monitor process *)
   134 
   134 
       
   135 (* FIXME workaround for 100% CPU usage in OS.Process.sleep *)
       
   136 structure OS =
       
   137 struct
       
   138   open OS;
       
   139   structure Process =
       
   140   struct
       
   141     open Process;
       
   142     fun sleep t =
       
   143       let
       
   144         open Thread;
       
   145         val lock = Mutex.mutex ();
       
   146         val cond = ConditionVar.conditionVar ();
       
   147       in ConditionVar.waitUntil (cond, lock, Time.now () + t) end;
       
   148   end;
       
   149 end;
       
   150 
   135 fun monitor pid delay =
   151 fun monitor pid delay =
   136   let
   152   let
   137     fun loop () =
   153     fun loop () =
   138       (TextIO.output (TextIO.stdOut, print_properties (get_external pid) ^ "\n");
   154       (TextIO.output (TextIO.stdOut, print_properties (get_external pid) ^ "\n");
   139        TextIO.flushOut TextIO.stdOut;
   155        TextIO.flushOut TextIO.stdOut;