# HG changeset patch
# User wenzelm
# Date 1537625011 -7200
# Node ID d75cd481f8d9f98d23d0777af1b905d98bfe917d
# Parent  855c3c501b098146180f24c76bd41e51ada0bb53
proper status after commit;

diff -r 855c3c501b09 -r d75cd481f8d9 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sat Sep 22 15:22:29 2018 +0200
+++ b/src/Pure/PIDE/headless.scala	Sat Sep 22 16:03:31 2018 +0200
@@ -142,31 +142,29 @@
           commit: Option[(Document.Snapshot, Document_Status.Node_Status) => Unit])
         : Use_Theories_State =
       {
-        val st1 =
+        val already_committed1 =
           if (commit.isDefined) {
-            val already_committed1 =
-              (already_committed /: dep_theories)({ case (committed, name) =>
-                def parents_committed: Boolean =
-                  version.nodes(name).header.imports.forall({ case (parent, _) =>
-                    Sessions.is_pure(parent.theory) || committed.isDefinedAt(parent)
-                  })
-                if (!committed.isDefinedAt(name) && parents_committed &&
-                    state.node_consolidated(version, name))
-                {
-                  val snapshot = stable_snapshot(state, version, name)
-                  val status = Document_Status.Node_Status.make(state, version, name)
-                  commit.get.apply(snapshot, status)
-                  committed + (name -> status)
-                }
-                else committed
-              })
-            copy(already_committed = already_committed1)
+            (already_committed /: dep_theories)({ case (committed, name) =>
+              def parents_committed: Boolean =
+                version.nodes(name).header.imports.forall({ case (parent, _) =>
+                  Sessions.is_pure(parent.theory) || committed.isDefinedAt(parent)
+                })
+              if (!committed.isDefinedAt(name) && parents_committed &&
+                  state.node_consolidated(version, name))
+              {
+                val snapshot = stable_snapshot(state, version, name)
+                val status = Document_Status.Node_Status.make(state, version, name)
+                commit.get.apply(snapshot, status)
+                committed + (name -> status)
+              }
+              else committed
+            })
           }
-          else this
+          else already_committed
 
         if (beyond_limit || watchdog(watchdog_timeout) ||
           dep_theories.forall(name =>
-            already_committed.isDefinedAt(name) ||
+            already_committed1.isDefinedAt(name) ||
             state.node_consolidated(version, name) ||
             nodes_status.quasi_consolidated(name)))
         {
@@ -176,14 +174,14 @@
           val nodes_committed =
             for {
               name <- dep_theories
-              status <- already_committed.get(name)
+              status <- already_committed1.get(name)
             } yield (name -> status)
 
           try { result.fulfill(new Use_Theories_Result(state, version, nodes, nodes_committed)) }
           catch { case _: IllegalStateException => }
         }
 
-        st1
+        copy(already_committed = already_committed1)
       }
     }