proper startup for Pure: its use_prelude produces stdout before stderr protocol init;
--- 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)