purge hidden nodes more thoroughly: is_hidden may become true only later;
authorwenzelm
Fri Dec 01 16:58:26 2017 +0100 (12 months ago)
changeset 671103156faac30a7
parent 67109 5fce3a24e476
child 67111 42f290d8ccbd
purge hidden nodes more thoroughly: is_hidden may become true only later;
src/Pure/PIDE/document.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Fri Dec 01 15:49:01 2017 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Fri Dec 01 16:58:26 2017 +0100
     1.3 @@ -341,6 +341,12 @@
     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 +
    1.13      def + (entry: (Node.Name, Node)): Nodes =
    1.14      {
    1.15        val (name, node) = entry
    1.16 @@ -349,10 +355,7 @@
    1.17          (graph.default_node(name, Node.empty) /: imports)((g, p) => g.default_node(p, Node.empty))
    1.18        val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
    1.19        val graph3 = (graph2 /: imports)((g, dep) => g.add_edge(dep, name))
    1.20 -      new Nodes(
    1.21 -        if (graph3.is_maximal(name) && node.is_empty) graph3.del_node(name)
    1.22 -        else graph3.map_node(name, _ => node)
    1.23 -      )
    1.24 +      new Nodes(graph3.map_node(name, _ => node))
    1.25      }
    1.26  
    1.27      def iterator: Iterator[(Node.Name, Node)] =
    1.28 @@ -389,6 +392,9 @@
    1.29      val nodes: Nodes = Nodes.empty)
    1.30    {
    1.31      override def toString: String = "Version(" + id + ")"
    1.32 +
    1.33 +    def purge_hidden: Option[Version] =
    1.34 +      nodes.purge_hidden.map(nodes1 => new Version(id, nodes1))
    1.35    }
    1.36  
    1.37  
    1.38 @@ -716,12 +722,16 @@
    1.39      def removed_versions(removed: List[Document_ID.Version]): State =
    1.40      {
    1.41        val versions1 = versions -- removed
    1.42 +      val versions2 =
    1.43 +        (versions1 /:
    1.44 +          (for ((id, v) <- versions1.iterator; v1 <- v.purge_hidden) yield (id, v1)))(_ + _)
    1.45 +
    1.46        val assignments1 = assignments -- removed
    1.47        var blobs1 = Set.empty[SHA1.Digest]
    1.48        var commands1 = Map.empty[Document_ID.Command, Command.State]
    1.49        var execs1 = Map.empty[Document_ID.Exec, Command.State]
    1.50        for {
    1.51 -        (version_id, version) <- versions1.iterator
    1.52 +        (version_id, version) <- versions2.iterator
    1.53          command_execs = assignments1(version_id).command_execs
    1.54          (_, node) <- version.nodes.iterator
    1.55          command <- node.commands.iterator
    1.56 @@ -738,7 +748,7 @@
    1.57          }
    1.58        }
    1.59        copy(
    1.60 -        versions = versions1,
    1.61 +        versions = versions2,
    1.62          blobs = blobs1,
    1.63          commands = commands1,
    1.64          execs = execs1,