# HG changeset patch
# User wenzelm
# Date 1353525325 -3600
# Node ID 76efdb6daab2288111eb0063ea5138d3d1e79f45
# Parent  12a65e2ee296f079e435c096ef25e50f59d9c22c
tuned whitespace;

diff -r 12a65e2ee296 -r 76efdb6daab2 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Wed Nov 21 16:43:14 2012 +0100
+++ b/src/Pure/PIDE/protocol.scala	Wed Nov 21 20:15:25 2012 +0100
@@ -141,7 +141,7 @@
 
   /* specific messages */
 
- def is_tracing(msg: XML.Tree): Boolean =
+  def is_tracing(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Isabelle_Markup.TRACING, _), _) => true
       case XML.Elem(Markup(Isabelle_Markup.TRACING_MESSAGE, _), _) => true
@@ -186,6 +186,7 @@
       val range = command.decode(raw_range).restrict(command.range)
       body.foldLeft(if (range.is_singularity) set else set + range)(positions)
     }
+
     def positions(set: Set[Text.Range], tree: XML.Tree): Set[Text.Range] =
       tree match {
         case XML.Wrapped_Elem(Markup(name, Position.Id_Range(id, range)), _, body)
@@ -200,6 +201,7 @@
 
         case _ => set
       }
+
     val set = positions(Set.empty, message)
     if (set.isEmpty && !is_state(message))
       set ++ Position.Range.unapply(message.markup.properties).map(command.decode(_))