src/Tools/jEdit/src/output_dockable.scala
changeset 56715 52125652e82a
parent 56662 f373fb77e0a4
child 56880 f8c1d2583699
     1.1 --- a/src/Tools/jEdit/src/output_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/output_dockable.scala	Fri Apr 25 12:51:08 2014 +0200
     1.3 @@ -9,8 +9,6 @@
     1.4  
     1.5  import isabelle._
     1.6  
     1.7 -import scala.actors.Actor._
     1.8 -
     1.9  import scala.swing.{Button, CheckBox}
    1.10  import scala.swing.event.ButtonClicked
    1.11  
    1.12 @@ -82,39 +80,34 @@
    1.13    }
    1.14  
    1.15  
    1.16 -  /* main actor */
    1.17 +  /* main */
    1.18  
    1.19 -  private val main_actor = actor {
    1.20 -    loop {
    1.21 -      react {
    1.22 -        case _: Session.Global_Options =>
    1.23 -          Swing_Thread.later { handle_resize() }
    1.24 +  private val main =
    1.25 +    Session.Consumer[Any](getClass.getName) {
    1.26 +      case _: Session.Global_Options =>
    1.27 +        Swing_Thread.later { handle_resize() }
    1.28  
    1.29 -        case changed: Session.Commands_Changed =>
    1.30 -          val restriction = if (changed.assignment) None else Some(changed.commands)
    1.31 -          Swing_Thread.later { handle_update(do_update, restriction) }
    1.32 +      case changed: Session.Commands_Changed =>
    1.33 +        val restriction = if (changed.assignment) None else Some(changed.commands)
    1.34 +        Swing_Thread.later { handle_update(do_update, restriction) }
    1.35  
    1.36 -        case Session.Caret_Focus =>
    1.37 -          Swing_Thread.later { handle_update(do_update, None) }
    1.38 -
    1.39 -        case bad => System.err.println("Output_Dockable: ignoring bad message " + bad)
    1.40 -      }
    1.41 +      case Session.Caret_Focus =>
    1.42 +        Swing_Thread.later { handle_update(do_update, None) }
    1.43      }
    1.44 -  }
    1.45  
    1.46    override def init()
    1.47    {
    1.48 -    PIDE.session.global_options += main_actor
    1.49 -    PIDE.session.commands_changed += main_actor
    1.50 -    PIDE.session.caret_focus += main_actor
    1.51 +    PIDE.session.global_options += main
    1.52 +    PIDE.session.commands_changed += main
    1.53 +    PIDE.session.caret_focus += main
    1.54      handle_update(true, None)
    1.55    }
    1.56  
    1.57    override def exit()
    1.58    {
    1.59 -    PIDE.session.global_options -= main_actor
    1.60 -    PIDE.session.commands_changed -= main_actor
    1.61 -    PIDE.session.caret_focus -= main_actor
    1.62 +    PIDE.session.global_options -= main
    1.63 +    PIDE.session.commands_changed -= main
    1.64 +    PIDE.session.caret_focus -= main
    1.65      delay_resize.revoke()
    1.66    }
    1.67