# HG changeset patch
# User wenzelm
# Date 1525275351 -7200
# Node ID 63f03ee4057eb3e3a923775bef6d6b042c9fcf6d
# Parent  d2daeef3ce4722d315a0574f7b0a5844d1e53d4c
purge history more thoroughly (see also 3156faac30a7);

diff -r d2daeef3ce47 -r 63f03ee4057e src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Wed May 02 12:48:08 2018 +0100
+++ b/src/Pure/PIDE/document.scala	Wed May 02 17:35:51 2018 +0200
@@ -412,6 +412,19 @@
     def purge(f: Version => Option[Version], versions: Map[Document_ID.Version, Version])
       : Map[Document_ID.Version, Version] =
       (versions /: (for ((id, v) <- versions.iterator; v1 <- f(v)) yield (id, v1)))(_ + _)
+
+    def purge_future(versions: Map[Document_ID.Version, Version], future: Future[Version])
+      : Future[Version] =
+    {
+      if (future.is_finished) {
+        val version = future.join
+        versions.get(version.id) match {
+          case Some(version1) if !(version eq version1) => Future.value(version1)
+          case _ => future
+        }
+      }
+      else future
+    }
   }
 
   final class Version private(
@@ -449,6 +462,14 @@
       version.is_finished
 
     def truncate: Change = new Change(None, Nil, version)
+
+    def purge(versions: Map[Document_ID.Version, Version]): Option[Change] =
+    {
+      val previous1 = previous.map(Version.purge_future(versions, _))
+      val version1 = Version.purge_future(versions, version)
+      if ((previous eq previous1) && (version eq version1)) None
+      else Some(new Change(previous1, rev_edits, version1))
+    }
   }
 
 
@@ -477,6 +498,13 @@
         case _ => None
       }
     }
+
+    def purge(versions: Map[Document_ID.Version, Version]): History =
+    {
+      val undo_list1 = undo_list.map(_.purge(versions))
+      if (undo_list1.forall(_.isEmpty)) this
+      else new History(for ((a, b) <- undo_list1 zip undo_list) yield a.getOrElse(b))
+    }
   }
 
 
@@ -786,13 +814,16 @@
         }
       }
 
+      val versions2 = Version.purge(_.purge_blobs(blobs1_names), versions1)
+
       copy(
-        versions = Version.purge(_.purge_blobs(blobs1_names), versions1),
+        versions = versions2,
         blobs = blobs1,
         commands = commands1,
         execs = execs1,
         commands_redirection = commands_redirection.restrict(commands1.isDefinedAt(_)),
         assignments = assignments1,
+        history = history.purge(versions2),
         removing_versions = false)
     }