src/Pure/PIDE/isar_document.scala
changeset 39441 4110cc1b8f9f
parent 39439 1c294d150ded
child 39511 5f318522e6fe
     1.1 --- a/src/Pure/PIDE/isar_document.scala	Fri Sep 17 17:09:31 2010 +0200
     1.2 +++ b/src/Pure/PIDE/isar_document.scala	Fri Sep 17 17:10:44 2010 +0200
     1.3 @@ -56,35 +56,42 @@
     1.4    }
     1.5  
     1.6  
     1.7 -  /* messages */
     1.8 +  /* result messages */
     1.9  
    1.10    def clean_message(body: XML.Body): XML.Body =
    1.11      body filter { case XML.Elem(Markup(Markup.NO_REPORT, _), _) => false case _ => true } map
    1.12        { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
    1.13  
    1.14 +  def message_reports(msg: XML.Tree): List[XML.Elem] =
    1.15 +    msg match {
    1.16 +      case elem @ XML.Elem(Markup(Markup.REPORT, _), _) => List(elem)
    1.17 +      case XML.Elem(_, body) => body.flatMap(message_reports)
    1.18 +      case XML.Text(_) => Nil
    1.19 +    }
    1.20 +
    1.21  
    1.22    /* reported positions */
    1.23  
    1.24 -  private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
    1.25 -
    1.26 -  private def is_state(msg: XML.Tree): Boolean =
    1.27 +  def is_state(msg: XML.Tree): Boolean =
    1.28      msg match {
    1.29        case XML.Elem(Markup(Markup.WRITELN, _), List(XML.Elem(Markup(Markup.STATE, _), _))) => true
    1.30        case _ => false
    1.31      }
    1.32  
    1.33 -  def reported_positions(command: Command, message: XML.Elem): Set[Text.Range] =
    1.34 +  private val include_pos = Set(Markup.BINDING, Markup.ENTITY, Markup.REPORT, Markup.POSITION)
    1.35 +
    1.36 +  def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
    1.37    {
    1.38 -    def reported(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
    1.39 +    def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
    1.40        tree match {
    1.41          case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
    1.42          if include_pos(name) && id == command.id =>
    1.43            val range = command.decode(raw_range).restrict(command.range)
    1.44 -          body.foldLeft(if (range.is_singularity) set else set + range)(reported)
    1.45 -        case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(reported)
    1.46 +          body.foldLeft(if (range.is_singularity) set else set + range)(positions)
    1.47 +        case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)
    1.48          case _ => set
    1.49        }
    1.50 -    val set = reported(Set.empty, message)
    1.51 +    val set = positions(Set.empty, message)
    1.52      if (set.isEmpty && !is_state(message))
    1.53        set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))
    1.54      else set