diff -r 7563367690a1 -r 9783e79a37c6 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)) } }