clarified signature;
authorwenzelm
Wed, 17 Nov 2021 12:10:48 +0100
changeset 74809 48fda7ee1973
parent 74808 23dc565cd4b2
child 74810 d540c36cd0d2
clarified signature;
src/Pure/Thy/document_build.scala
src/Pure/Thy/presentation.scala
src/Pure/Thy/sessions.scala
--- 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 =>