more conservative Document_Model.init: avoid Document.Node.Clear due to change of token marker (e.g. due to change of jEdit mode properties);
clarified Isabelle.buffer_token_marker;

--- a/src/Tools/jEdit/src/document_model.scala	Thu May 07 22:12:05 2015 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Fri May 08 10:19:44 2015 +0200
@@ -50,18 +50,19 @@
   {
     GUI_Thread.require {}
 
-    old_model match {
-      case Some(old)
-      if old.node_name == node_name && Isabelle.buffer_token_marker(buffer).isEmpty => old
-
-      case _ =>
-        apply(buffer).map(_.deactivate)
-        val model = new Document_Model(session, buffer, node_name)
-        buffer.setProperty(key, model)
-        model.activate()
-        buffer.propertiesChanged
-        model
-    }
+    val model =
+      old_model match {
+        case Some(old) if old.node_name == node_name => old
+        case _ =>
+          apply(buffer).map(_.deactivate)
+          val model = new Document_Model(session, buffer, node_name)
+          buffer.setProperty(key, model)
+          model.activate()
+          buffer.propertiesChanged
+          model
+      }
+    model.init_token_marker
+    model
   }
 }
 

--- a/src/Tools/jEdit/src/isabelle.scala	Thu May 07 22:12:05 2015 +0200
+++ b/src/Tools/jEdit/src/isabelle.scala	Fri May 08 10:19:44 2015 +0200
@@ -78,10 +78,8 @@
   def buffer_token_marker(buffer: Buffer): Option[TokenMarker] =
   {
     val mode = JEdit_Lib.buffer_mode(buffer)
-    val new_token_marker =
-      if (mode == "isabelle") Some(new Token_Markup.Marker(mode, Some(buffer)))
-      else mode_token_marker(mode)
-    if (new_token_marker == Some(buffer.getTokenMarker)) None else new_token_marker
+    if (mode == "isabelle") Some(new Token_Markup.Marker(mode, Some(buffer)))
+    else mode_token_marker(mode)
   }