# 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