# HG changeset patch
# User wenzelm
# Date 1585738639 -7200
# Node ID c1409b9c2b221dd7069c783be26ff4685165ad09
# Parent  494704309099df1f425e3694fe6cbbe1276a26b1
proper startup for Pure: its use_prelude produces stdout before stderr protocol init;

diff -r 494704309099 -r c1409b9c2b22 src/Pure/PIDE/prover.scala
--- a/src/Pure/PIDE/prover.scala	Wed Apr 01 12:56:19 2020 +0200
+++ b/src/Pure/PIDE/prover.scala	Wed Apr 01 12:57:19 2020 +0200
@@ -114,6 +114,8 @@
 
   private val process_manager = Standard_Thread.fork("process_manager")
   {
+    val stdout = physical_output(false)
+
     val (startup_failed, startup_errors) =
     {
       var finished: Option[Boolean] = None
@@ -127,7 +129,7 @@
           }
           catch { case _: IOException => finished = Some(false) }
         }
-        Thread.sleep(10)
+        Thread.sleep(50)
       }
       (finished.isEmpty || !finished.get, result.toString.trim)
     }
@@ -136,13 +138,13 @@
     if (startup_failed) {
       terminate_process()
       process_result.join
+      stdout.join
       exit_message(Process_Result(127))
     }
     else {
       val (command_stream, message_stream) = channel.rendezvous()
 
       command_input_init(command_stream)
-      val stdout = physical_output(false)
       val stderr = physical_output(true)
       val message = message_output(message_stream)