init/exit model/view synchronously within the swing thread -- EditBus.send in jedit-4.4.1 always runs there;

--- a/src/Tools/jEdit/src/document_view.scala	Wed Jun 22 20:21:22 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Jun 22 20:25:35 2011 +0200
@@ -77,7 +77,7 @@
       Swing_Thread.require()
       if (model.buffer == text_area.getBuffer) body
       else {
-        // FIXME Log.log(Log.ERROR, this, new RuntimeException("Inconsistent document model"))
+        Log.log(Log.ERROR, this, new RuntimeException("Inconsistent document model"))
         default
       }
     }

--- a/src/Tools/jEdit/src/plugin.scala	Wed Jun 22 20:21:22 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Jun 22 20:25:35 2011 +0200
@@ -191,6 +191,54 @@
   def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
   def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
 
+  def init_model(buffer: Buffer)
+  {
+    swing_buffer_lock(buffer) {
+      val opt_model =
+        document_model(buffer) match {
+          case Some(model) => Some(model)
+          case None =>
+            // FIXME strip protocol prefix of URL
+            Thy_Header.split_thy_path(system.posix_path(buffer.getPath)) match {
+              case Some((dir, thy_name)) =>
+                Some(Document_Model.init(session, buffer, dir + "/" + thy_name))
+              case None => None
+            }
+        }
+      if (opt_model.isDefined) {
+        for (text_area <- jedit_text_areas(buffer)) {
+          if (document_view(text_area).map(_.model) != opt_model)
+            Document_View.init(opt_model.get, text_area)
+        }
+      }
+    }
+  }
+
+  def exit_model(buffer: Buffer)
+  {
+    swing_buffer_lock(buffer) {
+      jedit_text_areas(buffer).foreach(Document_View.exit)
+      Document_Model.exit(buffer)
+    }
+  }
+
+  def init_view(buffer: Buffer, text_area: JEditTextArea)
+  {
+    swing_buffer_lock(buffer) {
+      document_model(buffer) match {
+        case Some(model) => Document_View.init(model, text_area)
+        case None =>
+      }
+    }
+  }
+
+  def exit_view(buffer: Buffer, text_area: JEditTextArea)
+  {
+    swing_buffer_lock(buffer) {
+      Document_View.exit(text_area)
+    }
+  }
+
 
   /* dockable windows */
 
@@ -267,47 +315,13 @@
 {
   /* session management */
 
-  private def init_model(buffer: Buffer)
-  {
-    Isabelle.swing_buffer_lock(buffer) {
-      val opt_model =
-        Document_Model(buffer) match {
-          case Some(model) => Some(model)
-          case None =>
-            Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
-              case Some((dir, thy_name)) =>
-                Some(Document_Model.init(Isabelle.session, buffer, dir + "/" + thy_name))
-              case None => None
-            }
-        }
-      if (opt_model.isDefined) {
-        for (text_area <- Isabelle.jedit_text_areas(buffer)) {
-          if (Document_View(text_area).map(_.model) != opt_model)
-            Document_View.init(opt_model.get, text_area)
-        }
-      }
-    }
-  }
-
-  private def exit_model(buffer: Buffer)
-  {
-    Isabelle.swing_buffer_lock(buffer) {
-      Isabelle.jedit_text_areas(buffer).foreach(Document_View.exit)
-      Document_Model.exit(buffer)
-    }
-  }
-
-  private case class Init_Model(buffer: Buffer)
-  private case class Exit_Model(buffer: Buffer)
-  private case class Init_View(buffer: Buffer, text_area: JEditTextArea)
-  private case class Exit_View(buffer: Buffer, text_area: JEditTextArea)
+  @volatile private var session_ready = false
 
   private val session_manager = actor {
-    var ready = false
     loop {
       react {
         case phase: Session.Phase =>
-          ready = phase == Session.Ready
+          session_ready = phase == Session.Ready
           phase match {
             case Session.Failed =>
               Swing_Thread.now {
@@ -316,32 +330,11 @@
                 Library.error_dialog(jEdit.getActiveView, "Failed to start Isabelle process", text)
               }
 
-            case Session.Ready => Isabelle.jedit_buffers.foreach(init_model)
-            case Session.Shutdown => Isabelle.jedit_buffers.foreach(exit_model)
+            case Session.Ready => Isabelle.jedit_buffers.foreach(Isabelle.init_model)
+            case Session.Shutdown => Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
             case _ =>
           }
 
-        case Init_Model(buffer) =>
-          if (ready) init_model(buffer)
-
-        case Exit_Model(buffer) =>
-          exit_model(buffer)
-
-        case Init_View(buffer, text_area) =>
-          if (ready) {
-            Isabelle.swing_buffer_lock(buffer) {
-              Document_Model(buffer) match {
-                case Some(model) => Document_View.init(model, text_area)
-                case None =>
-              }
-            }
-          }
-
-        case Exit_View(buffer, text_area) =>
-          Isabelle.swing_buffer_lock(buffer) {
-            Document_View.exit(text_area)
-          }
-
         case bad => System.err.println("session_manager: ignoring bad message " + bad)
       }
     }
@@ -352,16 +345,19 @@
 
   override def handleMessage(message: EBMessage)
   {
+    Swing_Thread.assert()
     message match {
       case msg: EditorStarted =>
-      Isabelle.check_jvm()
-      if (Isabelle.Boolean_Property("auto-start")) Isabelle.start_session()
+        Isabelle.check_jvm()
+        if (Isabelle.Boolean_Property("auto-start"))
+          Isabelle.start_session()
 
       case msg: BufferUpdate
       if msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
 
         val buffer = msg.getBuffer
-        if (buffer != null) session_manager ! Init_Model(buffer)
+        if (buffer != null && session_ready)
+          Isabelle.init_model(buffer)
 
       case msg: EditPaneUpdate
       if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGING ||
@@ -375,10 +371,11 @@
 
         if (buffer != null && text_area != null) {
           if (msg.getWhat == EditPaneUpdate.BUFFER_CHANGED ||
-              msg.getWhat == EditPaneUpdate.CREATED)
-            session_manager ! Init_View(buffer, text_area)
-          else
-            session_manager ! Exit_View(buffer, text_area)
+              msg.getWhat == EditPaneUpdate.CREATED) {
+            if (session_ready)
+              Isabelle.init_view(buffer, text_area)
+          }
+          else Isabelle.exit_view(buffer, text_area)
         }
 
       case msg: PropertiesChanged =>