# HG changeset patch
# User wenzelm
# Date 1309632878 -7200
# Node ID 474745a899ea310ef0a2577d27f9fd26a399c814
# Parent  9ef5479da29f24502d857149028c176172e4e471
eliminated redundant session_ready;

diff -r 9ef5479da29f -r 474745a899ea src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Sat Jul 02 20:22:02 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Jul 02 20:54:38 2011 +0200
@@ -316,13 +316,10 @@
 {
   /* session management */
 
-  @volatile private var session_ready = false
-
   private val session_manager = actor {
     loop {
       react {
         case phase: Session.Phase =>
-          session_ready = phase == Session.Ready
           phase match {
             case Session.Failed =>
               Swing_Thread.now {
@@ -335,7 +332,6 @@
             case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
             case _ =>
           }
-
         case bad => System.err.println("session_manager: ignoring bad message " + bad)
       }
     }
@@ -357,7 +353,7 @@
       if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
 
         val buffer = msg.getBuffer
-        if (buffer != null && session_ready)
+        if (buffer != null && Isabelle.session.is_ready)
           Isabelle.init_model(buffer)
 
       case msg: EditPaneUpdate
@@ -373,7 +369,7 @@
         if (buffer != null && text_area != null) {
           if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
               msg.getWhat == EditPaneUpdate.CREATED) {
-            if (session_ready)
+            if (Isabelle.session.is_ready)
               Isabelle.init_view(buffer, text_area)
           }
           else Isabelle.exit_view(buffer, text_area)