show displaced messages (e.g. from protocol thread) as raw output;
--- 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)
}