simplified via Position extractors;

--- a/src/Pure/General/position.scala	Wed May 05 22:23:45 2010 +0200
+++ b/src/Pure/General/position.scala	Wed May 05 23:09:34 2010 +0200
@@ -33,10 +33,13 @@
   def get_file(pos: T): Option[String] = get_string(Markup.FILE, pos)
   def get_id(pos: T): Option[String] = get_string(Markup.ID, pos)
 
-  def get_offsets(pos: T): (Option[Int], Option[Int]) =
-  {
-    val begin = get_offset(pos)
-    val end = get_end_offset(pos)
-    (begin, if (end.isDefined) end else begin.map(_ + 1))
-  }
+  def get_range(pos: T): Option[(Int, Int)] =
+    (get_offset(pos), get_end_offset(pos)) match {
+      case (Some(begin), Some(end)) => Some(begin, end)
+      case (Some(begin), None) => Some(begin, begin + 1)
+      case (None, _) => None
+    }
+
+  object Id { def unapply(pos: T): Option[String] = get_id(pos) }
+  object Range { def unapply(pos: T): Option[(Int, Int)] = get_range(pos) }
 }

--- a/src/Pure/PIDE/state.scala	Wed May 05 22:23:45 2010 +0200
+++ b/src/Pure/PIDE/state.scala	Wed May 05 23:09:34 2010 +0200
@@ -81,29 +81,31 @@
               case XML.Elem(Markup.FINISHED, _, _) => state.set_status(Command.Status.FINISHED)
               case XML.Elem(Markup.FAILED, _, _) => state.set_status(Command.Status.FAILED)
               case XML.Elem(kind, atts, body) =>
-                val (begin, end) = Position.get_offsets(atts)
-                if (begin.isEmpty || end.isEmpty) state
-                else if (kind == Markup.ML_TYPING) {
-                  val info = body.head.asInstanceOf[XML.Text].content   // FIXME proper match!?
-                  state.add_markup(
-                    command.markup_node(begin.get - 1, end.get - 1, Command.TypeInfo(info)))
-                }
-                else if (kind == Markup.ML_REF) {
-                  body match {
-                    case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
-                      state.add_markup(command.markup_node(
-                        begin.get - 1, end.get - 1,
-                        Command.RefInfo(
-                          Position.get_file(atts),
-                          Position.get_line(atts),
-                          Position.get_id(atts),
-                          Position.get_offset(atts))))
-                    case _ => state
-                  }
-                }
-                else {
-                  state.add_markup(
-                    command.markup_node(begin.get - 1, end.get - 1, Command.HighlightInfo(kind)))
+                atts match {
+                  case Position.Range(begin, end) =>
+                    if (kind == Markup.ML_TYPING) {
+                      val info = body.head.asInstanceOf[XML.Text].content   // FIXME proper match!?
+                      state.add_markup(
+                        command.markup_node(begin - 1, end - 1, Command.TypeInfo(info)))
+                    }
+                    else if (kind == Markup.ML_REF) {
+                      body match {
+                        case List(XML.Elem(Markup.ML_DEF, atts, _)) =>
+                          state.add_markup(command.markup_node(
+                            begin - 1, end - 1,
+                            Command.RefInfo(
+                              Position.get_file(atts),
+                              Position.get_line(atts),
+                              Position.get_id(atts),
+                              Position.get_offset(atts))))
+                        case _ => state
+                      }
+                    }
+                    else {
+                      state.add_markup(
+                        command.markup_node(begin - 1, end - 1, Command.HighlightInfo(kind)))
+                    }
+                  case _ => state
                 }
               case _ =>
                 System.err.println("ignored status report: " + elem)