# HG changeset patch
# User wenzelm
# Date 1596824933 -7200
# Node ID 2d9e40cfe9afea331951ca9189d44be262fdc713
# Parent  3546dd4ade74c14ebb286209878851f9f4114036
temporary workaround for 100% CPU usage in OS.Process.sleep;

diff -r 3546dd4ade74 -r 2d9e40cfe9af src/Pure/ML/ml_init.ML
--- a/src/Pure/ML/ml_init.ML	Fri Aug 07 20:19:49 2020 +0200
+++ b/src/Pure/ML/ml_init.ML	Fri Aug 07 20:28:53 2020 +0200
@@ -33,3 +33,19 @@
     if n = 1 then String.str (String.sub (s, i))
     else String.substring (s, i, n);
 end;
+
+(* 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;
diff -r 3546dd4ade74 -r 2d9e40cfe9af src/Pure/ML/ml_statistics.ML
--- 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 () =