src/Tools/jEdit/src/plugin.scala
changeset 47058 34761733526c
parent 46997 395b7277ed76
child 47867 dd9cbe708e6b
--- a/src/Tools/jEdit/src/plugin.scala	Tue Mar 20 20:00:13 2012 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Tue Mar 20 21:34:42 2012 +0100
@@ -185,21 +185,30 @@
       if doc_view.isDefined
     } yield doc_view.get
 
+  def exit_model(buffer: Buffer)
+  {
+    swing_buffer_lock(buffer) {
+      jedit_text_areas(buffer).foreach(Document_View.exit)
+      Document_Model.exit(buffer)
+    }
+  }
+
   def init_model(buffer: Buffer)
   {
     swing_buffer_lock(buffer) {
       val opt_model =
-        document_model(buffer) match {
-          case Some(model) => Some(model)
-          case None =>
-            val name = buffer_name(buffer)
-            Thy_Header.thy_name(name) match {
-              case Some(theory) =>
-                val node_name = Document.Node.Name(name, buffer.getDirectory, theory)
-                Some(Document_Model.init(session, buffer, node_name))
-              case None => None
+      {
+        val name = buffer_name(buffer)
+        Thy_Header.thy_name(name) match {
+          case Some(theory) =>
+            val node_name = Document.Node.Name(name, buffer.getDirectory, theory)
+            document_model(buffer) match {
+              case Some(model) if model.name == node_name => Some(model)
+              case _ => Some(Document_Model.init(session, buffer, node_name))
             }
+          case None => None
         }
+      }
       if (opt_model.isDefined) {
         for (text_area <- jedit_text_areas(buffer)) {
           if (document_view(text_area).map(_.model) != opt_model)
@@ -209,14 +218,6 @@
     }
   }
 
-  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) {
@@ -419,10 +420,10 @@
           Isabelle.start_session()
 
       case msg: BufferUpdate
-      if msg.getWhat == BufferUpdate.LOADED =>
+      if msg.getWhat == BufferUpdate.LOADED || msg.getWhat == BufferUpdate.PROPERTIES_CHANGED =>
         if (Isabelle.session.is_ready) {
           val buffer = msg.getBuffer
-          if (buffer != null) Isabelle.init_model(buffer)
+          if (buffer != null && !buffer.isLoading) Isabelle.init_model(buffer)
           delay_load(true)
         }