equal
deleted
inserted
replaced
27 /* main actor */ |
27 /* main actor */ |
28 |
28 |
29 private val main_actor = actor { |
29 private val main_actor = actor { |
30 loop { |
30 loop { |
31 react { |
31 react { |
32 case input: Isabelle_Process.Input => |
|
33 |
|
34 case result: Isabelle_Process.Result => |
32 case result: Isabelle_Process.Result => |
35 if (result.is_stdout) |
33 if (result.is_stdout) |
36 Swing_Thread.now { text_area.append(XML.content(result.message).mkString) } |
34 Swing_Thread.now { text_area.append(XML.content(result.message).mkString) } |
37 |
35 |
38 case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad) |
36 case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad) |
39 } |
37 } |
40 } |
38 } |
41 } |
39 } |
42 |
40 |
43 override def init() { Isabelle.session.raw_messages += main_actor } |
41 override def init() { Isabelle.session.raw_output_messages += main_actor } |
44 override def exit() { Isabelle.session.raw_messages -= main_actor } |
42 override def exit() { Isabelle.session.raw_output_messages -= main_actor } |
45 } |
43 } |