# HG changeset patch
# User wenzelm
# Date 1348049469 -7200
# Node ID 98960e2fadd7d3ad0732b133f5d4a5906cc6f1c1
# Parent  0ae4216a17838121d5da761d1b1809d6bf780e2b# Parent  491363c6feb4dcd95d27d9d27e420c2abb745110
merged

diff -r 0ae4216a1783 -r 98960e2fadd7 Admin/isatest/settings/mac-poly-M2
--- a/Admin/isatest/settings/mac-poly-M2	Wed Sep 19 10:57:44 2012 +0200
+++ b/Admin/isatest/settings/mac-poly-M2	Wed Sep 19 12:11:09 2012 +0200
@@ -6,7 +6,7 @@
 
 ML_SYSTEM="polyml-5.5.0"
 ML_PLATFORM="x86-darwin"
-ML_HOME="/home/polyml/polyml-svn/$ML_PLATFORM"
+ML_HOME="/home/polyml/polyml-5.5.0/$ML_PLATFORM"
 ML_OPTIONS="-H 500"
 
 
diff -r 0ae4216a1783 -r 98960e2fadd7 Admin/isatest/settings/mac-poly-M4
--- a/Admin/isatest/settings/mac-poly-M4	Wed Sep 19 10:57:44 2012 +0200
+++ b/Admin/isatest/settings/mac-poly-M4	Wed Sep 19 12:11:09 2012 +0200
@@ -2,7 +2,7 @@
 
 init_components /home/isabelle/contrib "$HOME/admin/components/main"
 
-  POLYML_HOME="/home/polyml/polyml-svn"
+  POLYML_HOME="/home/polyml/polyml-5.5.0"
   ML_SYSTEM="polyml-5.5.0"
   ML_PLATFORM="x86-darwin"
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
diff -r 0ae4216a1783 -r 98960e2fadd7 Admin/isatest/settings/mac-poly-M8
--- a/Admin/isatest/settings/mac-poly-M8	Wed Sep 19 10:57:44 2012 +0200
+++ b/Admin/isatest/settings/mac-poly-M8	Wed Sep 19 12:11:09 2012 +0200
@@ -2,7 +2,7 @@
 
 init_components /home/isabelle/contrib "$HOME/admin/components/main"
 
-  POLYML_HOME="/home/polyml/polyml-svn"
+  POLYML_HOME="/home/polyml/polyml-5.5.0"
   ML_SYSTEM="polyml-5.5.0"
   ML_PLATFORM="x86-darwin"
   ML_HOME="$POLYML_HOME/$ML_PLATFORM"
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Pure/General/position.scala
--- a/src/Pure/General/position.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/General/position.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -20,6 +20,12 @@
   val File = new Properties.String(Isabelle_Markup.FILE)
   val Id = new Properties.Long(Isabelle_Markup.ID)
 
+  val Def_Line = new Properties.Int(Isabelle_Markup.DEF_LINE)
+  val Def_Offset = new Properties.Int(Isabelle_Markup.DEF_OFFSET)
+  val Def_End_Offset = new Properties.Int(Isabelle_Markup.DEF_END_OFFSET)
+  val Def_File = new Properties.String(Isabelle_Markup.DEF_FILE)
+  val Def_Id = new Properties.Long(Isabelle_Markup.DEF_ID)
+
   object Line_File
   {
     def unapply(pos: T): Option[(Int, String)] =
@@ -30,6 +36,16 @@
       }
   }
 
+  object Def_Line_File
+  {
+    def unapply(pos: T): Option[(Int, String)] =
+      (pos, pos) match {
+        case (Def_Line(i), Def_File(name)) => Some((i, name))
+        case (_, Def_File(name)) => Some((1, name))
+        case _ => None
+      }
+  }
+
   object Range
   {
     def apply(range: Text.Range): T = Offset(range.start) ++ Offset(range.stop)
@@ -50,6 +66,15 @@
       }
   }
 
+  object Def_Id_Offset
+  {
+    def unapply(pos: T): Option[(Long, Text.Offset)] =
+      (pos, pos) match {
+        case (Def_Id(id), Def_Offset(offset)) => Some((id, offset))
+        case _ => None
+      }
+  }
+
   object Id_Range
   {
     def unapply(pos: T): Option[(Long, Text.Range)] =
@@ -59,16 +84,7 @@
       }
   }
 
-  private val purge_pos = Map(
-    Isabelle_Markup.DEF_LINE -> Isabelle_Markup.LINE,
-    Isabelle_Markup.DEF_OFFSET -> Isabelle_Markup.OFFSET,
-    Isabelle_Markup.DEF_END_OFFSET -> Isabelle_Markup.END_OFFSET,
-    Isabelle_Markup.DEF_FILE -> Isabelle_Markup.FILE,
-    Isabelle_Markup.DEF_ID -> Isabelle_Markup.ID)
-
-  def purge(props: T): T =
-    for ((x, y) <- props if !Isabelle_Markup.POSITION_PROPERTIES(x))
-      yield (if (purge_pos.isDefinedAt(x)) (purge_pos(x), y) else (x, y))
+  def purge(props: T): T = props.filterNot(p => Isabelle_Markup.POSITION_PROPERTIES(p._1))
 
 
   /* here: inlined formal markup */
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Pure/General/pretty.scala
--- a/src/Pure/General/pretty.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/General/pretty.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -146,7 +146,7 @@
 
   def string_of(input: XML.Body, margin: Int = margin_default,
       metric: String => Double = metric_default): String =
-    formatted(input, margin, metric).iterator.flatMap(XML.content).mkString
+    XML.content(formatted(input, margin, metric))
 
 
   /* unformatted output */
@@ -164,6 +164,5 @@
     input.flatMap(standard_format).flatMap(fmt)
   }
 
-  def str_of(input: XML.Body): String =
-    unformatted(input).iterator.flatMap(XML.content).mkString
+  def str_of(input: XML.Body): String = XML.content(unformatted(input))
 }
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Pure/PIDE/blob.scala
--- a/src/Pure/PIDE/blob.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/PIDE/blob.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -24,5 +24,5 @@
   def decode(i: Text.Offset): Text.Offset = symbol_index.decode(i)
   def decode(r: Text.Range): Text.Range = symbol_index.decode(r)
 
-  val empty_state: Blob.State = Blob.State(this)
+  val init_state: Blob.State = Blob.State(this)
 }
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -60,10 +60,13 @@
         case XML.Elem(Markup(name, atts), body) =>
           atts match {
             case Isabelle_Markup.Serial(i) =>
-              val result = XML.Elem(Markup(name, Position.purge(atts)), body)
-              val st0 = copy(results = results + (i -> result))
+              val props = Position.purge(atts)
+              val result = XML.Elem(Markup(name, props), body)
+              val result_message = XML.Elem(Markup(Isabelle_Markup.message(name), props), body)
+
+              val st0 = copy(results = results + (i -> result_message))
               val st1 =
-                if (Protocol.is_tracing(message)) st0
+                if (Protocol.is_tracing(result)) st0
                 else
                   (st0 /: Protocol.message_positions(command, message))(
                     (st, range) => st.add_markup(Text.Info(range, result)))
@@ -79,7 +82,8 @@
 
   type Span = List[Token]
 
-  def apply(id: Document.Command_ID, node_name: Document.Node.Name, span: Span): Command =
+  def apply(id: Document.Command_ID, node_name: Document.Node.Name,
+    span: Span, markup: Markup_Tree): Command =
   {
     val source: String =
       span match {
@@ -96,13 +100,21 @@
       i += n
     }
 
-    new Command(id, node_name, span1.toList, source)
+    new Command(id, node_name, span1.toList, source, markup)
   }
 
-  def unparsed(source: String): Command =
-    Command(Document.no_id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)))
+  val empty = Command(Document.no_id, Document.Node.Name.empty, Nil, Markup_Tree.empty)
+
+  def unparsed(id: Document.Command_ID, source: String, markup: Markup_Tree): Command =
+    Command(id, Document.Node.Name.empty, List(Token(Token.Kind.UNPARSED, source)), markup)
 
-  val empty = Command(Document.no_id, Document.Node.Name.empty, Nil)
+  def unparsed(source: String): Command = unparsed(Document.no_id, source, Markup_Tree.empty)
+
+  def rich_text(id: Document.Command_ID, body: XML.Body): Command =
+  {
+    val (text, markup) = XML.content_markup(body)
+    unparsed(id, text, markup)
+  }
 
 
   /* perspective */
@@ -131,7 +143,8 @@
     val id: Document.Command_ID,
     val node_name: Document.Node.Name,
     val span: Command.Span,
-    val source: String)
+    val source: String,
+    val init_markup: Markup_Tree)
 {
   /* classification */
 
@@ -167,5 +180,5 @@
 
   /* accumulated results */
 
-  val empty_state: Command.State = Command.State(this)
+  val init_state: Command.State = Command.State(this, markup = init_markup)
 }
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -350,7 +350,7 @@
     def define_command(command: Command): State =
     {
       val id = command.id
-      copy(commands = commands + (id -> command.empty_state))
+      copy(commands = commands + (id -> command.init_state))
     }
 
     def defined_command(id: Command_ID): Boolean = commands.isDefinedAt(id)
@@ -474,7 +474,7 @@
       catch {
         case _: State.Fail =>
           try { the_command_state(command.id) }
-          catch { case _: State.Fail => command.empty_state }
+          catch { case _: State.Fail => command.init_state }
       }
     }
 
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Pure/PIDE/isabelle_markup.scala
--- a/src/Pure/PIDE/isabelle_markup.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/PIDE/isabelle_markup.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -231,6 +231,16 @@
   val STDERR = "stderr"
   val EXIT = "exit"
 
+  val WRITELN_MESSAGE = "writeln_message"
+  val TRACING_MESSAGE = "tracing_message"
+  val WARNING_MESSAGE = "warning_message"
+  val ERROR_MESSAGE = "error_message"
+
+  val message: String => String =
+    Map(WRITELN -> WRITELN_MESSAGE, TRACING -> TRACING_MESSAGE,
+        WARNING -> WARNING_MESSAGE, ERROR -> ERROR_MESSAGE)
+      .withDefault((name: String) => name + "_message")
+
   val Return_Code = new Properties.Int("return_code")
 
   val LEGACY = "legacy"
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Pure/PIDE/markup_tree.scala
--- a/src/Pure/PIDE/markup_tree.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/PIDE/markup_tree.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -35,23 +35,30 @@
       else copy(rev_markup = info :: rev_markup, elements = elements + info.markup.name)
 
     def markup: List[XML.Elem] = rev_markup.reverse
+
+    def reverse_markup: Entry =
+      copy(rev_markup = rev_markup.reverse, subtree = subtree.reverse_markup)
   }
 
   object Branches
   {
     type T = SortedMap[Text.Range, Entry]
     val empty: T = SortedMap.empty(Text.Range.Ordering)
+
+    def reverse_markup(branches: T): T =
+      (empty /: branches.iterator) { case (bs, (r, entry)) => bs + (r -> entry.reverse_markup) }
   }
 }
 
 
 final class Markup_Tree private(branches: Markup_Tree.Branches.T)
 {
+  import Markup_Tree._
+
   private def this(branches: Markup_Tree.Branches.T, entry: Markup_Tree.Entry) =
     this(branches + (entry.range -> entry))
 
-
-  import Markup_Tree._
+  def reverse_markup: Markup_Tree = new Markup_Tree(Branches.reverse_markup(branches))
 
   override def toString =
     branches.toList.map(_._2) match {
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/PIDE/protocol.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -135,18 +135,21 @@
  def is_tracing(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true
+      case XML.Elem(Markup(Isabelle_Markup.TRACING_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_warning(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Isabelle_Markup.WARNING, _), _) => true
+      case XML.Elem(Markup(Isabelle_Markup.WARNING_MESSAGE, _), _) => true
       case _ => false
     }
 
   def is_error(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Isabelle_Markup.ERROR, _), _) => true
+      case XML.Elem(Markup(Isabelle_Markup.ERROR_MESSAGE, _), _) => true
       case _ => false
     }
 
@@ -154,6 +157,8 @@
     msg match {
       case XML.Elem(Markup(Isabelle_Markup.WRITELN, _),
         List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
+      case XML.Elem(Markup(Isabelle_Markup.WRITELN_MESSAGE, _),
+        List(XML.Elem(Markup(Isabelle_Markup.STATE, _), _))) => true
       case _ => false
     }
 
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Pure/PIDE/xml.scala
--- a/src/Pure/PIDE/xml.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/PIDE/xml.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -12,8 +12,6 @@
 import java.lang.ref.WeakReference
 import javax.xml.parsers.DocumentBuilderFactory
 
-import scala.collection.mutable
-
 
 object XML
 {
@@ -71,18 +69,32 @@
   def string_of_tree(tree: XML.Tree): String = string_of_body(List(tree))
 
 
-  /* text content */
+  /* content -- text and markup */
+
+  private def make_content(body: Body, record_markup: Boolean): (String, Markup_Tree) =
+  {
+    var text = new StringBuilder
+    var markup_tree = Markup_Tree.empty
 
-  def content_stream(tree: Tree): Stream[String] =
-    tree match {
-      case Elem(_, body) => content_stream(body)
-      case Text(content) => Stream(content)
-    }
-  def content_stream(body: Body): Stream[String] =
-    body.toStream.flatten(content_stream(_))
+    def traverse(tree: Tree): Unit =
+      tree match {
+        case Elem(markup, trees) =>
+          val offset = text.length
+          trees.foreach(traverse)
+          val end_offset = text.length
+          if (record_markup)
+            markup_tree +=
+              isabelle.Text.Info(isabelle.Text.Range(offset, end_offset), Elem(markup, Nil))
+        case Text(s) => text.append(s)
+      }
 
-  def content(tree: Tree): Iterator[String] = content_stream(tree).iterator
-  def content(body: Body): Iterator[String] = content_stream(body).iterator
+    body.foreach(traverse)
+    (text.toString, markup_tree.reverse_markup)
+  }
+
+  def content_markup(body: Body): (String, Markup_Tree) = make_content(body, true)
+  def content(body: Body): String = make_content(body, false)._1
+  def content(tree: Tree): String = make_content(List(tree), false)._1
 
 
 
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/System/session.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -125,7 +125,7 @@
   /* global state */
 
   private val syslog = Volatile(Queue.empty[XML.Elem])
-  def current_syslog(): String = cat_lines(syslog().iterator.map(msg => XML.content(msg).mkString))
+  def current_syslog(): String = cat_lines(syslog().iterator.map(XML.content))
 
   @volatile private var _phase: Session.Phase = Session.Inactive
   private def phase_=(new_phase: Session.Phase)
@@ -311,7 +311,7 @@
           }
 
         case Isabelle_Markup.Assign_Execs if output.is_protocol =>
-          XML.content(output.body).mkString match {
+          XML.content(output.body) match {
             case Protocol.Assign(id, assign) =>
               try {
                 val cmds = global_state >>> (_.assign(id, assign))
@@ -328,7 +328,7 @@
           }
 
         case Isabelle_Markup.Removed_Versions if output.is_protocol =>
-          XML.content(output.body).mkString match {
+          XML.content(output.body) match {
             case Protocol.Removed(removed) =>
               try {
                 global_state >> (_.removed_versions(removed))
@@ -339,7 +339,7 @@
 
         case Isabelle_Markup.Invoke_Scala(name, id) if output.is_protocol =>
           Future.fork {
-            val arg = XML.content(output.body).mkString
+            val arg = XML.content(output.body)
             val (tag, res) = Invoke_Scala.method(name, arg)
             prover.get.invoke_scala(id, tag, res)
           }
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -68,7 +68,7 @@
       /* result structure */
 
       val spans = parse_spans(syntax.scan(text))
-      spans.foreach(span => add(Command(Document.no_id, node_name, span)))
+      spans.foreach(span => add(Command(Document.no_id, node_name, span, Markup_Tree.empty)))
       result()
     }
   }
@@ -226,7 +226,7 @@
         commands
       case cmd :: _ =>
         val hook = commands.prev(cmd)
-        val inserted = spans2.map(span => Command(Document.new_id(), name, span))
+        val inserted = spans2.map(span => Command(Document.new_id(), name, span, Markup_Tree.empty))
         (commands /: cmds2)(_ - _).append_after(hook, inserted)
     }
   }
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Tools/jEdit/etc/isabelle-jedit.css
--- a/src/Tools/jEdit/etc/isabelle-jedit.css	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/etc/isabelle-jedit.css	Wed Sep 19 12:11:09 2012 +0200
@@ -2,10 +2,10 @@
 
 .message { margin-top: 0.3ex; background-color: #F0F0F0; }
 
-.writeln { }
-.tracing { background-color: #F0F8FF; }
-.warning { background-color: #EEE8AA; }
-.error { background-color: #FFC1C1; }
+.writeln_message { }
+.tracing_message { background-color: #F0F8FF; }
+.warning_message { background-color: #EEE8AA; }
+.error_message { background-color: #FFC1C1; }
 
 .report { display: none; }
 
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/etc/options	Wed Sep 19 12:11:09 2012 +0200
@@ -31,6 +31,10 @@
 option warning_color : string = "FF8C00FF"
 option error_color : string = "B22222FF"
 option error1_color : string = "B2222232"
+option writeln_message_color : string = "F0F0F0FF"
+option tracing_message_color : string = "F0F8FFFF"
+option warning_message_color : string = "EEE8AAFF"
+option error_message_color : string = "FFC1C1FF"
 option bad_color : string = "FF6A6A64"
 option intensify_color : string = "FFCC6664"
 option quoted_color : string = "8B8B8B19"
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Wed Sep 19 12:11:09 2012 +0200
@@ -18,6 +18,7 @@
   "src/isabelle_options.scala"
   "src/isabelle_rendering.scala"
   "src/isabelle_sidekick.scala"
+  "src/jedit_lib.scala"
   "src/jedit_thy_load.scala"
   "src/jedit_options.scala"
   "src/output_dockable.scala"
@@ -27,10 +28,10 @@
   "src/protocol_dockable.scala"
   "src/raw_output_dockable.scala"
   "src/readme_dockable.scala"
+  "src/rich_text_area.scala"
   "src/scala_console.scala"
   "src/session_dockable.scala"
   "src/syslog_dockable.scala"
-  "src/text_area_painter.scala"
   "src/text_overview.scala"
   "src/token_markup.scala"
 )
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -66,7 +66,7 @@
   def node_header(): Document.Node.Header =
   {
     Swing_Thread.require()
-    Isabelle.buffer_lock(buffer) {
+    JEdit_Lib.buffer_lock(buffer) {
       Exn.capture {
         Isabelle.thy_load.check_thy_text(name, buffer.getSegment(0, buffer.getLength))
       } match {
@@ -92,24 +92,6 @@
   }
 
 
-
-  /* point range */
-
-  def point_range(offset: Text.Offset): Text.Range =
-    Isabelle.buffer_lock(buffer) {
-      def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
-      try {
-        val c = text(offset)
-        if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
-          Text.Range(offset, offset + 2)
-        else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
-          Text.Range(offset - 1, offset + 1)
-        else Text.Range(offset, offset + 1)
-      }
-      catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
-    }
-
-
   /* pending text edits */
 
   private object pending_edits  // owned by Swing thread
@@ -151,7 +133,7 @@
     def init()
     {
       flush()
-      session.init_node(name, node_header(), perspective(), Isabelle.buffer_text(buffer))
+      session.init_node(name, node_header(), perspective(), JEdit_Lib.buffer_text(buffer))
     }
 
     def exit()
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/document_view.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -17,13 +17,9 @@
 import java.lang.System
 import java.text.BreakIterator
 import java.awt.{Color, Graphics2D, Point}
-import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
-  FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
 import javax.swing.event.{CaretListener, CaretEvent}
 
-import org.gjt.sp.util.Log
-
-import org.gjt.sp.jedit.{jEdit, OperatingSystem, Debug}
+import org.gjt.sp.jedit.{jEdit, Debug}
 import org.gjt.sp.jedit.gui.RolloverButton
 import org.gjt.sp.jedit.options.GutterOptionPane
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
@@ -71,46 +67,10 @@
 {
   private val session = model.session
 
-
-  /* robust extension body */
-
-  def robust_body[A](default: A)(body: => A): A =
-  {
-    try {
-      Swing_Thread.require()
-      if (model.buffer == text_area.getBuffer) body
-      else {
-        Log.log(Log.ERROR, this, ERROR("Inconsistent document model"))
-        default
-      }
-    }
-    catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
-  }
-
-
-  /* visible text range */
+  def get_rendering(): Isabelle_Rendering =
+    Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
 
-  // NB: TextArea.getScreenLineEndOffset of last line is beyond Buffer.getLength
-  def proper_line_range(start: Text.Offset, end: Text.Offset): Text.Range =
-    Text.Range(start, end min model.buffer.getLength)
-
-  def visible_range(): Option[Text.Range] =
-  {
-    val n = text_area.getVisibleLines
-    if (n > 0) {
-      val start = text_area.getScreenLineStartOffset(0)
-      val raw_end = text_area.getScreenLineEndOffset(n - 1)
-      Some(proper_line_range(start, if (raw_end >= 0) raw_end else model.buffer.getLength))
-    }
-    else None
-  }
-
-  def invalidate_range(range: Text.Range)
-  {
-    text_area.invalidateLineRange(
-      model.buffer.getLineOfOffset(range.start),
-      model.buffer.getLineOfOffset(range.stop))
-  }
+  val rich_text_area = new Rich_Text_Area(text_area.getView, text_area, get_rendering _)
 
 
   /* perspective */
@@ -137,101 +97,13 @@
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
+      // no robust_body
       model.update_perspective()
     }
   }
 
 
-  /* active areas within the text */
-
-  private class Active_Area[A](
-    rendering: Isabelle_Rendering => Text.Range => Option[Text.Info[A]])
-  {
-    private var the_info: Option[Text.Info[A]] = None
-
-    def info: Option[Text.Info[A]] = the_info
-
-    def update(new_info: Option[Text.Info[A]])
-    {
-      val old_info = the_info
-      if (new_info != old_info) {
-        for { opt <- List(old_info, new_info); Text.Info(range, _) <- opt }
-          invalidate_range(range)
-        the_info = new_info
-      }
-    }
-
-    def update_rendering(r: Isabelle_Rendering, range: Text.Range)
-    { update(rendering(r)(range)) }
-
-    def reset { update(None) }
-  }
-
-  // owned by Swing thread
-
-  private var control: Boolean = false
-
-  private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
-  def highlight_info(): Option[Text.Info[Color]] = highlight_area.info
-
-  private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
-  def hyperlink_info(): Option[Text.Info[Hyperlink]] = hyperlink_area.info
-
-  private val active_areas = List(highlight_area, hyperlink_area)
-  private def active_reset(): Unit = active_areas.foreach(_.reset)
-
-  private val focus_listener = new FocusAdapter {
-    override def focusLost(e: FocusEvent) { active_reset() }
-  }
-
-  private val window_listener = new WindowAdapter {
-    override def windowIconified(e: WindowEvent) { active_reset() }
-    override def windowDeactivated(e: WindowEvent) { active_reset() }
-  }
-
-  private val mouse_listener = new MouseAdapter {
-    override def mouseClicked(e: MouseEvent) {
-      hyperlink_area.info match {
-        case Some(Text.Info(range, link)) => link.follow(text_area.getView)
-        case None =>
-      }
-    }
-  }
-
-  private val mouse_motion_listener = new MouseMotionAdapter {
-    override def mouseMoved(e: MouseEvent) {
-      control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
-      if (control && model.buffer.isLoaded) {
-        Isabelle.buffer_lock(model.buffer) {
-          val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
-          val mouse_range = model.point_range(text_area.xyToOffset(e.getX(), e.getY()))
-          active_areas.foreach(_.update_rendering(rendering, mouse_range))
-        }
-      }
-      else active_reset()
-    }
-  }
-
-
-  /* text area painting */
-
-  private val text_area_painter = new Text_Area_Painter(this)
-
-  private val tooltip_painter = new TextAreaExtension
-  {
-    override def getToolTipText(x: Int, y: Int): String =
-    {
-      robust_body(null: String) {
-        val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
-        val offset = text_area.xyToOffset(x, y)
-        val range = Text.Range(offset, offset + 1)
-        val tip =
-          if (control) rendering.tooltip(range)
-          else rendering.tooltip_message(range)
-        tip.map(Isabelle.tooltip(_)) getOrElse null
-      }
-    }
-  }
+  /* gutter */
 
   private val gutter_painter = new TextAreaExtension
   {
@@ -239,7 +111,7 @@
       first_line: Int, last_line: Int, physical_lines: Array[Int],
       start: Array[Int], end: Array[Int], y: Int, line_height: Int)
     {
-      robust_body(()) {
+      rich_text_area.robust_body(()) {
         Swing_Thread.assert()
 
         val gutter = text_area.getGutter
@@ -248,12 +120,13 @@
         val FOLD_MARKER_SIZE = 12
 
         if (gutter.isSelectionAreaEnabled && !gutter.isExpanded && width >= 12 && line_height >= 12) {
-          Isabelle.buffer_lock(model.buffer) {
-            val rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
+          val buffer = model.buffer
+          JEdit_Lib.buffer_lock(buffer) {
+            val rendering = get_rendering()
 
             for (i <- 0 until physical_lines.length) {
               if (physical_lines(i) != -1) {
-                val line_range = proper_line_range(start(i), end(i))
+                val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
 
                 // gutter icons
                 rendering.gutter_message(line_range) match {
@@ -308,7 +181,7 @@
         case changed: Session.Commands_Changed =>
           val buffer = model.buffer
           Swing_Thread.later {
-            Isabelle.buffer_lock(buffer) {
+            JEdit_Lib.buffer_lock(buffer) {
               if (model.buffer == text_area.getBuffer) {
                 val snapshot = model.snapshot()
 
@@ -317,9 +190,9 @@
                      changed.commands.exists(snapshot.node.commands.contains)))
                   Swing_Thread.later { overview.delay_repaint.invoke() }
 
-                visible_range() match {
+                JEdit_Lib.visible_range(text_area) match {
                   case Some(visible) =>
-                    if (changed.assignment) invalidate_range(visible)
+                    if (changed.assignment) JEdit_Lib.invalidate_range(text_area, visible)
                     else {
                       val visible_cmds =
                         snapshot.node.command_range(snapshot.revert(visible)).map(_._1)
@@ -328,7 +201,7 @@
                           line <- 0 until text_area.getVisibleLines
                           start = text_area.getScreenLineStartOffset(line) if start >= 0
                           end = text_area.getScreenLineEndOffset(line) if end >= 0
-                          range = proper_line_range(start, end)
+                          range = JEdit_Lib.proper_line_range(buffer, start, end)
                           line_cmds = snapshot.node.command_range(snapshot.revert(range)).map(_._1)
                           if line_cmds.exists(changed.commands)
                         } text_area.invalidateScreenLineRange(line, line)
@@ -351,14 +224,10 @@
   private def activate()
   {
     val painter = text_area.getPainter
+
     painter.addExtension(TextAreaPainter.LOWEST_LAYER, update_perspective)
-    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
-    text_area_painter.activate()
+    rich_text_area.activate()
     text_area.getGutter.addExtension(gutter_painter)
-    text_area.addFocusListener(focus_listener)
-    text_area.getView.addWindowListener(window_listener)
-    painter.addMouseListener(mouse_listener)
-    painter.addMouseMotionListener(mouse_motion_listener)
     text_area.addCaretListener(caret_listener)
     text_area.addLeftOfScrollBar(overview)
     session.raw_edits += main_actor
@@ -368,17 +237,13 @@
   private def deactivate()
   {
     val painter = text_area.getPainter
+
     session.raw_edits -= main_actor
     session.commands_changed -= main_actor
-    text_area.removeFocusListener(focus_listener)
-    text_area.getView.removeWindowListener(window_listener)
-    painter.removeMouseMotionListener(mouse_motion_listener)
-    painter.removeMouseListener(mouse_listener)
     text_area.removeCaretListener(caret_listener); delay_caret_update.revoke()
     text_area.removeLeftOfScrollBar(overview); overview.delay_repaint.revoke()
     text_area.getGutter.removeExtension(gutter_painter)
-    text_area_painter.deactivate()
-    painter.removeExtension(tooltip_painter)
+    rich_text_area.deactivate()
     painter.removeExtension(update_perspective)
   }
 }
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Tools/jEdit/src/hyperlink.scala
--- a/src/Tools/jEdit/src/hyperlink.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/hyperlink.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -31,7 +31,7 @@
   {
     Swing_Thread.require()
 
-    Isabelle.jedit_buffer(jedit_file) match {
+    JEdit_Lib.jedit_buffer(jedit_file) match {
       case Some(buffer) =>
         view.goToBuffer(buffer)
         val text_area = view.getTextArea
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Tools/jEdit/src/isabelle_rendering.scala
--- a/src/Tools/jEdit/src/isabelle_rendering.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_rendering.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -14,6 +14,8 @@
 import java.io.{File => JFile}
 
 import org.gjt.sp.jedit.syntax.{Token => JEditToken}
+import org.gjt.sp.jedit.GUIUtilities
+import org.gjt.sp.util.Log
 
 import scala.collection.immutable.SortedMap
 
@@ -24,17 +26,28 @@
     new Isabelle_Rendering(snapshot, options)
 
 
-  /* physical rendering */
+  /* message priorities */
 
   private val writeln_pri = 1
   private val warning_pri = 2
   private val legacy_pri = 3
   private val error_pri = 4
 
+
+  /* icons */
+
+  private def load_icon(name: String): Icon =
+  {
+    val icon = GUIUtilities.loadIcon(name)
+    if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
+      Log.log(Log.ERROR, icon, "Bad icon: " + name)
+    icon
+  }
+
   private val gutter_icons = Map(
-    warning_pri -> Isabelle.load_icon("16x16/status/dialog-information.png"),
-    legacy_pri -> Isabelle.load_icon("16x16/status/dialog-warning.png"),
-    error_pri -> Isabelle.load_icon("16x16/status/dialog-error.png"))
+    warning_pri -> load_icon("16x16/status/dialog-information.png"),
+    legacy_pri -> load_icon("16x16/status/dialog-warning.png"),
+    error_pri -> load_icon("16x16/status/dialog-error.png"))
 
 
   /* token markup -- text styles */
@@ -96,6 +109,10 @@
   val warning_color = color_value("warning_color")
   val error_color = color_value("error_color")
   val error1_color = color_value("error1_color")
+  val writeln_message_color = color_value("writeln_message_color")
+  val tracing_message_color = color_value("tracing_message_color")
+  val warning_message_color = color_value("warning_message_color")
+  val error_message_color = color_value("error_message_color")
   val bad_color = color_value("bad_color")
   val intensify_color = color_value("intensify_color")
   val quoted_color = color_value("quoted_color")
@@ -189,7 +206,7 @@
               case _ => false }).isEmpty) =>
 
             props match {
-              case Position.Line_File(line, name) if Path.is_ok(name) =>
+              case Position.Def_Line_File(line, name) if Path.is_ok(name) =>
                 Isabelle_System.source_file(Path.explode(name)) match {
                   case Some(path) =>
                     val jedit_file = Isabelle_System.platform_path(path)
@@ -197,7 +214,7 @@
                   case None => links
                 }
 
-              case Position.Id_Offset(id, offset) if !snapshot.is_outdated =>
+              case Position.Def_Id_Offset(id, offset) =>
                 snapshot.state.find_command(snapshot.version, id) match {
                   case Some((node, command)) =>
                     val sources =
@@ -346,11 +363,21 @@
         Text.Info(r, result) <-
           snapshot.cumulate_markup[(Option[Protocol.Status], Option[Color])](
             range, (Some(Protocol.Status.init), None),
-            Some(Protocol.command_status_markup + Isabelle_Markup.BAD + Isabelle_Markup.INTENSIFY),
+            Some(Protocol.command_status_markup + Isabelle_Markup.WRITELN_MESSAGE +
+              Isabelle_Markup.TRACING_MESSAGE + Isabelle_Markup.WARNING_MESSAGE +
+              Isabelle_Markup.ERROR_MESSAGE + Isabelle_Markup.BAD + Isabelle_Markup.INTENSIFY),
             {
               case (((Some(status), color), Text.Info(_, XML.Elem(markup, _))))
               if (Protocol.command_status_markup(markup.name)) =>
                 (Some(Protocol.command_status(status, markup)), color)
+              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WRITELN_MESSAGE, _), _))) =>
+                (None, Some(writeln_message_color))
+              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.TRACING_MESSAGE, _), _))) =>
+                (None, Some(tracing_message_color))
+              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.WARNING_MESSAGE, _), _))) =>
+                (None, Some(warning_message_color))
+              case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.ERROR_MESSAGE, _), _))) =>
+                (None, Some(error_message_color))
               case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.BAD, _), _))) =>
                 (None, Some(bad_color))
               case (_, Text.Info(_, XML.Elem(Markup(Isabelle_Markup.INTENSIFY, _), _))) =>
@@ -387,6 +414,7 @@
 
 
   private val text_colors: Map[String, Color] = Map(
+      Isabelle_Markup.COMMAND -> keyword1_color,
       Isabelle_Markup.STRING -> Color.BLACK,
       Isabelle_Markup.ALTSTRING -> Color.BLACK,
       Isabelle_Markup.VERBATIM -> Color.BLACK,
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -91,7 +91,7 @@
     Swing_Thread.assert()
 
     val buffer = pane.getBuffer
-    Isabelle.buffer_lock(buffer) {
+    JEdit_Lib.buffer_lock(buffer) {
       get_syntax match {
         case None => null
         case Some(syntax) =>
@@ -166,7 +166,7 @@
 
     node_name(buffer) match {
       case Some(name) =>
-        val text = Isabelle.buffer_text(buffer)
+        val text = JEdit_Lib.buffer_text(buffer)
         val structure = Structure.parse(syntax, name, text)
         make_tree(0, structure) foreach (node => data.root.add(node))
         true
@@ -177,15 +177,15 @@
 
 
 class Isabelle_Sidekick_Default extends Isabelle_Sidekick_Structure(
-  "isabelle", Isabelle.get_recent_syntax, Isabelle.buffer_node_name)
+  "isabelle", Isabelle.get_recent_syntax, JEdit_Lib.buffer_node_name)
 
 
 class Isabelle_Sidekick_Options extends Isabelle_Sidekick_Structure(
-  "isabelle-options", Some(Options.options_syntax), Isabelle.buffer_node_dummy)
+  "isabelle-options", Some(Options.options_syntax), JEdit_Lib.buffer_node_dummy)
 
 
 class Isabelle_Sidekick_Root extends Isabelle_Sidekick_Structure(
-  "isabelle-root", Some(Build.root_syntax), Isabelle.buffer_node_dummy)
+  "isabelle-root", Some(Build.root_syntax), JEdit_Lib.buffer_node_dummy)
 
 
 class Isabelle_Sidekick_Raw
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Tools/jEdit/src/jedit_lib.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/jedit_lib.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -0,0 +1,148 @@
+/*  Title:      Tools/jEdit/src/jedit_lib.scala
+    Author:     Makarius
+
+Misc library functions for jEdit.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+
+import org.gjt.sp.jedit.{jEdit, Buffer, View}
+import org.gjt.sp.jedit.buffer.JEditBuffer
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
+
+
+object JEdit_Lib
+{
+  /* buffers */
+
+  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
+    Swing_Thread.now { buffer_lock(buffer) { body } }
+
+  def buffer_text(buffer: JEditBuffer): String =
+    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
+
+  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
+
+  def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
+    Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))
+
+  def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
+  {
+    val name = buffer_name(buffer)
+    Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
+  }
+
+
+  /* main jEdit components */
+
+  def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
+
+  def jedit_buffer(name: String): Option[Buffer] =
+    jedit_buffers().find(buffer => buffer_name(buffer) == name)
+
+  def jedit_views(): Iterator[View] = jEdit.getViews().iterator
+
+  def jedit_text_areas(view: View): Iterator[JEditTextArea] =
+    view.getEditPanes().iterator.map(_.getTextArea)
+
+  def jedit_text_areas(): Iterator[JEditTextArea] =
+    jedit_views().flatMap(jedit_text_areas(_))
+
+  def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
+    jedit_text_areas().filter(_.getBuffer == buffer)
+
+  def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
+  {
+    try { buffer.readLock(); body }
+    finally { buffer.readUnlock() }
+  }
+
+
+  /* point range */
+
+  def point_range(buffer: JEditBuffer, offset: Text.Offset): Text.Range =
+    buffer_lock(buffer) {
+      def text(i: Text.Offset): Char = buffer.getText(i, 1).charAt(0)
+      try {
+        val c = text(offset)
+        if (Character.isHighSurrogate(c) && Character.isLowSurrogate(text(offset + 1)))
+          Text.Range(offset, offset + 2)
+        else if (Character.isLowSurrogate(c) && Character.isHighSurrogate(text(offset - 1)))
+          Text.Range(offset - 1, offset + 1)
+        else Text.Range(offset, offset + 1)
+      }
+      catch { case _: ArrayIndexOutOfBoundsException => Text.Range(offset, offset + 1) }
+    }
+
+
+  /* proper line range */
+
+  // NB: TextArea.getScreenLineEndOffset of last line is beyond Buffer.getLength
+  def proper_line_range(buffer: JEditBuffer, start: Text.Offset, end: Text.Offset): Text.Range =
+    Text.Range(start, end min buffer.getLength)
+
+
+  /* visible text range */
+
+  def visible_range(text_area: TextArea): Option[Text.Range] =
+  {
+    val buffer = text_area.getBuffer
+    val n = text_area.getVisibleLines
+    if (n > 0) {
+      val start = text_area.getScreenLineStartOffset(0)
+      val raw_end = text_area.getScreenLineEndOffset(n - 1)
+      Some(proper_line_range(buffer, start, if (raw_end >= 0) raw_end else buffer.getLength))
+    }
+    else None
+  }
+
+  def invalidate_range(text_area: TextArea, range: Text.Range)
+  {
+    val buffer = text_area.getBuffer
+    text_area.invalidateLineRange(
+      buffer.getLineOfOffset(range.start),
+      buffer.getLineOfOffset(range.stop))
+  }
+
+
+  /* char width */
+
+  def char_width(text_area: TextArea): Int =
+  {
+    val painter = text_area.getPainter
+    val font = painter.getFont
+    val font_context = painter.getFontRenderContext
+    font.getStringBounds(" ", font_context).getWidth.round.toInt
+  }
+
+
+  /* graphics range */
+
+  class Gfx_Range(val x: Int, val y: Int, val length: Int)
+
+  // NB: jEdit already normalizes \r\n and \r to \n
+  // NB: last line lacks \n
+  def gfx_range(text_area: TextArea, range: Text.Range): Option[Gfx_Range] =
+  {
+    val buffer = text_area.getBuffer
+
+    val p = text_area.offsetToXY(range.start)
+
+    val end = buffer.getLength
+    val stop = range.stop
+    val (q, r) =
+      if (stop >= end) (text_area.offsetToXY(end), char_width(text_area))
+      else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
+        (text_area.offsetToXY(stop - 1), char_width(text_area))
+      else (text_area.offsetToXY(stop), 0)
+
+    if (p != null && q != null && p.x < q.x + r && p.y == q.y)
+      Some(new Gfx_Range(p.x, p.y, q.x + r - p.x))
+    else None
+  }
+}
+
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Tools/jEdit/src/jedit_thy_load.scala
--- a/src/Tools/jEdit/src/jedit_thy_load.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/jedit_thy_load.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -36,9 +36,9 @@
   override def with_thy_text[A](name: Document.Node.Name, f: CharSequence => A): A =
   {
     Swing_Thread.now {
-      Isabelle.jedit_buffer(name.node) match {
+      JEdit_Lib.jedit_buffer(name.node) match {
         case Some(buffer) =>
-          Isabelle.buffer_lock(buffer) {
+          JEdit_Lib.buffer_lock(buffer) {
             Some(f(buffer.getSegment(0, buffer.getLength)))
           }
         case None => None
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Tools/jEdit/src/output2_dockable.scala
--- a/src/Tools/jEdit/src/output2_dockable.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/output2_dockable.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -31,13 +31,14 @@
   private var zoom_factor = 100
   private var show_tracing = false
   private var do_update = true
-  private var current_state = Command.empty.empty_state
-  private var current_body: XML.Body = Nil
+  private var current_snapshot = Document.State.init.snapshot()
+  private var current_state = Command.empty.init_state
+  private var current_output: List[XML.Tree] = Nil
 
 
   /* pretty text panel */
 
-  private val pretty_text_area = new Pretty_Text_Area
+  private val pretty_text_area = new Pretty_Text_Area(view)
   set_content(pretty_text_area)
 
 
@@ -53,33 +54,34 @@
   {
     Swing_Thread.require()
 
-    val new_state =
-      if (follow) {
-        Document_View(view.getTextArea) match {
-          case Some(doc_view) =>
-            val snapshot = doc_view.model.snapshot()
+    val (new_snapshot, new_state) =
+      Document_View(view.getTextArea) match {
+        case Some(doc_view) =>
+          val snapshot = doc_view.model.snapshot()
+          if (follow && !snapshot.is_outdated) {
             snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
-              case Some(cmd) => snapshot.state.command_state(snapshot.version, cmd)
-              case None => Command.empty.empty_state
+              case Some(cmd) =>
+                (snapshot, snapshot.state.command_state(snapshot.version, cmd))
+              case None =>
+                (Document.State.init.snapshot(), Command.empty.init_state)
             }
-          case None => Command.empty.empty_state
-        }
+          }
+          else (current_snapshot, current_state)
+        case None => (current_snapshot, current_state)
       }
-      else current_state
 
-    val new_body =
+    val new_output =
       if (!restriction.isDefined || restriction.get.contains(new_state.command))
-        new_state.results.iterator.map(_._2).filter(
-        { // FIXME not scalable
-          case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing
-          case _ => true
-        }).toList
-      else current_body
+        new_state.results.iterator.map(_._2)
+          .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList  // FIXME not scalable
+      else current_output
 
-    if (new_body != current_body) pretty_text_area.update(new_body)
+    if (new_output != current_output)
+      pretty_text_area.update(new_snapshot, Library.separate(Pretty.FBreak, new_output))
 
+    current_snapshot = new_snapshot
     current_state = new_state
-    current_body = new_body
+    current_output = new_output
   }
 
 
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Tools/jEdit/src/output_dockable.scala
--- a/src/Tools/jEdit/src/output_dockable.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/output_dockable.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -31,7 +31,7 @@
   private var zoom_factor = 100
   private var show_tracing = false
   private var do_update = true
-  private var current_state = Command.empty.empty_state
+  private var current_state = Command.empty.init_state
   private var current_body: XML.Body = Nil
 
 
@@ -47,7 +47,7 @@
         val sendback = Protocol.Sendback.unapply(elem.getUserData(Markup.Data.name)).get
         Document_View(view.getTextArea) match {
           case Some(doc_view) =>
-            doc_view.robust_body() {
+            doc_view.rich_text_area.robust_body() {
               val cmd = current_state.command
               val model = doc_view.model
               val buffer = model.buffer
@@ -91,20 +91,17 @@
             val snapshot = doc_view.model.snapshot()
             snapshot.node.command_at(doc_view.text_area.getCaretPosition).map(_._1) match {
               case Some(cmd) => snapshot.state.command_state(snapshot.version, cmd)
-              case None => Command.empty.empty_state
+              case None => Command.empty.init_state
             }
-          case None => Command.empty.empty_state
+          case None => Command.empty.init_state
         }
       }
       else current_state
 
     val new_body =
       if (!restriction.isDefined || restriction.get.contains(new_state.command))
-        new_state.results.iterator.map(_._2).filter(
-        { // FIXME not scalable
-          case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => show_tracing
-          case _ => true
-        }).toList
+        new_state.results.iterator.map(_._2)
+          .filter(msg => !Protocol.is_tracing(msg) || show_tracing).toList  // FIXME not scalable
       else current_body
 
     if (new_body != current_body) html_panel.render(new_body)
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -9,23 +9,17 @@
 
 import isabelle._
 
-import java.lang.System
-import java.awt.Font
 import javax.swing.JOptionPane
 
-import scala.collection.mutable
 import scala.swing.{ListView, ScrollPane}
 
-import org.gjt.sp.jedit.{jEdit, GUIUtilities, EBMessage, EBPlugin,
-  Buffer, EditPane, ServiceManager, View}
-import org.gjt.sp.jedit.buffer.JEditBuffer
+import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View}
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
 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
 
 import org.gjt.sp.util.SyntaxUtilities
-import org.gjt.sp.util.Log
 
 import scala.actors.Actor._
 
@@ -82,62 +76,6 @@
   }
 
 
-  /* icons */
-
-  def load_icon(name: String): javax.swing.Icon =
-  {
-    val icon = GUIUtilities.loadIcon(name)
-    if (icon.getIconWidth < 0 || icon.getIconHeight < 0)
-      Log.log(Log.ERROR, icon, "Bad icon: " + name)
-    icon
-  }
-
-
-  /* buffers */
-
-  def swing_buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
-    Swing_Thread.now { buffer_lock(buffer) { body } }
-
-  def buffer_text(buffer: JEditBuffer): String =
-    buffer_lock(buffer) { buffer.getText(0, buffer.getLength) }
-
-  def buffer_name(buffer: Buffer): String = buffer.getSymlinkPath
-
-  def buffer_node_dummy(buffer: Buffer): Option[Document.Node.Name] =
-    Some(Document.Node.Name(buffer_name(buffer), buffer.getDirectory, buffer.getName))
-
-  def buffer_node_name(buffer: Buffer): Option[Document.Node.Name] =
-  {
-    val name = buffer_name(buffer)
-    Thy_Header.thy_name(name).map(theory => Document.Node.Name(name, buffer.getDirectory, theory))
-  }
-
-
-  /* main jEdit components */
-
-  def jedit_buffers(): Iterator[Buffer] = jEdit.getBuffers().iterator
-
-  def jedit_buffer(name: String): Option[Buffer] =
-    jedit_buffers().find(buffer => buffer_name(buffer) == name)
-
-  def jedit_views(): Iterator[View] = jEdit.getViews().iterator
-
-  def jedit_text_areas(view: View): Iterator[JEditTextArea] =
-    view.getEditPanes().iterator.map(_.getTextArea)
-
-  def jedit_text_areas(): Iterator[JEditTextArea] =
-    jedit_views().flatMap(jedit_text_areas(_))
-
-  def jedit_text_areas(buffer: JEditBuffer): Iterator[JEditTextArea] =
-    jedit_text_areas().filter(_.getBuffer == buffer)
-
-  def buffer_lock[A](buffer: JEditBuffer)(body: => A): A =
-  {
-    try { buffer.readLock(); body }
-    finally { buffer.readUnlock() }
-  }
-
-
   /* document model and view */
 
   def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
@@ -145,24 +83,24 @@
 
   def document_views(buffer: Buffer): List[Document_View] =
     for {
-      text_area <- jedit_text_areas(buffer).toList
+      text_area <- JEdit_Lib.jedit_text_areas(buffer).toList
       doc_view = document_view(text_area)
       if doc_view.isDefined
     } yield doc_view.get
 
   def exit_model(buffer: Buffer)
   {
-    swing_buffer_lock(buffer) {
-      jedit_text_areas(buffer).foreach(Document_View.exit)
+    JEdit_Lib.swing_buffer_lock(buffer) {
+      JEdit_Lib.jedit_text_areas(buffer).foreach(Document_View.exit)
       Document_Model.exit(buffer)
     }
   }
 
   def init_model(buffer: Buffer)
   {
-    swing_buffer_lock(buffer) {
+    JEdit_Lib.swing_buffer_lock(buffer) {
       val opt_model =
-        buffer_node_name(buffer) match {
+        JEdit_Lib.buffer_node_name(buffer) match {
           case Some(node_name) =>
             document_model(buffer) match {
               case Some(model) if model.name == node_name => Some(model)
@@ -171,7 +109,7 @@
           case None => None
         }
       if (opt_model.isDefined) {
-        for (text_area <- jedit_text_areas(buffer)) {
+        for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
           if (document_view(text_area).map(_.model) != opt_model)
             Document_View.init(opt_model.get, text_area)
         }
@@ -181,7 +119,7 @@
 
   def init_view(buffer: Buffer, text_area: JEditTextArea)
   {
-    swing_buffer_lock(buffer) {
+    JEdit_Lib.swing_buffer_lock(buffer) {
       document_model(buffer) match {
         case Some(model) => Document_View.init(model, text_area)
         case None =>
@@ -191,7 +129,7 @@
 
   def exit_view(buffer: Buffer, text_area: JEditTextArea)
   {
-    swing_buffer_lock(buffer) {
+    JEdit_Lib.swing_buffer_lock(buffer) {
       Document_View.exit(text_area)
     }
   }
@@ -264,10 +202,10 @@
     {
       val view = jEdit.getActiveView()
 
-      val buffers = Isabelle.jedit_buffers().toList
+      val buffers = JEdit_Lib.jedit_buffers().toList
       if (buffers.forall(_.isLoaded)) {
         def loaded_buffer(name: String): Boolean =
-          buffers.exists(buffer => Isabelle.buffer_name(buffer) == name)
+          buffers.exists(buffer => JEdit_Lib.buffer_name(buffer) == name)
 
         val thys =
           for (buffer <- buffers; model <- Isabelle.document_model(buffer))
@@ -314,16 +252,16 @@
               }
 
             case Session.Ready =>
-              Isabelle.jedit_buffers.foreach(Isabelle.init_model)
+              JEdit_Lib.jedit_buffers.foreach(Isabelle.init_model)
               Swing_Thread.later { delay_load.invoke() }
 
             case Session.Shutdown =>
-              Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
+              JEdit_Lib.jedit_buffers.foreach(Isabelle.exit_model)
               Swing_Thread.later { delay_load.revoke() }
 
             case _ =>
           }
-        case bad => System.err.println("session_manager: ignoring bad message " + bad)
+        case bad => java.lang.System.err.println("session_manager: ignoring bad message " + bad)
       }
     }
   }
@@ -426,7 +364,7 @@
       Isabelle.options.value.save_prefs()
 
     Isabelle.session.phase_changed -= session_manager
-    Isabelle.jedit_buffers.foreach(Isabelle.exit_model)
+    JEdit_Lib.jedit_buffers.foreach(Isabelle.exit_model)
     Isabelle.session.stop()
   }
 }
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Tools/jEdit/src/pretty_text_area.scala
--- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -9,24 +9,71 @@
 
 import isabelle._
 
-import java.awt.{Font, FontMetrics}
+import java.awt.{Font, FontMetrics, Toolkit}
+import java.awt.event.{ActionListener, ActionEvent, KeyEvent}
+import javax.swing.{KeyStroke, JComponent}
+
+import org.gjt.sp.jedit.{jEdit, View, Registers}
 import org.gjt.sp.jedit.textarea.{AntiAlias, JEditEmbeddedTextArea}
-import org.gjt.sp.jedit.jEdit
 import org.gjt.sp.util.SyntaxUtilities
+
 import scala.swing.{BorderPanel, Component}
 
 
-class Pretty_Text_Area extends BorderPanel
+object Pretty_Text_Area
+{
+  def document_state(base_snapshot: Document.Snapshot, formatted_body: XML.Body)
+    : (String, Document.State) =
+  {
+    val command = Command.rich_text(Document.new_id(), formatted_body)
+    val node_name = command.node_name
+    val edits: List[Document.Edit_Text] =
+      List(node_name -> Document.Node.Edits(List(Text.Edit.insert(0, command.source))))
+
+    val state0 = base_snapshot.state.define_command(command)
+    val version0 = base_snapshot.version
+    val nodes0 = version0.nodes
+
+    assert(nodes0(node_name).commands.isEmpty)
+
+    val nodes1 = nodes0 + (node_name -> nodes0(node_name).update_commands(Linear_Set(command)))
+    val version1 = Document.Version.make(version0.syntax, nodes1)
+    val state1 =
+      state0.continue_history(Future.value(version0), edits, Future.value(version1))._2
+        .define_version(version1, state0.the_assignment(version0))
+        .assign(version1.id, List(command.id -> Some(Document.new_id())))._2
+
+    (command.source, state1)
+  }
+}
+
+class Pretty_Text_Area(view: View) extends BorderPanel
 {
   Swing_Thread.require()
 
-  val text_area = new JEditEmbeddedTextArea
-
   private var current_font_metrics: FontMetrics = null
   private var current_font_family = "Dialog"
   private var current_font_size: Int = 12
   private var current_margin: Int = 0
   private var current_body: XML.Body = Nil
+  private var current_base_snapshot = Document.State.init.snapshot()
+  private var current_rendering: Isabelle_Rendering = text_rendering()._2
+
+  private val text_area = new JEditEmbeddedTextArea
+  private val rich_text_area = new Rich_Text_Area(view, text_area, () => current_rendering)
+  private val buffer = text_area.getBuffer
+
+  private def text_rendering(): (String, Isabelle_Rendering) =
+  {
+    Swing_Thread.require()
+
+    val body =
+      Pretty.formatted(current_body, current_margin, Pretty.font_metric(current_font_metrics))
+    val (text, state) = Pretty_Text_Area.document_state(current_base_snapshot, body)
+    val rendering = Isabelle_Rendering(state.snapshot(), Isabelle.options.value)
+
+    (text, rendering)
+  }
 
   def refresh()
   {
@@ -42,14 +89,15 @@
     current_font_metrics = painter.getFontMetrics(font)
     current_margin = (size.width / (current_font_metrics.charWidth(Pretty.spc) max 1) - 4) max 20
 
-    val text =
-      Pretty.string_of(current_body, current_margin, Pretty.font_metric(current_font_metrics))
+    val (text, rendering) = text_rendering()
+    current_rendering = rendering
 
-    val buffer = text_area.getBuffer
     try {
       buffer.beginCompoundEdit
+      buffer.setReadOnly(false)
       text_area.setText(text)
       text_area.setCaretPosition(0)
+      buffer.setReadOnly(true)
     }
     finally {
       buffer.endCompoundEdit
@@ -65,14 +113,40 @@
     refresh()
   }
 
-  def update(body: XML.Body)
+  def update(base_snapshot: Document.Snapshot, body: XML.Body)
   {
     Swing_Thread.require()
+    require(!base_snapshot.is_outdated)
 
+    current_base_snapshot = base_snapshot
     current_body = body
     refresh()
   }
 
+
+  /* keyboard actions */
+
+  private val action_listener = new ActionListener {
+    def actionPerformed(e: ActionEvent) {
+      e.getActionCommand match {
+        case "copy" => Registers.copy(text_area, '$')
+        case _ =>
+      }
+    }
+  }
+
+  text_area.registerKeyboardAction(action_listener, "copy",
+    KeyStroke.getKeyStroke(KeyEvent.VK_COPY, 0), JComponent.WHEN_FOCUSED)
+  text_area.registerKeyboardAction(action_listener, "copy",
+    KeyStroke.getKeyStroke(KeyEvent.VK_C,
+      Toolkit.getDefaultToolkit().getMenuShortcutKeyMask()), JComponent.WHEN_FOCUSED)
+
+
+  /* init */
+
+  buffer.setTokenMarker(new Token_Markup.Marker(true, None))
+  buffer.setReadOnly(true)
   layout(Component.wrap(text_area)) = BorderPanel.Position.Center
+  rich_text_area.activate()
 }
 
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Tools/jEdit/src/raw_output_dockable.scala
--- a/src/Tools/jEdit/src/raw_output_dockable.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/raw_output_dockable.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -31,7 +31,7 @@
       react {
         case output: Isabelle_Process.Output =>
           if (output.is_stdout || output.is_stderr)
-            Swing_Thread.later { text_area.append(XML.content(output.message).mkString) }
+            Swing_Thread.later { text_area.append(XML.content(output.message)) }
 
         case bad => System.err.println("Raw_Output_Dockable: ignoring bad message " + bad)
       }
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Tools/jEdit/src/rich_text_area.scala
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/rich_text_area.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -0,0 +1,489 @@
+/*  Title:      Tools/jEdit/src/rich_text_area.scala
+    Author:     Makarius
+
+Enhanced version of jEdit text area, with rich text rendering,
+tooltips, hyperlinks etc.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.awt.{Graphics2D, Shape, Window, Color}
+import java.awt.event.{MouseMotionAdapter, MouseAdapter, MouseEvent,
+  FocusAdapter, FocusEvent, WindowEvent, WindowAdapter}
+import java.awt.font.TextAttribute
+import java.text.AttributedString
+import java.util.ArrayList
+
+import org.gjt.sp.util.Log
+import org.gjt.sp.jedit.{OperatingSystem, Debug, View}
+import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
+import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter, TextArea}
+
+
+class Rich_Text_Area(view: View, text_area: TextArea, get_rendering: () => Isabelle_Rendering)
+{
+  private val buffer = text_area.getBuffer
+
+
+  /* robust extension body */
+
+  def robust_body[A](default: A)(body: => A): A =
+  {
+    try {
+      Swing_Thread.require()
+      if (buffer == text_area.getBuffer) body
+      else {
+        Log.log(Log.ERROR, this, ERROR("Implicit change of text area buffer"))
+        default
+      }
+    }
+    catch { case t: Throwable => Log.log(Log.ERROR, this, t); default }
+  }
+
+
+  /* original painters */
+
+  private def pick_extension(name: String): TextAreaExtension =
+  {
+    text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
+    match {
+      case List(x) => x
+      case _ => error("Expected exactly one " + name)
+    }
+  }
+
+  private val orig_text_painter =
+    pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
+
+
+  /* common painter state */
+
+  @volatile private var painter_rendering: Isabelle_Rendering = null
+  @volatile private var painter_clip: Shape = null
+
+  private val set_state = 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)
+    {
+      painter_rendering = get_rendering()
+      painter_clip = gfx.getClip
+    }
+  }
+
+  private val reset_state = 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)
+    {
+      painter_rendering = null
+      painter_clip = null
+    }
+  }
+
+  private def robust_rendering(body: Isabelle_Rendering => Unit)
+  {
+    robust_body(()) { body(painter_rendering) }
+  }
+
+
+  /* active areas within the text */
+
+  private class Active_Area[A](
+    rendering: Isabelle_Rendering => Text.Range => Option[Text.Info[A]])
+  {
+    private var the_info: Option[Text.Info[A]] = None
+
+    def info: Option[Text.Info[A]] = the_info
+
+    def update(new_info: Option[Text.Info[A]])
+    {
+      val old_info = the_info
+      if (new_info != old_info) {
+        for { opt <- List(old_info, new_info); Text.Info(range, _) <- opt }
+          JEdit_Lib.invalidate_range(text_area, range)
+        the_info = new_info
+      }
+    }
+
+    def update_rendering(r: Isabelle_Rendering, range: Text.Range)
+    { update(rendering(r)(range)) }
+
+    def reset { update(None) }
+  }
+
+  // owned by Swing thread
+
+  private var control: Boolean = false
+
+  private val highlight_area = new Active_Area[Color]((r: Isabelle_Rendering) => r.highlight _)
+  private val hyperlink_area = new Active_Area[Hyperlink]((r: Isabelle_Rendering) => r.hyperlink _)
+  private val active_areas = List(highlight_area, hyperlink_area)
+  private def active_reset(): Unit = active_areas.foreach(_.reset)
+
+  private val focus_listener = new FocusAdapter {
+    override def focusLost(e: FocusEvent) { robust_body(()) { active_reset() } }
+  }
+
+  private val window_listener = new WindowAdapter {
+    override def windowIconified(e: WindowEvent) { robust_body(()) { active_reset() } }
+    override def windowDeactivated(e: WindowEvent) { robust_body(()) { active_reset() } }
+  }
+
+  private val mouse_listener = new MouseAdapter {
+    override def mouseClicked(e: MouseEvent) {
+      robust_body(()) {
+        hyperlink_area.info match {
+          case Some(Text.Info(range, link)) => link.follow(view)
+          case None =>
+        }
+      }
+    }
+  }
+
+  private val mouse_motion_listener = new MouseMotionAdapter {
+    override def mouseMoved(e: MouseEvent) {
+      robust_body(()) {
+        control = if (OperatingSystem.isMacOS()) e.isMetaDown else e.isControlDown
+        if (control && !buffer.isLoading) {
+          JEdit_Lib.buffer_lock(buffer) {
+            val rendering = get_rendering()
+            val mouse_offset = text_area.xyToOffset(e.getX(), e.getY())
+            val mouse_range = JEdit_Lib.point_range(buffer, mouse_offset)
+            active_areas.foreach(_.update_rendering(rendering, mouse_range))
+          }
+        }
+        else active_reset()
+      }
+    }
+  }
+
+
+  /* tooltips */
+
+  private val tooltip_painter = new TextAreaExtension
+  {
+    override def getToolTipText(x: Int, y: Int): String =
+    {
+      robust_body(null: String) {
+        val rendering = get_rendering()
+        val offset = text_area.xyToOffset(x, y)
+        val range = Text.Range(offset, offset + 1)
+        val tip =
+          if (control) rendering.tooltip(range)
+          else rendering.tooltip_message(range)
+        tip.map(Isabelle.tooltip(_)) getOrElse null
+      }
+    }
+  }
+
+
+  /* text background */
+
+  private val background_painter = 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)
+    {
+      robust_rendering { rendering =>
+        val ascent = text_area.getPainter.getFontMetrics.getAscent
+
+        for (i <- 0 until physical_lines.length) {
+          if (physical_lines(i) != -1) {
+            val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
+
+            // background color (1)
+            for {
+              Text.Info(range, color) <- rendering.background1(line_range)
+              r <- JEdit_Lib.gfx_range(text_area, range)
+            } {
+              gfx.setColor(color)
+              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
+            }
+
+            // background color (2)
+            for {
+              Text.Info(range, color) <- rendering.background2(line_range)
+              r <- JEdit_Lib.gfx_range(text_area, range)
+            } {
+              gfx.setColor(color)
+              gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
+            }
+
+            // squiggly underline
+            for {
+              Text.Info(range, color) <- rendering.squiggly_underline(line_range)
+              r <- JEdit_Lib.gfx_range(text_area, range)
+            } {
+              gfx.setColor(color)
+              val x0 = (r.x / 2) * 2
+              val y0 = r.y + ascent + 1
+              for (x1 <- Range(x0, x0 + r.length, 2)) {
+                val y1 = if (x1 % 4 < 2) y0 else y0 + 1
+                gfx.drawLine(x1, y1, x1 + 1, y1)
+              }
+            }
+          }
+        }
+      }
+    }
+  }
+
+
+  /* text */
+
+  private def paint_chunk_list(rendering: Isabelle_Rendering,
+    gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
+  {
+    val clip_rect = gfx.getClipBounds
+    val painter = text_area.getPainter
+    val font_context = painter.getFontRenderContext
+
+    var w = 0.0f
+    var chunk = head
+    while (chunk != null) {
+      val chunk_offset = line_start + chunk.offset
+      if (x + w + chunk.width > clip_rect.x &&
+          x + w < clip_rect.x + clip_rect.width && chunk.accessable)
+      {
+        val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
+        val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str
+        val chunk_font = chunk.style.getFont
+        val chunk_color = chunk.style.getForegroundColor
+
+        def string_width(s: String): Float =
+          if (s.isEmpty) 0.0f
+          else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
+
+        val caret_range =
+          if (text_area.isCaretVisible)
+            JEdit_Lib.point_range(buffer, text_area.getCaretPosition)
+          else Text.Range(-1)
+
+        val markup =
+          for {
+            r1 <- rendering.text_color(chunk_range, chunk_color)
+            r2 <- r1.try_restrict(chunk_range)
+          } yield r2
+
+        val padded_markup =
+          if (markup.isEmpty)
+            Iterator(Text.Info(chunk_range, chunk_color))
+          else
+            Iterator(
+              Text.Info(Text.Range(chunk_range.start, markup.head.range.start), chunk_color)) ++
+            markup.iterator ++
+            Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), chunk_color))
+
+        var x1 = x + w
+        gfx.setFont(chunk_font)
+        for (Text.Info(range, color) <- padded_markup if !range.is_singularity) {
+          val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
+          gfx.setColor(color)
+
+          range.try_restrict(caret_range) match {
+            case Some(r) if !r.is_singularity =>
+              val i = r.start - range.start
+              val j = r.stop - range.start
+              val s1 = str.substring(0, i)
+              val s2 = str.substring(i, j)
+              val s3 = str.substring(j)
+
+              if (!s1.isEmpty) gfx.drawString(s1, x1, y)
+
+              val astr = new AttributedString(s2)
+              astr.addAttribute(TextAttribute.FONT, chunk_font)
+              astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor)
+              astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
+              gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
+
+              if (!s3.isEmpty)
+                gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y)
+
+            case _ =>
+              gfx.drawString(str, x1, y)
+          }
+          x1 += string_width(str)
+        }
+      }
+      w += chunk.width
+      chunk = chunk.next.asInstanceOf[Chunk]
+    }
+    w
+  }
+
+  private val text_painter = 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)
+    {
+      robust_rendering { rendering =>
+        val clip = gfx.getClip
+        val x0 = text_area.getHorizontalOffset
+        val fm = text_area.getPainter.getFontMetrics
+        var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
+
+        for (i <- 0 until physical_lines.length) {
+          val line = physical_lines(i)
+          if (line != -1) {
+            val screen_line = first_line + i
+            val chunks = text_area.getChunksOfScreenLine(screen_line)
+            if (chunks != null) {
+              val line_start = buffer.getLineStartOffset(line)
+              gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
+              val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0, y0).toInt
+              gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
+              orig_text_painter.paintValidLine(gfx,
+                screen_line, line, start(i), end(i), y + line_height * i)
+              gfx.setClip(clip)
+            }
+          }
+          y0 += line_height
+        }
+      }
+    }
+  }
+
+
+  /* foreground */
+
+  private val foreground_painter = 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)
+    {
+      robust_rendering { rendering =>
+        for (i <- 0 until physical_lines.length) {
+          if (physical_lines(i) != -1) {
+            val line_range = JEdit_Lib.proper_line_range(buffer, start(i), end(i))
+
+            // foreground color
+            for {
+              Text.Info(range, color) <- rendering.foreground(line_range)
+              r <- JEdit_Lib.gfx_range(text_area, range)
+            } {
+              gfx.setColor(color)
+              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
+            }
+
+            // highlight range -- potentially from other snapshot
+            for {
+              info <- highlight_area.info
+              Text.Info(range, color) <- info.try_restrict(line_range)
+              r <- JEdit_Lib.gfx_range(text_area, range)
+            } {
+              gfx.setColor(color)
+              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
+            }
+
+            // hyperlink range -- potentially from other snapshot
+            for {
+              info <- hyperlink_area.info
+              Text.Info(range, _) <- info.try_restrict(line_range)
+              r <- JEdit_Lib.gfx_range(text_area, range)
+            } {
+              gfx.setColor(rendering.hyperlink_color)
+              gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
+            }
+          }
+        }
+      }
+    }
+  }
+
+
+  /* caret -- outside of text range */
+
+  private class Caret_Painter(before: Boolean) extends TextAreaExtension
+  {
+    override def paintValidLine(gfx: Graphics2D,
+      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
+    {
+      robust_rendering { _ =>
+        if (before) gfx.clipRect(0, 0, 0, 0)
+        else gfx.setClip(painter_clip)
+      }
+    }
+  }
+
+  private val before_caret_painter1 = new Caret_Painter(true)
+  private val after_caret_painter1 = new Caret_Painter(false)
+  private val before_caret_painter2 = new Caret_Painter(true)
+  private val after_caret_painter2 = new Caret_Painter(false)
+
+  private val caret_painter = new TextAreaExtension
+  {
+    override def paintValidLine(gfx: Graphics2D,
+      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
+    {
+      robust_rendering { _ =>
+        if (text_area.isCaretVisible) {
+          val caret = text_area.getCaretPosition
+          if (start <= caret && caret == end - 1) {
+            val painter = text_area.getPainter
+            val fm = painter.getFontMetrics
+
+            val offset = caret - text_area.getLineStartOffset(physical_line)
+            val x = text_area.offsetToXY(physical_line, offset).x
+            gfx.setColor(painter.getCaretColor)
+            gfx.drawRect(x, y, JEdit_Lib.char_width(text_area) - 1, fm.getHeight - 1)
+          }
+        }
+      }
+    }
+  }
+
+
+  /* activation */
+
+  def activate()
+  {
+    val painter = text_area.getPainter
+    painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
+    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, tooltip_painter)
+    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
+    painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
+    painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
+    painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1)
+    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
+    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
+    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
+    painter.addExtension(500, foreground_painter)
+    painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
+    painter.removeExtension(orig_text_painter)
+    painter.addMouseListener(mouse_listener)
+    painter.addMouseMotionListener(mouse_motion_listener)
+    text_area.addFocusListener(focus_listener)
+    view.addWindowListener(window_listener)
+  }
+
+  def deactivate()
+  {
+    val painter = text_area.getPainter
+    view.removeWindowListener(window_listener)
+    text_area.removeFocusListener(focus_listener)
+    painter.removeMouseMotionListener(mouse_motion_listener)
+    painter.removeMouseListener(mouse_listener)
+    painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
+    painter.removeExtension(reset_state)
+    painter.removeExtension(foreground_painter)
+    painter.removeExtension(caret_painter)
+    painter.removeExtension(after_caret_painter2)
+    painter.removeExtension(before_caret_painter2)
+    painter.removeExtension(after_caret_painter1)
+    painter.removeExtension(before_caret_painter1)
+    painter.removeExtension(text_painter)
+    painter.removeExtension(background_painter)
+    painter.removeExtension(tooltip_painter)
+    painter.removeExtension(set_state)
+  }
+}
+
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Tools/jEdit/src/text_area_painter.scala
--- a/src/Tools/jEdit/src/text_area_painter.scala	Wed Sep 19 10:57:44 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,401 +0,0 @@
-/*  Title:      Tools/jEdit/src/text_area_painter.scala
-    Author:     Makarius
-
-Painter setup for main jEdit text area, depending on common snapshot.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import java.awt.{Graphics2D, Shape}
-import java.awt.font.TextAttribute
-import java.text.AttributedString
-import java.util.ArrayList
-
-import org.gjt.sp.jedit.Debug
-import org.gjt.sp.jedit.syntax.{DisplayTokenHandler, Chunk}
-import org.gjt.sp.jedit.textarea.{TextAreaExtension, TextAreaPainter}
-
-
-class Text_Area_Painter(doc_view: Document_View)
-{
-  private val model = doc_view.model
-  private val buffer = model.buffer
-  private val text_area = doc_view.text_area
-
-
-  /* graphics range */
-
-  private def char_width(): Int =
-  {
-    val painter = text_area.getPainter
-    val font = painter.getFont
-    val font_context = painter.getFontRenderContext
-    font.getStringBounds(" ", font_context).getWidth.round.toInt
-  }
-
-  private class Gfx_Range(val x: Int, val y: Int, val length: Int)
-
-  // NB: jEdit already normalizes \r\n and \r to \n
-  // NB: last line lacks \n
-  private def gfx_range(range: Text.Range): Option[Gfx_Range] =
-  {
-    val p = text_area.offsetToXY(range.start)
-
-    val end = buffer.getLength
-    val stop = range.stop
-    val (q, r) =
-      if (stop >= end) (text_area.offsetToXY(end), char_width())
-      else if (stop > 0 && buffer.getText(stop - 1, 1) == "\n")
-        (text_area.offsetToXY(stop - 1), char_width())
-      else (text_area.offsetToXY(stop), 0)
-
-    if (p != null && q != null && p.x < q.x + r && p.y == q.y)
-      Some(new Gfx_Range(p.x, p.y, q.x + r - p.x))
-    else None
-  }
-
-
-  /* original painters */
-
-  private def pick_extension(name: String): TextAreaExtension =
-  {
-    text_area.getPainter.getExtensions.iterator.filter(x => x.getClass.getName == name).toList
-    match {
-      case List(x) => x
-      case _ => error("Expected exactly one " + name)
-    }
-  }
-
-  private val orig_text_painter =
-    pick_extension("org.gjt.sp.jedit.textarea.TextAreaPainter$PaintText")
-
-
-  /* common painter state */
-
-  @volatile private var painter_rendering: Isabelle_Rendering = null
-  @volatile private var painter_clip: Shape = null
-
-  private val set_state = 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)
-    {
-      painter_rendering = Isabelle_Rendering(model.snapshot(), Isabelle.options.value)
-      painter_clip = gfx.getClip
-    }
-  }
-
-  private val reset_state = 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)
-    {
-      painter_rendering = null
-      painter_clip = null
-    }
-  }
-
-  private def robust_rendering(body: Isabelle_Rendering => Unit)
-  {
-    doc_view.robust_body(()) { body(painter_rendering) }
-  }
-
-
-  /* text background */
-
-  private val background_painter = 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)
-    {
-      robust_rendering { rendering =>
-        val ascent = text_area.getPainter.getFontMetrics.getAscent
-
-        for (i <- 0 until physical_lines.length) {
-          if (physical_lines(i) != -1) {
-            val line_range = doc_view.proper_line_range(start(i), end(i))
-
-            // background color (1)
-            for {
-              Text.Info(range, color) <- rendering.background1(line_range)
-              r <- gfx_range(range)
-            } {
-              gfx.setColor(color)
-              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
-            }
-
-            // background color (2)
-            for {
-              Text.Info(range, color) <- rendering.background2(line_range)
-              r <- gfx_range(range)
-            } {
-              gfx.setColor(color)
-              gfx.fillRect(r.x + 2, y + i * line_height + 2, r.length - 4, line_height - 4)
-            }
-
-            // squiggly underline
-            for {
-              Text.Info(range, color) <- rendering.squiggly_underline(line_range)
-              r <- gfx_range(range)
-            } {
-              gfx.setColor(color)
-              val x0 = (r.x / 2) * 2
-              val y0 = r.y + ascent + 1
-              for (x1 <- Range(x0, x0 + r.length, 2)) {
-                val y1 = if (x1 % 4 < 2) y0 else y0 + 1
-                gfx.drawLine(x1, y1, x1 + 1, y1)
-              }
-            }
-          }
-        }
-      }
-    }
-  }
-
-
-  /* text */
-
-  private def paint_chunk_list(rendering: Isabelle_Rendering,
-    gfx: Graphics2D, line_start: Text.Offset, head: Chunk, x: Float, y: Float): Float =
-  {
-    val clip_rect = gfx.getClipBounds
-    val painter = text_area.getPainter
-    val font_context = painter.getFontRenderContext
-
-    var w = 0.0f
-    var chunk = head
-    while (chunk != null) {
-      val chunk_offset = line_start + chunk.offset
-      if (x + w + chunk.width > clip_rect.x &&
-          x + w < clip_rect.x + clip_rect.width && chunk.accessable)
-      {
-        val chunk_range = Text.Range(chunk_offset, chunk_offset + chunk.length)
-        val chunk_str = if (chunk.str == null) " " * chunk.length else chunk.str
-        val chunk_font = chunk.style.getFont
-        val chunk_color = chunk.style.getForegroundColor
-
-        def string_width(s: String): Float =
-          if (s.isEmpty) 0.0f
-          else chunk_font.getStringBounds(s, font_context).getWidth.toFloat
-
-        val caret_range =
-          if (text_area.isCaretVisible) model.point_range(text_area.getCaretPosition)
-          else Text.Range(-1)
-
-        val markup =
-          for {
-            r1 <- rendering.text_color(chunk_range, chunk_color)
-            r2 <- r1.try_restrict(chunk_range)
-          } yield r2
-
-        val padded_markup =
-          if (markup.isEmpty)
-            Iterator(Text.Info(chunk_range, chunk_color))
-          else
-            Iterator(
-              Text.Info(Text.Range(chunk_range.start, markup.head.range.start), chunk_color)) ++
-            markup.iterator ++
-            Iterator(Text.Info(Text.Range(markup.last.range.stop, chunk_range.stop), chunk_color))
-
-        var x1 = x + w
-        gfx.setFont(chunk_font)
-        for (Text.Info(range, color) <- padded_markup if !range.is_singularity) {
-          val str = chunk_str.substring(range.start - chunk_offset, range.stop - chunk_offset)
-          gfx.setColor(color)
-
-          range.try_restrict(caret_range) match {
-            case Some(r) if !r.is_singularity =>
-              val i = r.start - range.start
-              val j = r.stop - range.start
-              val s1 = str.substring(0, i)
-              val s2 = str.substring(i, j)
-              val s3 = str.substring(j)
-
-              if (!s1.isEmpty) gfx.drawString(s1, x1, y)
-
-              val astr = new AttributedString(s2)
-              astr.addAttribute(TextAttribute.FONT, chunk_font)
-              astr.addAttribute(TextAttribute.FOREGROUND, painter.getCaretColor)
-              astr.addAttribute(TextAttribute.SWAP_COLORS, TextAttribute.SWAP_COLORS_ON)
-              gfx.drawString(astr.getIterator, x1 + string_width(s1), y)
-
-              if (!s3.isEmpty)
-                gfx.drawString(s3, x1 + string_width(str.substring(0, j)), y)
-
-            case _ =>
-              gfx.drawString(str, x1, y)
-          }
-          x1 += string_width(str)
-        }
-      }
-      w += chunk.width
-      chunk = chunk.next.asInstanceOf[Chunk]
-    }
-    w
-  }
-
-  private val text_painter = 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)
-    {
-      robust_rendering { rendering =>
-        val clip = gfx.getClip
-        val x0 = text_area.getHorizontalOffset
-        val fm = text_area.getPainter.getFontMetrics
-        var y0 = y + fm.getHeight - (fm.getLeading + 1) - fm.getDescent
-
-        for (i <- 0 until physical_lines.length) {
-          val line = physical_lines(i)
-          if (line != -1) {
-            val screen_line = first_line + i
-            val chunks = text_area.getChunksOfScreenLine(screen_line)
-            if (chunks != null) {
-              val line_start = text_area.getBuffer.getLineStartOffset(line)
-              gfx.clipRect(x0, y + line_height * i, Integer.MAX_VALUE, line_height)
-              val w = paint_chunk_list(rendering, gfx, line_start, chunks, x0, y0).toInt
-              gfx.clipRect(x0 + w.toInt, 0, Integer.MAX_VALUE, Integer.MAX_VALUE)
-              orig_text_painter.paintValidLine(gfx,
-                screen_line, line, start(i), end(i), y + line_height * i)
-              gfx.setClip(clip)
-            }
-          }
-          y0 += line_height
-        }
-      }
-    }
-  }
-
-
-  /* foreground */
-
-  private val foreground_painter = 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)
-    {
-      robust_rendering { rendering =>
-        for (i <- 0 until physical_lines.length) {
-          if (physical_lines(i) != -1) {
-            val line_range = doc_view.proper_line_range(start(i), end(i))
-
-            // foreground color
-            for {
-              Text.Info(range, color) <- rendering.foreground(line_range)
-              r <- gfx_range(range)
-            } {
-              gfx.setColor(color)
-              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
-            }
-
-            // highlight range -- potentially from other snapshot
-            for {
-              info <- doc_view.highlight_info()
-              Text.Info(range, color) <- info.try_restrict(line_range)
-              r <- gfx_range(range)
-            } {
-              gfx.setColor(color)
-              gfx.fillRect(r.x, y + i * line_height, r.length, line_height)
-            }
-
-            // hyperlink range -- potentially from other snapshot
-            for {
-              info <- doc_view.hyperlink_info()
-              Text.Info(range, _) <- info.try_restrict(line_range)
-              r <- gfx_range(range)
-            } {
-              gfx.setColor(rendering.hyperlink_color)
-              gfx.drawRect(r.x, y + i * line_height, r.length - 1, line_height - 1)
-            }
-          }
-        }
-      }
-    }
-  }
-
-
-  /* caret -- outside of text range */
-
-  private class Caret_Painter(before: Boolean) extends TextAreaExtension
-  {
-    override def paintValidLine(gfx: Graphics2D,
-      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
-    {
-      robust_rendering { _ =>
-        if (before) gfx.clipRect(0, 0, 0, 0)
-        else gfx.setClip(painter_clip)
-      }
-    }
-  }
-
-  private val before_caret_painter1 = new Caret_Painter(true)
-  private val after_caret_painter1 = new Caret_Painter(false)
-  private val before_caret_painter2 = new Caret_Painter(true)
-  private val after_caret_painter2 = new Caret_Painter(false)
-
-  private val caret_painter = new TextAreaExtension
-  {
-    override def paintValidLine(gfx: Graphics2D,
-      screen_line: Int, physical_line: Int, start: Int, end: Int, y: Int)
-    {
-      robust_rendering { _ =>
-        if (text_area.isCaretVisible) {
-          val caret = text_area.getCaretPosition
-          if (start <= caret && caret == end - 1) {
-            val painter = text_area.getPainter
-            val fm = painter.getFontMetrics
-
-            val offset = caret - text_area.getLineStartOffset(physical_line)
-            val x = text_area.offsetToXY(physical_line, offset).x
-            gfx.setColor(painter.getCaretColor)
-            gfx.drawRect(x, y, char_width() - 1, fm.getHeight - 1)
-          }
-        }
-      }
-    }
-  }
-
-
-  /* activation */
-
-  def activate()
-  {
-    val painter = text_area.getPainter
-    painter.addExtension(TextAreaPainter.LOWEST_LAYER, set_state)
-    painter.addExtension(TextAreaPainter.LINE_BACKGROUND_LAYER + 1, background_painter)
-    painter.addExtension(TextAreaPainter.TEXT_LAYER, text_painter)
-    painter.addExtension(TextAreaPainter.CARET_LAYER - 1, before_caret_painter1)
-    painter.addExtension(TextAreaPainter.CARET_LAYER + 1, after_caret_painter1)
-    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER - 1, before_caret_painter2)
-    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 1, after_caret_painter2)
-    painter.addExtension(TextAreaPainter.BLOCK_CARET_LAYER + 2, caret_painter)
-    painter.addExtension(500, foreground_painter)
-    painter.addExtension(TextAreaPainter.HIGHEST_LAYER, reset_state)
-    painter.removeExtension(orig_text_painter)
-  }
-
-  def deactivate()
-  {
-    val painter = text_area.getPainter
-    painter.addExtension(TextAreaPainter.TEXT_LAYER, orig_text_painter)
-    painter.removeExtension(reset_state)
-    painter.removeExtension(foreground_painter)
-    painter.removeExtension(caret_painter)
-    painter.removeExtension(after_caret_painter2)
-    painter.removeExtension(before_caret_painter2)
-    painter.removeExtension(after_caret_painter1)
-    painter.removeExtension(before_caret_painter1)
-    painter.removeExtension(text_painter)
-    painter.removeExtension(background_painter)
-    painter.removeExtension(set_state)
-  }
-}
-
diff -r 0ae4216a1783 -r 98960e2fadd7 src/Tools/jEdit/src/text_overview.scala
--- a/src/Tools/jEdit/src/text_overview.scala	Wed Sep 19 10:57:44 2012 +0200
+++ b/src/Tools/jEdit/src/text_overview.scala	Wed Sep 19 12:11:09 2012 +0200
@@ -65,8 +65,8 @@
     super.paintComponent(gfx)
     Swing_Thread.assert()
 
-    doc_view.robust_body(()) {
-      Isabelle.buffer_lock(buffer) {
+    doc_view.rich_text_area.robust_body(()) {
+      JEdit_Lib.buffer_lock(buffer) {
         val snapshot = doc_view.model.snapshot()
 
         if (snapshot.is_outdated) {