removed inaccessible blobs from Document.Nodes;
authorwenzelm
Fri Dec 01 20:29:58 2017 +0100 (12 months ago)
changeset 67112deb2fcbda16e
parent 67111 42f290d8ccbd
child 67113 79ab935a7e22
removed inaccessible blobs from Document.Nodes;
src/Pure/PIDE/document.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Dec 01 18:20:15 2017 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Dec 01 20:29:58 2017 +0100
     1.3 @@ -341,11 +341,11 @@
     1.4        graph1.is_maximal(name) && graph1.get_node(name).is_empty
     1.5      }
     1.6  
     1.7 -    def purge_hidden: Option[Nodes] =
     1.8 -    {
     1.9 -      val hidden = graph.keys_iterator.filter(is_hidden(_)).toList
    1.10 -      if (hidden.isEmpty) None else Some(new Nodes((graph /: hidden)(_.del_node(_))))
    1.11 -    }
    1.12 +    def purge(pred: Node.Name => Boolean): Option[Nodes] =
    1.13 +      graph.keys_iterator.filter(pred).toList match {
    1.14 +        case Nil => None
    1.15 +        case del => Some(new Nodes((graph /: del)(_.del_node(_))))
    1.16 +      }
    1.17  
    1.18      def + (entry: (Node.Name, Node)): Nodes =
    1.19      {
    1.20 @@ -385,6 +385,10 @@
    1.21    {
    1.22      val init: Version = new Version()
    1.23      def make(nodes: Nodes): Version = new Version(Document_ID.make(), nodes)
    1.24 +
    1.25 +    def purge(f: Version => Option[Version], versions: Map[Document_ID.Version, Version])
    1.26 +      : Map[Document_ID.Version, Version] =
    1.27 +      (versions /: (for ((id, v) <- versions.iterator; v1 <- f(v)) yield (id, v1)))(_ + _)
    1.28    }
    1.29  
    1.30    final class Version private(
    1.31 @@ -394,7 +398,11 @@
    1.32      override def toString: String = "Version(" + id + ")"
    1.33  
    1.34      def purge_hidden: Option[Version] =
    1.35 -      nodes.purge_hidden.map(nodes1 => new Version(id, nodes1))
    1.36 +      nodes.purge(nodes.is_hidden(_)).map(new Version(id, _))
    1.37 +
    1.38 +    def purge_blobs(blobs: Set[Node.Name]): Option[Version] =
    1.39 +      nodes.purge(name => nodes(name).get_blob.isDefined && !blobs.contains(name)).
    1.40 +        map(new Version(id, _))
    1.41    }
    1.42  
    1.43  
    1.44 @@ -721,23 +729,23 @@
    1.45  
    1.46      def removed_versions(removed: List[Document_ID.Version]): State =
    1.47      {
    1.48 -      val versions1 = versions -- removed
    1.49 -      val versions2 =
    1.50 -        (versions1 /:
    1.51 -          (for ((id, v) <- versions1.iterator; v1 <- v.purge_hidden) yield (id, v1)))(_ + _)
    1.52 +      val versions1 = Version.purge(_.purge_hidden, versions -- removed)
    1.53  
    1.54        val assignments1 = assignments -- removed
    1.55 +      var blobs1_names = Set.empty[Node.Name]
    1.56        var blobs1 = Set.empty[SHA1.Digest]
    1.57        var commands1 = Map.empty[Document_ID.Command, Command.State]
    1.58        var execs1 = Map.empty[Document_ID.Exec, Command.State]
    1.59        for {
    1.60 -        (version_id, version) <- versions2.iterator
    1.61 +        (version_id, version) <- versions1.iterator
    1.62          command_execs = assignments1(version_id).command_execs
    1.63          (_, node) <- version.nodes.iterator
    1.64          command <- node.commands.iterator
    1.65        } {
    1.66 -        for ((_, digest) <- command.blobs_defined; if !blobs1.contains(digest))
    1.67 +        for ((name, digest) <- command.blobs_defined) {
    1.68 +          blobs1_names += name
    1.69            blobs1 += digest
    1.70 +        }
    1.71  
    1.72          if (!commands1.isDefinedAt(command.id))
    1.73            commands.get(command.id).foreach(st => commands1 += (command.id -> st))
    1.74 @@ -747,8 +755,9 @@
    1.75              execs.get(exec_id).foreach(st => execs1 += (exec_id -> st))
    1.76          }
    1.77        }
    1.78 +
    1.79        copy(
    1.80 -        versions = versions2,
    1.81 +        versions = Version.purge(_.purge_blobs(blobs1_names), versions1),
    1.82          blobs = blobs1,
    1.83          commands = commands1,
    1.84          execs = execs1,