--- a/src/Pure/Thy/document_build.scala Wed Nov 17 11:57:34 2021 +0100
+++ b/src/Pure/Thy/document_build.scala Wed Nov 17 12:10:48 2021 +0100
@@ -174,7 +174,7 @@
{
val info = deps.sessions_structure(session)
val base = deps(session)
- val hierarchy = deps.sessions_structure.hierarchy(session)
+ val hierarchy = deps.sessions_structure.build_hierarchy(session)
new Context(info, base, hierarchy, db_context, progress)
}
--- a/src/Pure/Thy/presentation.scala Wed Nov 17 11:57:34 2021 +0100
+++ b/src/Pure/Thy/presentation.scala Wed Nov 17 12:10:48 2021 +0100
@@ -511,7 +511,7 @@
val options = info.options
val base = deps(session)
- val hierarchy = deps.sessions_structure.hierarchy(session)
+ val hierarchy = deps.sessions_structure.build_hierarchy(session)
val hierarchy_theories = hierarchy.reverse.flatMap(a => deps(a).used_theories.map(_._1))
val session_dir = Isabelle_System.make_directory(html_context.session_dir(info))
--- a/src/Pure/Thy/sessions.scala Wed Nov 17 11:57:34 2021 +0100
+++ b/src/Pure/Thy/sessions.scala Wed Nov 17 12:10:48 2021 +0100
@@ -837,17 +837,17 @@
deps
}
- def hierarchy(session: String): List[String] = build_graph.all_preds(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 =>