clarified output;
authorwenzelm
Wed Jun 07 21:19:33 2017 +0200 (23 months ago)
changeset 66033e4a8e1e20d45
parent 66032 fd8a65b026f1
child 66034 ded1c636aece
clarified output;
src/Pure/Tools/imports.scala
     1.1 --- a/src/Pure/Tools/imports.scala	Wed Jun 07 20:46:03 2017 +0200
     1.2 +++ b/src/Pure/Tools/imports.scala	Wed Jun 07 21:19:33 2017 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4  
     1.5      if (operation_imports) {
     1.6        progress.echo("\nPotential session imports:")
     1.7 -      selected.sorted.foreach(session_name =>
     1.8 +      selected.flatMap(session_name =>
     1.9        {
    1.10          val info = full_sessions(session_name)
    1.11          val session_resources = new Resources(deps(session_name))
    1.12 @@ -110,10 +110,11 @@
    1.13              if !declared_imports.contains(qualifier)
    1.14            } yield qualifier).toSet
    1.15  
    1.16 -        if (extra_imports.nonEmpty) {
    1.17 -          progress.echo("session " + Token.quote_name(root_keywords, session_name) + ": " +
    1.18 -            extra_imports.toList.sorted.map(Token.quote_name(root_keywords, _)).mkString(" "))
    1.19 -        }
    1.20 +        if (extra_imports.isEmpty) None
    1.21 +        else Some((session_name, extra_imports.toList.sorted, declared_imports.size))
    1.22 +      }).sortBy(_._3).foreach({ case (session_name, extra_imports, _) =>
    1.23 +        progress.echo("session " + Token.quote_name(root_keywords, session_name) + ": " +
    1.24 +          extra_imports.map(Token.quote_name(root_keywords, _)).mkString(" "))
    1.25        })
    1.26      }
    1.27