# HG changeset patch
# User wenzelm
# Date 1521307133 -3600
# Node ID c854e50c211402cd0898a12e590d0b9286d9146e
# Parent  25e2b621bdcb0535a18721d69bdbf0251ad5f855
synchronized Session.update;

diff -r 25e2b621bdcb -r c854e50c2114 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Sat Mar 17 17:23:35 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Sat Mar 17 18:18:53 2018 +0100
@@ -204,43 +204,41 @@
         new Thy_Resources.Theory(node_name, node_header, text, true)
       }
 
-    val edits =
-      state.change_result(st =>
-        {
-          val st1 = st.insert_required(id, dep_theories)
-          val theory_edits =
-            for (theory <- loaded_theories)
-            yield {
-              val node_name = theory.node_name
-              val theory1 = theory.required(st1.is_required(node_name))
-              val edits = theory1.node_edits(st1.theories.get(node_name))
-              (edits, (node_name, theory1))
-            }
-          (theory_edits.flatMap(_._1), st1.update_theories(theory_edits.map(_._2)))
-        })
-    session.update(Document.Blobs.empty, edits)
+    state.change(st =>
+      {
+        val st1 = st.insert_required(id, dep_theories)
+        val theory_edits =
+          for (theory <- loaded_theories)
+          yield {
+            val node_name = theory.node_name
+            val theory1 = theory.required(st1.is_required(node_name))
+            val edits = theory1.node_edits(st1.theories.get(node_name))
+            (edits, (node_name, theory1))
+          }
+        session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
+        st1.update_theories(theory_edits.map(_._2))
+      })
 
     dep_theories
   }
 
   def unload_theories(session: Session, id: UUID, dep_theories: List[Document.Node.Name])
   {
-    val edits =
-      state.change_result(st =>
-        {
-          val st1 = st.remove_required(id, dep_theories)
-          val theory_edits =
-            for {
-              node_name <- dep_theories
-              theory <- st1.theories.get(node_name)
-            }
-            yield {
-              val theory1 = theory.required(st1.is_required(node_name))
-              val edits = theory1.node_edits(Some(theory))
-              (edits, (node_name, theory1))
-            }
-          (theory_edits.flatMap(_._1), st1.update_theories(theory_edits.map(_._2)))
-        })
-    session.update(Document.Blobs.empty, edits)
+    state.change(st =>
+      {
+        val st1 = st.remove_required(id, dep_theories)
+        val theory_edits =
+          for {
+            node_name <- dep_theories
+            theory <- st1.theories.get(node_name)
+          }
+          yield {
+            val theory1 = theory.required(st1.is_required(node_name))
+            val edits = theory1.node_edits(Some(theory))
+            (edits, (node_name, theory1))
+          }
+        session.update(Document.Blobs.empty, theory_edits.flatMap(_._1))
+        st1.update_theories(theory_edits.map(_._2))
+      })
   }
 }