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;