--- a/src/Pure/ML/ml_statistics.ML Fri Aug 07 20:19:49 2020 +0200
+++ b/src/Pure/ML/ml_statistics.ML Fri Aug 07 20:28:53 2020 +0200
@@ -132,6 +132,22 @@
(* monitor process *)
+(* FIXME workaround for 100% CPU usage in OS.Process.sleep *)
+structure OS =
+struct
+ open OS;
+ structure Process =
+ struct
+ open Process;
+ fun sleep t =
+ let
+ open Thread;
+ val lock = Mutex.mutex ();
+ val cond = ConditionVar.conditionVar ();
+ in ConditionVar.waitUntil (cond, lock, Time.now () + t) end;
+ end;
+end;
+
fun monitor pid delay =
let
fun loop () =