# HG changeset patch
# User wenzelm
# Date 1346253588 -7200
# Node ID 3bdebf6ad9dabe483a70e8537b357811137aab80
# Parent  b6dd664fa9bc05c3a7a97dab2c719a7a4e2c25a9
clarified handling of raw output messages;

diff -r b6dd664fa9bc -r 3bdebf6ad9da src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Wed Aug 29 14:29:38 2012 +0200
+++ b/src/Pure/System/session.scala	Wed Aug 29 17:19:48 2012 +0200
@@ -356,8 +356,6 @@
           if (rc == 0) phase = Session.Inactive
           else phase = Session.Failed
 
-        case _ if output.is_stdout =>
-
         case _ => bad_output(output)
       }
     }
@@ -409,9 +407,9 @@
               all_messages.event(input)
 
             case output: Isabelle_Process.Output =>
-              handle_output(output)
+              if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
+              else handle_output(output)
               if (output.is_syslog) syslog_messages.event(output)
-              if (output.is_stdout || output.is_stderr) raw_output_messages.event(output)
               all_messages.event(output)
           }