--- 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 */