src/Pure/Thy/sessions.scala
changeset 74809 48fda7ee1973
parent 74731 161e84e6b40a
child 74810 d540c36cd0d2
equal deleted inserted replaced
74808:23dc565cd4b2 74809:48fda7ee1973
   835       }
   835       }
   836 
   836 
   837       deps
   837       deps
   838     }
   838     }
   839 
   839 
   840     def hierarchy(session: String): List[String] = build_graph.all_preds(List(session))
       
   841 
       
   842     def build_selection(sel: Selection): List[String] = selected(build_graph, sel)
   840     def build_selection(sel: Selection): List[String] = selected(build_graph, sel)
   843     def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss)
   841     def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss)
   844     def build_requirements(ss: List[String]): List[String] = build_graph.all_preds_rev(ss)
   842     def build_requirements(ss: List[String]): List[String] = build_graph.all_preds_rev(ss)
   845     def build_topological_order: List[String] = build_graph.topological_order
   843     def build_topological_order: List[String] = build_graph.topological_order
       
   844     def build_hierarchy(session: String): List[String] = build_graph.all_preds(List(session))
   846 
   845 
   847     def imports_selection(sel: Selection): List[String] = selected(imports_graph, sel)
   846     def imports_selection(sel: Selection): List[String] = selected(imports_graph, sel)
   848     def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss)
   847     def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss)
   849     def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds_rev(ss)
   848     def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds_rev(ss)
   850     def imports_topological_order: List[String] = imports_graph.topological_order
   849     def imports_topological_order: List[String] = imports_graph.topological_order
       
   850     def imports_hierarchy(session: String): List[String] = imports_graph.all_preds(List(session))
   851 
   851 
   852     def bibtex_entries: List[(String, List[String])] =
   852     def bibtex_entries: List[(String, List[String])] =
   853       build_topological_order.flatMap(name =>
   853       build_topological_order.flatMap(name =>
   854         apply(name).bibtex_entries match {
   854         apply(name).bibtex_entries match {
   855           case Nil => None
   855           case Nil => None