eliminated redundant session_ready;
authorwenzelm
Sat, 02 Jul 2011 20:54:38 +0200
changeset 44520474745a899ea
parent 44519 9ef5479da29f
child 44521 ea08ce1c314b
eliminated redundant session_ready;
src/Tools/jEdit/src/plugin.scala
     1.1 --- a/src/Tools/jEdit/src/plugin.scala	Sat Jul 02 20:22:02 2011 +0200
     1.2 +++ b/src/Tools/jEdit/src/plugin.scala	Sat Jul 02 20:54:38 2011 +0200
     1.3 @@ -316,13 +316,10 @@
     1.4  {
     1.5    /* session management */
     1.6  
     1.7 -  @volatile private var session_ready = false
     1.8 -
     1.9    private val session_manager = actor {
    1.10      loop {
    1.11        react {
    1.12          case phase: Session.Phase =>
    1.13 -          session_ready = phase == Session.Ready
    1.14            phase match {
    1.15              case Session.Failed =>
    1.16                Swing_Thread.now {
    1.17 @@ -335,7 +332,6 @@
    1.18              case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
    1.19              case _ =>
    1.20            }
    1.21 -
    1.22          case bad => System.err.println("session_manager: ignoring bad message " + bad)
    1.23        }
    1.24      }
    1.25 @@ -357,7 +353,7 @@
    1.26        if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
    1.27  
    1.28          val buffer = msg.getBuffer
    1.29 -        if (buffer != null && session_ready)
    1.30 +        if (buffer != null && Isabelle.session.is_ready)
    1.31            Isabelle.init_model(buffer)
    1.32  
    1.33        case msg: EditPaneUpdate
    1.34 @@ -373,7 +369,7 @@
    1.35          if (buffer != null && text_area != null) {
    1.36            if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
    1.37                msg.getWhat == EditPaneUpdate.CREATED) {
    1.38 -            if (session_ready)
    1.39 +            if (Isabelle.session.is_ready)
    1.40                Isabelle.init_view(buffer, text_area)
    1.41            }
    1.42            else Isabelle.exit_view(buffer, text_area)