# HG changeset patch
# User wenzelm
# Date 1397033046 -7200
# Node ID 884e8f37492c2a218cefd5837dd7b9643cec2822
# Parent  47500d0881f940ee5de33ec9ecd95426d9c0477b
tuned;

diff -r 47500d0881f9 -r 884e8f37492c src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Wed Apr 09 09:37:49 2014 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Apr 09 10:44:06 2014 +0200
@@ -75,6 +75,8 @@
 
   final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
   {
+    def is_empty: Boolean = rep.isEmpty
+
     def apply(index: Markup_Index): Markup_Tree =
       rep.getOrElse(index, Markup_Tree.empty)
 
@@ -86,11 +88,14 @@
         yield id
 
     def redirect(other_id: Document_ID.Generic): Markups =
-      new Markups(
+    {
+      val rep1 =
         (for {
           (Markup_Index(status, Text.Chunk.Id(id)), markup) <- rep.iterator
           if other_id == id
-        } yield (Markup_Index(status, Text.Chunk.Default), markup)).toMap)
+        } yield (Markup_Index(status, Text.Chunk.Default), markup)).toMap
+      if (rep1.isEmpty) Markups.empty else new Markups(rep1)
+    }
 
     override def hashCode: Int = rep.hashCode
     override def equals(that: Any): Boolean =
@@ -135,9 +140,12 @@
 
     def markup(index: Markup_Index): Markup_Tree = markups(index)
 
-    def redirect(other_command: Command): State =
-      new State(other_command, Nil, Results.empty, markups.redirect(other_command.id))
-
+    def redirect(other_command: Command): Option[State] =
+    {
+      val markups1 = markups.redirect(other_command.id)
+      if (markups1.is_empty) None
+      else Some(new State(other_command, Nil, Results.empty, markups1))
+    }
 
     def eq_content(other: State): Boolean =
       command.source == other.command.source &&
diff -r 47500d0881f9 -r 884e8f37492c src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed Apr 09 09:37:49 2014 +0200
+++ b/src/Pure/PIDE/document.scala	Wed Apr 09 10:44:06 2014 +0200
@@ -688,7 +688,7 @@
           } yield (id, st)).toMap.valuesIterator.toList
         }
         else Nil
-      self.map(_._2) ::: others.map(_.redirect(command))
+      self.map(_._2) ::: others.flatMap(_.redirect(command))
     }
 
     def command_results(version: Version, command: Command): Command.Results =