equal
deleted
inserted
replaced
103 /* main actor */ |
103 /* main actor */ |
104 |
104 |
105 private val main_actor = actor { |
105 private val main_actor = actor { |
106 loop { |
106 loop { |
107 react { |
107 react { |
108 case input: Isabelle_Process.Input => |
|
109 |
|
110 case result: Isabelle_Process.Result => |
108 case result: Isabelle_Process.Result => |
111 if (result.is_syslog) |
109 if (result.is_syslog) |
112 Swing_Thread.now { |
110 Swing_Thread.now { |
113 val text = Isabelle.session.syslog() |
111 val text = Isabelle.session.syslog() |
114 if (text != syslog.text) { |
112 if (text != syslog.text) { |
125 } |
123 } |
126 } |
124 } |
127 } |
125 } |
128 |
126 |
129 override def init() { |
127 override def init() { |
130 Isabelle.session.raw_messages += main_actor |
128 Isabelle.session.syslog_messages += main_actor |
131 Isabelle.session.phase_changed += main_actor |
129 Isabelle.session.phase_changed += main_actor |
132 Isabelle.session.commands_changed += main_actor |
130 Isabelle.session.commands_changed += main_actor |
133 } |
131 } |
134 |
132 |
135 override def exit() { |
133 override def exit() { |
136 Isabelle.session.raw_messages -= main_actor |
134 Isabelle.session.syslog_messages -= main_actor |
137 Isabelle.session.phase_changed -= main_actor |
135 Isabelle.session.phase_changed -= main_actor |
138 Isabelle.session.commands_changed -= main_actor |
136 Isabelle.session.commands_changed -= main_actor |
139 } |
137 } |
140 } |
138 } |