proper startup for Pure: its use_prelude produces stdout before stderr protocol init;
authorwenzelm
Wed, 01 Apr 2020 12:57:19 +0200
changeset 71856 c1409b9c2b22
parent 71855 494704309099
child 71857 77327455b00d
proper startup for Pure: its use_prelude produces stdout before stderr protocol init;
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)