some direct text foreground painting, instead of token marking;
common snapshot for all text area painters (NOT gutter etc.)
tuned;

--- a/src/Tools/jEdit/src/document_view.scala	Mon Jun 13 14:22:33 2011 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Mon Jun 13 23:09:01 2011 +0200
@@ -62,7 +62,7 @@
 }
 
 
-class Document_View(val model: Document_Model, text_area: JEditTextArea)
+class Document_View(val model: Document_Model, val text_area: JEditTextArea)
 {
   private val session = model.session
 
@@ -207,7 +207,35 @@
   }
 
 
-  /* TextArea painters */
+  /* TextArea painting */
+
+  @volatile private var _text_area_snapshot: Option[Document.Snapshot] = None
+
+  def text_area_snapshot(): Document.Snapshot =
+    _text_area_snapshot match {
+      case Some(snapshot) => snapshot
+      case None => error("Missing text area snapshot")
+    }
+
+  private val set_snapshot = new TextAreaExtension
+  {
+    override def paintScreenLineRange(gfx: Graphics2D,
+      first_line: Int, last_line: Int, physical_lines: Array[Int],
+      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+    {
+      _text_area_snapshot = Some(model.snapshot())
+    }
+  }
+
+  private val reset_snapshot = new TextAreaExtension
+  {
+    override def paintScreenLineRange(gfx: Graphics2D,
+      first_line: Int, last_line: Int, physical_lines: Array[Int],
+      start: Array[Int], end: Array[Int], y: Int, line_height: Int)
+    {
+      _text_area_snapshot = None
+    }
+  }
 
   private val background_painter = new TextAreaExtension
   {
@@ -216,7 +244,7 @@
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
       Isabelle.swing_buffer_lock(model.buffer) {
-        val snapshot = model.snapshot()
+        val snapshot = text_area_snapshot()
         val ascent = text_area.getPainter.getFontMetrics.getAscent
 
         for (i <- 0 until physical_lines.length) {
@@ -310,7 +338,10 @@
     }
   }
 
-  val text_painter = new Text_Painter(model, text_area)
+  val text_painter = new Text_Painter(this)
+
+
+  /* Gutter painting */
 
   private val gutter_painter = new TextAreaExtension
   {
@@ -480,8 +511,12 @@
   private def activate()
   {
     val painter = text_area.getPainter
+
+    painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_snapshot)
     painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
     text_painter.activate()
+    painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_snapshot)
+
     text_area.getGutter.addExtension(gutter_painter)
     text_area.addFocusListener(focus_listener)
     text_area.getView.addWindowListener(window_listener)
@@ -495,6 +530,7 @@
   private def deactivate()
   {
     val painter = text_area.getPainter
+
     session.commands_changed -= main_actor
     session.global_settings -= main_actor
     text_area.removeFocusListener(focus_listener)
@@ -503,8 +539,11 @@
     text_area.removeCaretListener(caret_listener)
     text_area.removeLeftOfScrollBar(overview)
     text_area.getGutter.removeExtension(gutter_painter)
+
+    painter.removeExtension(reset_snapshot)
     text_painter.deactivate()
     painter.removeExtension(background_painter)
+    painter.removeExtension(set_snapshot)
     exit_popup()
   }
 }

--- a/src/Tools/jEdit/src/isabelle_markup.scala	Mon Jun 13 14:22:33 2011 +0200
+++ b/src/Tools/jEdit/src/isabelle_markup.scala	Mon Jun 13 23:09:01 2011 +0200
@@ -28,6 +28,10 @@
   val bad_color = new Color(255, 106, 106, 100)
   val hilite_color = new Color(255, 204, 102, 100)
 
+  val free_color = new Color(0, 0, 0xFF)
+  val skolem_color = new Color(0xD2, 0x69, 0x1E)
+  val bound_color = new Color(0, 0x8B, 0)
+
   class Icon(val priority: Int, val icon: javax.swing.Icon)
   {
     def >= (that: Icon): Boolean = this.priority >= that.priority
@@ -100,6 +104,13 @@
     case Text.Info(_, XML.Elem(Markup(Markup.TOKEN_RANGE, _), _)) => light_color
   }
 
+  val foreground: Markup_Tree.Select[Color] =
+  {
+    case Text.Info(_, XML.Elem(Markup(Markup.FREE, _), _)) => free_color
+    case Text.Info(_, XML.Elem(Markup(Markup.SKOLEM, _), _)) => skolem_color
+    case Text.Info(_, XML.Elem(Markup(Markup.BOUND, _), _)) => bound_color
+  }
+
   val tooltip: Markup_Tree.Select[String] =
   {
     case Text.Info(_, XML.Elem(Markup.Entity(kind, name), _)) => kind + " \"" + name + "\""
@@ -157,10 +168,10 @@
       Markup.DYNAMIC_FACT -> LABEL,
       // inner syntax
       Markup.TFREE -> NULL,
-      Markup.FREE -> MARKUP,
+      Markup.FREE -> NULL,
       Markup.TVAR -> NULL,
-      Markup.SKOLEM -> COMMENT2,
-      Markup.BOUND -> LABEL,
+      Markup.SKOLEM -> NULL,
+      Markup.BOUND -> NULL,
       Markup.VAR -> NULL,
       Markup.NUM -> DIGIT,
       Markup.FLOAT -> DIGIT,

--- a/src/Tools/jEdit/src/text_painter.scala	Mon Jun 13 14:22:33 2011 +0200
+++ b/src/Tools/jEdit/src/text_painter.scala	Mon Jun 13 23:09:01 2011 +0200
@@ -17,8 +17,10 @@
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
 
 
-class Text_Painter(model: Document_Model, text_area: JEditTextArea) extends TextAreaExtension
+class Text_Painter(doc_view: Document_View) extends TextAreaExtension
 {
+  private val text_area = doc_view.text_area
+
   private val orig_text_painter: TextAreaExtension =
   {
     val name = "org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText"
@@ -33,35 +35,56 @@
     first_line: Int, last_line: Int, physical_lines: Array[Int],
     start: Array[Int], end: Array[Int], y_start: Int, line_height: Int)
   {
-    def paint_chunk_list(head: Chunk, x: Float, y: Float): Float =
-    {
-      val clip_rect = gfx.getClipBounds
-      var w = 0.0f
-      var chunk = head
-      while (chunk != null) {
-        if (x + w + chunk.width > clip_rect.x &&
-            x + w < clip_rect.x + clip_rect.width &&
-            chunk.accessable && chunk.visible)
-        {
-          gfx.setFont(chunk.style.getFont)
-          gfx.setColor(chunk.style.getForegroundColor)
-          if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null)
-            gfx.drawGlyphVector(chunk.gv, x + w, y)
-          else if (chunk.str != null)
-            gfx.drawString(chunk.str, (x + w).toInt, y.toInt)
-        }
-        w += chunk.width
-        chunk = chunk.next.asInstanceOf[Chunk]
-      }
-      w
-    }
-
     val buffer = text_area.getBuffer
     Isabelle.swing_buffer_lock(buffer) {
       val painter = text_area.getPainter
       val font = painter.getFont
       val font_context = painter.getFontRenderContext
-      val fm = painter.getFontMetrics
+      val font_metrics = painter.getFontMetrics
+
+      def paint_chunk_list(head_offset: Text.Offset, head: Chunk, x: Float, y: Float): Float =
+      {
+        val clip_rect = gfx.getClipBounds
+
+        var w = 0.0f
+        var offset = head_offset
+        var chunk = head
+        while (chunk != null) {
+          val chunk_length = if (chunk.str == null) 0 else chunk.str.length
+
+          if (x + w + chunk.width > clip_rect.x &&
+              x + w < clip_rect.x + clip_rect.width &&
+              chunk.accessable && chunk.visible)
+          {
+            val chunk_range = Text.Range(offset, offset + chunk_length)
+            val chunk_font = chunk.style.getFont
+            val chunk_color = chunk.style.getForegroundColor
+
+            val markup =
+              doc_view.text_area_snapshot.select_markup(chunk_range)(Isabelle_Markup.foreground)
+
+            gfx.setFont(chunk_font)
+            if (!Debug.DISABLE_GLYPH_VECTOR && chunk.gv != null &&
+                markup.forall(info => info.info.isEmpty)) {
+              gfx.setColor(chunk_color)
+              gfx.drawGlyphVector(chunk.gv, x + w, y)
+            }
+            else {
+              var xpos = x + w
+              for (Text.Info(range, info) <- markup) {
+                val str = chunk.str.substring(range.start - offset, range.stop - offset)
+                gfx.setColor(info.getOrElse(chunk_color))
+                gfx.drawString(str, xpos.toInt, y.toInt)
+                xpos += chunk_font.getStringBounds(str, font_context).getWidth.toFloat
+              }
+            }
+          }
+          w += chunk.width
+          offset += chunk_length
+          chunk = chunk.next.asInstanceOf[Chunk]
+        }
+        w
+      }
 
       // see org.gjt.sp.jedit.textarea.TextArea.propertiesChanged
       // see org.gjt.sp.jedit.textarea.TextArea.setMaxLineLength
@@ -98,12 +121,14 @@
 
       val clip = gfx.getClip
       val x0 = text_area.getHorizontalOffset
-      var y0 = y_start + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
+      var y0 =
+        y_start + font_metrics.getHeight - (font_metrics.getLeading + 1) - font_metrics.getDescent
+
       for (i <- 0 until physical_lines.length) {
         if (physical_lines(i) != -1) {
           line_infos.get(start(i)) match {
             case Some(chunk) =>
-              val w = paint_chunk_list(chunk, x0, y0).toInt
+              val w = paint_chunk_list(start(i), chunk, x0, y0).toInt
               gfx.clipRect(x0 + w, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
               orig_text_painter.paintValidLine(gfx,
                 first_line + i, physical_lines(i), start(i), end(i), y_start + line_height * i)