--- a/src/Pure/PIDE/session.scala Sat Jun 08 19:43:08 2024 +0200
+++ b/src/Pure/PIDE/session.scala Sat Jun 08 19:47:14 2024 +0200
@@ -21,9 +21,13 @@
new Consumer[A](name, consume)
}
final class Consumer[-A] private(val name: String, val consume: A => Unit) {
- def failure(exn: Throwable): Unit =
+ private def failure(exn: Throwable): Unit =
Output.error_message(
"Session consumer failure: " + quote(name) + "\n" + Exn.print(exn))
+
+ def consume_robust(a: A): Unit =
+ try { consume(a) }
+ catch { case exn: Throwable => failure(exn) }
}
class Outlet[A](dispatcher: Consumer_Thread[() => Unit]) {
@@ -34,9 +38,7 @@
def post(a: A): Unit = {
for (c <- consumers.value.iterator) {
- dispatcher.send(() =>
- try { c.consume(a) }
- catch { case exn: Throwable => c.failure(exn) })
+ dispatcher.send(() => c.consume_robust(a))
}
}
}