# HG changeset patch
# User wenzelm
# Date 1431073184 -7200
# Node ID c2837a39da01631064c95c5b69c287d7ad05bc8f
# Parent  83de10e270077b1d6303e57620c67ae43f2c4345
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;

diff -r 83de10e27007 -r c2837a39da01 src/Tools/jEdit/src/document_model.scala
--- 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
   }
 }
 
diff -r 83de10e27007 -r c2837a39da01 src/Tools/jEdit/src/isabelle.scala
--- 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)
   }