# HG changeset patch
# User wenzelm
# Date 1659698632 -7200
# Node ID f8be63d2ec6f5fe5687c4d70d5bd20a20fbbd2ef
# Parent  0cdccd0d16991c624091a4c2811d5907974e4bd5
more robust build_hierarchy: support Resources.empty / Sessions.Structure.empty (required for Build_Job.print_log);
removed unused imports_hierarchy;

diff -r 0cdccd0d1699 -r f8be63d2ec6f src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Thu Aug 04 22:15:50 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Aug 05 13:23:52 2022 +0200
@@ -830,17 +830,19 @@
       deps
     }
 
+    def build_hierarchy(session: String): List[String] =
+      if (build_graph.defined(session)) build_graph.all_preds(List(session))
+      else List(session)
+
     def build_selection(sel: Selection): List[String] = selected(build_graph, sel)
     def build_descendants(ss: List[String]): List[String] = build_graph.all_succs(ss)
     def build_requirements(ss: List[String]): List[String] = build_graph.all_preds_rev(ss)
     def build_topological_order: List[String] = build_graph.topological_order
-    def build_hierarchy(session: String): List[String] = build_graph.all_preds(List(session))
 
     def imports_selection(sel: Selection): List[String] = selected(imports_graph, sel)
     def imports_descendants(ss: List[String]): List[String] = imports_graph.all_succs(ss)
     def imports_requirements(ss: List[String]): List[String] = imports_graph.all_preds_rev(ss)
     def imports_topological_order: List[String] = imports_graph.topological_order
-    def imports_hierarchy(session: String): List[String] = imports_graph.all_preds(List(session))
 
     def bibtex_entries: List[(String, List[String])] =
       build_topological_order.flatMap(name =>