tuned whitespace;
authorwenzelm
Wed Nov 21 20:15:25 2012 +0100 (2012-11-21 ago)
changeset 5015776efdb6daab2
parent 50156 12a65e2ee296
child 50158 7b61a539721e
tuned whitespace;
src/Pure/PIDE/protocol.scala
     1.1 --- a/src/Pure/PIDE/protocol.scala	Wed Nov 21 16:43:14 2012 +0100
     1.2 +++ b/src/Pure/PIDE/protocol.scala	Wed Nov 21 20:15:25 2012 +0100
     1.3 @@ -141,7 +141,7 @@
     1.4  
     1.5    /* specific messages */
     1.6  
     1.7 - def is_tracing(msg: XML.Tree): Boolean =
     1.8 +  def is_tracing(msg: XML.Tree): Boolean =
     1.9      msg match {
    1.10        case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true
    1.11        case XML.Elem(Markup(Isabelle_Markup.TRACING_MESSAGE, _), _) => true
    1.12 @@ -186,6 +186,7 @@
    1.13        val range = command.decode(raw_range).restrict(command.range)
    1.14        body.foldLeft(if (range.is_singularity) set else set + range)(positions)
    1.15      }
    1.16 +
    1.17      def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
    1.18        tree match {
    1.19          case XML.Wrapped_Elem(Markup(name, Position.Id_Range(id, range)), _, body)
    1.20 @@ -200,6 +201,7 @@
    1.21  
    1.22          case _ => set
    1.23        }
    1.24 +
    1.25      val set = positions(Set.empty, message)
    1.26      if (set.isEmpty && !is_state(message))
    1.27        set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))