src/Pure/ML/ml_statistics.ML
changeset 72111 b9ded33bd58c
parent 72041 7b112eedc859
child 72113 2d9e40cfe9af
equal deleted inserted replaced
72110:16fab31feadc 72111:b9ded33bd58c
   138       (TextIO.output (TextIO.stdOut, print_properties (get_external pid) ^ "\n");
   138       (TextIO.output (TextIO.stdOut, print_properties (get_external pid) ^ "\n");
   139        TextIO.flushOut TextIO.stdOut;
   139        TextIO.flushOut TextIO.stdOut;
   140        OS.Process.sleep (Time.fromReal delay);
   140        OS.Process.sleep (Time.fromReal delay);
   141        loop ());
   141        loop ());
   142     fun exit () = OS.Process.exit OS.Process.success;
   142     fun exit () = OS.Process.exit OS.Process.success;
   143   in loop () handle Interrupt => exit () | Fail _ => exit () end;
   143   in loop () handle _ (*sic!*) => exit () end;
   144 
   144 
   145 end;
   145 end;