more uniform warning/error handling, potentially with propagation to send_wait caller;
--- 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
//}}}