# HG changeset patch
# User wenzelm
# Date 1607170338 -3600
# Node ID 0f01783400b20ee9d7c18a8b63a292acb0b3513a
# Parent  55792cb3892f56a88e8255286dfb43d0a4d56af6
tuned;

diff -r 55792cb3892f -r 0f01783400b2 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sat Dec 05 13:01:46 2020 +0100
+++ b/src/Pure/PIDE/document.scala	Sat Dec 05 13:12:18 2020 +0100
@@ -1100,11 +1100,9 @@
       pending_edits: List[Text.Edit] = Nil,
       snippet_command: Option[Command] = None): Snapshot =
     {
-      val stable = recent_stable
-      val latest = history.tip
+      /* pending edits and unstable changes */
 
-
-      /* pending edits and unstable changes */
+      val stable = recent_stable
 
       val rev_pending_changes =
         for {
@@ -1123,7 +1121,7 @@
       new Snapshot(
         state = this,
         version = stable.version.get_finished,
-        is_outdated = pending_edits.nonEmpty || latest != stable,
+        is_outdated = edits.nonEmpty,
         node_name = node_name,
         snippet_command = snippet_command)
       {