# HG changeset patch
# User wenzelm
# Date 1717868834 -7200
# Node ID d1c7da4ff0f5a17b1ff39996b8b0a48ee73b0ec8
# Parent  f5055150b70b950888985e3bc17094af69ce5cec
clarified signature;

diff -r f5055150b70b -r d1c7da4ff0f5 src/Pure/PIDE/session.scala
--- 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))
       }
     }
   }