purge history more thoroughly (see also 3156faac30a7);
authorwenzelm
Wed May 02 17:35:51 2018 +0200 (22 months ago ago)
changeset 6806763f03ee4057e
parent 68065 d2daeef3ce47
child 68068 b91c4acc1aaf
purge history more thoroughly (see also 3156faac30a7);
src/Pure/PIDE/document.scala
     1.1 --- a/src/Pure/PIDE/document.scala	Wed May 02 12:48:08 2018 +0100
     1.2 +++ b/src/Pure/PIDE/document.scala	Wed May 02 17:35:51 2018 +0200
     1.3 @@ -412,6 +412,19 @@
     1.4      def purge(f: Version => Option[Version], versions: Map[Document_ID.Version, Version])
     1.5        : Map[Document_ID.Version, Version] =
     1.6        (versions /: (for ((id, v) <- versions.iterator; v1 <- f(v)) yield (id, v1)))(_ + _)
     1.7 +
     1.8 +    def purge_future(versions: Map[Document_ID.Version, Version], future: Future[Version])
     1.9 +      : Future[Version] =
    1.10 +    {
    1.11 +      if (future.is_finished) {
    1.12 +        val version = future.join
    1.13 +        versions.get(version.id) match {
    1.14 +          case Some(version1) if !(version eq version1) => Future.value(version1)
    1.15 +          case _ => future
    1.16 +        }
    1.17 +      }
    1.18 +      else future
    1.19 +    }
    1.20    }
    1.21  
    1.22    final class Version private(
    1.23 @@ -449,6 +462,14 @@
    1.24        version.is_finished
    1.25  
    1.26      def truncate: Change = new Change(None, Nil, version)
    1.27 +
    1.28 +    def purge(versions: Map[Document_ID.Version, Version]): Option[Change] =
    1.29 +    {
    1.30 +      val previous1 = previous.map(Version.purge_future(versions, _))
    1.31 +      val version1 = Version.purge_future(versions, version)
    1.32 +      if ((previous eq previous1) && (version eq version1)) None
    1.33 +      else Some(new Change(previous1, rev_edits, version1))
    1.34 +    }
    1.35    }
    1.36  
    1.37  
    1.38 @@ -477,6 +498,13 @@
    1.39          case _ => None
    1.40        }
    1.41      }
    1.42 +
    1.43 +    def purge(versions: Map[Document_ID.Version, Version]): History =
    1.44 +    {
    1.45 +      val undo_list1 = undo_list.map(_.purge(versions))
    1.46 +      if (undo_list1.forall(_.isEmpty)) this
    1.47 +      else new History(for ((a, b) <- undo_list1 zip undo_list) yield a.getOrElse(b))
    1.48 +    }
    1.49    }
    1.50  
    1.51  
    1.52 @@ -786,13 +814,16 @@
    1.53          }
    1.54        }
    1.55  
    1.56 +      val versions2 = Version.purge(_.purge_blobs(blobs1_names), versions1)
    1.57 +
    1.58        copy(
    1.59 -        versions = Version.purge(_.purge_blobs(blobs1_names), versions1),
    1.60 +        versions = versions2,
    1.61          blobs = blobs1,
    1.62          commands = commands1,
    1.63          execs = execs1,
    1.64          commands_redirection = commands_redirection.restrict(commands1.isDefinedAt(_)),
    1.65          assignments = assignments1,
    1.66 +        history = history.purge(versions2),
    1.67          removing_versions = false)
    1.68      }
    1.69