# HG changeset patch
# User wenzelm
# Date 1398373997 -7200
# Node ID 8f102c18eab7a04e029fc4c9850c67546ec5ae1c
# Parent  e83356e94380939b313edaba6c9fe8c83d8230f9
more uniform warning/error handling, potentially with propagation to send_wait caller;

diff -r e83356e94380 -r 8f102c18eab7 src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Thu Apr 24 23:02:10 2014 +0200
+++ b/src/Pure/PIDE/session.scala	Thu Apr 24 23:13:17 2014 +0200
@@ -483,7 +483,7 @@
 
     /* main thread */
 
-    Consumer_Thread.fork[Any]("manager", daemon = true)
+    Consumer_Thread.fork[Any]("Session.manager", daemon = true)
     {
       case arg: Any =>
         //{{{
@@ -540,8 +540,6 @@
             if (global_state.value.is_assigned(change.previous))
               handle_change(change)
             else postponed_changes.store(change)
-
-          case bad => System.err.println("Session.manager: ignoring bad message " + bad)
         }
         true
         //}}}