# HG changeset patch
# User wenzelm
# Date 1717868588 -7200
# Node ID f5055150b70b950888985e3bc17094af69ce5cec
# Parent  152d6c58adb3d15914997e9cc6814bd7f3a2cc4c
clarified output, following Consumer_Thread.failure;

diff -r 152d6c58adb3 -r f5055150b70b src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Sat Jun 08 19:35:28 2024 +0200
+++ b/src/Pure/PIDE/session.scala	Sat Jun 08 19:43:08 2024 +0200
@@ -20,7 +20,11 @@
     def apply[A](name: String)(consume: A => Unit): Consumer[A] =
       new Consumer[A](name, consume)
   }
-  final class Consumer[-A] private(val name: String, val consume: A => Unit)
+  final class Consumer[-A] private(val name: String, val consume: A => Unit) {
+    def failure(exn: Throwable): Unit =
+      Output.error_message(
+        "Session consumer failure: " + quote(name) + "\n" + Exn.print(exn))
+  }
 
   class Outlet[A](dispatcher: Consumer_Thread[() => Unit]) {
     private val consumers = Synchronized[List[Consumer[A]]](Nil)
@@ -32,10 +36,7 @@
       for (c <- consumers.value.iterator) {
         dispatcher.send(() =>
           try { c.consume(a) }
-          catch {
-            case exn: Throwable =>
-              Output.error_message("Consumer failed: " + quote(c.name) + "\n" + Exn.print(exn))
-          })
+          catch { case exn: Throwable => c.failure(exn) })
       }
     }
   }