# HG changeset patch
# User wenzelm
# Date 1313954682 -7200
# Node ID 2a2df4de1bbe7711c53f1964a37ee6ebbc25fa39
# Parent  5f5649ac82352e69f946dd279ee18109cadaaf0e
more robust initialization of token marker and line context wrt. session startup;

diff -r 5f5649ac8235 -r 2a2df4de1bbe src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Sun Aug 21 20:42:26 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Sun Aug 21 21:24:42 2011 +0200
@@ -139,13 +139,13 @@
   {
     buffer.addBufferListener(buffer_listener)
     pending_edits.init()
-    buffer.propertiesChanged()
+    Token_Markup.refresh_buffer(buffer)
   }
 
   private def deactivate()
   {
     pending_edits.flush()
     buffer.removeBufferListener(buffer_listener)
-    buffer.propertiesChanged()
+    Token_Markup.refresh_buffer(buffer)
   }
 }
diff -r 5f5649ac8235 -r 2a2df4de1bbe src/Tools/jEdit/src/token_markup.scala
--- a/src/Tools/jEdit/src/token_markup.scala	Sun Aug 21 20:42:26 2011 +0200
+++ b/src/Tools/jEdit/src/token_markup.scala	Sun Aug 21 21:24:42 2011 +0200
@@ -14,9 +14,10 @@
 import java.awt.geom.AffineTransform
 
 import org.gjt.sp.util.SyntaxUtilities
-import org.gjt.sp.jedit.Mode
+import org.gjt.sp.jedit.{jEdit, Mode}
 import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler,
   ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle}
+import org.gjt.sp.jedit.buffer.JEditBuffer
 
 import javax.swing.text.Segment
 
@@ -150,7 +151,7 @@
 
   private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN")
 
-  private class Line_Context(val context: Scan.Context)
+  private class Line_Context(val context: Option[Scan.Context])
     extends TokenMarker.LineContext(isabelle_rules, null)
   {
     override def hashCode: Int = context.hashCode
@@ -166,17 +167,17 @@
     override def markTokens(context: TokenMarker.LineContext,
         handler: TokenHandler, line: Segment): TokenMarker.LineContext =
     {
+      val line_ctxt =
+        context match {
+          case c: Line_Context => c.context
+          case _ => Some(Scan.Finished)
+        }
       val context1 =
-        if (Isabelle.session.is_ready) {
+        if (line_ctxt.isDefined && Isabelle.session.is_ready) {
           val syntax = Isabelle.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)
+          val (tokens, ctxt1) = syntax.scan_context(line, line_ctxt.get)
+          val context1 = new Line_Context(Some(ctxt1))
     
           val extended = extended_styles(line)
     
@@ -202,7 +203,7 @@
           context1
         }
         else {
-          val context1 = new Line_Context(Scan.Finished)
+          val context1 = new Line_Context(None)
           handler.handleToken(line, JEditToken.NULL, 0, line.count, context1)
           handler.handleToken(line, JEditToken.END, line.count, 0, context1)
           context1
@@ -216,12 +217,12 @@
 
   /* mode provider */
 
+  private val isabelle_token_marker = new Token_Markup.Marker
+
   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)
@@ -229,5 +230,12 @@
         mode.setTokenMarker(isabelle_token_marker)
     }
   }
+
+  def refresh_buffer(buffer: JEditBuffer)
+  {
+    buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
+    buffer.setTokenMarker(isabelle_token_marker)
+    buffer.propertiesChanged
+  }
 }