show displaced messages (e.g. from protocol thread) as raw output;
authorwenzelm
Mon, 29 Jul 2013 14:37:59 +0200
changeset 52766 36c3c051b355
parent 52765 260949bf6529
child 52767 9c28559e5fff
show displaced messages (e.g. from protocol thread) as raw output;
src/Pure/System/session.scala
src/Tools/jEdit/src/raw_output_dockable.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)
         }
       }
     }
--- 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)
       }