# HG changeset patch
# User wenzelm
# Date 1375101479 -7200
# Node ID 36c3c051b355640a4f3fcf36fef828a6b7e67865
# Parent  260949bf6529d3bfc9d6fb795845d2af8c6c923a
show displaced messages (e.g. from protocol thread) as raw output;

diff -r 260949bf6529 -r 36c3c051b355 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Mon Jul 29 14:18:57 2013 +0200
+++ b/src/Pure/System/session.scala	Mon Jul 29 14:37:59 2013 +0200
@@ -461,7 +461,7 @@
             if (rc == 0) phase = Session.Inactive
             else phase = Session.Failed
 
-          case _ => bad_output()
+          case _ => raw_output_messages.event(output)
         }
       }
     }
diff -r 260949bf6529 -r 36c3c051b355 src/Tools/jEdit/src/raw_output_dockable.scala
--- a/src/Tools/jEdit/src/raw_output_dockable.scala	Mon Jul 29 14:18:57 2013 +0200
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Mon Jul 29 14:37:59 2013 +0200
@@ -29,8 +29,10 @@
     loop {
       react {
         case output: Isabelle_Process.Output =>
-          if (output.is_stdout || output.is_stderr)
-            Swing_Thread.later { text_area.append(XML.content(output.message)) }
+          Swing_Thread.later {
+            text_area.append(XML.content(output.message))
+            if (!output.is_stdout && !output.is_stderr) text_area.append("\n")
+          }
 
         case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
       }