equal
deleted
inserted
replaced
453 raw_messages.event(input) |
453 raw_messages.event(input) |
454 |
454 |
455 case result: Isabelle_Process.Result => |
455 case result: Isabelle_Process.Result => |
456 handle_result(result) |
456 handle_result(result) |
457 if (result.is_syslog) syslog_messages.event(result) |
457 if (result.is_syslog) syslog_messages.event(result) |
458 if (result.is_stdout) raw_output_messages.event(result) |
458 if (result.is_stdout || result.is_stderr) raw_output_messages.event(result) |
459 raw_messages.event(result) |
459 raw_messages.event(result) |
460 } |
460 } |
461 |
461 |
462 case bad => System.err.println("session_actor: ignoring bad message " + bad) |
462 case bad => System.err.println("session_actor: ignoring bad message " + bad) |
463 } |
463 } |