# HG changeset patch
# User wenzelm
# Date 1496863173 -7200
# Node ID e4a8e1e20d45b2ff2aff5d0cbdb625292b72e358
# Parent  fd8a65b026f17dd85bf603e324021d03eda0ef68
clarified output;

diff -r fd8a65b026f1 -r e4a8e1e20d45 src/Pure/Tools/imports.scala
--- 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(" "))
       })
     }