# HG changeset patch # User wenzelm # Date 1273093774 -7200 # Node ID 1225dd15827da8b7c47a57bbfe93c74c65a37ef3 # Parent ac7961d42ac35f0b6bae8b97142a273ad9a8ace3 simplified via Position extractors; diff -r ac7961d42ac3 -r 1225dd15827d src/Pure/General/position.scala --- 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) } } diff -r ac7961d42ac3 -r 1225dd15827d src/Pure/PIDE/state.scala --- 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)