src/Pure/Thy/sessions.scala
changeset 75760 f8be63d2ec6f
parent 75759 0cdccd0d1699
child 75764 07e097f60b85
equal deleted inserted replaced
75759:0cdccd0d1699 75760:f8be63d2ec6f
   828       }
   828       }
   829 
   829 
   830       deps
   830       deps
   831     }
   831     }
   832 
   832 
       
   833     def build_hierarchy(session: String): List[String] =
       
   834       if (build_graph.defined(session)) build_graph.all_preds(List(session))
       
   835       else List(session)
       
   836 
   833     def build_selection(sel: Selection): List[String] = selected(build_graph, sel)
   837     def build_selection(sel: Selection): List[String] = selected(build_graph, sel)
   834     def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss)
   838     def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss)
   835     def build_requirements(ss: List[String]): List[String] = build_graph.all_preds_rev(ss)
   839     def build_requirements(ss: List[String]): List[String] = build_graph.all_preds_rev(ss)
   836     def build_topological_order: List[String] = build_graph.topological_order
   840     def build_topological_order: List[String] = build_graph.topological_order
   837     def build_hierarchy(session: String): List[String] = build_graph.all_preds(List(session))
       
   838 
   841 
   839     def imports_selection(sel: Selection): List[String] = selected(imports_graph, sel)
   842     def imports_selection(sel: Selection): List[String] = selected(imports_graph, sel)
   840     def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss)
   843     def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss)
   841     def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds_rev(ss)
   844     def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds_rev(ss)
   842     def imports_topological_order: List[String] = imports_graph.topological_order
   845     def imports_topological_order: List[String] = imports_graph.topological_order
   843     def imports_hierarchy(session: String): List[String] = imports_graph.all_preds(List(session))
       
   844 
   846 
   845     def bibtex_entries: List[(String, List[String])] =
   847     def bibtex_entries: List[(String, List[String])] =
   846       build_topological_order.flatMap(name =>
   848       build_topological_order.flatMap(name =>
   847         apply(name).bibtex_entries match {
   849         apply(name).bibtex_entries match {
   848           case Nil => None
   850           case Nil => None