equal
deleted
inserted
replaced
27 |
27 |
28 private val main_actor = actor { |
28 private val main_actor = actor { |
29 loop { |
29 loop { |
30 react { |
30 react { |
31 case output: Isabelle_Process.Output => |
31 case output: Isabelle_Process.Output => |
32 if (output.is_stdout || output.is_stderr) |
32 Swing_Thread.later { |
33 Swing_Thread.later { text_area.append(XML.content(output.message)) } |
33 text_area.append(XML.content(output.message)) |
|
34 if (!output.is_stdout && !output.is_stderr) text_area.append("\n") |
|
35 } |
34 |
36 |
35 case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad) |
37 case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad) |
36 } |
38 } |
37 } |
39 } |
38 } |
40 } |