Command.State: accumulate markup reports uniformly;
Document_Model.token_marker: select relevant information directly from Markup_Tree, without intermediate HighlightInfo;
tuned;

--- a/src/Pure/PIDE/command.scala	Fri Aug 20 22:35:01 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Sun Aug 22 12:54:12 2010 +0200
@@ -14,9 +14,6 @@
 
 object Command
 {
-  case class HighlightInfo(kind: String, sub_kind: Option[String]) {
-    override def toString = kind
-  }
   case class TypeInfo(ty: String)
   case class RefInfo(file: Option[String], line: Option[Int],
     command_id: Option[Document.Command_ID], offset: Option[Int])  // FIXME Command_ID vs. Exec_ID !?
@@ -46,14 +43,6 @@
 
     /* markup */
 
-    lazy val highlight: List[Markup_Tree.Node[Any]] =
-    {
-      markup.filter(_.info match {
-        case Command.HighlightInfo(_, _) => true
-        case _ => false
-      }).flatten(markup_root_node)
-    }
-
     private lazy val types: List[Markup_Tree.Node[Any]] =
       markup.filter(_.info match {
         case Command.TypeInfo(_) => true
@@ -85,38 +74,16 @@
     def accumulate(message: XML.Tree): Command.State =
       message match {
         case XML.Elem(Markup(Markup.STATUS, _), body) => copy(status = body ::: status)
-
-        case XML.Elem(Markup(Markup.REPORT, _), elems) =>
-          (this /: elems)((state, elem) =>
-            elem match {
-              case XML.Elem(Markup(kind, atts), body) if Position.get_id(atts) == Some(command.id) =>
-                atts match {
-                  case Position.Range(range) =>
-                    if (kind == Markup.ML_TYPING) {
-                      val info = Pretty.string_of(body, margin = 40)
-                      state.add_markup(command.decode_range(range, Command.TypeInfo(info)))
-                    }
-                    else if (kind == Markup.ML_REF) {
-                      body match {
-                        case List(XML.Elem(Markup(Markup.ML_DEF, props), _)) =>
-                          state.add_markup(
-                            command.decode_range(range,
-                              Command.RefInfo(
-                                Position.get_file(props),
-                                Position.get_line(props),
-                                Position.get_id(props),
-                                Position.get_offset(props))))
-                        case _ => state
-                      }
-                    }
-                    else {
-                      state.add_markup(
-                        command.decode_range(range,
-                          Command.HighlightInfo(kind, Markup.get_string(Markup.KIND, atts))))
-                    }
-                  case _ => state
-                }
-              case _ => System.err.println("Ignored report message: " + elem); state
+        case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
+          (this /: msgs)((state, msg) =>
+            msg match {
+              case XML.Elem(Markup(name, atts), args)
+              if Position.get_id(atts) == Some(command.id) && Position.get_range(atts).isDefined =>
+                val range = command.decode_range(Position.get_range(atts).get)
+                val props = atts.filterNot(p => Markup.POSITION_PROPERTIES(p._1))
+                val node = Markup_Tree.Node[Any](range, XML.Elem(Markup(name, props), args))
+                add_markup(node)
+              case _ => System.err.println("Ignored report message: " + msg); state
             })
         case _ => add_result(message)
       }
@@ -152,15 +119,11 @@
   val source: String = span.map(_.source).mkString
   def source(range: Text.Range): String = source.substring(range.start, range.stop)
   def length: Int = source.length
+
   val range: Text.Range = Text.Range(0, length)
 
   lazy val symbol_index = new Symbol.Index(source)
-
-
-  /* markup */
-
-  def decode_range(range: Text.Range, info: Any): Markup_Tree.Node[Any] =
-    new Markup_Tree.Node(symbol_index.decode(range), info)
+  def decode_range(r: Text.Range): Text.Range = symbol_index.decode(r)
 
 
   /* accumulated results */

--- a/src/Tools/jEdit/src/jedit/document_model.scala	Fri Aug 20 22:35:01 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 22 12:54:12 2010 +0200
@@ -257,14 +257,17 @@
     override def markTokens(prev: TokenMarker.LineContext,
         handler: TokenHandler, line_segment: Segment): TokenMarker.LineContext =
     {
+      // FIXME proper synchronization / thread context (!??)
+      val snapshot = Swing_Thread.now { Document_Model.this.snapshot() }
+
       val previous = prev.asInstanceOf[Document_Model.Token_Markup.LineContext]
       val line = if (prev == null) 0 else previous.line + 1
       val context = new Document_Model.Token_Markup.LineContext(line, previous)
+
       val start = buffer.getLineStartOffset(line)
       val stop = start + line_segment.count
-
-      // FIXME proper synchronization / thread context (!??)
-      val snapshot = Swing_Thread.now { Document_Model.this.snapshot() }
+      val range = Text.Range(start, stop)
+      val former_range = snapshot.revert(range)
 
       /* FIXME
       for (text_area <- Isabelle.jedit_text_areas(buffer)
@@ -275,35 +278,39 @@
       def handle_token(style: Byte, offset: Text.Offset, length: Int) =
         handler.handleToken(line_segment, style, offset, length, context)
 
+      val syntax = session.current_syntax()
+      val token_markup: PartialFunction[Any, Byte] =
+      {
+        case XML.Elem(Markup(Markup.COMMAND, List((Markup.NAME, name))), _)
+        if syntax.keyword_kind(name).isDefined =>
+          Document_Model.Token_Markup.command_style(syntax.keyword_kind(name).get)
+
+        case XML.Elem(Markup(name, _), _)
+        if Document_Model.Token_Markup.token_style(name) != Token.NULL =>
+          Document_Model.Token_Markup.token_style(name)
+      }
+
       var next_x = start
       for {
-        (command, command_start) <-
-          snapshot.node.command_range(snapshot.revert(Text.Range(start, stop)))
-        markup <- snapshot.state(command).highlight
-        val Text.Range(abs_start, abs_stop) = snapshot.convert(markup.range + command_start)
-        if (abs_stop > start)
-        if (abs_start < stop)
+        (command, command_start) <- snapshot.node.command_range(former_range)
+        val root_node =
+          Markup_Tree.Node((former_range - command_start).restrict(command.range), Token.NULL)
+        node <- snapshot.state(command).markup.select(root_node)(token_markup)
+        val Text.Range(abs_start, abs_stop) = snapshot.convert(node.range + command_start)
+        if abs_stop > start && abs_start < stop  // FIXME abs_range overlaps range (redundant!?)
+      }
+      {
         val token_start = (abs_start - start) max 0
         val token_length =
           (abs_stop - abs_start) -
           ((start - abs_start) max 0) -
           ((abs_stop - stop) max 0)
-      }
-      {
-        val token_type =
-          markup.info match {
-            case Command.HighlightInfo(Markup.COMMAND, Some(kind)) =>
-              Document_Model.Token_Markup.command_style(kind)
-            case Command.HighlightInfo(kind, _) =>
-              Document_Model.Token_Markup.token_style(kind)
-            case _ => Token.NULL
-          }
-        if (start + token_start > next_x)
+        if (start + token_start > next_x)  // FIXME ??
           handle_token(Token.COMMENT1, next_x - start, start + token_start - next_x)
-        handle_token(token_type, token_start, token_length)
+        handle_token(node.info, token_start, token_length)
         next_x = start + token_start + token_length
       }
-      if (next_x < stop)
+      if (next_x < stop)  // FIXME ??
         handle_token(Token.COMMENT1, next_x - start, stop - next_x)
 
       handle_token(Token.END, line_segment.count, 0)