avoid setTokenMarker fluctuation on buffer reload etc. via static isabelle_token_marker, which is installed by hijacking the jEdit ModeProvider;

--- a/src/Tools/jEdit/src/document_model.scala	Sat Jun 18 22:01:22 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Sat Jun 18 23:34:34 2011 +0200
@@ -129,30 +129,18 @@
   }
 
 
-  /* token marker */
-
-  private val token_marker = Token_Markup.token_marker(session, buffer)
-
-
   /* activation */
 
   def activate()
   {
-    buffer.setTokenMarker(token_marker)
     buffer.addBufferListener(buffer_listener)
     buffer.propertiesChanged()
     pending_edits.init()
   }
 
-  def refresh()
-  {
-    buffer.setTokenMarker(token_marker)
-  }
-
   def deactivate()
   {
     pending_edits.flush()
-    buffer.setTokenMarker(buffer.getMode.getTokenMarker)
     buffer.removeBufferListener(buffer_listener)
   }
 }

--- a/src/Tools/jEdit/src/plugin.scala	Sat Jun 18 22:01:22 2011 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Sat Jun 18 23:34:34 2011 +0200
@@ -19,7 +19,7 @@
   Buffer, EditPane, ServiceManager, View}
 import org.gjt.sp.jedit.buffer.JEditBuffer
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
-import org.gjt.sp.jedit.syntax.{Token => JEditToken}
+import org.gjt.sp.jedit.syntax.{Token => JEditToken, ModeProvider}
 import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
 import org.gjt.sp.jedit.gui.DockableWindowManager
 
@@ -290,7 +290,7 @@
     Isabelle.swing_buffer_lock(buffer) {
       val opt_model =
         Document_Model(buffer) match {
-          case Some(model) => model.refresh; Some(model)
+          case Some(model) => Some(model)
           case None =>
             Thy_Header.split_thy_path(Isabelle.system.posix_path(buffer.getPath)) match {
               case Some((dir, thy_name)) =>
@@ -408,8 +408,10 @@
     }
   }
 
+
   override def start()
   {
+    ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)
     Isabelle.plugin = this
     Isabelle.setup_tooltips()
     Isabelle.system = new Isabelle_System

--- a/src/Tools/jEdit/src/token_markup.scala	Sat Jun 18 22:01:22 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Sat Jun 18 23:34:34 2011 +0200
@@ -9,8 +9,10 @@
 
 import isabelle._
 
-import org.gjt.sp.jedit.Buffer
-import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, ParserRuleSet}
+import org.gjt.sp.jedit.Mode
+import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler,
+  ParserRuleSet, ModeProvider, XModeHandler}
+
 import javax.swing.text.Segment
 
 
@@ -78,46 +80,65 @@
       }
   }
 
-  def token_marker(session: Session, buffer: Buffer): TokenMarker =
-    new TokenMarker {
-      override def markTokens(context: TokenMarker.LineContext,
-          handler: TokenHandler, line: Segment): TokenMarker.LineContext =
-      {
-        val syntax = session.current_syntax()
-        val ctxt =
-          context match {
-            case c: Line_Context => c.context
-            case _ => Scan.Finished
-          }
-        val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
-        val context1 = new Line_Context(ctxt1)
+  class Marker extends TokenMarker
+  {
+    override def markTokens(context: TokenMarker.LineContext,
+        handler: TokenHandler, line: Segment): TokenMarker.LineContext =
+    {
+      val symbols = Isabelle.system.symbols
+      val syntax = Isabelle.session.current_syntax()
 
-        val extended = extended_styles(session.system.symbols, line)
+      val ctxt =
+        context match {
+          case c: Line_Context => c.context
+          case _ => Scan.Finished
+        }
+      val (tokens, ctxt1) = syntax.scan_context(line, ctxt)
+      val context1 = new Line_Context(ctxt1)
+
+      val extended = extended_styles(symbols, line)
 
-        var offset = 0
-        for (token <- tokens) {
-          val style = Isabelle_Markup.token_markup(syntax, token)
-          val length = token.source.length
-          val end_offset = offset + length
-          if ((offset until end_offset) exists extended.isDefinedAt) {
-            for (i <- offset until end_offset) {
-              val style1 =
-                extended.get(i) match {
-                  case None => style
-                  case Some(ext) => ext(style)
-                }
-              handler.handleToken(line, style1, i, 1, context1)
-            }
+      var offset = 0
+      for (token <- tokens) {
+        val style = Isabelle_Markup.token_markup(syntax, token)
+        val length = token.source.length
+        val end_offset = offset + length
+        if ((offset until end_offset) exists extended.isDefinedAt) {
+          for (i <- offset until end_offset) {
+            val style1 =
+              extended.get(i) match {
+                case None => style
+                case Some(ext) => ext(style)
+              }
+            handler.handleToken(line, style1, i, 1, context1)
           }
-          else handler.handleToken(line, style, offset, length, context1)
-          offset += length
         }
-        handler.handleToken(line, JEditToken.END, line.count, 0, context1)
+        else handler.handleToken(line, style, offset, length, context1)
+        offset += length
+      }
+      handler.handleToken(line, JEditToken.END, line.count, 0, context1)
+
+      val context2 = context1.intern
+      handler.setLineContext(context2)
+      context2
+    }
+  }
+
 
-        val context2 = context1.intern
-        handler.setLineContext(context2)
-        context2
-      }
+  /* mode provider */
+
+  class Mode_Provider(orig_provider: ModeProvider) extends ModeProvider
+  {
+    for (mode <- orig_provider.getModes) addMode(mode)
+
+    val isabelle_token_marker = new Token_Markup.Marker
+
+    override def loadMode(mode: Mode, xmh: XModeHandler)
+    {
+      super.loadMode(mode, xmh)
+      if (mode.getName == "isabelle")
+        mode.setTokenMarker(isabelle_token_marker)
     }
+  }
 }