src/Pure/PIDE/isar_document.scala
changeset 38887 1261481ef5e5
parent 38581 d503a0912e14
child 39042 470fd769ae53
     1.1 --- a/src/Pure/PIDE/isar_document.scala	Tue Aug 31 22:03:55 2010 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Tue Aug 31 23:28:21 2010 +0200
     1.3 @@ -54,6 +54,22 @@
     1.4      else if (markup.exists(_.name == Markup.FINISHED)) Finished
     1.5      else Unprocessed
     1.6    }
     1.7 +
     1.8 +
     1.9 +  /* reported positions */
    1.10 +
    1.11 +  def reported_positions(command_id: Document.Command_ID, message: XML.Elem): Set[Text.Range] =
    1.12 +  {
    1.13 +    def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
    1.14 +      tree match {
    1.15 +        case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
    1.16 +        if (name == Markup.BINDING || name == Markup.ENTITY || name == Markup.REPORT) &&
    1.17 +          id == command_id => body.foldLeft(set + range)(reported)
    1.18 +        case XML.Elem(_, body) => body.foldLeft(set)(reported)
    1.19 +        case XML.Text(_) => set
    1.20 +      }
    1.21 +    reported(Set.empty, message) ++ Position.Range.unapply(message.markup.properties)
    1.22 +  }
    1.23  }
    1.24  
    1.25