src/Pure/Tools/imports.scala
changeset 67023 e27e05d6f2a7
parent 66966 f3f9a492bee6
child 67025 961285f581e6
--- 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)
         })
       }