# HG changeset patch
# User wenzelm
# Date 1570044471 -7200
# Node ID 9e3f359820219842afd9ca781c8832abfe5bd169
# Parent  a37e2ea96c6dcff8b0382c3cc58c514e06d7baa9
clarified signature -- potentially more robust;

diff -r a37e2ea96c6d -r 9e3f35982021 src/Pure/PIDE/headless.scala
--- a/src/Pure/PIDE/headless.scala	Wed Oct 02 20:58:09 2019 +0200
+++ b/src/Pure/PIDE/headless.scala	Wed Oct 02 21:27:51 2019 +0200
@@ -580,11 +580,11 @@
         st1.update_theories(theory_edits.map(_._2))
       }
 
-      def purge_theories(session: Session, nodes: List[Document.Node.Name])
+      def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]])
         : ((List[Document.Node.Name], List[Document.Node.Name]), State) =
       {
         val all_nodes = theory_graph.topological_order
-        val purge = nodes.filterNot(is_required(_)).toSet
+        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)
@@ -697,14 +697,13 @@
     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, theories)._2
-      )
+        st.unload_theories(session, id, theories).purge_theories(session, None)._2)
     }
 
     def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]])
       : (List[Document.Node.Name], List[Document.Node.Name]) =
     {
-      state.change_result(st => st.purge_theories(session, nodes getOrElse st.theory_graph.keys))
+      state.change_result(_.purge_theories(session, nodes))
     }
   }
 }