src/Pure/Tools/imports.scala
changeset 66033 e4a8e1e20d45
parent 66030 f551ab947569
child 66234 836898197296
--- a/src/Pure/Tools/imports.scala	Wed Jun 07 20:46:03 2017 +0200
+++ b/src/Pure/Tools/imports.scala	Wed Jun 07 21:19:33 2017 +0200
@@ -94,7 +94,7 @@
 
     if (operation_imports) {
       progress.echo("\nPotential session imports:")
-      selected.sorted.foreach(session_name =>
+      selected.flatMap(session_name =>
       {
         val info = full_sessions(session_name)
         val session_resources = new Resources(deps(session_name))
@@ -110,10 +110,11 @@
             if !declared_imports.contains(qualifier)
           } yield qualifier).toSet
 
-        if (extra_imports.nonEmpty) {
-          progress.echo("session " + Token.quote_name(root_keywords, session_name) + ": " +
-            extra_imports.toList.sorted.map(Token.quote_name(root_keywords, _)).mkString(" "))
-        }
+        if (extra_imports.isEmpty) None
+        else Some((session_name, extra_imports.toList.sorted, declared_imports.size))
+      }).sortBy(_._3).foreach({ case (session_name, extra_imports, _) =>
+        progress.echo("session " + Token.quote_name(root_keywords, session_name) + ": " +
+          extra_imports.map(Token.quote_name(root_keywords, _)).mkString(" "))
       })
     }