static token markup, based on outer syntax only;
eliminated obsolete buffer.propertiesChanged (expensive due to remarking of full buffer etc.);

--- a/src/Tools/jEdit/lib/Tools/jedit	Thu Jun 16 20:12:59 2011 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Jun 16 22:05:40 2011 +0200
@@ -24,6 +24,7 @@
   "src/scala_console.scala"
   "src/session_dockable.scala"
   "src/text_area_painter.scala"
+  "src/token_markup.scala"
 )
 
 declare -a RESOURCES=(

--- a/src/Tools/jEdit/src/document_model.scala	Thu Jun 16 20:12:59 2011 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Thu Jun 16 22:05:40 2011 +0200
@@ -14,44 +14,13 @@
 
 import org.gjt.sp.jedit.Buffer
 import org.gjt.sp.jedit.buffer.{BufferAdapter, BufferListener, JEditBuffer}
-import org.gjt.sp.jedit.syntax.{SyntaxStyle, Token, TokenMarker, TokenHandler, ParserRuleSet}
 import org.gjt.sp.jedit.textarea.TextArea
 
 import java.awt.font.TextAttribute
-import javax.swing.text.Segment;
 
 
 object Document_Model
 {
-  object Token_Markup
-  {
-    /* extended token styles */
-
-    private val plain_range: Int = Token.ID_COUNT
-    private def check_range(i: Int) { require(0 <= i && i < plain_range) }
-
-    def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
-    def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
-    val hidden: Byte = (3 * plain_range).toByte
-
-
-    /* line context */
-
-    private val dummy_rules = new ParserRuleSet("isabelle", "MAIN")
-
-    class Line_Context(val line: Int, prev: Line_Context)
-      extends TokenMarker.LineContext(dummy_rules, prev)
-    {
-      override def hashCode: Int = line
-      override def equals(that: Any): Boolean =
-        that match {
-          case other: Line_Context => line == other.line
-          case _ => false
-        }
-    }
-  }
-
-
   /* document model of buffer */
 
   private val key = "isabelle.document_model"
@@ -160,46 +129,9 @@
   }
 
 
-  /* semantic token marker */
-
-  private val token_marker = new TokenMarker
-  {
-    override def markTokens(prev: TokenMarker.LineContext,
-        handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
-    {
-      Isabelle.swing_buffer_lock(buffer) {
-        val snapshot = Document_Model.this.snapshot()
-
-        val previous = prev.asInstanceOf[Document_Model.Token_Markup.Line_Context]
-        val line = if (prev == null) 0 else previous.line + 1
-        val context = new Document_Model.Token_Markup.Line_Context(line, previous)
-
-        val start = buffer.getLineStartOffset(line)
-        val stop = start + line_segment.count
-
-        def handle_token(style: Byte, offset: Text.Offset, length: Int) =
-          handler.handleToken(line_segment, style, offset, length, context)
+  /* token marker */
 
-        val syntax = session.current_syntax()
-        val tokens = snapshot.select_markup(Text.Range(start, stop))(Isabelle_Markup.tokens(syntax))
-
-        var last = start
-        for (token <- tokens.iterator) {
-          val Text.Range(token_start, token_stop) = token.range
-          if (last < token_start)
-            handle_token(Token.COMMENT1, last - start, token_start - last)
-          handle_token(token.info getOrElse Token.NULL,
-            token_start - start, token_stop - token_start)
-          last = token_stop
-        }
-        if (last < stop) handle_token(Token.COMMENT1, last - start, stop - last)
-
-        handle_token(Token.END, line_segment.count, 0)
-        handler.setLineContext(context)
-        context
-      }
-    }
-  }
+  private val token_marker = Token_Markup.token_marker(session, buffer)
 
 
   /* activation */

--- a/src/Tools/jEdit/src/document_view.scala	Thu Jun 16 20:12:59 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Thu Jun 16 22:05:40 2011 +0200
@@ -386,10 +386,6 @@
                 val line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
                 if line_cmds.exists(changed)
               } text_area.invalidateScreenLineRange(line, line)
-
-              // FIXME danger of deadlock!?
-              // FIXME potentially slow!?
-              model.buffer.propertiesChanged()
             }
           }
 

--- a/src/Tools/jEdit/src/isabelle_markup.scala	Thu Jun 16 20:12:59 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Thu Jun 16 22:05:40 2011 +0200
@@ -12,7 +12,7 @@
 import java.awt.Color
 
 import org.lobobrowser.util.gui.ColorFactory
-import org.gjt.sp.jedit.syntax.Token
+import org.gjt.sp.jedit.syntax.{Token => JEditToken}
 
 
 object Isabelle_Markup
@@ -108,6 +108,14 @@
     case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
   }
 
+  /* FIXME update
+      Markup.ML_SOURCE -> COMMENT3,
+      Markup.DOC_SOURCE -> COMMENT3,
+      Markup.ANTIQ -> COMMENT4,
+      Markup.ML_ANTIQ -> COMMENT4,
+      Markup.DOC_ANTIQ -> COMMENT4,
+  */
+
   private val foreground_colors: Map[String, Color] =
     Map(
       Markup.TCLASS -> get_color("red"),
@@ -172,7 +180,7 @@
 
   private val command_style: Map[String, Byte] =
   {
-    import Token._
+    import JEditToken._
     Map[String, Byte](
       Keyword.THY_END -> KEYWORD2,
       Keyword.THY_SCRIPT -> LABEL,
@@ -182,39 +190,30 @@
     ).withDefaultValue(KEYWORD1)
   }
 
-  private val token_style: Map[String, Byte] =
+  private val token_style: Map[Token.Kind.Value, Byte] =
   {
-    import Token._
-    Map[String, Byte](
-      // embedded source text
-      Markup.ML_SOURCE -> COMMENT3,
-      Markup.DOC_SOURCE -> COMMENT3,
-      Markup.ANTIQ -> COMMENT4,
-      Markup.ML_ANTIQ -> COMMENT4,
-      Markup.DOC_ANTIQ -> COMMENT4,
-      // outer syntax
-      Markup.KEYWORD -> KEYWORD2,
-      Markup.OPERATOR -> OPERATOR,
-      Markup.COMMAND -> KEYWORD1,
-      Markup.IDENT -> NULL,
-      Markup.VERBATIM -> COMMENT3,
-      Markup.COMMENT -> COMMENT1,
-      Markup.CONTROL -> COMMENT3,
-      Markup.MALFORMED -> INVALID,
-      Markup.STRING -> LITERAL3,
-      Markup.ALTSTRING -> LITERAL1
+    import JEditToken._
+    Map[Token.Kind.Value, Byte](
+      Token.Kind.KEYWORD -> KEYWORD2,
+      Token.Kind.IDENT -> NULL,
+      Token.Kind.LONG_IDENT -> NULL,
+      Token.Kind.SYM_IDENT -> NULL,
+      Token.Kind.VAR -> NULL,
+      Token.Kind.TYPE_IDENT -> NULL,
+      Token.Kind.TYPE_VAR -> NULL,
+      Token.Kind.NAT -> NULL,
+      Token.Kind.FLOAT -> NULL,
+      Token.Kind.STRING -> LITERAL3,
+      Token.Kind.ALT_STRING -> LITERAL1,
+      Token.Kind.VERBATIM -> COMMENT3,
+      Token.Kind.SPACE -> NULL,
+      Token.Kind.COMMENT -> COMMENT1,
+      Token.Kind.UNPARSED -> INVALID
     ).withDefaultValue(NULL)
   }
 
-  def tokens(syntax: Outer_Syntax): Markup_Tree.Select[Byte] =
-  {
-    case Text.Info(_, XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _))
-    if syntax.keyword_kind(name).isDefined => command_style(syntax.keyword_kind(name).get)
-
-    case Text.Info(_, XML.Elem(Markup(Markup.ENTITY, Markup.Kind(kind)), _))
-    if token_style(kind) != Token.NULL => token_style(kind)
-
-    case Text.Info(_, XML.Elem(Markup(name, _), _))
-    if token_style(name) != Token.NULL => token_style(name)
-  }
+  def token_markup(syntax: Outer_Syntax, token: Token): Byte =
+    if (token.is_command)
+      command_style(syntax.keyword_kind(token.content).getOrElse(""))
+    else token_style(token.kind)
 }

--- a/src/Tools/jEdit/src/text_area_painter.scala	Thu Jun 16 20:12:59 2011 +0200
+++ b/src/Tools/jEdit/src/text_area_painter.scala	Thu Jun 16 22:05:40 2011 +0200
@@ -231,6 +231,7 @@
         else {
           var x1 = x + w
           for (Text.Info(range, info) <- markup) {
+            // FIXME range check!?
             val str = chunk.str.substring(range.start - chunk_offset, range.stop - chunk_offset)
             gfx.setColor(info.getOrElse(chunk_color))
             if (range.contains(caret_offset)) {

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/token_markup.scala	Thu Jun 16 22:05:40 2011 +0200
@@ -0,0 +1,75 @@
+/*  Title:      Tools/jEdit/src/token_markup.scala
+    Author:     Makarius
+
+Outer syntax token markup.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import org.gjt.sp.jedit.Buffer
+import org.gjt.sp.jedit.syntax.{Token => JToken, TokenMarker, TokenHandler, ParserRuleSet}
+import javax.swing.text.Segment
+
+
+object Token_Markup
+{
+  /* extended jEdit syntax styles */
+
+  private val plain_range: Int = JToken.ID_COUNT
+  private def check_range(i: Int) { require(0 <= i && i < plain_range) }
+
+  def subscript(i: Byte): Byte = { check_range(i); (i + plain_range).toByte }
+  def superscript(i: Byte): Byte = { check_range(i); (i + 2 * plain_range).toByte }
+  val hidden: Byte = (3 * plain_range).toByte
+
+
+  /* token marker */
+
+  private val isabelle_rules = new ParserRuleSet("isabelle", "MAIN")
+
+  private class Line_Context(val context: Scan.Context)
+    extends TokenMarker.LineContext(isabelle_rules, null)
+  {
+    override def hashCode: Int = context.hashCode
+    override def equals(that: Any): Boolean =
+      that match {
+        case other: Line_Context => context == other.context
+        case _ => false
+      }
+  }
+
+  def token_marker(session: Session, buffer: Buffer): TokenMarker =
+    new TokenMarker {
+      override def markTokens(context: TokenMarker.LineContext,
+          handler: TokenHandler, line: Segment): TokenMarker.LineContext =
+      {
+        Isabelle.swing_buffer_lock(buffer) {
+          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)
+
+          var offset = 0
+          for (token <- tokens) {
+            val style = Isabelle_Markup.token_markup(syntax, token)
+            val length = token.source.length
+            handler.handleToken(line, style, offset, length, context1)
+            offset += length
+          }
+          handler.handleToken(line, JToken.END, line.count, 0, context1)
+          handler.setLineContext(context1)
+          context1
+        }
+      }
+    }
+}
+