src/Tools/jEdit/src/session_dockable.scala
changeset 44734 7313e2db3d39
parent 44672 07dad1433cd7
child 44775 27930cf6f0f7
     1.1 --- a/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 06 11:18:19 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/session_dockable.scala	Tue Sep 06 11:25:27 2011 +0200
     1.3 @@ -105,8 +105,6 @@
     1.4    private val main_actor = actor {
     1.5      loop {
     1.6        react {
     1.7 -        case input: Isabelle_Process.Input =>
     1.8 -
     1.9          case result: Isabelle_Process.Result =>
    1.10            if (result.is_syslog)
    1.11              Swing_Thread.now {
    1.12 @@ -127,13 +125,13 @@
    1.13    }
    1.14  
    1.15    override def init() {
    1.16 -    Isabelle.session.raw_messages += main_actor
    1.17 +    Isabelle.session.syslog_messages += main_actor
    1.18      Isabelle.session.phase_changed += main_actor
    1.19      Isabelle.session.commands_changed += main_actor
    1.20    }
    1.21  
    1.22    override def exit() {
    1.23 -    Isabelle.session.raw_messages -= main_actor
    1.24 +    Isabelle.session.syslog_messages -= main_actor
    1.25      Isabelle.session.phase_changed -= main_actor
    1.26      Isabelle.session.commands_changed -= main_actor
    1.27    }