tuned signature;

--- a/src/Pure/Admin/build_doc.scala	Tue Nov 07 11:11:37 2017 +0100
+++ b/src/Pure/Admin/build_doc.scala	Tue Nov 07 15:45:33 2017 +0100
@@ -22,13 +22,15 @@
     system_mode: Boolean = false,
     docs: List[String] = Nil): Int =
   {
+    val sessions_structure = Sessions.load(options)
     val selection =
       for {
-        info <- Sessions.load(options).build_topological_order
+        name <- sessions_structure.build_topological_order
+        info = sessions_structure(name)
         if info.groups.contains("doc")
         doc = info.options.string("document_variants")
         if all_docs || docs.contains(doc)
-      } yield (doc, info.name)
+      } yield (doc, name)
 
     val selected_docs = selection.map(_._1)
     val sessions = selection.map(_._2)

--- a/src/Pure/Thy/sessions.scala	Tue Nov 07 11:11:37 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Tue Nov 07 15:45:33 2017 +0100
@@ -204,9 +204,10 @@
 
     val session_bases =
       (Map.empty[String, Base] /: sessions.imports_topological_order)({
-        case (session_bases, info) =>
+        case (session_bases, session_name) =>
           if (progress.stopped) throw Exn.Interrupt()
 
+          val info = sessions(session_name)
           try {
             val parent_base: Sessions.Base =
               info.parent match {
@@ -624,15 +625,15 @@
       build_graph.all_succs(names)
     def build_requirements(names: List[String]): List[String] =
       build_graph.all_preds(names).reverse
-    def build_topological_order: List[Info] =
-      build_graph.topological_order.map(apply(_))
+    def build_topological_order: List[String] =
+      build_graph.topological_order
 
     def imports_descendants(names: List[String]): List[String] =
       imports_graph.all_succs(names)
     def imports_requirements(names: List[String]): List[String] =
       imports_graph.all_preds(names).reverse
-    def imports_topological_order: List[Info] =
-      imports_graph.topological_order.map(apply(_))
+    def imports_topological_order: List[String] =
+      imports_graph.topological_order
 
     override def toString: String =
       imports_graph.keys_iterator.mkString("Sessions.T(", ", ", ")")

--- a/src/Pure/Tools/imports.scala	Tue Nov 07 11:11:37 2017 +0100
+++ b/src/Pure/Tools/imports.scala	Tue Nov 07 15:45:33 2017 +0100
@@ -138,7 +138,7 @@
 
         def make_result(set: Set[String]): Option[List[String]] =
           if (set.isEmpty) None
-          else Some(selected_sessions.imports_topological_order.map(_.name).filter(set))
+          else Some(selected_sessions.imports_topological_order.filter(set))
 
         Report(info, declared_imports, make_result(extra_imports),
           if (loaded_imports == declared_imports - session_name) None
@@ -313,11 +313,11 @@
       else if (operation_update && incremental_update) {
         val (selected, selected_sessions) =
           Sessions.load(options, dirs = dirs, select_dirs = select_dirs).selection(selection)
-        selected_sessions.imports_topological_order.foreach(info =>
+        selected_sessions.imports_topological_order.foreach(name =>
         {
           imports(options, operation_update = operation_update, progress = progress,
-            update_message = " for session " + quote(info.name),
-            selection = Sessions.Selection(sessions = List(info.name)),
+            update_message = " for session " + quote(name),
+            selection = Sessions.Selection(sessions = List(name)),
             dirs = dirs ::: select_dirs, verbose = verbose)
         })
       }

--- a/src/Tools/jEdit/src/jedit_sessions.scala	Tue Nov 07 11:11:37 2017 +0100
+++ b/src/Tools/jEdit/src/jedit_sessions.scala	Tue Nov 07 15:45:33 2017 +0100
@@ -68,10 +68,11 @@
 
     val session_list =
     {
-      val sessions = Sessions.load(options.value, dirs = session_dirs())
+      val sessions_structure = Sessions.load(options.value, dirs = session_dirs())
       val (main_sessions, other_sessions) =
-        sessions.imports_topological_order.partition(info => info.groups.contains("main"))
-      main_sessions.map(_.name).sorted ::: other_sessions.map(_.name).sorted
+        sessions_structure.imports_topological_order.
+          partition(name => sessions_structure(name).groups.contains("main"))
+      main_sessions.sorted ::: other_sessions.sorted
     }
 
     val entries =