src/Pure/PIDE/command.scala

       }
     override def toString: String = entries.mkString("Results(", ", ", ")")
   }
 
 
+  /* markup */
+
+  object Markup_Index
+  {
+    val markup: Markup_Index = Markup_Index(false, "")
+  }
+
+  sealed case class Markup_Index(status: Boolean, file_name: String)
+
+  object Markups
+  {
+    val empty: Markups = new Markups(Map.empty)
+
+    def init(markup: Markup_Tree): Markups =
+      new Markups(Map(Markup_Index.markup -> markup))
+  }
+
+  final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
+  {
+    def apply(index: Markup_Index): Markup_Tree =
+      rep.getOrElse(index, Markup_Tree.empty)
+
+    def add(index: Markup_Index, markup: Text.Markup): Markups =
+      new Markups(rep + (index -> (this(index) + markup)))
+
+    def ++ (other: Markups): Markups =
+      new Markups(
+        (rep.keySet ++ other.rep.keySet)
+          .map(index => index -> (this(index) ++ other(index))).toMap)
+
+    override def hashCode: Int = rep.hashCode
+    override def equals(that: Any): Boolean =
+      that match {
+        case other: Markups => rep == other.rep
+        case _ => false
+      }
+    override def toString: String = rep.iterator.mkString("Markups(", ", ", ")")
+  }
+
+
   /* state */
 
   sealed case class State(
     command: Command,
     status: List[Markup] = Nil,
     results: Results = Results.empty,
-    markups: Map[String, Markup_Tree] = Map.empty)
-  {
-    def get_markup(file_name: String): Markup_Tree =
-      markups.getOrElse(file_name, Markup_Tree.empty)
-
-    def markup: Markup_Tree = get_markup("")
+    markups: Markups = Markups.empty)
+  {
+    /* markup */
+
+    def get_markup(index: Markup_Index): Markup_Tree = markups(index)
+
+    def markup: Markup_Tree = get_markup(Markup_Index.markup)
 
     def markup_to_XML(filter: XML.Elem => Boolean): XML.Body =
       markup.to_XML(command.range, command.source, filter)
 
 

       command.source == other.command.source &&
       status == other.status &&
       results == other.results &&
       markups == other.markups
 
-    private def add_status(st: Markup): State = copy(status = st :: status)
-
-    private def add_markup(file_name: String, m: Text.Markup): State =
-      copy(markups = markups + (file_name -> (get_markup(file_name) + m)))
+    private def add_status(st: Markup): State =
+      copy(status = st :: status)
+
+    private def add_markup(status: Boolean, file_name: String, m: Text.Markup): State =
+    {
+      val markups1 =
+        if (status || Protocol.status_elements(m.info.name))
+          markups.add(Markup_Index(true, file_name), m)
+        else markups
+      copy(markups = markups1.add(Markup_Index(false, file_name), m))
+    }
 
     def + (alt_id: Document_ID.Generic, message: XML.Elem): State =
       message match {
         case XML.Elem(Markup(Markup.STATUS, _), msgs) =>
           (this /: msgs)((state, msg) =>
             msg match {
               case elem @ XML.Elem(markup, Nil) =>
-                state.add_status(markup).add_markup("", Text.Info(command.proper_range, elem))
-
+                state.
+                  add_status(markup).
+                  add_markup(true, "", Text.Info(command.proper_range, elem))
               case _ =>
                 System.err.println("Ignored status message: " + msg)
                 state
             })
 

                     case Some(chunk) =>
                       chunk.decode(raw_range).try_restrict(chunk.range) match {
                         case Some(range) =>
                           if (!range.is_singularity) {
                             val props = Position.purge(atts)
-                            state.add_markup(file_name,
-                              Text.Info(range, XML.Elem(Markup(name, props), args)))
+                            val info = Text.Info(range, XML.Elem(Markup(name, props), args))
+                            state.add_markup(false, file_name, info)
                           }
                           else state
                         case None => bad(); state
                       }
                     case None => bad(); state

                 case XML.Elem(Markup(name, atts), args)
                 if !atts.exists({ case (a, _) => Markup.POSITION_PROPERTIES(a) }) =>
                   val range = command.proper_range
                   val props = Position.purge(atts)
                   val info: Text.Markup = Text.Info(range, XML.Elem(Markup(name, props), args))
-                  state.add_markup("", info)
+                  state.add_markup(false, "", info)
 
                 case _ => /* FIXME bad(); */ state
               }
             })
         case XML.Elem(Markup(name, props), body) =>

               var st = copy(results = results + (i -> message1))
               if (Protocol.is_inlined(message)) {
                 for {
                   (file_name, chunk) <- command.chunks
                   range <- Protocol.message_positions(command.id, alt_id, chunk, message)
-                } st = st.add_markup(file_name, Text.Info(range, message2))
+                } st = st.add_markup(false, file_name, Text.Info(range, message2))
               }
               st
 
             case _ =>
               System.err.println("Ignored message without serial number: " + message)

 
     def ++ (other: State): State =
       copy(
         status = other.status ::: status,
         results = results ++ other.results,
-        markups =
-          (markups.keySet ++ other.markups.keySet)
-            .map(a => a -> (get_markup(a) ++ other.get_markup(a))).toMap
+        markups = markups ++ other.markups
       )
   }
 
 
 

 
 
   /* accumulated results */
 
   val init_state: Command.State =
-    Command.State(this, results = init_results, markups = Map("" -> init_markup))
+    Command.State(this, results = init_results, markups = Command.Markups.init(init_markup))
 
   val empty_state: Command.State = Command.State(this)
 }