src/Tools/jEdit/src/theories_dockable.scala
changeset 56715 52125652e82a
parent 56662 f373fb77e0a4
child 57612 990ffb84489b
     1.1 --- a/src/Tools/jEdit/src/theories_dockable.scala	Fri Apr 25 12:27:18 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/theories_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.{Button, TextArea, Label, ListView, Alignment,
     1.9    ScrollPane, Component, CheckBox, BorderPanel}
    1.10  import scala.swing.event.{MouseClicked, MouseMoved}
    1.11 @@ -216,35 +215,30 @@
    1.12    }
    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 phase: Session.Phase =>
    1.22 -          Swing_Thread.later { handle_phase(phase) }
    1.23 +  private val main =
    1.24 +    Session.Consumer[Any](getClass.getName) {
    1.25 +      case phase: Session.Phase =>
    1.26 +        Swing_Thread.later { handle_phase(phase) }
    1.27  
    1.28 -        case _: Session.Global_Options =>
    1.29 -          Swing_Thread.later {
    1.30 -            continuous_checking.load()
    1.31 -            logic.load ()
    1.32 -            update_nodes_required()
    1.33 -            status.repaint()
    1.34 -          }
    1.35 +      case _: Session.Global_Options =>
    1.36 +        Swing_Thread.later {
    1.37 +          continuous_checking.load()
    1.38 +          logic.load ()
    1.39 +          update_nodes_required()
    1.40 +          status.repaint()
    1.41 +        }
    1.42  
    1.43 -        case changed: Session.Commands_Changed =>
    1.44 -          Swing_Thread.later { handle_update(Some(changed.nodes)) }
    1.45 -
    1.46 -        case bad => System.err.println("Theories_Dockable: ignoring bad message " + bad)
    1.47 -      }
    1.48 +      case changed: Session.Commands_Changed =>
    1.49 +        Swing_Thread.later { handle_update(Some(changed.nodes)) }
    1.50      }
    1.51 -  }
    1.52  
    1.53    override def init()
    1.54    {
    1.55 -    PIDE.session.phase_changed += main_actor
    1.56 -    PIDE.session.global_options += main_actor
    1.57 -    PIDE.session.commands_changed += main_actor
    1.58 +    PIDE.session.phase_changed += main
    1.59 +    PIDE.session.global_options += main
    1.60 +    PIDE.session.commands_changed += main
    1.61  
    1.62      handle_phase(PIDE.session.phase)
    1.63      handle_update()
    1.64 @@ -252,8 +246,8 @@
    1.65  
    1.66    override def exit()
    1.67    {
    1.68 -    PIDE.session.phase_changed -= main_actor
    1.69 -    PIDE.session.global_options -= main_actor
    1.70 -    PIDE.session.commands_changed -= main_actor
    1.71 +    PIDE.session.phase_changed -= main
    1.72 +    PIDE.session.global_options -= main
    1.73 +    PIDE.session.commands_changed -= main
    1.74    }
    1.75  }