src/Pure/Thy/thy_resources.scala
changeset 68915 634768c0bd22
parent 68914 51bd9e9501fb
child 68916 2a1583baaaa0
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Wed Sep 05 20:00:38 2018 +0200
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Wed Sep 05 20:29:23 2018 +0200
     1.3 @@ -255,12 +255,15 @@
     1.4      }
     1.5  
     1.6      def purge_theories(
     1.7 -        theories: List[String],
     1.8 -        qualifier: String = Sessions.DRAFT,
     1.9 -        master_dir: String = "",
    1.10 -        all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
    1.11 -      resources.purge_theories(session, theories = theories, qualifier = qualifier,
    1.12 -        master_dir = proper_string(master_dir) getOrElse tmp_dir_name, all = all)
    1.13 +      theories: List[String],
    1.14 +      qualifier: String = Sessions.DRAFT,
    1.15 +      master_dir: String = "",
    1.16 +      all: Boolean = false): (List[Document.Node.Name], List[Document.Node.Name]) =
    1.17 +    {
    1.18 +      val master = proper_string(master_dir) getOrElse tmp_dir_name
    1.19 +      val nodes = if (all) None else Some(theories.map(resources.import_name(qualifier, master, _)))
    1.20 +      resources.purge_theories(session, nodes)
    1.21 +    }
    1.22    }
    1.23  
    1.24  
    1.25 @@ -399,21 +402,16 @@
    1.26        })
    1.27    }
    1.28  
    1.29 -  def purge_theories(session: Session,
    1.30 -    theories: List[String],
    1.31 -    qualifier: String,
    1.32 -    master_dir: String,
    1.33 -    all: Boolean): (List[Document.Node.Name], List[Document.Node.Name]) =
    1.34 +  def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]])
    1.35 +    : (List[Document.Node.Name], List[Document.Node.Name]) =
    1.36    {
    1.37 -    val nodes = theories.map(import_name(qualifier, master_dir, _))
    1.38 -
    1.39      state.change_result(st =>
    1.40        {
    1.41          val graph = st.theories_graph
    1.42          val all_nodes = graph.topological_order
    1.43  
    1.44          val purge =
    1.45 -          (if (all) all_nodes else nodes.filter(graph.defined(_))).
    1.46 +          (if (nodes.isEmpty) all_nodes else nodes.get.filter(graph.defined(_))).
    1.47              filterNot(st.is_required(_)).toSet
    1.48  
    1.49          val retain = graph.all_preds(all_nodes.filterNot(purge)).toSet