equal
deleted
inserted
replaced
38 loop { |
38 loop { |
39 react { |
39 react { |
40 case output: Isabelle_Process.Output => |
40 case output: Isabelle_Process.Output => |
41 if (output.is_syslog) Swing_Thread.later { update_syslog() } |
41 if (output.is_syslog) Swing_Thread.later { update_syslog() } |
42 |
42 |
43 case bad => java.lang.System.err.println("Syslog_Dockable: ignoring bad message " + bad) |
43 case bad => System.err.println("Syslog_Dockable: ignoring bad message " + bad) |
44 } |
44 } |
45 } |
45 } |
46 } |
46 } |
47 |
47 |
48 override def init() |
48 override def init() |