src/Pure/PIDE/protocol.scala
changeset 49650 9fad6480300d
parent 49648 e5c16ccc5a87
child 50128 599c935aac82
     1.1 --- a/src/Pure/PIDE/protocol.scala	Fri Sep 28 17:06:07 2012 +0200
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Fri Sep 28 22:53:18 2012 +0200
     1.3 @@ -123,12 +123,17 @@
     1.4        case XML.Elem(Markup(Isabelle_Markup.REPORT, _), _) => false
     1.5        case XML.Elem(Markup(Isabelle_Markup.NO_REPORT, _), _) => false
     1.6        case _ => true
     1.7 -    } map { case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts)) case t => t }
     1.8 +    } map {
     1.9 +      case XML.Wrapped_Elem(markup, body, ts) => XML.Wrapped_Elem(markup, body, clean_message(ts))
    1.10 +      case XML.Elem(markup, ts) => XML.Elem(markup, clean_message(ts))
    1.11 +      case t => t
    1.12 +    }
    1.13  
    1.14    def message_reports(props: Properties.T, body: XML.Body): List[XML.Elem] =
    1.15      body flatMap {
    1.16        case XML.Elem(Markup(Isabelle_Markup.REPORT, ps), ts) =>
    1.17          List(XML.Elem(Markup(Isabelle_Markup.REPORT, props ::: ps), ts))
    1.18 +      case XML.Wrapped_Elem(_, _, ts) => message_reports(props, ts)
    1.19        case XML.Elem(_, ts) => message_reports(props, ts)
    1.20        case XML.Text(_) => Nil
    1.21      }
    1.22 @@ -175,13 +180,24 @@
    1.23  
    1.24    def message_positions(command: Command, message: XML.Elem): Set[Text.Range] =
    1.25    {
    1.26 +    def elem_positions(raw_range: Text.Range, set: Set[Text.Range], body: XML.Body)
    1.27 +      : Set[Text.Range] =
    1.28 +    {
    1.29 +      val range = command.decode(raw_range).restrict(command.range)
    1.30 +      body.foldLeft(if (range.is_singularity) set else set + range)(positions)
    1.31 +    }
    1.32      def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
    1.33        tree match {
    1.34 -        case XML.Elem(Markup(name, Position.Id_Range(id, raw_range)), body)
    1.35 -        if include_pos(name) && id == command.id =>
    1.36 -          val range = command.decode(raw_range).restrict(command.range)
    1.37 -          body.foldLeft(if (range.is_singularity) set else set + range)(positions)
    1.38 -        case XML.Elem(Markup(name, _), body) => body.foldLeft(set)(positions)
    1.39 +        case XML.Wrapped_Elem(Markup(name, Position.Id_Range(id, range)), _, body)
    1.40 +        if include_pos(name) && id == command.id => elem_positions(range, set, body)
    1.41 +
    1.42 +        case XML.Elem(Markup(name, Position.Id_Range(id, range)), body)
    1.43 +        if include_pos(name) && id == command.id => elem_positions(range, set, body)
    1.44 +
    1.45 +        case XML.Wrapped_Elem(_, _, body) => body.foldLeft(set)(positions)
    1.46 +
    1.47 +        case XML.Elem(_, body) => body.foldLeft(set)(positions)
    1.48 +
    1.49          case _ => set
    1.50        }
    1.51      val set = positions(Set.empty, message)