refined init_model: allow change of buffer name as caused by "Save as", for example;
avoid init_model while buffer.isLoading -- potentially prevent NPE of getText;
avoid emitting nested buffer.propertiesChanged events;

--- a/src/Tools/jEdit/src/document_model.scala	Tue Mar 20 20:00:13 2012 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Mar 20 21:34:42 2012 +0100
@@ -42,15 +42,18 @@
       case Some(model) =>
         model.deactivate()
         buffer.unsetProperty(key)
+        buffer.propertiesChanged
     }
   }
 
   def init(session: Session, buffer: Buffer, name: Document.Node.Name): Document_Model =
   {
-    exit(buffer)
+    Swing_Thread.require()
+    apply(buffer).map(_.deactivate)
     val model = new Document_Model(session, buffer, name)
     buffer.setProperty(key, model)
     model.activate()
+    buffer.propertiesChanged
     model
   }
 }

--- 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)
         }
 

--- a/src/Tools/jEdit/src/token_markup.scala	Tue Mar 20 20:00:13 2012 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Tue Mar 20 21:34:42 2012 +0100
@@ -239,7 +239,6 @@
   {
     buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
     buffer.setTokenMarker(isabelle_token_marker)
-    buffer.propertiesChanged
   }
 }