clarified messages streaming (again, amending 5ea3ed3c52b3): avoid too many small messages stacking up, e.g. when loading HOL-Analysis.Analysis.thy into Isabelle/jEdit;
--- a/src/Pure/Concurrent/consumer_thread.scala Wed Dec 04 15:36:58 2019 +0100
+++ b/src/Pure/Concurrent/consumer_thread.scala Wed Dec 04 19:40:22 2019 +0100
@@ -104,11 +104,7 @@
}
}
- if (continue) {
- val msgs1 = msgs.drop(reqs.length)
- val msgs2 = mailbox.receive(timeout = Some(Time.zero))
- main_loop(msgs1 ::: msgs2)
- }
+ if (continue) main_loop(msgs.drop(reqs.length))
else robust_finish()
}