clarified handling of raw output messages;
authorwenzelm
Wed, 29 Aug 2012 17:19:48 +0200
changeset 48999 3bdebf6ad9da
parent 48998 b6dd664fa9bc
child 49000 0cebcbeac4c7
clarified handling of raw output messages;
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)
           }