tuned;
authorwenzelm
Sun, 16 Oct 2022 15:35:38 +0200
changeset 76317 9783e79a37c6
parent 76316 7563367690a1
child 76318 4556f76d216e
tuned;
src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Sun Oct 16 15:23:07 2022 +0200
+++ b/src/Pure/PIDE/headless.scala	Sun Oct 16 15:35:38 2022 +0200
@@ -516,13 +516,13 @@
       def remove_required(id: UUID.T, names: List[Document.Node.Name]): State =
         copy(required = names.foldLeft(required)(_.remove(_, id)))
 
-      def update_theories(update: List[(Document.Node.Name, Theory)]): State =
+      def update_theories(update: List[Theory]): State =
         copy(theories =
           update.foldLeft(theories) {
-            case (thys, (name, thy)) =>
-              thys.get(name) match {
+            case (thys, thy) =>
+              thys.get(thy.node_name) match {
                 case Some(thy1) if thy1 == thy => thys
-                case _ => thys + (name -> thy)
+                case _ => thys + (thy.node_name -> thy)
               }
           })
 
@@ -544,9 +544,9 @@
           yield {
             val theory1 = theory.set_required(st1.is_required(node_name))
             val edits = theory1.node_edits(Some(theory))
-            (edits, (node_name, theory1))
+            (theory1, edits)
           }
-        (theory_edits.flatMap(_._1), st1.update_theories(theory_edits.map(_._2)))
+        (theory_edits.flatMap(_._2), st1.update_theories(theory_edits.map(_._1)))
       }
 
       def purge_theories(
@@ -632,14 +632,14 @@
             val old_theory = st.theories.get(node_name)
             val theory1 = theory.set_required(st1.is_required(node_name))
             val edits = theory1.node_edits(old_theory)
-            (edits, (node_name, theory1))
+            (theory1, edits)
           }
         val file_edits =
           for { node_name <- files if doc_blobs1.changed(node_name) }
           yield st1.blob_edits(node_name, st.blobs.get(node_name))
 
-        session.update(doc_blobs1, theory_edits.flatMap(_._1) ::: file_edits.flatten)
-        st1.update_theories(theory_edits.map(_._2))
+        session.update(doc_blobs1, theory_edits.flatMap(_._2) ::: file_edits.flatten)
+        st1.update_theories(theory_edits.map(_._1))
       }
     }