src/Pure/Tools/imports.scala
changeset 67023 e27e05d6f2a7
parent 66966 f3f9a492bee6
child 67025 961285f581e6
     1.1 --- a/src/Pure/Tools/imports.scala	Tue Nov 07 11:11:37 2017 +0100
     1.2 +++ b/src/Pure/Tools/imports.scala	Tue Nov 07 15:45:33 2017 +0100
     1.3 @@ -138,7 +138,7 @@
     1.4  
     1.5          def make_result(set: Set[String]): Option[List[String]] =
     1.6            if (set.isEmpty) None
     1.7 -          else Some(selected_sessions.imports_topological_order.map(_.name).filter(set))
     1.8 +          else Some(selected_sessions.imports_topological_order.filter(set))
     1.9  
    1.10          Report(info, declared_imports, make_result(extra_imports),
    1.11            if (loaded_imports == declared_imports - session_name) None
    1.12 @@ -313,11 +313,11 @@
    1.13        else if (operation_update && incremental_update) {
    1.14          val (selected, selected_sessions) =
    1.15            Sessions.load(options, dirs = dirs, select_dirs = select_dirs).selection(selection)
    1.16 -        selected_sessions.imports_topological_order.foreach(info =>
    1.17 +        selected_sessions.imports_topological_order.foreach(name =>
    1.18          {
    1.19            imports(options, operation_update = operation_update, progress = progress,
    1.20 -            update_message = " for session " + quote(info.name),
    1.21 -            selection = Sessions.Selection(sessions = List(info.name)),
    1.22 +            update_message = " for session " + quote(name),
    1.23 +            selection = Sessions.Selection(sessions = List(name)),
    1.24              dirs = dirs ::: select_dirs, verbose = verbose)
    1.25          })
    1.26        }