clarified signature -- more like use_theories;
authorwenzelm
Fri Mar 23 22:44:43 2018 +0100 (14 months ago)
changeset 67939544a7a21298e
parent 67938 da44f151f716
child 67940 b4e80f062fbf
clarified signature -- more like use_theories;
src/Pure/Thy/thy_resources.scala
     1.1 --- a/src/Pure/Thy/thy_resources.scala	Fri Mar 23 22:38:38 2018 +0100
     1.2 +++ b/src/Pure/Thy/thy_resources.scala	Fri Mar 23 22:44:43 2018 +0100
     1.3 @@ -138,8 +138,13 @@
     1.4        result.join
     1.5      }
     1.6  
     1.7 -    def purge_theories(nodes: List[Document.Node.Name] = Nil, all: Boolean = false)
     1.8 -      : List[Document.Node.Name] = resources.purge_theories(session, if (all) None else Some(nodes))
     1.9 +    def purge_theories(
    1.10 +        theories: List[String],
    1.11 +        qualifier: String = Sessions.DRAFT,
    1.12 +        master_dir: String = "",
    1.13 +        all: Boolean = false): List[Document.Node.Name] =
    1.14 +      resources.purge_theories(session, theories = theories, qualifier = qualifier,
    1.15 +        master_dir = master_dir, all = all)
    1.16    }
    1.17  
    1.18  
    1.19 @@ -288,16 +293,21 @@
    1.20        })
    1.21    }
    1.22  
    1.23 -  def purge_theories(session: Session, nodes: Option[List[Document.Node.Name]])
    1.24 -    : List[Document.Node.Name] =
    1.25 +  def purge_theories(session: Session,
    1.26 +    theories: List[String],
    1.27 +    qualifier: String = Sessions.DRAFT,
    1.28 +    master_dir: String = "",
    1.29 +    all: Boolean = false): List[Document.Node.Name] =
    1.30    {
    1.31 +    val nodes = theories.map(import_name(qualifier, master_dir, _))
    1.32 +
    1.33      state.change_result(st =>
    1.34        {
    1.35          val graph = st.theories_graph
    1.36          val all_nodes = graph.topological_order
    1.37  
    1.38          val purge =
    1.39 -          (if (nodes.isEmpty) all_nodes else nodes.get.filter(graph.defined(_))).
    1.40 +          (if (all) all_nodes else nodes.filter(graph.defined(_))).
    1.41              filterNot(st.is_required(_)).toSet
    1.42          val purged = all_nodes.filterNot(graph.all_preds(all_nodes.filterNot(purge)).toSet)
    1.43