# HG changeset patch
# User wenzelm
# Date 1521841483 -3600
# Node ID 544a7a21298ec7cc3dc7b0a665300f227c2be0f0
# Parent  da44f151f716cb7d3ba180a31fedc5b7b9039d7e
clarified signature -- more like use_theories;

diff -r da44f151f716 -r 544a7a21298e src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Fri Mar 23 22:38:38 2018 +0100
+++ b/src/Pure/Thy/thy_resources.scala	Fri Mar 23 22:44:43 2018 +0100
@@ -138,8 +138,13 @@
       result.join
     }
 
-    def purge_theories(nodes: List[Document.Node.Name] = Nil, all: Boolean = false)
-      : List[Document.Node.Name] = resources.purge_theories(session, if (all) None else Some(nodes))
+    def purge_theories(
+        theories: List[String],
+        qualifier: String = Sessions.DRAFT,
+        master_dir: String = "",
+        all: Boolean = false): List[Document.Node.Name] =
+      resources.purge_theories(session, theories = theories, qualifier = qualifier,
+        master_dir = master_dir, all = all)
   }
 
 
@@ -288,16 +293,21 @@
       })
   }
 
-  def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]])
-    : List[Document.Node.Name] =
+  def purge_theories(session: Session,
+    theories: List[String],
+    qualifier: String = Sessions.DRAFT,
+    master_dir: String = "",
+    all: Boolean = false): List[Document.Node.Name] =
   {
+    val nodes = theories.map(import_name(qualifier, master_dir, _))
+
     state.change_result(st =>
       {
         val graph = st.theories_graph
         val all_nodes = graph.topological_order
 
         val purge =
-          (if (nodes.isEmpty) all_nodes else nodes.get.filter(graph.defined(_))).
+          (if (all) all_nodes else nodes.filter(graph.defined(_))).
             filterNot(st.is_required(_)).toSet
         val purged = all_nodes.filterNot(graph.all_preds(all_nodes.filterNot(purge)).toSet)