more uniform warning/error handling, potentially with propagation to send_wait caller;
authorwenzelm
Thu Apr 24 23:13:17 2014 +0200 (2014-04-24)
changeset 567108f102c18eab7
parent 56709 e83356e94380
child 56711 ef3d00153e3b
more uniform warning/error handling, potentially with propagation to send_wait caller;
src/Pure/PIDE/session.scala
     1.1 --- a/src/Pure/PIDE/session.scala	Thu Apr 24 23:02:10 2014 +0200
     1.2 +++ b/src/Pure/PIDE/session.scala	Thu Apr 24 23:13:17 2014 +0200
     1.3 @@ -483,7 +483,7 @@
     1.4  
     1.5      /* main thread */
     1.6  
     1.7 -    Consumer_Thread.fork[Any]("manager", daemon = true)
     1.8 +    Consumer_Thread.fork[Any]("Session.manager", daemon = true)
     1.9      {
    1.10        case arg: Any =>
    1.11          //{{{
    1.12 @@ -540,8 +540,6 @@
    1.13              if (global_state.value.is_assigned(change.previous))
    1.14                handle_change(change)
    1.15              else postponed_changes.store(change)
    1.16 -
    1.17 -          case bad => System.err.println("Session.manager: ignoring bad message " + bad)
    1.18          }
    1.19          true
    1.20          //}}}