clarified token marker / syntax for mode vs. buffer;

--- a/src/Tools/jEdit/src/document_model.scala	Mon Dec 01 17:51:07 2014 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Mon Dec 01 19:25:20 2014 +0100
@@ -281,12 +281,14 @@
   {
     pending_edits.edit(true, Text.Edit.insert(0, JEdit_Lib.buffer_text(buffer)))
     buffer.addBufferListener(buffer_listener)
-    Token_Markup.refresh_buffer(buffer)
+    Isabelle.buffer_token_marker(buffer).foreach(marker =>
+      JEdit_Lib.update_token_marker(buffer, marker))
   }
 
   private def deactivate()
   {
     buffer.removeBufferListener(buffer_listener)
-    Token_Markup.refresh_buffer(buffer)
+    Isabelle.mode_token_marker(JEdit_Lib.buffer_mode(buffer)).foreach(marker =>
+      JEdit_Lib.update_token_marker(buffer, marker))
   }
 }

--- a/src/Tools/jEdit/src/isabelle.scala	Mon Dec 01 17:51:07 2014 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Mon Dec 01 19:25:20 2014 +0100
@@ -47,15 +47,18 @@
   private lazy val news_syntax: Outer_Syntax =
     Outer_Syntax.init().no_tokens
 
+  private lazy val bootstrap_syntax: Outer_Syntax =
+    Thy_Header.bootstrap_syntax()
+
   def session_syntax(): Option[Outer_Syntax] =
     PIDE.session.recent_syntax match {
       case syntax: Outer_Syntax if syntax != Outer_Syntax.empty => Some(syntax)
       case _ => None
     }
 
-  def mode_syntax(name: String): Option[Outer_Syntax] =
-    name match {
-      case "isabelle" => session_syntax()
+  def mode_syntax(mode: String): Option[Outer_Syntax] =
+    mode match {
+      case "isabelle" => Some(bootstrap_syntax)
       case "isabelle-options" => Some(Options.options_syntax)
       case "isabelle-root" => Some(Build.root_syntax)
       case "isabelle-ml" => Some(ml_syntax)
@@ -66,16 +69,26 @@
     }
 
   def buffer_syntax(buffer: JEditBuffer): Option[Outer_Syntax] =
-    mode_syntax(JEdit_Lib.buffer_mode(buffer))
+    JEdit_Lib.buffer_mode(buffer) match {
+      case "isabelle" => session_syntax()
+      case mode => mode_syntax(mode)
+    }
 
 
   /* token markers */
 
-  private val markers: Map[String, TokenMarker] =
-    Map(modes.map(name => (name, new Token_Markup.Marker(name))): _*) +
+  private val mode_markers: Map[String, TokenMarker] =
+    Map(modes.map(mode => (mode, new Token_Markup.Marker(mode, None))): _*) +
       ("bibtex" -> new Bibtex_JEdit.Token_Marker)
 
-  def token_marker(name: String): Option[TokenMarker] = markers.get(name)
+  def mode_token_marker(mode: String): Option[TokenMarker] = mode_markers.get(mode)
+
+  def buffer_token_marker(buffer: Buffer): Option[TokenMarker] =
+  {
+    val mode = JEdit_Lib.buffer_mode(buffer)
+    if (mode == "isabelle") Some(new Token_Markup.Marker(mode, Some(buffer)))
+    else mode_token_marker(mode)
+  }
 
 
   /* structure matchers */

--- a/src/Tools/jEdit/src/jedit_lib.scala	Mon Dec 01 17:51:07 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Mon Dec 01 19:25:20 2014 +0100
@@ -20,6 +20,7 @@
 import org.gjt.sp.jedit.gui.KeyEventWorkaround
 import org.gjt.sp.jedit.buffer.JEditBuffer
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaPainter}
+import org.gjt.sp.jedit.syntax.TokenMarker
 
 
 object JEdit_Lib
@@ -113,6 +114,12 @@
 
   def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
 
+  def update_token_marker(buffer: JEditBuffer, marker: TokenMarker)
+  {
+    buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
+    buffer.setTokenMarker(marker)
+  }
+
 
   /* main jEdit components */
 

--- a/src/Tools/jEdit/src/pretty_text_area.scala	Mon Dec 01 17:51:07 2014 +0100
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Mon Dec 01 19:25:20 2014 +0100
@@ -261,7 +261,7 @@
   getPainter.setStructureHighlightEnabled(false)
   getPainter.setLineHighlightEnabled(false)
 
-  getBuffer.setTokenMarker(Isabelle.token_marker("isabelle-output").get)
+  getBuffer.setTokenMarker(Isabelle.mode_token_marker("isabelle-output").get)
   getBuffer.setReadOnly(true)
   getBuffer.setStringProperty("noWordSep", "_'.?")
 

--- a/src/Tools/jEdit/src/token_markup.scala	Mon Dec 01 17:51:07 2014 +0100
+++ b/src/Tools/jEdit/src/token_markup.scala	Mon Dec 01 19:25:20 2014 +0100
@@ -14,7 +14,7 @@
 import java.awt.geom.AffineTransform
 
 import org.gjt.sp.util.SyntaxUtilities
-import org.gjt.sp.jedit.{jEdit, Mode}
+import org.gjt.sp.jedit.{jEdit, Mode, Buffer}
 import org.gjt.sp.jedit.syntax.{Token => JEditToken, TokenMarker, TokenHandler, DummyTokenHandler,
   ParserRuleSet, ModeProvider, XModeHandler, SyntaxStyle}
 import org.gjt.sp.jedit.textarea.{TextArea, Selection}
@@ -308,8 +308,14 @@
 
   /* token marker */
 
-  class Marker(mode: String) extends TokenMarker
+  class Marker(mode: String, opt_buffer: Option[Buffer]) extends TokenMarker
   {
+    override def toString: String =
+      opt_buffer match {
+        case None => "Marker(" + mode + ")"
+        case Some(buffer) => "Marker(" + mode + "," + JEdit_Lib.buffer_name(buffer) + ")"
+      }
+
     override def markTokens(context: TokenMarker.LineContext,
         handler: TokenHandler, raw_line: Segment): TokenMarker.LineContext =
     {
@@ -319,8 +325,13 @@
 
       val context1 =
       {
+        val opt_syntax =
+          opt_buffer match {
+            case Some(buffer) => Isabelle.buffer_syntax(buffer)
+            case None => Isabelle.mode_syntax(mode)
+          }
         val (styled_tokens, context1) =
-          (line_context.context, Isabelle.mode_syntax(mode)) match {
+          (line_context.context, opt_syntax) match {
             case (Some(ctxt), _) if mode == "isabelle-ml" || mode == "sml" =>
               val (tokens, ctxt1) = ML_Lex.tokenize_line(mode == "sml", line, ctxt)
               val styled_tokens = tokens.map(tok => (Rendering.ml_token_markup(tok), tok.source))
@@ -378,17 +389,7 @@
     override def loadMode(mode: Mode, xmh: XModeHandler)
     {
       super.loadMode(mode, xmh)
-      Isabelle.token_marker(mode.getName).foreach(mode.setTokenMarker _)
-    }
-  }
-
-  def refresh_buffer(buffer: JEditBuffer)
-  {
-    Isabelle.token_marker(JEdit_Lib.buffer_mode(buffer)) match {
-      case None =>
-      case Some(marker) =>
-        buffer.setTokenMarker(jEdit.getMode("text").getTokenMarker)
-        buffer.setTokenMarker(marker)
+      Isabelle.mode_token_marker(mode.getName).foreach(mode.setTokenMarker _)
     }
   }
 }