src/Tools/jEdit/src/syslog_dockable.scala
changeset 56715 52125652e82a
parent 56662 f373fb77e0a4
child 56775 59f70b89e5fd
     1.1 --- a/src/Tools/jEdit/src/syslog_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/syslog_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
     1.3 @@ -9,7 +9,6 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 -import scala.actors.Actor._
     1.8  import scala.swing.TextArea
     1.9  
    1.10  import org.gjt.sp.jedit.View
    1.11 @@ -32,27 +31,22 @@
    1.12    set_content(syslog)
    1.13  
    1.14  
    1.15 -  /* main actor */
    1.16 +  /* main */
    1.17  
    1.18 -  private val main_actor = actor {
    1.19 -    loop {
    1.20 -      react {
    1.21 -        case output: Prover.Output =>
    1.22 -          if (output.is_syslog) Swing_Thread.later { update_syslog() }
    1.23 -
    1.24 -        case bad => System.err.println("Syslog_Dockable: ignoring bad message " + bad)
    1.25 -      }
    1.26 +  private val main =
    1.27 +    Session.Consumer[Prover.Output](getClass.getName) {
    1.28 +      case output =>
    1.29 +        if (output.is_syslog) Swing_Thread.later { update_syslog() }
    1.30      }
    1.31 -  }
    1.32  
    1.33    override def init()
    1.34    {
    1.35 -    PIDE.session.syslog_messages += main_actor
    1.36 +    PIDE.session.syslog_messages += main
    1.37      update_syslog()
    1.38    }
    1.39  
    1.40    override def exit()
    1.41    {
    1.42 -    PIDE.session.syslog_messages -= main_actor
    1.43 +    PIDE.session.syslog_messages -= main
    1.44    }
    1.45  }