# HG changeset patch
# User wenzelm
# Date 1536172163 -7200
# Node ID 634768c0bd2273f4ec3979d4fe3ae21022fa188b
# Parent  51bd9e9501fb21be8899aa958dee36c14e134003
tuned signature;

diff -r 51bd9e9501fb -r 634768c0bd22 src/Pure/Thy/thy_resources.scala
--- a/src/Pure/Thy/thy_resources.scala	Wed Sep 05 20:00:38 2018 +0200
+++ b/src/Pure/Thy/thy_resources.scala	Wed Sep 05 20:29:23 2018 +0200
@@ -255,12 +255,15 @@
     }
 
     def purge_theories(
-        theories: List[String],
-        qualifier: String = Sessions.DRAFT,
-        master_dir: String = "",
-        all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
-      resources.purge_theories(session, theories = theories, qualifier = qualifier,
-        master_dir = proper_string(master_dir) getOrElse tmp_dir_name, all = all)
+      theories: List[String],
+      qualifier: String = Sessions.DRAFT,
+      master_dir: String = "",
+      all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
+    {
+      val master = proper_string(master_dir) getOrElse tmp_dir_name
+      val nodes = if (all) None else Some(theories.map(resources.import_name(qualifier, master, _)))
+      resources.purge_theories(session, nodes)
+    }
   }
 
 
@@ -399,21 +402,16 @@
       })
   }
 
-  def purge_theories(session: Session,
-    theories: List[String],
-    qualifier: String,
-    master_dir: String,
-    all: Boolean): (List[Document.Node.Name], List[Document.Node.Name]) =
+  def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]])
+    : (List[Document.Node.Name], 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 (all) all_nodes else nodes.filter(graph.defined(_))).
+          (if (nodes.isEmpty) all_nodes else nodes.get.filter(graph.defined(_))).
             filterNot(st.is_required(_)).toSet
 
         val retain = graph.all_preds(all_nodes.filterNot(purge)).toSet