# HG changeset patch
# User wenzelm
# Date 1570046464 -7200
# Node ID 92f56fbfbab3779047293d12ca98cc39a18c5c8d
# Parent  9e3f359820219842afd9ca781c8832abfe5bd169
prefer atomic edits -- potentially more robust;

diff -r 9e3f35982021 -r 92f56fbfbab3 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Wed Oct 02 21:27:51 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Wed Oct 02 22:01:04 2019 +0200
@@ -563,7 +563,7 @@
       }
 
       def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name])
-        : State =
+        : (List[Document.Edit_Text], State) =
       {
         val st1 = remove_required(id, theories)
         val theory_edits =
@@ -576,23 +576,20 @@
             val edits = theory1.node_edits(Some(theory))
             (edits, (node_name, theory1))
           }
-        session.update(doc_blobs, theory_edits.flatMap(_._1))
-        st1.update_theories(theory_edits.map(_._2))
+        (theory_edits.flatMap(_._1), st1.update_theories(theory_edits.map(_._2)))
       }
 
       def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]])
-        : ((List[Document.Node.Name], List[Document.Node.Name]), State) =
+        : ((List[Document.Node.Name], List[Document.Node.Name], List[Document.Edit_Text]), State) =
       {
         val all_nodes = theory_graph.topological_order
         val purge = nodes.getOrElse(all_nodes).filterNot(is_required(_)).toSet
 
         val retain = theory_graph.all_preds(all_nodes.filterNot(purge)).toSet
         val (retained, purged) = all_nodes.partition(retain)
+        val purge_edits = purged.flatMap(name => theories(name).purge_edits)
 
-        val purge_edits = purged.flatMap(name => theories(name).purge_edits)
-        session.update(doc_blobs, purge_edits)
-
-        ((purged, retained), remove_theories(purged))
+        ((purged, retained, purge_edits), remove_theories(purged))
       }
     }
   }
@@ -691,19 +688,33 @@
 
     def unload_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name])
     {
-      state.change(_.unload_theories(session, id, theories))
+      state.change(st =>
+      {
+        val (edits, st1) = st.unload_theories(session, id, theories)
+        session.update(st.doc_blobs, edits)
+        st1
+      })
     }
 
     def clean_theories(session: Session, id: UUID.T, theories: List[Document.Node.Name])
     {
       state.change(st =>
-        st.unload_theories(session, id, theories).purge_theories(session, None)._2)
+      {
+        val (edits1, st1) = st.unload_theories(session, id, theories)
+        val ((_, _, edits2), st2) = st1.purge_theories(session, None)
+        session.update(st.doc_blobs, edits1 ::: edits2)
+        st2
+      })
     }
 
     def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]])
       : (List[Document.Node.Name], List[Document.Node.Name]) =
     {
-      state.change_result(_.purge_theories(session, nodes))
+      state.change_result(st =>
+      {
+        val ((purged, retained, _), st1) = st.purge_theories(session, nodes)
+        ((purged, retained), st1)
+      })
     }
   }
 }