tuned;
authorwenzelm
Wed Apr 09 10:44:06 2014 +0200 (2014-04-09)
changeset 56489884e8f37492c
parent 56481 47500d0881f9
child 56490 16d00478b518
tuned;
src/Pure/PIDE/command.scala
src/Pure/PIDE/document.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Wed Apr 09 09:37:49 2014 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Wed Apr 09 10:44:06 2014 +0200
     1.3 @@ -75,6 +75,8 @@
     1.4  
     1.5    final class Markups private(private val rep: Map[Markup_Index, Markup_Tree])
     1.6    {
     1.7 +    def is_empty: Boolean = rep.isEmpty
     1.8 +
     1.9      def apply(index: Markup_Index): Markup_Tree =
    1.10        rep.getOrElse(index, Markup_Tree.empty)
    1.11  
    1.12 @@ -86,11 +88,14 @@
    1.13          yield id
    1.14  
    1.15      def redirect(other_id: Document_ID.Generic): Markups =
    1.16 -      new Markups(
    1.17 +    {
    1.18 +      val rep1 =
    1.19          (for {
    1.20            (Markup_Index(status, Text.Chunk.Id(id)), markup) <- rep.iterator
    1.21            if other_id == id
    1.22 -        } yield (Markup_Index(status, Text.Chunk.Default), markup)).toMap)
    1.23 +        } yield (Markup_Index(status, Text.Chunk.Default), markup)).toMap
    1.24 +      if (rep1.isEmpty) Markups.empty else new Markups(rep1)
    1.25 +    }
    1.26  
    1.27      override def hashCode: Int = rep.hashCode
    1.28      override def equals(that: Any): Boolean =
    1.29 @@ -135,9 +140,12 @@
    1.30  
    1.31      def markup(index: Markup_Index): Markup_Tree = markups(index)
    1.32  
    1.33 -    def redirect(other_command: Command): State =
    1.34 -      new State(other_command, Nil, Results.empty, markups.redirect(other_command.id))
    1.35 -
    1.36 +    def redirect(other_command: Command): Option[State] =
    1.37 +    {
    1.38 +      val markups1 = markups.redirect(other_command.id)
    1.39 +      if (markups1.is_empty) None
    1.40 +      else Some(new State(other_command, Nil, Results.empty, markups1))
    1.41 +    }
    1.42  
    1.43      def eq_content(other: State): Boolean =
    1.44        command.source == other.command.source &&
     2.1 --- a/src/Pure/PIDE/document.scala	Wed Apr 09 09:37:49 2014 +0200
     2.2 +++ b/src/Pure/PIDE/document.scala	Wed Apr 09 10:44:06 2014 +0200
     2.3 @@ -688,7 +688,7 @@
     2.4            } yield (id, st)).toMap.valuesIterator.toList
     2.5          }
     2.6          else Nil
     2.7 -      self.map(_._2) ::: others.map(_.redirect(command))
     2.8 +      self.map(_._2) ::: others.flatMap(_.redirect(command))
     2.9      }
    2.10  
    2.11      def command_results(version: Version, command: Command): Command.Results =