equal
deleted
inserted
replaced
24 /* main actor */ |
24 /* main actor */ |
25 |
25 |
26 private val main_actor = actor { |
26 private val main_actor = actor { |
27 loop { |
27 loop { |
28 react { |
28 react { |
29 case output: Isabelle_Process.Output => |
29 case output: Prover.Output => |
30 Swing_Thread.later { |
30 Swing_Thread.later { |
31 text_area.append(XML.content(output.message)) |
31 text_area.append(XML.content(output.message)) |
32 if (!output.is_stdout && !output.is_stderr) text_area.append("\n") |
32 if (!output.is_stdout && !output.is_stderr) text_area.append("\n") |
33 } |
33 } |
34 |
34 |