# 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) }